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

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 3

Maybe this blog entry by Gowers will be of interest.

Answer 4

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 two articles by Lambek, this 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.

Answer 5

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 6

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 7

Maybe this might be of interest: Andreas Blass, Nachum Dershowitz, Yuri Gurevich: WHEN ARE TWO ALGORITHMS THE SAME?

Answer 8

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 9

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 10

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.