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

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 http://mathoverflow.net/a/43285/8217 for a proof.