- #1

- 1,866

- 34

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

Theoretically, a proof could also proceed by way of a metatheorem, stating that a proof of the original theorem exists (for example, that a proof by exhaustion search for a proof would always succeed). Such theorems are relatively unproblematic when all of the proofs involved are constructive; however, the status of "pure existence metatheorems" is extremely unclear,

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.

Last edited: