# Example of a pure existence metaproof

• disregardthat
In summary, a pure existence theorem is a theorem that states the existence of something without providing a construction for it. This can be problematic as theorems are traditionally considered independent of their proofs. Pure existence proofs, on the other hand, demonstrate the existence of something in a non-constructive manner. This concept also applies to metaproofs, where a proof of the existence of a proof is given without explicitly constructing the proof. While pure existence proofs can always be complemented with constructive proofs in models with a finite set of axioms such as ZFC, it is unclear if pure existence metaproofs exist in this system. There may be examples of pure existence metaproofs in systems with non-denumerable axioms, but in
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.

Last edited:

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)

Hurkyl said:
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?

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.

yossell said:
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?

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

## 1. What is a "pure existence metaproof"?

A pure existence metaproof is a concept in philosophy that seeks to prove the existence of an entity without relying on any external evidence or prior assumptions. It is a means of demonstrating the self-evident existence of something that cannot be proven through traditional scientific or logical methods.

## 2. Can you provide an example of a pure existence metaproof?

One example of a pure existence metaproof is René Descartes' famous statement, "Cogito, ergo sum" or "I think, therefore I am." This statement relies on the self-evident fact that one must exist in order to think, and therefore, the existence of the self is proven without the need for any external evidence or assumptions.

## 3. How does a pure existence metaproof differ from traditional scientific or logical proofs?

A pure existence metaproof differs from traditional proofs in that it does not rely on external evidence or assumptions. In traditional scientific or logical proofs, evidence and assumptions are used to support a conclusion, while a pure existence metaproof seeks to prove the existence of something without any external support.

## 4. Is a pure existence metaproof considered a valid form of proof in the scientific community?

The validity of a pure existence metaproof is a debated topic in the scientific community. While some may argue that it lacks empirical evidence and therefore cannot be considered a valid form of proof, others may argue that it is a valid philosophical concept that can provide insight into the nature of existence.

## 5. Are there any limitations to using a pure existence metaproof?

One limitation of using a pure existence metaproof is that it may not be applicable to all entities. Some may argue that it can only be used to prove the existence of abstract concepts or the self, and may not be applicable to things that can be observed or measured in the physical world.

Replies
3
Views
1K
Replies
11
Views
1K
Replies
19
Views
3K
Replies
9
Views
1K
Replies
3
Views
768
Replies
9
Views
843
Replies
15
Views
2K
Replies
2
Views
4K
Replies
7
Views
2K
Replies
1
Views
1K