The problem is addressed of establishing the satisfiability of prenex formulas involving a single universal quantifier, in diversified axiomatic set theories. A rather general decision method for solving this problem is illustrated through the treatment of membership theories of increasing strength, ending with a subtheory of Zermelo-Fraenkel which is already complete with respect to the ∀*∀ class of sentences. NP-hardness and NP-completeness results concerning the problems under study are achieved and a technique for restricting the universal quantifier is presented.
We develop a bottom-up approach to truth-value semantics for classical logic of partial terms based on equality and apply it to prove the conservativity of the addition of partial description and selection functions, independently of any strictness assumption.
The still unsettled decision problem for the restricted purely universal formulae 0-formulae) of the first order set-theoretic language based over =, ∈ is discussed in relation with the adoption or rejection of the axiom of foundation. Assuming the axiom of foundation, the related finite set-satisfiability problem for the very significant subclass of the 0-formulae consisting of the formulae involving only nested variables of level 1 is proved to be semidecidable on the ground of a reflection property over the hereditarily finite (...) sets, and various extensions of this result are obtained. When variables are restricted to range only over sets, in universes with infinitely many urelements the set-satisfiability problem is shown to be solvable provided the axiom of foundation is assumed; if it is not, then the decidability of a related derivability problem still holds. That, in turn, suggests the alternative adoption of an antifoundation axiom under which the set-satisfiability problem is also solvable . Turning to set theory without urelements, assuming a form of Boffa's antifoundation axiom, the complement of the set-satisfiability problem for the full class of Δ0-formulae is shown to be semidecidable; a result that is known not to hold, for the set-satisfiability problem itself, even for a very restricted subclass of the Δ0-formulae. (shrink)
We show that if the structural rules are admissible over a set \ of atomic rules, then they are admissible in the sequent calculus obtained by adding the rules in \ to the multisuccedent minimal and intuitionistic \ calculi as well as to the classical one. Two applications to pure logic and to the sequent calculus with equality are presented.
We show that the Axiom of Foundation, as well as the Antifoundation Axiom AFA, plays a crucial role in determining the decidability of the following problem. Given a first-order theory T over the language , and a sentence F of the form with quantifier-free in the same language, are there models of T in which F is true? Furthermore we show that the Extensionality Axiom is quite irrelevant in that respect.
Let HF be the collection of the hereditarily finite well-founded sets and let the primitive language of set theory be the first-order language which contains binary symbols for equality and membership only. As announced in a previous paper by the authors, "Truth in V for ∃*∀∀-sentences is decidable," truth in HF for ∃*∀∀-sentences of the primitive language is decidable. The paper provides the proof of that claim.
Let V be the cumulative set theoretic hierarchy, generated from the empty set by taking powers at successor stages and unions at limit stages and, following , let the primitive language of set theory be the first order language which contains binary symbols for equality and membership only. Despite the existence of ∀∀-formulae in the primitive language, with two free variables, which are satisfiable in V but not by finite sets (), and therefore of ƎƎ∀∀ sentences of the same language, (...) which are undecidable in ZFC without the Axiom of Infinity, truth in V for Ǝ*∀∀-sentences of the primitive language, is decidable (). Completeness of ZF with respect to such sentences follows. (shrink)
We establish the decidability, with respect to open formulas in the first order language with equality =, the membership relation , the constant for the empty set, and a binary operation w which, applied to any two sets x and y, yields the results of adding y as an element to x, of the theory NW having the obvious axioms for and w. Furthermore we establish the completeness with respect to purely universal sentences of the theory , obtained from NW (...) by adding the Extensionality Axiom E and the Regularity Axiom R, and of the theory obtained by adding to NW (a slight variant of) the Antifoundation Axiom AFA. (shrink)