[FOM] Quantifier free sentences in set theory (redirected from Franco Parlamento)

[Martin Davis]

Paul Studtmann writes:

 >Robinson's Arithmetic is complete with respect to quantifier free sentences.
 >I am wondering whether anyone can tell me if an analog of this holds in set
 >theory. Suppose, for instance, that the language contains two constants --
 >one for the empty set and one for the set of finite ordinals -- as well as
 >function symbols for the basic set theoretic operations like set union, set
 >difference, power set, pairing, etc. Is ZF (or a fragment thereof) or some >
 >other theory complete with respect to all the quantifier free sentences in
 >the language?

If you omit the power set operator from the list and by "union"  binary 
union is
meant, then ZF, but also ZF-Power Set Axiom and even weaker
theories,  are complete with respect to quantifier free sentences (equiv.
atomic sentences).
That can be inferred from the decidability of truth in V for existential
closures of restricted purely universal formulae with no nesting of
quantified variables, over the primitive language of set theory with the
addition of constants for the empty set and the set of finite ordinals (as
well as a unary predicate Ord(x) for "x is an ordinal") (Breban M., Ferro
A., Omodeo E., Schwartz J.T. "Decision Procedures for Elementary
Sublanguages of Set TheoryII. Formulas involving restricted quantifiers
together with ordinal, integer, map and domain notions" Comm. on Pure and
Applied Mathematics XLI 221-251 (1988) - see also Ch.7 in Cantone D., Ferro
A., Omodeo E "Computable Set Theory Vol 1" Oxford University Press, 1989
and my [FOM] of june 3th, 2003)

In fact the operations of (binary) union, intersection and set-difference
as well as the operation of n-tuple formation have a restricted purely
universal definition with no nesting of quantified variables, so that an
atomic sentence which also involves them, turns out to be equivalent to a
sentence which belong to the decidable class described above.
Completeness follows since the proof of the decidability of the class in
question, which exhibits an actual algorithm that shows that it does what
it is supposed to do, can be formalized inside ZF- Power Set Axiom (and
even weaker theories).



Franco Parlamento
Dipartimento di Matematica e Informatica
Universita' di udine
Via delle Scienze 208
33100 UDINE
Italy
parlamen at dimi.uniud