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