Premium
THE DECISION PROBLEM FOR RESTRICTED UNIVERSAL QUANTIFICATION IN SET THEORY AND THE AXIOM OF FOUNDATION
Author(s) -
Parlamento Franco,
Policriti Alberto
Publication year - 1992
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.19920380110
Subject(s) - mathematics , axiom , axiom of choice , satisfiability , zermelo–fraenkel set theory , class (philosophy) , decidability , urelement , discrete mathematics , set (abstract data type) , boolean satisfiability problem , characterization (materials science) , constructive set theory , relation (database) , set theory , computer science , materials science , geometry , database , artificial intelligence , programming language , nanotechnology
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 (of course with different answers). 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.