Decision Procedures for Elementary Sublanguages of Set Theory XIII. Model Graphs, Reflection and Decidability.

Positive solutions to the decision problem for a class of quantified formulae of the first order set theoretic language based on φ{symbol}, ε, =, involving particular occurrences of restricted universal quantifiers and for the unquantified formulae of φ{symbol}, ε, =, {...}, η, where {...} is the tuple operator and η 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 φ{symbol}, ε, =, {...}, η, obtained by adding the operators of binary union, intersection and difference and the relation of inclusion, provided no nested term involving η is allowed.