[FOM] Infinity and the "Noble Lie"

[friedman@math.ohio-state.edu]

Shipman wrote:

> There are no famous Pi^0_1 theorems which have been shown to be
> unprovable without the Axiom of Infinity, so the question is still
> avoidable by saying "I believe the use of Infinity in the proof of X
> will eventually be eliminated, and in any case I don't think a
> contradiction will ever be found in ZFC, so I'm happy to simply assert
> X."

No famous ones at the moment, but I am trying to remedy this by
constructing better and better nonfamous examples, that will eventually
get famous - because of a combination of their intrinsically compelling
nature and the development of compelling new areas of mathematics in which
they prominently reside. (These examples even require large cardinals of
various levels). You can wish me luck. Certainly by the year 2100 there
will be an overwhelming sea change of the most profound and satisfying (to
logicians) kind.

> But for Pi^0_2 this is not an option. The Graph Minor theorem
> provably requires the Axiom of Infinity (query for Harvey: is there a
> proof in ZFC of the Graph Minor Theorem which avoids the use of the
> Power Set axiom, or does the theorem actually require an uncountably
> infinite set?).

The Graph Minor Theorem proves the consistency of Pi11-CA0 over RCA0, and
thus has a very substantial inherent impredicativity. One has to form sets
of natural numbers obtained only through quantification over what amounts
to all sets of natural numbers - in substantially stronger senses than the
earlier Kruskal tree theorm. GMT is certainly proved in weak fragments of
Pi12-CA0. This is a more exact answer than "requires an uncountable set",
although it is easy to identify reasonable frameworks for which "requires
an uncountable set" is literally true.

Harvey Friedman