FOM: Does Mathematics Need New Axioms?
Harvey Friedman
friedman at math.ohio-state.edu
Mon May 1 23:32:11 EDT 2000
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.
More information about the FOM
mailing list