Example of a pure existence metaproof

[disregardthat]

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.

 

[Hurkyl]

Proofs are finite, and can be validated by computation. Therefore, if you can prove that a proof of some theorem exists, it can be found by brute force, by enumerating all strings of symbols one at a time, and checking whether it is a proof of the theorem or not.

Of course, it's rather impractical.


(I'm assuming the specific idea you have in mind doesn't suffer from any issues of "internal" vs "external" or the like. e.g. things like Skolem's paradox)

 

[disregardthat]

Proofs are finite, and can be validated by computation. Therefore, if you can prove that a proof of some theorem exists, it can be found by brute force, by enumerating all strings of symbols one at a time, and checking whether it is a proof of the theorem or not.

Of course, it's rather impractical.


(I'm assuming the specific idea you have in mind doesn't suffer from any issues of "internal" vs "external" or the like. e.g. things like Skolem's paradox)

Ok, so you suggest that any proof can a priori be validated through computation? Is it not conceivable that any given method of enumerating strings to check whether a given proof it is actually a proof will necessarily fail (perhaps in the same sense as enumerating reals would), but that we simultaneously have a pure existence proof of the proof?

I guess it is possible to create a legal string based on any enumeration of strings which is not in the enumeration, i.e. strings are not recursively enumerable. But wouldn't any specific proof necessarily be "recursively enumerable" in some way, if that makes sense?

 

[yossell]

If you're thinking of a system where the axioms and rules are, say, non-denumerable, or not recursively presented, then the kind of metaproofs you have in mind might exist. But in normal systems, and in the traditional conception of proof, proofs are constructible objects.

 

[disregardthat]

If you're thinking of a system where the axioms and rules are, say, non-denumerable, or not recursively presented, then the kind of metaproofs you have in mind might exist. But in normal systems, and in the traditional conception of proof, proofs are constructible objects.

I see, so actually pure existence metaproofs can always be complemented with constructive metaproofs (in models with a finite set of axioms like ZFC), since any proof must be constructible.

Are there any examples of pure existence metaproofs at all in ZFC?

 

[yossell]

Um - just a slight correction to your post - the axioms only have to be recursive rather than finite. Indeed, if we're talking about first order ZFC, this theory is normally presented as having infinitely many axioms, separation and replacement being represented by a schema, and each having denumerably many instances.

I seem to remember some meta- stuff about the lengths of proofs, how you can show that adding certain parts of set-theory results in a conservative extension of certain parts of arithmetic, but that the corresponding proofs in arithmetic are hideously long, and practically impossible to carry out, while the set-theoretic versions are relatively simple. But I'm having a hard time finding that stuff, or getting it accurately from memory...and it may not be the kind of thing you're looking for anyway...