FOM: Does Mathematics Need New Axioms?

[Harvey Friedman]

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
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 natural statements by H. Friedman 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 is the relevant metatheorem of interest in its own right.

THEOREM. 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.

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.