FOM: counterexamples (?) to FOM 94: Relative Completeness
mfrank at math.uchicago.edu
Sun Oct 29 11:38:58 EST 2000
Harvey Friedman's FOM post #94 (Sep. 19) made a "CONJECTURE: All of the
main systems of f.o.m. that are finitely axiomatizable, and are inteneded
to fully formalize a kind or level of mathematical reasoning, are
relatively complete", i.e. such a theory T proves or refutes all sentences
P less complicated then the minimal complexity of axiomatizations of T.
While this conjecture surprised me with its robustness, I would like to
point out some possible counterexamles.
Ex. 1: T=any constructive set theory (perhaps with bounded
separation/replacement so as to make it finitely axiomatizable), P = "for
all x, for all y, x in y or not x in y".
There are set theories intended to formalize constructive mathematical
practice; the principle of excluded middle is independent of them, and
less complicated than some of their axioms.
Ex. 2: T= ZFC- with bounded separation, P = the axiom of foundation.
Here we can write P as "forall x, exists y, forall z, z in x -> y in x and
not z in y." (complexity 18 by the proposed way of counting), whereas T
seems to require complexity at least 19 for even a weak power set axiom
like "forall x, exists y, forall z (forall w, w in z -> w in x) -> z in
y." (This is weak because it has a conditional where a biconditional
would be more usual; but the formal languages of post #94 do not include
biconditionals. In any case, this or other axioms of T might require even
more complicated formulas.)
To make this a counterexample, one also needs to argue that ZFC- with
bounded separation can reasonably be intended to formalize ordinary
mathematical practice. It seems that (set-theoretically formalized)
ordinary mathematical practice does not make implict appeals to the axiom
of foundation as it does to other set-theoretic axioms.
Ex. 3 (more questionable; I don't have the references with me to do this
right): T=a Boolos-style neo-logicist axiom system, P="something is not a
number", i.e. "exists x, forall y, not y eta x". These systems are
characterized by axioms asserting the existence of numbers, axioms which
are certainly more complicated than P. Perhaps someone else can give a
reference for one of these axiom systems, say whether they are finitely
axiomatizatable, and defend it as fully formalizing a kind or level of
mathematical reasoning. In any case, this potential example points out
that small changes in language (in particular, including anything like a
cardinality operator) can have big effects on the relative completeness of
Any of these examples might also be considered with respect to axiom
schemes (so that finite axiomatizability is not needed), and the
appropriate sort of relative completeness.
All in all I remain skeptical of anything foundational with a quantitative
measure of simplicity/complexity. Still the above conjecture points to an
interesting phenomenon: we would be unlikely to accept an axiom scheme as
foundational if it left too many simple questions unanswered.
More information about the FOM