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.
Decision Procedures for Elementary Sublanguages of Set Theory XIII. Model Graphs, Reflection and Decidability.
PARLAMENTO, Franco;POLICRITI, Alberto
1991-01-01
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
