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

-
Just for fun, you may find Löb's theorem interesting: Suppose $T$ is a sufficiently strong theory (say, Peano Arithmetic). If $T$ proves of some statement $P$ that "If there is a proof of $P$, then $P$ holds" then, in fact, $T$ proves $P$. Although this may look trivial, it is not, since it is essentially the incompleteness theorem repackaged. yudkowsky.net/rational/lobs-theorem – Andrés E. Caicedo Jan 19 '11 at 6:51
@Andres, thanks, that was nice! Not sure if I understood all of it, but that is along the lines of what I was looking for :) – picakhu Jan 19 '11 at 7:07
Along the lines of the end of Qiaochu's answer, I think the following needs to be clarified: in what sense does a proof that a proof of A exists not count as a proof of A? – Pete L. Clark Jan 19 '11 at 15:32
Pete: It could be that your theory $T$ is consistent but not sound. So, it won't prove $\phi\land\lnot\phi$ for any $\phi$, but it may very well prove false things (such as "there is a proof of $\phi$ in $T$"). Of course, if your theory is sound, then there is no difference. And "of course", the usual theories we assume are sound. (That's the point of the comment I made above: PA cannot prove its soundness.) – Andrés E. Caicedo Jan 19 '11 at 17:55
@Andres: ah, so that's what it's called. I think I learned about it on Scott Aaronson's blog, but he called it the "you-had-the-mojo-all-along" theorem. – Qiaochu Yuan Jan 19 '11 at 19:25

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.

-
about edit: That was why I was a bit reluctant to accept your answer. A proof that a proof exists is a proof. However, it is not a direct proof. In essence that one cannot generate the proof, but one knows a proof exists. An example that will probably not count is "let x be the largest even number, prove that there is a prime number larger than x". Now, the assumption is wrong, but we can say that there is no bound for prime numbers, so there must be a prime larger than x. yet, we have not answered the question directly. (we have not demonstrated the existence of a prime larger than x) – picakhu Jan 19 '11 at 6:06
I have never heard of zeroth-order logic. – AD. Jan 19 '11 at 6:15
@picakhu: no, that statement is just true without any further inspection, since a false statement implies anything. You seem to be worrying about the difference between a direct and indirect proof, which is different. @AD.: that's what the Wikipedia link is for. – Qiaochu Yuan Jan 19 '11 at 15:19
@picakhu: As an example of what Qiaochu's answer implies for propositional logic, you know that $(p \land \lnot p) \rightarrow (q \lor r)$ is provable because it is always true (everything follows from a contradiction). More generally, if you can make a truth table showing that a statement $A$ is always true, then this proves that $A$ is a theorem of propositional logic. But I'm sure you could draw a truth table to show that the statement is always true without knowing how to actually prove the theorem in the formal system. – Jason Jan 19 '11 at 18:54

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.

-

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

-
Also, I need to add the word computable (or "identifiable") to the first place where I mention $T$ in order to guarantee such a statement $Prov_T(x)$. In order to avoid bumping this question to the top of this list again, I'm making this as a comment instead of an edit. – Jason Jan 19 '11 at 18:31

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.

-