[FOM] On the decision problem for fragments of set theory
Franco Parlamento
parlamen at dimi.uniud.it
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}
More information about the FOM
mailing list