Can one prove that there is only one proof?

Question

I have a simple (maybe even silly) question. Can one prove that there is only one proof?

The reason why I came up with the question is the proof of the famous Fermat's theorem by Andrew Wiles. Also Fermat himself said that he had a proof (although he said the margin was to small to write it down). I was wondering, what if you could prove that the way Andrew Wiles proved Fermat's theorem is the only way to prove this theorem, you could cancel out that Fermat had a proof himself (which would be quite hard I admit). (Indeed, one needs to define what is a single proof as @Bram28 says.)

Thank you for your comments.

Answer 1

Your question is rather a general one, but there has been quite a lot of research into logical systems where it makes sense to identify proofs modulo some natural notion of equivalence and then ask questions like "how many distinct proofs does such-and-such a proposition have".

The Curry-Howard correspondence for various logics provides contexts in which it is natural to ask about the number of proofs of a proposition. Under the Curry-Howard correspondence, propositions correspond to something like types in a functional programming language and well-typed functions correspond to proofs. The simplest example is simple type theory, where the logical language is built up from primitive types using implication only and implication is viewed as the function-arrow in the programming language. Terms of the $\lambda$-calculus that can be typed in simple type theory correspond to proofs in minimal propositional logic (i.e., intuitionistic logic but without the rule ex falso quodlibet).

The inhabitants of the type $(A \to A) \to (A \to A)$ are the Church numerals: the sequence of $\lambda$-terms that iterate their argument of type $A \to A$, $0, 1, 2, 3, \dots$ times ($\lambda f.\lambda x.x$, $\lambda f.\lambda x.f x$, $\lambda f. \lambda x.f(f x)$, $\ldots$),

The unique inhabitant of $A \to (B \to A)$ is the function $\lambda x.\lambda y.x$. Here $\lambda$-terms are being compared for equality modulo $\beta\eta$-equivalence (so something like $\lambda x .\lambda y.(\lambda z . z)x$ is considered equal to $\lambda x.\lambda y.x$.

See the book Proofs and Types by Girard, Lafont and Taylor for more about the Curry-Howard correspondence. It discusses much more powerful logics than simple type theory, such as Gödel's system $T$ and Girard's system $F$.

See the book Basic Simple Type Theory by Hindley for more about simple type theory. In particular, chapter 8 presents Ben-Yelles' algorithm for counting and enumerating the inhabitants of a type, or, equivalently, in logical terminology counting and enumerating the proofs of a proposition.

Answer 2

To expand on my earlier comment, if you undertake a proper study of logic, you will find that your question as stated is not meaningful at least for classical first-order logic, because any theorem has infinitely many proofs. Even if you ask for a minimum length proof, there may still be more than one, for many reasons. One is that there may be two statements that you need to deduce at some point in your proof, and can each be deduced from the previous statements. Then you could choose to deduce them in any order you wish, but the resulting proofs would be distinct. Another is that at some point you may introduce a new variable, possibly in an existential elimination step. You may very well have chosen to use a different variable name, and the resulting proof could be the same except for that variable name.

It is an interesting idea, but not obviously possible, to deterministically and unambiguously classify proofs in such a way to deal with all these issues and result in proofs being considered the same when humans consider them to be morally equivalent. This term "morally" is used by some mathematicians to refer (not to ethics but) to what they feel is the core or crux of a proof. When mathematicians say that all proofs of the fundamental theorem of algebra have to rely on some analysis and not purely algebra, that is the kind of vague notion that would need to be captured, for such a classification to be valuable enough in attempting to determine 'whether' Fermat could have had a proof of his famous conjecture.

---

But what you may be interested in is rather the field of Reverse Mathematics (which is a part of the bigger field of Proof Theory), where one studies which axioms are 'needed' to prove which theorems over a base system. For example, it is possible to make certain claims such as the following precise:

• You need induction to prove that every natural number is either a multiple of two or one more than a multiple of two. This is made precise as the claim that PA$^-$ does not prove the sentence "$\forall n \exists k ( n=k+k \lor n=k+k+1 )$". And this claim can be proven by constructing a model of PA$^-$ that does not satisfy this sentence.

• You need induction to prove that there is no rational square-root of two. Again this can be made precise as the claim that PA$^-$ does not prove "$\neg \exists m,n ( m·m=n·n·2 \land n>0 )$".

In both the above examples, PA proves the given sentence, and the only difference between PA$^-$ and PA is that PA also includes induction axioms.

These can be considered basic results in the spirit of reverse mathematics. More interesting to logicians are the axioms needed to prove some important theorems. Our modern conventional foundational system of ZFC is not really needed to prove most of real analysis, and it seems that ACA (see this for definition) is mostly sufficient. In between there are a lot of possible systems, and for any particular choice of base system we can ask the question of what additional axioms do we need to prove certain theorems. For example, over Z we cannot prove AC, and there are theorems that are equivalent to AC over Z, such as the theorem that if $S$ surjects onto $T$ then $T$ injects into $S$. In that sense we can say every proof of this theorem over Z+AC must use AC.

---

To what extent can we use the second viewpoint to address the question of whether Fermat had a proof? Well, we could attempt to find a base system $S$ and some additional axiom $A$ such that $S$ alone cannot prove FLT but $S+A$ can. Then we would have isolated $A$ as a crucial ingredient in any proof of FLT, and the question comes down to whether we believe Fermat could have used $A$ or not. If $A$ is some impredicative set-theoretic axiom, then we could be rather certain that Fermat was wrong.

In fact, this has been of interest to logicians and number theorists alike. On the surface, Wiles' proof invoked results that were proven in such generality as to involve a very strong axiom even beyond ZFC called Grothendieck universe existence. But experts quickly noticed that Wiles only used those results for certain special cases that definitely did not need those axioms. Even more so, experts now believe that Wiles' proof can be converted mechanically into a proof over an incredibly weak system, even weaker than PA! (See this.) And certainly Fermat knew and used the axioms of PA even if not in modern form. He had reductio ad absurdum in place of induction, for example. So it seems that Reverse Mathematics cannot actually answer the question about whether Fermat could prove FLT!

Therefore we are not really left with anything substantial. The only approach that seems possible now is to attempt to show that any proof of FLT over PA is far too long for Fermat to have possibly discovered it, but that sounds harder than even proving FLT...