Proving the existence of a proof without actually giving a proof

Question

In some areas of mathematics it is everyday practice to prove the existence of things by entirely non-constructive arguments that say nothing about the object in question other than it exists, e.g. the celebrated probabilistic method and many things found in this thread: What are some things we can prove they must exist, but have no idea what they are?

Now what about proofs themselves? Is there some remote (or not so remote) area of mathematics or logic which contains a concrete theorem that is actually capable of being proved by showing that a proof must exist without actually giving such a proof?

Naively, I imagine that this would require formalizing a proof in such a way that it can be regarded as a mathematical object itself and then maybe showing that the set of such is non-empty. The only thing in this direction that I've seen so far is the "category of proofs", but that's not the answer.

This may sound like mathematical science fiction, but initially so does e.g. the idea of proving that some statement is unprovable in a framework, which has become standard in axiomatic set theory.

Feel free to change my speculative tags.

Answer 1

There are various ways to interpret the question. One interesting class of examples consists of "speed up" theorems. These generally involve two formal systems, $T_1$ and $T_2$, and family of statements which are provable in both $T_1$ and $T_2$, but for which the shortest formal proofs in $T_1$ are much longer than the shortest formal proofs in $T_2$.

One of the oldest such theorems is due to Gödel. He noticed that statements such as "This theorem cannot be proved in Peano Arithmetic in fewer than $10^{1000}$ symbols" are, in fact, provable in Peano Arithmetic.

Knowing this, we know that we could make a formal proof by cases that examines every Peano Arithmetic formal proof with fewer than $10^{1000}$ symbols and checks that none of them proves the statement. So we can prove indirectly that a formal proof of the statement in Peano Arithmetic exists.

But, because the statement is true, the shortest formal proof of the statement in Peano Arithmetic will in fact require more than $10^{1000}$ symbols. So nobody will be able to write out that formal proof completely. We can replace $10^{1000}$ with any number we wish, to obtain results whose shortest formal proof in Peano arithmetic must have at least that many symbols.

Similarly, if we prefer another formal system such as ZFC, we can consider statements such as "This theorem cannot be proved in ZFC in fewer than $10^{1000}$ symbols". In this way each sufficiently strong formal system will have some results which we know are formally provable, but for which the shortest formal proof in that system is too long to write down.

Answer 2

Henkin's completeness proof is an example of what you seek: It demonstrates that for a certain statement there is a proof, but does not establish what that proof is.

Answer 3

I'd like to expand Brian Tung's answer above, and add a further example.

In the following I'll be talking about first order (FO) sentences and structures. In a nutshell, a FO structure is a set $A$ with some operations and relations attached to it (e.g., a group, an ordered field, a graph), and a FO sentence is a statement you can write about $A$ with the restriction that $\forall x$ and $\exists x$ are only used for $x$ ranging over elements of $A$. Example from group theory are “$A$ is abelian”, “$A$ has exponent $2$”, but “$A$ has a finite subgroup” (“$\exists n\in\mathbb{N} : \dots$”) is not. An FO class is the class of all FO structures that satisfy a given set of FO sentences $\Phi$ (the class of all groups, all rings; less trivially, the class of $k$-vector spaces for a fixed $k$.)

Gödel's Completeness Theorem states that every FO sentence $\phi$ that holds in a FO class $\mathcal{M}$ has a formal proof from the axioms that define $\mathcal{M}$.

For the sake of clarity, let $\mathcal{M}$ the class of all rings. The important point to make is, no matter how you figured out that $\phi$ holds for every ring (using category theory, algebraic geometry or whatever), there must be some formal (finite!) proof that shows $\phi$ is a consequence of the axioms for $\mathcal{M}$.

Admittedly, having an FO proof of a statement would sound as something still too abstract (or useless) for an average mathematician. But we can push this example a little further.

It is a theorem by Jacobson that for each fixed $n\geq 2$, every ring that satisfies $\forall x: x^n=x$ is commutative. So if we take the axioms of rings and add $\forall x: x^{100}=x$, we obtain an FO class $\mathcal{M}'$ that satisfies $\forall x,y : xy = yx$. Actually, every axiom of $\mathcal{M}'$ is equational. Now Birkhoff's completeness theorem says the same as Gödel's but for equational proofs: Those that everyone here knows how to perform. That is, you start from the few axioms of $\mathcal{M}'$ and the only substantive rule to apply is

From $s=t$, conclude $p(s,y,z,\dots) = p(t,y,z,\dots)$,

where $p(x,y,z,\dots)$ is any expression built with the ring operations. So, despite Jacobson used other methods in his proof, for each $n$, there is purely elementary, simple-step, equational proof from the axioms of rings plus $\forall x: x^n=x$ of $\forall x,y : xy = yx$.

See this MO post for more on this example.

Answer 4

There are two different notions of proof that other answers did not distinguish.

Proofs from 'without'

One is when we are in a meta-system and talking about proofs inside a formal system. For example, the completeness theorem for first-order logic says that for any set $S$ of formulae and formula $φ$, we have $S \vdash φ$ if and only if $S \vDash φ$, which in English says that we can from $S$ derive $φ$ if and only if every model satisfying $S$ also satisfies $φ$. This is surprising at first since it states that every logically necessary consequence of $S$ (which is a semantic matter) is actually derivable (which is a syntactic matter). This somewhat answers your question, because the proof of the completeness theorem is non-constructive in some sense (uses weak Konig's lemma).

The completeness theorem has an important obvious consequence, which is that if $S \vDash \bot$, then also $S \vdash \bot$, which in English says that if $S$ is unsatisfiable (by any model) then from $S$ we can actually derive a contradiction. This is useful because derivations are always finite sequences of deductive steps, each of which use finitely many given or previously derived sentences, and so any derivation from $S$ uses only finitely many sentences from $S$. Thus if $S \vdash \bot$ then there is actually a finite subset $T$ of $S$ such that $T \vdash \bot$. Now since our deductive rules are sound, we also know that $T \vDash \bot$. Therefore any unsatisfiable set of sentences has a finite subset that is already unsatisfiable. This is the compactness theorem, which is an incredibly useful tool to prove facts about first-order logic.

There are of course also those results in logic concerning how proofs carry from one structure to another. For example, given any isomorphic structures over the same language, any sentence is provable for one if and only if it is provable for the other. This can be used to show for example that $i$ is not definable by a first-order formula over $\mathbb{C}$, namely that there is no formula $φ$ such that for any $x \in \mathbb{C}$ we have that $φ(x)$ is true if and only if $x = i$, because complex conjugation is an isomorphism that maps $i$ to $-i$. $\def\nn{\mathbb{N}}$ $\def\imp{\rightarrow}$

Proofs from 'within'

The other notion of proof arises when the formal system under consideration is nice, meaning that it is strong enough to manipulate finite strings, and one can algorithmically verify whether a string is a valid proof in it. Any nice formal system can reason (to some extent) about proofs in itself, and one such nice formal system is Peano Arithmetic, because there are tricks to encode strings as natural numbers and to extract from an encoding of a string the symbol at any arbitrary position. An excellent free online book is Godel without tears, that describes all these as the preliminaries needed to prove Godel's incompleteness theorems.

We still need to work outside in a meta-system that already knows $\nn$ in order to define "$\square_T φ$" as some first-order formula over a formal system $T$ that is true in $\nn$ if and only if $T \vdash φ$, which formula is constructed by saying in the language of $T$ "There is a string representing a proof of $φ$.". Note that this construction is completely constructive and can be done by a computer given any input formula $φ$, though the resulting formula is gigantic for some formal systems like $PA$ and $ZFC$.

For convenience we shall write "$T \vdash \cdots \square φ \cdots$" instead of "$T \vdash \cdots \square_T φ \cdots$". It turns out that every nice formal system $T$ satisfies the following 4 conditions:

1. (F) Modal fixed-point axiom: For any formula $P$ with only one free propositional variable, there is a formula $α$ such that $T \vdash α \leftrightarrow P(\square α)$.
2. (D1) Derivability condition 1: For any formula $α$, if $T \vdash α$ then $T \vdash \square α$.
3. (D2) Derivability condition 2: For any formula $α,β$, we have $T \vdash \square α \land \square( α \imp β ) \imp \square β$.
4. (D3) Derivability condition 3: For any formula $α$, we have $T \vdash \square α \imp \square \square α$.

The use of "$\square$" is to explicitly capture the properties of derivability in the form of a modal logic, in the sense that we no longer have to care what exact first-order formula "$\square_T φ$" denotes, and can in fact extend $T$ to a new formal system $T'$ that has "$\square$" as a new internal symbol just like "$\forall$" and "$\exists$". This way we can in some sense say that $T'$ actually can internally refer to the notion of provability in $T$.

The consistency of $T$ is equivalent to "$T \nvdash \bot$", which can be internally represented within $T$ by "$\neg \square_T \bot$", and this formula is in the meta-logic denoted by $Con(T)$. Godel showed that if $T$ is a nice first-order formal system that is omega-consistent (there is a model that has exactly the same natural numbers (equivalently strings) as the meta-system), then $Con(T)$ is independent of $T$, meaning that $T \nvdash Con(T)$ and also $T \nvdash \neg Con(T)$. By the completeness theorem, this then implies that $( T + Con(T) )$ is consistent, and $( T + \neg Con(T) )$ is also consistent.

Is this surprising? This does not contradict the completeness theorem, but implies that there are different models of $T$, some satisfying $Con(T)$ and some satisfying $\neg Con(T)$. For example, in the meta-system $\nn$ is called the standard model of $PA$, which satisfies $Con(PA)$, but there are also non-standard models of $PA$, some of which satisfy $\neg Con(PA)$ instead.

The above is known as the Godel incompleteness theorem. Rosser showed that even if we drop the condition that $T$ is omega-consistent, there is still some sentence that is independent of $T$, though $Con(T)$ may not be independent anymore, as we shall see in a later example.

Interestingly, an internal version can be proven using just (F) and (D1) to (D3), namely $T \vdash Con(T) \imp \neg \square Con(T)$, equivalently $T \vdash \square Con(T) \imp \neg Con(T)$, or using just boxes, $T \vdash \square \neg \square \bot \imp \square \bot$. If we rewrite it equivalently as $T \vdash \square( \square \bot \imp \bot ) \imp \square \bot$, then it is clearly just a special case of Lob's theorem, namely that for any sentence $φ$ we have $T \vdash \square( \square φ \imp φ ) \imp \square φ$, which also can be proven from the 4 conditions alone.

With the basics in place, we can now ask interesting questions. Is the converse to (D1) true? Yes if $T$ is satisfied by $\nn$, by construction of $\square_T$, but not necessarily in general, even if $T$ is consistent! For example, let $PA' = PA + \neg Con(PA)$. Then $PA'$ is consistent, equivalently $PA' \nvdash \bot$. But $PA' \vdash \square_{PA} \bot$ and hence (after a bit of work) $PA' \vdash \square_{PA'}\bot$. Strange, $PA'$ seems to say that itself is inconsistent, although it is not! The reason is that every model of $PA'$ is a non-standard model of $PA$. Every model of $PA$ has a standard element for each term of the form "$1+1+\cdots+1$", but non-standard models have extra non-standard elements. In any model of $PA'$ the existential sentence $\square_{PA'} \bot$ is witnessed by a non-standard element, and we can never find a standard witness that we can decode to obtain an actual proof of contradiction in $PA'$.

In short, the above considerations show that $PA'$ is consistent but derives "the existence of a proof of contradiction", yet there is in fact no such proof if $PA$ is consistent. This is a different sort of answer to your question, but may be worth thinking about. This also implies that consistency of a formal system is nowhere near sufficient to justify it, since we also do not want it to 'prove itself inconsistent'.

Next, is the 'converse' of (D3) true, namely is it true that $T \vdash \square \square φ \imp \square φ$ for any sentence φ? It turns out that it is also false, because $PA \nvdash \square \square \bot \imp \square \bot$, otherwise by Lob's theorem $PA \vdash \square \bot$, which is impossible because the standard model of PA does not satisfy "$\square \bot$".

Finally, notice that (D1) and (D3) would be implied by a rule (C), stating that $T \vdash α \imp \square α$ for any formula $α$. However, (C) is not valid for any nice omega-consistent formal system $T$, because otherwise $T \vdash Con(T) \imp \square Con(T)$, and hence $T \vdash \neg Con(T)$, contradicting Godel's incompleteness theorem.

These all show us that what a formal system can 'know' about proofs in itself is severely limited, and that one always needs to work in a meta-system which 'knows' more in some aspect if one wants a full picture of provability.

Answer 5

One can prove that either there is a proof that $1361$ is prime or there is a proof that $1361$ is composite without knowing which alternative is right.

But what if I can prove that there is a proof that $X$, where $X$ is some proposition? Is that a proof of $X$? In one sense it is: it is a convincing argument showing that $X$ must be true. However, logicians deal with something they call proofs that are mathematical objects in their own right, and rather than being intended to be intellectually convincing arguments, they are really a mathematical model of a sort of intellectually convincing argument. To prove that such a "proof" exists may amount to giving a proof in the sense of an intellectually convincing argument, but may also fail to be a "proof" in the sense in which logicians use the term.

Answer 6

Various good answers here, but the following seems to have been left out and is surely the simplest.

Consider the propositional calculus. (If you are not familiar with this term: essentially it is logic using basic terms like "and", "or", "not", but which does not have quantifiers "for all" or "there exists".)

One can determine whether or not a statement of propositional calculus is "always true" (technically, a tautology) by constructing a truth table.

One can also define proofs in such a system; a theorem is any statement which can be proved.

However, it turns out that tautologies and theorems are in fact the same. So, by constructing a truth table and proving that a statement is a tautology, you have also proved that it has a proof, but you have not given the proof.

I think this gives an answer to your question, though it should also be remarked that there is an algorithm which in effect "turns a truth table into a proof". So although in the situation I have described you would not have written down a proof, you would be able to do so by purely mechanical procedures.