Example of a "pure existence metaproof" http://en.wikipedia.org/wiki/Existence_theorem A pure existence theorem is a theorem which states the existence of something, but the proof of the theorem does not indicate a construction of the thing in question. As the article mentions, this is problematic due to the principle (in classical logic I guess) that theorems are independent of proofs of them. So we will rather call a pure existence proof a proof which demonstrates the existence of something but which also is non-constructive. There are also examples of pure existence proofs of theorems for which no constructive proof is possible, for example the existence of a maximal ideal of any ring. The article above contains the sentence Hence a theorem could essentially be proved by means of (what I will call) a "metaproof": a proof which proves the existence of a proof of the theorem. Pure metaproofs proves the existence of proofs in a non-constructive manner, i.e. it does not contain a procedure for which a direct proof could be constructed. On to my question: are there examples of pure metaproofs of theorems for which no constructive metaproof exists? That is, as I interpret it, a proof of the existence of a proof of a theorem for which no proof can be explicitly given.