Premium
Decidability of ∀*∀‐Sentences in Membership Theories
Author(s) -
Omodeo Eugenio G.,
Parlamento Franco,
Policriti Alberto
Publication year - 1996
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.19960420105
Subject(s) - mathematics , decidability , quantifier (linguistics) , completeness (order theory) , axiom , quantifier elimination , class (philosophy) , mathematics subject classification , satisfiability , set (abstract data type) , subject (documents) , boolean satisfiability problem , discrete mathematics , calculus (dental) , algebra over a field , pure mathematics , artificial intelligence , computer science , medicine , mathematical analysis , geometry , dentistry , library science , programming language
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. Mathematics Subject Classification: 03B25, 03E30.