FOM: counterexamples (?) to FOM 94: Relative Completeness

[Matthew Frank]

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
a theory. 

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.

--Matt Frank