The ∀∃-theory of ℛ(≤,∨,∧) is undecidable

The three quantifier theory of ( R , ≤ T ) (\mathcal {R},\leq _{T}) , the recursively enumerable degrees under Turing reducibility, was proven undecidable by Lempp, Nies and Slaman (1998). The two quantifier theory includes the lattice embedding problem and its decidability is a long-standing open question. A negative solution to this problem seems out of reach of the standard methods of interpretation of theories because the language is relational. We prove the undecidability of a fragment of the theory of R \mathcal {R} that lies between the two and three quantifier theories with ≤ T \leq _{T} but includes function symbols. Theorem. The two quantifier theory of ( R , ≤ , ∨ , ∧ ) (\mathcal {R},\leq ,\vee ,\wedge ) , the r.e. degrees with Turing reducibility, supremum and infimum (taken to be any total function extending the infimum relation on R \mathcal {R} ) is undecidable. The same result holds for various lattices of ideals of R \mathcal {R} which are natural extensions of R \mathcal {R} preserving join and infimum when it exits.