Existence Proofs

This may be a stretch, but are there examples of proofs that prove that a proof exists for a theorem.

For example, if A is a theorem, and it is too tedious to prove that, is it possible to show that a proof exists for theorem A.

Solution 1:

Sure. For example, using the completeness theorem, showing that a statement is semantically true is equivalent to showing that it has a syntactic proof, even though you don't have to actually give such a syntactic proof. For example (!), you can show that a statement in zeroth-order logic is a tautology by arguing by contradiction, and it follows by the completeness theorem that that tautology has a proof from the axioms of zeroth-order logic.

I can't immediately think of any examples of "real" theorems with this property, but here's one way to generate a class of them: suppose you can reduce an infinitary statement to the checking of finitely many cases. Then without checking them, you know that the act of checking them corresponds to the proof of some theorem even though you know neither (all the steps of) the proof nor the theorem! Maybe you want to know the theorem as well, though.

There is also the notion of a zero-knowledge proof. This might not be quite what you had in mind, though, as it is interactive and probabilistic.

Upon further thought, without a clear distinction between the first and second uses of the word "proof" in your question (as is made by the first example above), I'm not sure what the difference between having a proof and having a proof that a proof exists is.

Solution 2:

I think one example of what you are talking about is the constant applications of the Deduction Theorem that are implicit in most of mathematics; the Deduction Theorem which says that if you can prove $B$ from $\Delta\cup\{A\}$, then from $\Delta$ you can prove $A\rightarrow B$: $$\Delta\cup \{A\}\models B \Longrightarrow \Delta\models A\rightarrow B.$$ Hofstadter, in Goedel, Escher and Bach, calls it "the fantasy rule", because in order to prove that $A\rightarrow B$ holds, you get to fantasize that you actually know $A$ is true and then prove $B$.

The proof of the Deduction Theorem actually tells you how to take a proof of $B$ from $\Delta\cup\{A\}$ and use it to produce a proof of $A\rightarrow B$ from $\Delta$. The procedure is mechanical, but somewhat involved; a short proof of $B$ from $\Delta\cup\{A\}$ will usually yield a somewhat lengthy proof of $A\rightarrow B$ from $\Delta$.

In a sense, almost every time we prove a theorem we are not really proving the theorem; the vast majority of theorems are of the form $\Delta\models A\rightarrow B$, but we almost invariably prove $\Delta\cup\{A\}\models B$ (when a theorem says something like "If $A$ and $B$ are disjoint, then $|A\cup B|=|A|+|B|$", then the proof will usually start with "Assume that $A$ and $B$ are disjoint..."). When we do so, what we have done is prove that a proof exists, without actually providing the proof of the proposition we claim to be proving.

There are similar "Metatheorems" for other typical rules proof arguments, like proofs by cases, proof by contradiction, etc.

Solution 3:

Somewhat along the lines of Andres's comment:

Suppose you were to assign every formula in arithmetic (e.g., $0 = 0$) a unique Natural number in such a way that you could mechanically figure out which formula corresponded to which Natural number. Then for any consistent (non-contradictory) theory $T$ that includes the 15 basic rules of arithmetic from PA^- and only includes statements true about the Natural numbers, there will be some formula $Prov_T(x)$ representing provability from $T$ under this coding. In particular, this means that if $\varphi_n$ is some formula assigned Natural number $n$ under our mechanical coding procedure and $T \vdash Prov_T(n)$ ("T proves that $\varphi_n$ is provable"), then $T \vdash \varphi_n$ ("T proves $\varphi_n$"). The representability of provability also means that if $T \vdash \lnot Prov_T(n)$ ("$T$ proves that $\varphi_n$ is not provable"), then $T \nvdash \varphi_n$ ("$T$ does not prove $\varphi_n$").

Incidentally, Gödel's first incompleteness theorem implies that there will be a statement $\varphi_n$ so that any (consistent) set of "identifiable" axioms $T$ true in the Natural numbers that includes all of those found in PA^- cannot prove $\varphi_n$ nor $\lnot\varphi_n$. In fact this statement was of the form $\lnot Prov_T(m)$ for some Natural number $m$. If $T$ also includes all axioms of full Peano Arithmetic, then by Gödel's second incompleteness theorem, we can find such a statement by using any Natural number $m$ coding a statement $\lnot\varphi$ where $\varphi$ is actually provable from $T$.

Solution 4:

If a theory $T$ proves a sentence $\varphi$ and is strong enough arithmetically (say includes $PA$), then we can prove inside $T$ that there is a proof of $\varphi$.

On the other hand, a theory $T$ might be able to prove that a formula $\varphi$ has a "proof", while the theory $T$ cannot prove $\varphi$, in fact $T$ might prove that a statement has a proof while there is no such proof at all (I mean that the statement that $\varphi$ has a proof is false in the standard model). However, this does not happen in practice because theories we use in mathematics are 1-consistent (or at least we believe so), i.e. any $\Sigma_1$ formula provable in $T$ is really true.

One can also ask if there are proofs which are too long to write them, but we can proof their existence, and the answer is also positive.