Decidability of the two-quantifier theory of the recursively enumerable weak truth-table degrees and other distributive upper semi-lattices

1996 ◽  
Vol 61 (3) ◽  
pp. 880-905 ◽  
Author(s):  
Klaus Ambos-Spies ◽  
Peter A. Fejer ◽  
Steffen Lempp ◽  
Manuel Lerman
Keyword(s):  
Decision Procedure ◽  
Finite Lattice ◽  
Truth Table ◽  
Recursively Enumerable ◽  
Finite Lattices ◽  
Recursively Enumerable Sets ◽  
Weak Truth Table Degrees ◽  
Quantifier Theory ◽  
The Ideal

AbstractWe give a decision procedure for the ∀∃-theory of the weak truth-table (wtt) degrees of the recursively enumerable sets. The key to this decision procedure is a characterization of the finite lattices which can be embedded into the r.e.wtt-degrees by a map which preserves the least and greatest elements: a finite lattice has such an embedding if and only if it is distributive and the ideal generated by its cappable elements and the filter generated by its cuppable elements are disjoint.We formulate general criteria that allow one to conclude that a distributive upper semi-lattice has a decidable two-quantifier theory. These criteria are applied not only to the weak truth-table degrees of the recursively enumerable sets but also to various substructures of the polynomial many-one (pm) degrees of the recursive sets. These applications to thepmdegrees require no new complexity-theoretic results. The fact that thepm-degrees of the recursive sets have a decidable two-quantifier theory answers a question raised by Shore and Slaman in [21].

Lattice embeddings into the recursively enumerable degrees. II

1989 ◽  
Vol 54 (3) ◽  
pp. 735-760 ◽  
Author(s):  
K. Ambos-Spies ◽  
M. Lerman
Keyword(s):  
Decision Procedure ◽  
Finite Lattice ◽  
Labeled Trees ◽  
Recursively Enumerable ◽  
Finite Lattices ◽  
Embeddability Condition

The problem of characterizing the finite lattices which can be embedded into the recursively enumerable degrees has a long history, which is summarized in [AL]. This problem is an important one, as its solution is necessary if a decision procedure for the ∀∃-theory of the poset of recursively emumerable degrees is to be found. A recursive nonembeddability condition, NEC, which subsumes all known nonembeddability conditions was presented in [AL]. This paper focuses on embeddability. An embeddability condition, EC, is introduced, and we prove that every finite lattice having EC can be embedded (as a lattice) into . EC subsumes all known embeddability conditions.EC is a Π3 condition which states that certain obstructions to proving embeddability do not exist. It seems likely that the recursive labeled trees used in EC can be replaced with trees which are effectively generated from uniformly defined finite trees, in which case EC would be equivalent to a recursive condition. We do not know whether EC and NEC are complementary. This problem seems to be combinatorial, rather than recursion-theoretic in nature. Our efforts to find a finite lattice satisfying neither EC nor NEC have, to this point, been unsuccessful. It is the second author's conjecture that the techniques for proving embeddability which are used in this paper cannot be refined very much to obtain new embeddability results.EC is introduced in §2, and the various conditions and definitions are motivated by presenting examples of embeddable lattices and indicating how the embedding proof works in those particular cases. The embedding construction is presented in §3, and the proof in §4.

The theory of the recursively enumerable weak truth-table degrees is undecidable

1992 ◽  
Vol 57 (3) ◽  
pp. 864-874 ◽  
Author(s):  
Klaus Ambos-Spies ◽  
André Nies ◽  
Richard A. Shore
Keyword(s):  
Partial Order ◽  
Open Problem ◽  
Truth Table ◽  
Recursively Enumerable ◽  
Undecidable Theory ◽  
Weak Truth Table Degrees

AbstractWe show that the partial order of -sets under inclusion is elementarily definable with parameters in the semilattice of r.e. wtt-degrees. Using a result of E. Herrmann, we can deduce that this semilattice has an undecidable theory, thereby solving an open problem of P. Odifreddi.

scholarly journals Infima in the Recursively Enumerable Weak Truth Table Degrees

1997 ◽  
Vol 38 (3) ◽  
pp. 406-418
Author(s):  
Rich Blaylock ◽  
Rod Downey ◽  
Steffen Lempp
Keyword(s):  
Truth Table ◽  
Recursively Enumerable ◽  
Weak Truth Table Degrees

Characterization of recursively enumerable sets

1972 ◽  
Vol 37 (3) ◽  
pp. 507-511 ◽  
Author(s):  
Jesse B. Wright
Keyword(s):  
Transitive Closure ◽  
Successor Function ◽  
Function Composition ◽  
Recursive Functions ◽  
Recursively Enumerable ◽  
Abstract Setting ◽  
Recursively Enumerable Sets ◽  
Bracket Operation

AbstractLet N, O and S denote the set of nonnegative integers, the graph of the constant 0 function and the graph of the successor function respectively. For sets P, Q, R ⊆ N2 operations of transposition, composition, and bracketing are defined as follows: P∪ = {〈x, y〉 ∣ 〈y, x〉 ∈ P}, PQ = {〈x, z〉 ∣ ∃y〈x, y〉 ∈ P & 〈y, z〉 ∈ Q}, and [P, Q, R] = ⋃n ∈ M(Pn Q Rn).Theorem. The class of recursively enumerable subsets of N2 is the smallest class of sets with O and S as members and closed under transposition, composition, and bracketing.This result is derived from a characterization by Julia Robinson of the class of general recursive functions of one variable in terms of function composition and “definition by general recursion.” A key step in the proof is to show that if a function F is defined by general recursion from functions A, M, P and R then F = [P∪, A∪M, R].The above definitions of the transposition, composition, and bracketing operations on subsets of N2 can be generalized to subsets of X2 for an arbitrary set X. In this abstract setting it is possible to show that the bracket operation can be defined in terms of K, L, transposition, composition, intersection, and reflexive transitive closure where K: X → X and L: X → X are functions for decoding pairs.

Simplicity of recursively enumerable sets

1967 ◽  
Vol 32 (2) ◽  
pp. 162-172 ◽  
Author(s):  
Robert W. Robinson
Keyword(s):  
Recursively Enumerable ◽  
Original Definition ◽  
Recursively Enumerable Sets ◽  
Simple Sets

In §1 is given a characterization of strongly hypersimple sets in terms of weak arrays which is in appearance more restrictive than the original definition. §1 also includes a new characterization of hyperhypersimple sets. This one is interesting because in §2 a characterization of dense simple sets is shown which is identical in all but the use of strong arrays instead of weak arrays. Another characterization of hyperhypersimple sets, in terms of descending sequences of sets, is given in §3. Also a theorem showing strongly contrasting behavior for simple sets is presented. In §4 a r-maximal set which is not contained in any maximal set is constructed.

Pairs without infimum in the recursively enumerable weak truth table degrees

1986 ◽  
Vol 51 (1) ◽  
pp. 117-129 ◽  
Author(s):  
Paul Fischer
Keyword(s):  
Structural Difference ◽  
Truth Table ◽  
Turing Degrees ◽  
Recursively Enumerable ◽  
Weak Truth Table Degrees ◽  
Result Theorem ◽  
Turing Reducibility ◽  
Carry Over

wtt-reducibility has become of some importance in the last years through the works of Ladner and Sasso [1975], Stob [1983] and Ambos-Spies [1984]. It differs from Turing reducibility by a recursive bound on the use of the reduction. This makes some proofs easier in the wtt degrees than in the Turing degrees. Certain proofs carry over directly from the Turing to the wtt degrees, especially those based on permitting. But the converse is also possible. There are some r.e. Turing degrees which consist of a single r.e. wtt degree (the so-called contiguous degrees; see Ladner and Sasso [1975]). Thus it suffices to prove a result about contiguous wtt degrees using an easier construction, and it carries over to the corresponding Turing degrees.In this work we prove some results on pairs of r.e. wtt degrees which have no infimum. The existence of such a pair has been shown by Ladner and Sasso. Here we use a different technique of Jockusch [1981] to prove this result (Theorem 1) together with some stronger ones. We show that a pair without infimum exists above a given incomplete wtt degree (Theorem 5) and below any promptly simple wtt degree (Theorem 12). In Theorem 17 we prove, however, that there are r.e. wtt degrees such that any pair below them has an infimum. This shows that certain initial segments of the wtt degrees are lattices. Thus there is a structural difference between the wtt and Turing degrees where the pairs without infimum are dense (Ambos-Spies [1984]).

Sign in / Sign up

Export Citation Format

Share Document