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 &epsilon;<sub>0</sub> 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!