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 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!