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!
 A: 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
A: 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.
A: The example I know is the 1933 Skewes' number, see 
http://en.wikipedia.org/wiki/Skewes'_number 
Looking at your question again, I have no idea whether this is what you wanted.
A: 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.
Gerhard "Ask Me About System Design" Paseman, 2010.04.11
A: Graham's number is surely a canonical example.
