43
$\begingroup$

Often, we find different proofs for certain theorems that, on the surface, seem to be very different but actually use the same fundamental ideas. For example, the topological proof of the infinitude of primes is quite different than the standard one, but the arguments are essentially the same, just using different vocabulary.

So, my question is the following:

Is there a rigorous notion of "proof isomorphism"?

$\endgroup$
4
  • 5
    $\begingroup$ You might want to look at "Homotopy Type Theory" (one of the authors is Dan Licata); in it, the authors describe an approach where proofs are indeed "types" in a type-theory, and a notion of "homotopy of proofs", which corresponds to a notion of "proof isomorphism". (I don't find it all that compelling, but it's a start...) $\endgroup$ Apr 19, 2015 at 16:22
  • 1
    $\begingroup$ All first order proofs have an equivalent simple tree where you satisfy existentially quantified variables in every possible way until every branch contradicts out. This suggests that there is little technical difference between any two proofs in the same first order theory. On the other hand, you could minimize the axioms for proofs of interest, and showing that two proofs rely on incomparable subsets of the contextual theory would, in a way, show two proofs to be fundamentally different. $\endgroup$
    – jack
    Apr 21, 2015 at 11:19
  • $\begingroup$ This blog posts contains wonderful discussion about this matter. $\endgroup$
    – Bumblebee
    Jul 17, 2015 at 8:31
  • $\begingroup$ I have stumbled upon a preprint Mathematical semantics of intuitionistic logic by Sergey Melikhov where this notion is mentioned as a motivation. I am reading it now. $\endgroup$
    – Alexey
    Jul 30, 2015 at 17:31

2 Answers 2

11
$\begingroup$

The question of proof equivalence is quite an old one! In fact, David Hilbert considered adding it (or a similar one) to his celebrated list of open problems, but finally decided to leave it out, so it is sometimes referred to as Hilbert's 24th problem.

There is a rather well-established field investigating proof equivalence, though definitely no clear answer to either your or Hilbert's question (and it is likely that this is quite out of reach). However, here are some various notions of proof equivalence of increasing strength.

  1. Equality w.r.t. variable re-naming (also called $\alpha$-renaming). This is much too fine: clearly there are proofs that are "morally" the same, but that differ by more than variable re-namings.

  2. Equality w.r.t. definition unfolding. This doesn't solve all of the above problems, but it's clear that if one proof involves a compact definition and the other does not, they should be seen to be the same.

  3. Equality w.r.t. cut elimination. This one is much more interesting! For two proofs $\Delta$, $\Phi$, we say that $\Delta\simeq_{\mathrm{cut}}\Phi$ if the two proofs are the same (modulo variable re-naming) after having eliminated all cuts. Now a lot of rather different proofs become quite similar, e.g. proofs in calculus involving abstract "open/closed" terminology can be reduced to simple proofs involving $\epsilon$-$\delta$ notation. This still isn't satisfactory since e.g., some hypotheses can be used in different orders, or some useless steps still remain. It's also not clear that this is not too coarse, since sometimes the use of crucial lemmas makes a proof much simpler, and cut-elimination makes all intermediate lemmas "disappear".

  4. Equality w.r.t. cut elimination with commutative cuts. See, for example these really nice slides by Clement Houtmann. This might get closer to the "right" notion, though as you can see things start to get a bit subjective at this point. What does it mean to "use the same idea"?

As Bruno mentioned, there is a deep connection between proofs of propositions and certain programs in particular programing languages, so one may re-formulate the question as

When are two programs the same?

with very fruitful results. The conclusion should be that this is a very active area of research in proof theory, with connections to computer science and categorical logic.


Addendum

Looking back at this answer a couple of years later, I feel like I should add a couple of more recent research directions around this idea of proof equivalence.

  1. Focusing is a proof system that refines the classical sequent presentation of derivations, trying to make irrelevant choices disappear by distinguishing between the "invertible" rules, which can be applied at any time without worry and the "positive" rules in which choices do matter. A pretty neat paper explaining the philosophy of this approach is Zeilberger, On the unity of duality

  2. Simlarly, proof nets try to represent families of proofs in ways that quotient out irrelevant proof search distinctions. I know less about this, but it is certainly related to focusing.

$\endgroup$
2
$\begingroup$

This proof irrelevance is one of the problems of classic foundations.

In Type Theory, however, we represent mathematical statements as types, which enables us to treat proofs as mathematical objects. This is because of a well-known isomorphism between types and propositions a.k.a. Curry-Howard Correspondence, which roughly says that to find a proof of a statement A is to find a inhabitant of this type: $$a:A$$ Which, in the point of view of logic, can be read 'a is a proof of the proposition A'.

In this sense, to prove a proposition is to construct an inhabitant of a type, which means that every mathematical proof can be seen as an algorithm. This is related with "constructive" (intuitionistic) conception of logic where (i) to prove a statement of the form "A and B" is to find a proof of A and a proof of B, (i) to prove that A implies B is to find a function that converts a proof of A into a proof of B (iii) every prove that something exists carries with it enough information to exhibit such object and so on. Hence equality of elements of a type (proofs) is treated intensionally.

Now Homotopy Type Theory thinks of types as "homotopical spaces", interpreting, as stated in the comments, the relation of identity $a=b$ between elements (proofs) of the same type (proposition) $a,b: A$ as homotopical equivalence, understood as a path from the point $a$ to the point $b$ in the space $A$. The HoTT book is available for free in the project website.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .