[FOM] On the decision problem for fragments of set theory

Tue Jun 3 07:43:40 EDT 2003

In his recent paper "Three quantifier sentences", Harvey Friedman has given
a complete proof of the completeness of a subtheory of ZFC, with respect to
sentences with three quantifiers in the primitive language of set theory,
containing binary simbols for equality and membership only, and has shown
that there are five quantifier sentences in that language that remains
undecided in ZFC.That improves earlier result of Daniel Gogol, who had also
established the  completeness of ZFC with respect to E...EA sentences of
the same language.

The present posting, written at Friedman's kind invitation,
overviews some of the work that has been done around the problem of
establishing decidability and undecidability results, concerning
(classical) derivability in fragments of set theory, and  satisfiability in
the "real" set theoretic world (V), focusing, except for a few remarks, on
the part that concerns the primitive language. For  results and
applications concerning more extended languages I refer to the momographs
[CFO] and [COP].

On the undecidability side, long before Gogol's work,  the "small axiomatic
fragment  of set theory", to use Tarski's wording, which consists of the
obvious axiom (N) for the existence of the empty set, (W) for the existence
of the addition of a single element to a given set, as well as the
Extensionality axiom  (E), had been shown to be essentially undecidable by
W.Szmielew and Tarski's himself ([TMR]), via interpretability of Robinson's
Arithmetic, and  R. Vaught in [Va] had established, by using a theorem of
Cobham, the essential undecidability of NW alone.

On the positive side, instead,  F. Ville, in [Vl], had shown the
completeness  of the theory that beside axiom N and E, has also those for
the existence of singletons and binary unions, for purely existential
sentences of the primitive language extended with the corresponding
function symbols of binary union and singleton's formation. In view of the
sequel it is of interest   to add  that there, axioms E plays a crucial
"positive" role, since,  if it is dropped, then
the (logical) satisfiability of A sentences, with a matrix which consists
of a conjunction of equalities with one inequality in the language with the
constant for the empty set and the binary operation  defined through axiom
W (which is immediately derivable  from those concerning binary union and
singleton), with respect to the theory NW, is turned into an undecidable
problem (Belle' D., Parlamento F.(BP from now on)) "Undecidability in weak
membership theories", in "Logic and Algebra", Lecture Notes in Pure and
applied Mathematics, Dekker NY 1996)

Shortly after Gogol's work,  at the Courant Institute in New York, J.
Schwartz started a research project, aiming at the development of a proof
verifier for"elementary set theory", viewed  as being a particularly
important subdomain of mathematics, which  led to the discovery of various
decision procedures for truth in V of purely existential sentences of
extensions of the primitive language,  such as  the  Multi Level
Syllogistic language (MLS),
which contains function symbols for the set theoretic boolean operations,
supplemented by function symbols for either the power set and singleton
operations or the unary union operation.

Under the heading  "Decision procedures for Elementary Sublanguages of
Set Theory" (DP from now on), a number of papers were published by Schwartz,
Breban, Ferro, Omodeo, Cantone and their results were afterwards collected
into [CFO].

First limitations to what could be accomplished in that direction were
obtained trough a (standard) development of Godel's incompleteness results.
By using a suitable coding of syntactic notions in the primitive
language, that  established the essential undecidability for
E...EA...AE...EA...A sentences, where all the quantifiers, except those of
the first block, are bounded, of the theory NWLE having, beside the axioms
already mentioned, also the one which states  the existence of the
subtraction of a single element from a given set. (Parlamento F., Policriti
A., (PP from now on )  " DP IX Unsolvability of the Decision Problem for a
Restricted Subclass of
the \Delta_0-formulas in Set Theory" Comm. on Pure and Applied Mathematics
(CPAM), Vol XLI 221-251 (1988)

Afterwards by using  a more or less straighforward coding of  (non halting) TM
computations,  it was established the non semidecidability of the
collection of true (in V)  E...EA...AE...E (equivalentely A...AE...EA...A)
sentences, with the second and third block consisting of bounded
quantifiers, a result that can be also established through a set theretic
reduction of Hilbert's tenth problem, as shown in
"D. Cantone, V. Cutello, A. Policriti. Set-theoretic reductions of
Hilbert's tenth problem. In E. Boerger, H. Kleine, Buening, and M.M.
Richter eds., CLS'89:
3rd workshop on Computer Science Logic, vol.440 of Lecture
Notes in Computer Science, pp.65-75, Springer-Verlag, 1990.

Furthermore, as was discovered by A. Policriti in his Ph.D.
thesis, if one adds to the language the 1-ary predicate "is-a-pair(x)",
meant to say that x consists of two distinct elements,  TM computations can
be  coded with restricted  A...A  formulae.  From that it follows that if
the language is so extended  then the true two-block sentences, with the
second one made of bounded quantifiers, form an undecidable collection.
(PP, "Undecidability results for Restricted Universally Quantified Formulae
of Set Theory" CPAM, Vol. XLVI, 57-73, 1993).

The decidability of true E...EA...A sentences, where the A quantifiers are
all restricted had been established already in Breban, M., Ferro A., Omodeo
E., Schwartz J.T. "DP II. Formulas involving restricted quantifiers
together with ordinal, integer, map and domain notions" CPAM Vol 34,
177-196, 1981,  BUT under the assumption  that there were no occurrences of
(universal) nested quantification such as the one that occurs in expressing
that a set is transitive. Under that assumption it is not hard to show that
if the A...A part of the sentence is satisfiable at all, then it is
satisfied already by hereditarily finite  sets (HF), whose rank is
bounded (w.r.t. the number of  variables).

Such a reflection property over HF, and the ensuing decidability result,
can be extended to a strong reflection propery for a more extended
subcollection of  the E...EA...A sentences, with bounded A's. In fact given
n sets there are corresponding hereditarily finite sets which satisfy the
same A...A formulae in the class, as the given ones. (PP, "DP XIII. Model
Graphs, Reflection and Decidability" Journal of Authomated Reasoning 7,
271-284, 1991)

On the other hand it was precisely in the attempt to extend the above
reflection properties to the full class that, contrary to what was commonly
expected, the counterexamples published in the papers cited in Friedman's
[FOM]:163, were discovered.

Briefly stated, there are restricted AA formulae with two free variables
which are satisfiable in infinite, but not in finite, extensional and well
founded structures. If the requirement of well foundedness is dropped the
same holds for restricted AAAA formulae (PP "Expressing Infinity Without
Foundation" JSL 56, n.4, 1230-1235  1991) ). As  was later shown by D.
Belle',
extensionality alone cannot force restricted AA formulae to be satisfiable,
but only in infinite structures. There are  examples of EEAAA sentence, with
restricted A's, which in  ZF deprived of the Foundation (R) and Infinity
axioms (Inf) entails the latter axiom (PP,"The decision problem for
restricted universal quantification in set theory and the axiom of
foundation" Zeitschrift f. math. Logik und Grundlagen d. Math. 38, 143-156
(1992). The  known example contradicts ZF. That  leaves it open whether
there are restricted AAA formula which are satisfiable in V, or at least
are compatible with ZF, entailing  Inf (in ZF-R-Inf).

Starting from the completeness of ZFC w.r.t. E...EA sentences, established
by Gogol, it was quite  natural to enquire how much  of ZFC was really
needed to have such a completeness result and, more generally, the
decidability of the satisfiablity w.r.t. the theory,  of such sentences.
Omodeo E., Parlamento F., Policriti A. "Decidability of E...EA-Sentences in
Membership Theories " Mathematical Logic Quarterly 42, 41-58, 1996,(OPP
from now on), establishes that indeed very little of ZFC is needed to have
a theory complete w.r.t. E...EA sentences, as already NWER has such a
completeness property. Furthermore OPP  proves that satisfiability of
E...EA sentences w.r.t. the (incomplete in that respect) theories NWL and
NWLE  is decidable. A. Policriti was then able, through a combinatorially
rather complex
argument, to apply the method introduced in OPP to show that also the
satisfiability of E...EAA sentences w.r.t. NWL is decidable. (PP, "The
satisfiability problem for the class E..EAA in a set-theoretic setting"
Technical Report 13/92, Universita' di Udine, 1992).

Afterwards D. Belle' had  a new start on the problem and introduced a
method that led to the extension of such a decidability result for NWL, as
well as NWLR,  to the full class of the two block E...EA...A sentences. (BP
"Decidability of the E..EA..A-Class in the Membership Theory NWL" in
HajeK P., editor, "Godel '96" Lecture Notes in Logic 96, Springer Verlag
1996, reprinted by ALS and A K Peters, Ltd.([Godel 96]))

The major source of difficulty in trying  to extend such decidability
results to the real world is, as by now the reader may certainly guess, the
addition of the Extensionality axiom. The fact that restricted  AA formulae
can "code" infinite sets and the mentioned undecidability results, together
with a certain analogy with the Godel's class with identity, whose
undecidability followed as soon as satisfiable but not finitely satisfiable
formulae in the class were discovered, might hint at the undecidability
(even  non semidecidability) of true E..EAA sentences (even with restricted
A's).

However D. Belle' (still unpublished) by extending to the AA case the
method introduced in [Godel96] was able to show that the satisfiablility of
AA formulae in extensional and well founded structures is decidable, from
which she could infer that truth in V, as well as in HF, of E...EAA
sentences is decidable.
One may perhaps say that if  reflection of E..EAA sentences over HF is not
true, it is nonetheless not too far from truth, in the sense that if  an
AA formula is satisfiable, then  it is so with sets that can be finitely,
if not exactly easily, described. Whether and how such a "distance  from
truth" increases with the number of (possibly restrited) A's, including
the passage from two to three,  it remains to be seen and the decision
problem for E..EA..A sentences,  remains open.

As the above shows  the Extensionality axiom plays a crucial role as far as
the decision problem for the primitive language of set theory is concerned,
in that it can make it  solvable, when, in its absence, it wouldn't, as
mentioned at the beginning, or very difficult to solve, if not unsolvable,
in cases in which in its absence it has been proved to be  solvable.

By contrast if one turns attention to  derivability in fragments of set
theory of E...EA sentences, than it is the axiom of Foundation that seems to
play a crucial role in determining whether it is decidable or not, while
the Extensionality axiom remains quite irrelevant in that respect (BP "The
Decidability of the A...AE Class and the Axiom of Foundation", to appear in
Notre Dame Journal of Formal Logic, Vol. 42 n.1 2003). To my knowledge, the
more general problem of the derivability of E..EA..A sentences in fragments of
set  theory still remains to be explored.

References

[CFO] Cantone D., Ferro A., Omodeo E. "Computable Set Theory Vol.1"
International Series of Monographs on Computer Science. Oxford University
Press, 1989

[COP] Cantone D., Omodeo E., Policriti A. "Set Theory For Computing. From
Decision Procedurs to Declarative Programming with Sets"  Monographs in
Computer Science, Springer-Verlag, Berlin, 2001

[TMR]  Tarski A., Mostowski A., Robinson R. "Undecidable Theries" North
Holland 1953

[Va]  Vaught R. L. "On a theorem of Cobham concerning undecidable
theories"  In  Logic, methodology, anf philosophy of science: Proc.
of the 1960 International Congress, eds. E. Nagel, P. Suppes,
and A. Tarski, Stanford Univ. Press, Stanford, 1962, pp.14-25.

[Vl]  F. Ville "Decidabilite' des Formules Existentielles en Theorie des
Ensembles" C.R. Acad. Sc. Paris, t.272, Ser. A,  513-516, 1971

Franco Parlamento
Dipartimento di Matematica e Informatica
Universita' di Udine
Via delle Scienze 208
33100 UDINE
Italy

{parlamen at dimi.uniud.it}