Decision procedures for elementary sublanguages of set theory: XIII. Model graphs, reflection and decidability. (English) Zbl 0734.03006

Summary: Positive solutions to the decision problem for a class of quantified formulae of the first order set theoretic language based on \(\phi\), \(\in\), \(=\), involving particular occurrences of restricted universal quantifiers and for the unquantified formulae of \(\phi\), \(\in\), \(=\), \(\{\)...\(\}\), \(\eta\), where \(\{\)...\(\}\) is the tuple operator and \(\eta\) is a general choice operator, are obtained. To that end a method is developed which also provides strong reflection principles over the hereditarily finite sets. As far as finite satisfiability is concerned such results apply also to the unquantified extention of \(\phi\), \(\in\), \(=\), \(\{\)...\(\}\), \(\eta\), obtained by adding the operators of binary union, intersection and difference and the relation of inclusion, provided no nested term involving \(\eta\) is allowed.


03B25 Decidability of theories and sets of sentences
03E99 Set theory
Full Text: DOI