18
votes
11answers
2k views

Are there any good nonconstructive “existential metatheorems”?

Are there any good examples of theorems in reasonably expressive theories (like Peano arithmetic) for which it is substantially easier to prove (in a metatheory) that a proof exists than it is ...