Effective inseparability, lattices, and pre-ordering relations

Abstract

We study effectively inseparable (e.i.) pre-lattices (i.e. structures of the form $L=⟨\omega ,\wedge ,\vee ,0,1,{\le }_L⟩$ where $\omega$ denotes the set of natural numbers and the following hold: $\wedge ,\vee$ are binary computable operations; ${\le }_L$ is a c.e. pre-ordering relation, with $0{\le }_{L}x{\le }_{L}1$ for every $x$; the equivalence relation ${\equiv }_L$ originated by ${\le }_L$ is a congruence on $L$ such that the corresponding quotient structure is a non-trivial bounded lattice; the ${\equiv }_L$-equivalence classes of $0$ and $1$ form an effectively inseparable pair), and show that if $L$ is an e.i. pre-lattice then ${\le }_L$ is universal with respect to all c.e. pre-ordering relations, i.e. for every c.e. pre-ordering relation $R$ there exists a computable function $f$ such that, for all $x,y$, $xRy$ if and only if $f(x){\le }_{L}f(y)$; in fact ${\le }_L$ is locally universal, i.e. for every pair $a{<}_{L}b$ and every c.e. pre ordering relation $R$ one can find a reducing function $f$ from $R$ to ${\le }_L$ such that the range of $f$ is contained in the interval $\{x:a{\le }_{L}x{\le }_{L}b\}$. Also ${\le }_L$ is uniformly dense, i.e. there exists a computable function $f$ such that for every $a,b$ if $a{<}_{L}b$ then $a{<}_{L}f(a,b){<}_{L}b$, and if $a{\equiv }_L{a}^{\prime }$ and $b{\equiv }_L{b}^{\prime }$ then $f(a,b){\equiv }_{L}f(a^{\prime },b^{\prime })$. Some consequences and applications of these results are discussed: in particular for $n\ge 1$ the c.e. pre-ordering relation on ${\Sigma }_n$ sentences yielded by the relation of provable implication of any c.e. consistent extension of Robinson's $Q$ or $R$ is locally universal and uniformly dense; and the c.e. pre-ordering relation of provable implication of Heyting Arithmetic is locally universal and uniformly dense.