Hacker News Reader

Comment by CurtMonash | Hacker News Reader

This discussion illustrates an interesting point -- it can be a little tricky to judge whether two proofs are actually "different" or not.

When I was a grad student I interrupted a study session to raise the simple question -- can a theorem really have two different proofs? We all thought the answer was yes, but the discussion went on for several minutes until I settled it by contriving a stupidly simple and synthetic set of axioms to construct a example.

Basically, the axioms were:

"All As are also Bs" "All As are also Cs" "All Bs are also Ds" "All Cs are also Ds"

and the theorem was

"All As are also Ds"

View on HN

From the point of view of category-theoretic logic – which is the area I did my PhD in – there is a sense in which all classical proofs are equivalent.

Roughly speaking, the argument goes like this. Intuitionistic propositional logic can be modelled by cartesian closed categories. (The canonical reference for this correspondence is the book “Introduction to Higher Order Categorical Logic” by Lambek and Scott.) But a lemma due to André Joyal shows that, if a cartesian closed category is a model of classical logic (i.e. validates the law of excluded middle), then there is at most one proof of any given implication: in the jargon, the category is a poset.

See http://mathoverflow.net/a/43285/8217 for a proof.

That was making my eyes cross, so I drew it out. In short, there are two distinct paths that you can apply a transitive rule over to get A -> D.

Very cool example!

It can get more complicated. When your logic can talk about equivalence of equivalences of proofs, then you can have two proofs that are equivalent in two ways that are not equivalent. Or, you could have two proofs that are equivalent in two ways whose equivalence can be proved, but maybe also in more than one way. You can iterate equivalences of equivalences in such a logic and equality becomes a significantly richer concept.

The study of such mathematical structures is the study of what is called an (infinity,1)-topos.

For readers who aren't already familiar with this, I'll note that this is in large part what Homotopy Type Theory is about making easy to work with. http://homotopytypetheory.org/book/ is a good introduction.

One could argue that the proof is just that all As are Xs where all Xs are Ds and therefore all As are Ds. This factors out the detail of choosing one path over the other. You have of course still to show that such an X exists and can use either pair of the axioms establishing this but as far as this proof is concerned both axiom pairs are really equivalent. So are this really two different proofs? How would one define equivalence between proofs to begin with? Isomorphic graphs of applied derivation rules?

Yes; putting essentially the same example another way, we might feel intuitively that there are two separate proofs of the propositional theorem that "B AND C" implies "B OR C".

Edit: Or, following up on danharaj's framing, we might feel intuitively that there are two separate proofs of "The set {B, C} is inhabited".

Good. Now do it with independent axioms / where no axioms follow from the rest.

I guess like how some sentences are provable with or without the axiom of choice.

> Good. Now do it with independent axioms / where no axioms follow from the rest.

They already did. Which of their four axioms do you think follows from the rest?

Sure.

Theorem: There exists an even natural number.

Proof 1:

  2. ∎

Proof 2:

  4. ∎

Reply on news.ycombinator.com