The classification of algebraic structures which can be embedded into ℛ, the uppersemilattice of recursively enumerable degrees, is the key to answering certain questions about Th(ℛ), the elementary theory of ℛ. In particular, these classification problems are important for answering decidability questions about fragments of Th(ℛ). Thus the solutions of Fried berg [F] and Mučnik [M] to Post's problem were easily extended to show that all finite partially ordered sets are embeddable into ℛ, and hence that ∃1 ∩ Th(ℛ), the existential theory of ℛ, is decidable. (The language used is ℒ′, the pure predicate calculus together with a binary relation symbol ≤ to be interpreted as the ordering of ℛ) The problem of determining which finite lattices are embeddable into ℛ has been a long-standing open problem, and is one of the major obstacles to determining whether ∀2 ∩ Th(ℛ), the universal-existential theory of ℛ, is decidable. Shore has obtained some nice partial results in this direction. Embeddings also played a central role in showing that Th(ℛ) is not ℵ0-categorical (Lerman, Shore and Soare [LeShSo]), thus resolving a problem posed by Jockusch. Harrington and Shelah [HS] embedded all 0′-presentable partially ordered sets into ℛ in such a way that the partially ordered sets can be uniformly recovered from four parameters. They used these embeddings to show that Th(ℛ) is undecidable.The first nontrivial extension of the embeddings of Friedberg and Mučnik to lattice embeddings was obtained independently by Lachlan [La1] and Yates [Y] who showed that the four-element Boolean algebra can be embedded into ℛ. Thomason [T] and Lerman independently extended this result to include all finite distributive lattices. The nondistributive case, however, was much more difficult. Lachlan [La2] embedded the two five-element nondistributive lattices M5 and N5 (see Figures 1 and 2) into ℛ, and his proof could easily have been extended to include a larger class of lattices.
Model Checking Existential Logic on Partially Ordered Sets
