# Proofs that require the existence of large finite numbers

I know some proofs require the existence of large infinite ordinals, they give the fuel that drives induction principles. An example of this is the use of ε0 to give a consistency proof of peano arithmetic.

What I would like to find is proofs that require the existence of a large finite ordinal. thank you!

-
In set theory like system, arbitrary large finite ordinal can be proven from axiom of set theory without axioms of infinity. In arithmetic like system, you can prove the existence of arbitrary large number only with axiom related to successor. If this is what you mean then you won't get far if you attempt something weaker. – abcdxyz Apr 11 '10 at 20:05
Or may be there is another meaning to your question? – abcdxyz Apr 11 '10 at 20:07
I think the question is just asking about proofs where you have some kind of gigantic finite upper bound like Graham's number. – Harry Gindi Apr 11 '10 at 20:53
If that is the case, I would cite the proof that there exist infinitely many primes. – abcdxyz Apr 11 '10 at 20:56
As others have said, the word "require" in the title of the question and the logic tag create the apparently misleading impression that the OP is interested in a foundational system so weak that sufficiently large finite numbers do not exist! (Note that D. Zeilberger sincerely subscribes to this, at least as a philosophy; I had a fun email exchange with him which appears off of his opinions page.) The question rather seems to be: "What are some proofs where you can give an explicit, but ridiculously large, bound for something?" To me this is not so fascinating, but to each his own... – Pete L. Clark Apr 12 '10 at 7:33

This isn't addressed to logicians, but it may be of interest. I happen to know of an example in PDE that was necessary in proving the well-posedness of radial solutions of the Nonlinear Schrodinger Equation:

$$i u_{t}+\Delta u=|u|^{4}u$$

for which J. Bourgain was awarded his Fields Medal for treating. (J. Bourgain, Global well-posedness of defocusing 3D critical NLS in the radial case, JAMS 12 (1999), 145-171).

In one of the many many critical steps required in this proof, a bound on energy is required. A team (J. COLLIANDER, M. KEEL, G. STAFFILANI, H. TAKAOKA, and T. TAO) have now treated the non-radial case and make explicit the large ordinals used for bounding the energy. I quote from page 36 of their paper "Global well-posedness and scattering for the energy-critical nonlinear Schrödinger equation in R^3":

"If one then runs the induction of energy argument in a direct way (rather than arguing by contradiction as we do here), this leads to very rapidly growing (but still finite) bound for M(E) for each E, which can only be expressed in terms of multiply iterated towers of exponentials (the Ackermann hierarchy). More precisely, if we use X ↑ Y to denote exponentiation X^Y, X↑↑Y :=X↑(X↑...↑X) to denote the tower formed by exponentiating Y copies of X, X↑↑↑Y :=X↑↑(X↑↑...↑↑X) to denote the double tower formed by tower-exponentiating Y copies of X, and so forth, then we have computed our final bound for M(E) for large E to essentially be M(E) ≤ C ↑↑↑↑↑↑↑↑ (CE^C). This rather Bunyanesque bound is mainly due to the large number of times we invoke the induction hypothesis Lemma 4.1, and is presumably not best possible."

http://arxiv.org/abs/math/0402129

-

Large numbers (Ackerman of Ackerman of Ackerman of ...... of something) tend to creep into modern additive combinatorics arguments due to some dark ergodic witchcraft tool which they call "PET induction" (PET = polynomial exhaustion technique), and some of its cousins. You can easily google-up the terms and find references; sadly understanding what they actually do is (at least for me) a different matter altogether.

-

The example I know is the 1933 Skewes' number, see

Looking at your question again, I have no idea whether this is what you wanted.

-

Large numbers are used in things like the busy beaver problem. However, since it has given me some good rep in the past, I once again recommend Harvey Friedman and his Enormous Numbers in Real Life. You can search Math Overflow for Harvey and see some of the posts which quote part of his article.