English

Effective inseparability, lattices, and pre-ordering relations

Logic 2019-07-22 v1

Abstract

We study effectively inseparable (e.i.) pre-lattices (i.e. structures of the form L=ω,,,0,1,LL=\langle \omega, \wedge, \lor, 0, 1, \leq_L\rangle where ω\omega denotes the set of natural numbers and the following hold: ,\wedge, \lor are binary computable operations; L\leq_L is a c.e. pre-ordering relation, with 0LxL10 \leq_{L} x \leq_{L} 1 for every xx; the equivalence relation L\equiv_L originated by L\leq_L is a congruence on LL such that the corresponding quotient structure is a non-trivial bounded lattice; the L\equiv_L-equivalence classes of 00 and 11 form an effectively inseparable pair), and show that if LL is an e.i. pre-lattice then L\le_{L} is universal with respect to all c.e. pre-ordering relations, i.e. for every c.e. pre-ordering relation RR there exists a computable function ff such that, for all x,yx,y, xRyx \mathrel{R} y if and only if f(x)Lf(y)f(x) \le_{L} f(y); in fact L\leq_L is locally universal, i.e. for every pair a<Lba<_{L} b and every c.e. pre ordering relation RR one can find a reducing function ff from RR to L\le_{L} such that the range of ff is contained in the interval {x:aLxLb}\{x: a \leq_{L} x \leq_{L} b\}. Also L\leq_L is uniformly dense, i.e. there exists a computable function ff such that for every a,ba,b if a<Lba<_{L} b then a<Lf(a,b)<Lba<_{L} f(a,b) <_{L} b, and if aLaa\equiv_{L} a' and bLbb \equiv_{L} b' then f(a,b)Lf(a,b)f(a,b)\equiv_{L} f(a',b'). Some consequences and applications of these results are discussed: in particular for n1n \ge 1 the c.e. pre-ordering relation on Σn\Sigma_{n} sentences yielded by the relation of provable implication of any c.e. consistent extension of Robinson's QQ or RR 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.

Keywords

Cite

@article{arxiv.1901.06136,
  title  = {Effective inseparability, lattices, and pre-ordering relations},
  author = {Uri Andrews and Andrea Sorbi},
  journal= {arXiv preprint arXiv:1901.06136},
  year   = {2019}
}
R2 v1 2026-06-23T07:15:27.237Z