When are two proofs of the same theorem really different proofs

Question

Many well-known theorems have lots of "different" proofs. Often new proofs of a theorem arise surprisingly from other branches of mathematics than the theorem itself.

When are two proofs really the same proof? What I mean is this. Suppose two different proofs of theorem are first presented formally and then expanded out so that the formal proofs are presented starting from first principles, that is, starting from the axioms. Then in some sense two proofs are the same if there are trivial operations on the sequence of steps of the first formal proof to transform that proof into the second formal proof. (I'm not sure what I mean by "trivial")

Answer 1

You've hit on an area of research that's picking up some momentum at the moment. It involves connections between proof theory, homotopy theory and higher categories. The idea is that a proof or deduction is something like a path (from the premiss to the conclusion), and when you "deform" one proof into another by a sequence of trivial steps, that's something like a homotopy between paths. Or, in the language of higher-dimensional categories, a deduction is a 1-morphism, and a deformation of deductions is a 2-morphism. You can keep going to higher deductions.

There are close connections with type theory too. If you have the right kind of background, the following papers might be helpful:

Awodey and Warren, Homotopy theoretic models of identity types, http://arxiv.org/abs/0709.0248

Van den Berg and Garner, Types are weak omega-groupoids, http://arxiv.org/abs/0812.0298

Answer 2

There is a very nice paper of Wagon, which can serve as a sort of case study. The paper presents fourteen different proofs of the following theorem.

Theorem. If a rectangle $R$ is tiled by rectangles, each of which has at least one integer side, then $R$ itself has at least one integer side.

If you have not thought about the problem, you may want to think about it before reading the paper. At first glance some of the proofs certainly appear different. For example, there is a proof using a complex double integral, and another which uses Sperner's lemma.

In fact, all fourteen proofs are shown to be different by considering generalizations of the problem. It turns out that no two of the fourteen proofs work for the same set of generalizations. I do not know if this can be formalized in general.

The paper contains an amusing Appendix titled Appendix to justify that the proofs are different, listing the generalizations that each proof works for.

Answer 3

This of course is a deep question in the philosophy of mathematics. The program mentioned by Tom Leinster is certainly a very interesting contribution to this, but if it proceeds at a purely mathematical level then at most it can define an equivalence relation on the class of proofs. There's still a further question whether this equivalence relation really is "the right one" to capture the notion of "same" or "different" proofs.

Also, note that there's an open question as to whether mathematical proofs really are the sort of thing studied by proof theorists. Certainly the sort of thing that is published in a math journal is not the sort of thing that is studied by proof theorists. To cite the most obvious differences, the former have words of English in them (or French or Japanese or Russian or some other language) while the latter don't. But for more significant differences, note that the former also cite well-known results from the literature, and skip steps that are sufficiently obvious to the reader, while the latter don't.

You can avoid this problem by assuming that published proofs are converted into formal proofs by means of spelling out all the steps in the proof of the well-known theorem, or the obvious fact. But this might not preserve the notion of "same proof".

For instance, consider a theorem that in some sense only has one proof, which happens to rely essentially on quadratic reciprocity. Do we really want to say that this theorem actually has just as many distinct proofs as quadratic reciprocity does?

There are lots of interesting questions here about the relation of proof theory to actual proofs, and what light it can shed on this intuitive notion of sameness of proof. And of course, there is probably also light to be shed in the other direction too, as our technical mathematical results in proof theory and category theory absorb results from the intuitive ideas we have about proof sameness.

Answer 4

Maybe this might be of interest: Blass, Andreas; Dershowitz, Nachum; Gurevich, Yuri, When are two algorithms the same?, Bull. Symb. Log. 15, No. 2, 145-168 (2009). ZBL1192.03021. JSTOR link.

Here is a free PDF version from the first author's webpage.

Answer 5

It is indeed an open task of proof theory to give a good formal definition of when two proofs should be considered equivalent.

A usual thing is to consider a category with formulas as objects and equivalence classes of proofs as morphisms, where two proofs are considered equivalent if they have the same normal form (in many logics every proof can be brought into a unique normal form, i.e. a chain of deductions of which the first half are e.g. elimination rules and the second half introduction rules). Moreover this transformation of a proof into normal form can often be done algorithmically and is then described by a rewriting system. This provides the link of syntactic proof theory to homotopy theory, mentioned by Tom Leinster, it can be made very plausible via rewriting systems, see e.g Y. Lafont's homepage or the corresponding sections of P.-A. Mellies' homepage. Also check out the "Categorical Semantics of Linear Logic" paper on Mellies' page - there he considers invariants of proofs, each of which should yield a notion of equivalence!

However all of these are syntactical notions of equivalence and, as Terry Tao mentions in his comment at Gowers' blog (see the link in Justin's answer), there is also a semantic notion of equivalence saying that two proofs are equivalent if they have the same degree of generalizability. And while the syntactic notions of equivalence capture quite well the formal operations by which one can relate different proofs, the real challenge is (imho) to give a formal definition of semantic equivalence and recognize it syntactically!

The earliest published attempt I know of are the two articles J. Lambek, Deductive systems and categories and J. Lambek, Deductive systems and categories II, in: Lecture Notes in Mathematics 86 (Springer, Berlin, 1969), especially the second where, if I remember well, he does in fact try to give a syntactic characterization of semantic equivalence. The idea is this: A proof A is a specialization of another proof B, and B a generalization of A, if A arises from B by substituting something into the variables of B. Proof A is more general than proof C if any maximal generalization of C uses more hypotheses than some maximal generalization of A...

Answer 6

My opinion, and it's only an opinion, is that it would be very difficult to formalise what it means for two proofs to be different. Here's an intuitive reason why. If I give you two proofs of theorem X, and both proofs are exactly the same, except that one proof had a couple of extra lines in the middle which proved an intermediate result which was of no relevance, then surely these two proofs would be "the same". So surely any sort of "sameness" equivalence relation that one is trying to formally set up on the set of proofs of a statement would have to allow for deleting or adding lines to a proof that aren't used. But now there's perhaps a problem, because proof A and proof B of theorem X might both be "the same" as proof C, where proof C is the disjoint union of proofs A and B.

On the other hand it's manifestly clear that sometimes two proofs of a fact are "different" on an intuitive level. For example I remember doing the exercise as an undergraduate that the map SL(2,Z)-->SL(2,Z/nZ) was surjective, but I used the fact that there was infinitely many primes in an AP. A couple of days later I found a proof that didn't use this and was entirely elementary. Clearly the proofs were "different". All I'm saying is that although this is in some sense obvious, what I'm saying is that it might be tough to formalise.

Answer 7

Some additional recent references on "equivalence" or "homotopy" between proofs include

1. S. Awodey, Type theory and homotopy, also on the arXiv

2. Various notes by V. Voevodsky

Not that I understand much of these - certainly not much enough to see a down-to-earth example of two explicit proofs of some elementary statement that are not homotopic, as detected by some invariant. Is anyone able to provide such an example?

3. J. Conant and O. Thistlethwaite, Boolean formulae, hypergraphs and combinatorial topology

Then, there are two very basic things to note. First, the question itself dates back to Hilbert's (would-be) 24th Problem, which R. Thiele discovered in Hilbert's notebooks a century later (translation and remarks by Thiele, boldface mine):

The 24th problem in my Paris lecture was to be: Criteria of simplicity, or proof of the greatest simplicity of certain proofs. Develop a theory of the method of proof in mathematics in general. Under a given set of conditions there can be but one simplest proof. Quite generally, if there are two proofs for a theorem, you must keep going until you have derived each from the other, or until it becomes quite evident what variant conditions (and aids) have been used in the two proofs. Given two routes, it is not right to take either of these two or to look for a third; it is necessary to investigate the area lying between the two routes. Attempts at judging the simplicity of a proof are in my examination of syzygies and syzygies between syzygies. The use or the knowledge of a syzygy simplifies in an essential way a proof that a certain identity is true. Because any process of addition [is] an application of the commutative law of addition etc. [and because] this always corresponds to geometric theorems or logical conclusions, one can count these [processes], and, for instance, in proving certain theorems of elementary geometry (the Pythagoras theorem, [theorems] on remarkable points of triangles), one can very well decide which of the proofs is the simplest. [Part of the last sentence is not only barely legible in Hilbert’s notebook but also grammatically incorrect. Corrections and insertions that Hilbert made in this entry show that he wrote down the problem in haste.]

Second, there is a good reason why the question has been traditionally treated in an intuitionistic setup, from Seely to Awodey. (Note that intuitionistic proofs are perhaps less scary if thought of as computer programs, via the Curry-Howard correspondence.) The reason is that in classical logic, with a standard formalization of the notion of "proof", every two proofs of the same statement must be equivalent with every reasonable notion of equivalence. The idea is in Kevin Buzzard's answer. For a rigorous explanation see Yves Lafont's Appendix B in Girard's Proofs and Types (The standard sequent calculus notation used in that appendix is introduced in the very beginning of the book.) It looks like Alessio Guglielmi has some way of overcoming this difficulty by using a non-standard proof-theoretic setup which I wish I understood better.

Answer 8

Maybe this blog entry by Gowers will be of interest.

Answer 9

Some other answers have alluded to this, but just to spell it out explicitly: The Curry-Howard isomorphism, in one of its simpler forms, says that objects of the free cartesian closed category CCC[S] on a set S of objects correspond to statements of the multiplicative fragment of intuitionistic logic (things we can build from /\ and ⇒) with free variables from S, and there is at least one morphism P → Q in CCC[S] iff P ⇒ Q is a theorem. Thus we can regard a morphism P → Q as a "proof" of P ⇒ Q. There may be several morphisms from P to Q; for instance if A ∈ S and P = A × A, Q = A, then there are exactly two morphisms from P to Q (projection to the first or second factor), which we can regard as two different proofs of the theorem (A /\ A) ⇒ A.

Probably the easiest way to see what the different proofs are in this system is to use the third part of the Curry-Howard isomorphism: morphisms P → Q in CCC[S] correspond to functions in the simply typed lambda calculus of type P ⇒ Q, where × in CCC[S] is interpreted as the product of types and the internal Hom as a function type. For instance there are two functions of type (A * A) → A, namely λ(a, b). a and λ(a, b). b. A more interesting example: the theorem (A ⇒ A) ⇒ (A ⇒ A) has one proof for every natural number, corresponding to λ f. λ x. f (f (... (f x)...)). See This Weeks' Finds week 240 for more along these lines.

Answer 10

Because nobody seems to have made the following (admittedly rather trivial) point so far in the discussion around this (old) question, I'd like to offer the following (contrived) example of a theorem with two seemingly very different proofs:

Theorem: either Fermat's last theorem holds, or the Poincaré conjecture holds.

Proof #1: [insert the contents of works by Ribet, Wiles, etc.] so Fermat's last theorem holds, so the stated theorem holds. ∎

Proof #2: [insert the content of works by Thurston, Perelman, etc.] so Poincaré's conjecture holds, so the stated theorem holds. ∎

I think we will all agree that if there exists a useful notion of “really different proofs”, then these two proofs should, indeed, be really different.

More generally, this argument shows something like this: if there exist two theorems which are “essentially different”, then there exists a theorem with two proofs which are “essentially different”. Or, contapositively, if all proofs of any given theorem are “essentially the same”, then in fact all theorems are “essentially the same”.

Answer 11

You can express any Proof as a typed Lambda-Term, looking at the theorem as a Type. This term can be normalized. I would say, if two of these Proof-Terms have the same normal form, then they name the same proof.

Answer 12

This might be of interest: http://arxiv.org/pdf/cs.LO/0610123

• Straßburger, Lutz (20 October 2006), "Proof Nets and the Identity of Proofs", Technical Report 6013, INRIA

Answer 13

The other posters have well pointed out that the proof identity problem can be approached from various directions. If you're interested in proof theory and are willing to delve into natural deduction and category theory, you might be interested in two proposals for addressing the proof identity problem: the Normalization Conjecture and the Generality Conjecture. See Dozen's "Identity of proofs based on normalization and generality" for a nice introduction to these two ways of viewing the proof identity problem.

Answer 14

I would distinguish proofs by what else they show beyond the fact that is "officially" proved.

For example, to show that Liouville's and Cantor's proof about the existence of transcendental numbers are different, I would argue:

• Liouville's proof shows that certain numbers are not algebraic, but it does not say anything about the set of algebraic numbers.

• Cantor's proof shows that the set of algebraic numbers is smaller than the set of real numbers, without constructing any transcendental number explicitly.

Since the additional facts shown by Liouville's and Cantor's proof are different, the proofs are different. (Note that I do not refer here to easy corollaries but to facts which are essential to the proofs.)

Answer 15

In combinatorics it is often useful to find bijections between two combinatorial structures one is studying. An example is a bijection between 321-avoiding permutations and 132-avoiding permutations. A lot of different bijections have been shown to exist and the paper Classification of bijections between 321- and 132-avoiding permutations by Claesson, Kitaev shows that some of these are related by "trivial" bijections. Maybe this is a very special case of what Tom Leinster mentions in his answer, about one proof (bijection in this case) is deformed into another by a sequence of trivial steps (trival bijections in this case).

Answer 16

Consider a theorem of a form $\ A\Rightarrow T.\ $

Consider two proofs:

Proof 1: $$ A\Rightarrow C\qquad\mbox{and} \qquad C\Rightarrow T $$ Proof 2: $$ A\Rightarrow \Gamma\qquad\mbox{and}\qquad \Gamma\Rightarrow T $$

If also another theorem is true:

$$ \neg(C\Rightarrow\Gamma) $$

then -- objectively -- Proof 1 and Proof 2 are not equivalent. And if someone provided proof of the last-mentioned theorem then Proof 1 and Proof 2 would be explicitly not equivalent.

Thus every explicit equivalence is objective but the inverse depends on the status of the last-mentioned theorem.

Answer 17

If we have two proofs of the same theorem such that each proof has a different normal forms, can we modify the set of axioms so that there is only one normal form proof of the theorem, yet the universe of theorems remains unchanged from the original set of axioms?

More generally, can we select a set of axioms that minimizes the number of normal form proofs for each and every theorem in the original axiom set?

Taking this train of thought to the limit, for any axiom system, does there exist another axiom system with the same universe of theorems but which admits only one normal form proof of each theorem? Such a system of axioms could be called a "tight" set of axioms for a given universe of theorems.

Answer 18

There is clearly something subjective in judging how much two proofs are "essentially equivalent".

A possible definition, which unfortunately only covers a portion of cases, is the following: two proofs are non-equivalent if one generalizes better than the other. Example: this proof that reals are uncountable is not equivalent to the proof using the identification between positive reals and a suitable subset of $\mathcal{P}(\mathbb{N})$. Indeed, the latter opens the way to Cantor's theorem, whereas the first one seems just a clever trick to get the job done for $\mathbb{R}$.

Answer 19

Two proofs are different if one of them relies on CFSG and the other doesn't.

This is not an exhaustive list of criteria.

---

[Added from comment, 2024] What I'm saying here expands to use of any classification of all X: if one makes statements about all X then uses a property proved by considering all cases in the classification, this is a different proof from one using 'universal' properties.