FOM: Does Mathematics Need New Axioms?

[Harvey Friedman]

I am grateful to Robert Solovay (private communication) for causing me to
realize that my posting of 11:32PM 5/1/00 needs significant amplification.
Here is a revised version. In particular, the Theorem that I gave there is
correct, but has to be made relevant to the situation at hand since the
Theorem talks about Pi-0-1 sentences yet the case at hand is a SIgma-0-1
sentence.

Also, the final comment about Sigma-0-0 sentences is clarified.

Steel 11:40AM 5/1/00 wrote

>   ZFC + V=L + -Con(ZFC) decides all remotely natural questions we know
>of, and is very likely consistent. What's wrong with it on pragmatic
>grounds?

Steel then gives an answer to his own question. Here we give an alternative
(or sharpened)
answer to Steel's question.

The background here is that

a) ZFC + V = L seems to decide all mathematically natural questions except
for those by H. Friedman and a few of his close associates;

b) ZFC + V = L + notCon(ZFC) in addition decides all of those exceptions by
H. Friedman a few of his close associates. This is because they are
provably equivalent to the consistency of large cardinals.

But we show that

*):    b) is false if we take into account lengths of proof.

In particular,

**)   there are mathematically natural statements by H. Friedman (not
metamathematical) which cannot be settled
in ZFC + V = L + notCon(ZFC) in fewer than, say, A(1000) symbols, where A
is the Ackerman function.

Specifically, I keep coming up with sentences of the form

(for all n)(phi(n))

which are generally equivalent to 1-Con(large cardinals), and where phi(n)
is Sigma-0-1. Here typically n stands for the arity of a function, or a
dimension. So it is natural to set n to be various small numbers, say, n =
4. I fully expect that the statement

phi(4)

is a Sigma-0-1 sentence which cannot be settled in ZFC with fewer than,
say, A(1001) symbols, where A is the Ackerman function.  It then follows
that

phi(4)

cannot be settled in ZFC + V = L + notCon(ZFC) with fewer than, say,
A(1000) symbols, where A is the Ackerman function.

Here are some metatheorems concerning the lack of power of notCon(T) to
shorten proofs.

THEOREM 1. Let T be any reasonable theory and phi be a Pi-0-1 sentence. For
any proof of phi in T + notCon(T) there is a proof of phi in T that is not
much longer.

To see this, let alpha be a proof of phi in T + notCon(T); i.e., a proof of
Con(T) in T + notphi. Then we get a proof not much longer than alpha of
Con(T + notphi) in T + notphi. From the proof of Godel's second
incompleteness theorem, we get a proof not much longer than alpha of an
inconsistency in T + notphi; i.e., a proof not much longer than alpha of
phi in T. QED

Here is a statement of my finite Godel's theorem:

THEOREM 2. Let T be any reasonable theory. Then, asymptotically, any proof
in T of "T has no inconsistency of size at most n" must have size at least
sqrt(n).

{I don't remember exactly, but I may have originally stated this with a
lower bound like n^1/4 , asymptotically, and I think that sqrt(n) is the
best known currently. See Handbook of Proof Theory, ed. Buss, which has an
article by Pudlak covering this topic, referring to my original work.}

This can be sharpened as follows:

THEOREM 3. Let T be any reasonable theory. Then, asymptotically, any proof
in T + notCon(T) of "T has no inconsistency of size at most n" must have
size at least sqrt(n).

Proof: Apply Theorem 1. QED

LEMMA 4. There is a short proof in ZFC + V = L that phi(4) implies "ZFC + V
= L has no inconsistency of size at most A(1002)".

THEOREM 5. There is no proof in ZFC + V = L + notCon(ZFC) of phi(4) of size
at most A(1000).

Proof: Suppose there is. By Lemma 4, there is a proof in ZFC + V = L that
"ZFC + V = L has no inconsistency of size at most A(1002)" of size at most
A(1001). This contradicts Theorem 2. QED

Probably the same thing will happen at the Sigma-0-0 level instead of the
Sigma-0-1 level. This is because I also have sentences of the form

(for all n)(phi(n))

where phi is Sigma-0-0. It is expected that I can also set n = a small
number like 4 and get a blowup in the length of proof of phi(n), although
the computations are going to be more delicate and somewhat down the road.
Of course, here we are talking about an exponential blowup like 2^1000,
enough to conclude total impracticality even for computer aided proofs and
abbreviation power, but not huge blowups involving the Ackerman function.
The needed margin is to be obtained because phi(n) will naturally live in a
couple of power sets above n, rather than below n.