The category of theorems and proofs

On a philosophy website, it said that you could have a category with theorems as objects and proofs as arrows. This sounds awesome, but I couldn't find anything on the web that has both "category" and "proofs" in the title. Where it's some literature as a PDF of this category.

This paper, called Physics, Topology, Logic and Computation: A Rosetta Stone does just that in section 3.2. If you have time and interest, I would suggest reading the entire paper (since the whole thing is pretty cool).

The right way to build such a category is a philosophical question. There are different approaches in the mathematical literature. One thing is clear though: the objects should be propositions, not just theorems.

The problem is to define equality of proofs in a sensible way. For example, let $\Pi$ be Pythagoras' theorem. Should each of the over 100 proofs of $\Pi$ found here be a different morphism $\top\to\Pi$? In that case, it is hard to see how composition of proofs can be defined in such a way that there is a unique "identity proof" for each proposition.

One approach is to consider some proofs essentially equal if some superficial transformations turn one proof into the other. This, however, shifts the problem of defining the equality of proofs to the problem of defining the equality of transformations of proofs. So proofs and propositions are actually part of some $\infty$-category. If you like this line of reasoning, take a look at homotopy type theory and its implementation in various proof assistents.

Another approach is to simply consider every proof equal to any other proof of the same proposition, so that the category of propositions and proofs is a poset. For classical first order logic this poset is known as the Lindenbaum-Taski algebra.

The $\lambda$-calculus is a middle way between the infinity categories and the posets. Proofs can be encoded as $\lambda$-terms. A lot of irrelevant differences between proofs are lost in this encoding. There are equivalence relations on $\lambda$-term based on transformations like $\beta$-reduction. The counterpart of $\lambda$-calculi are Cartesian closed categories.

See for example Lambek and Scott: Introduction to higher order categorical logic, ch 0.1 (unfortunately not in the net but for sure in ur university library). There first is defined a graph, then a deductive system as a graph with

• For each object $A$ an identity arrow $1_A:A\rightarrow A$
• For each pair of arrows $f:A\rightarrow B$ and $g:B\rightarrow C$ the composition $gf:A\rightarrow C$

The idea of a logician might be that of objects as formulas and arrows as deductions, the composition in this context becoming a rule of inference $$\frac{f:A\rightarrow B\space\space\space g:B\rightarrow C}{gf:A\rightarrow C}$$

However this is just an interpretation and letting this aside one can take that abstract definition of a deductive system to come out with the usual category:

A category is a deductive system with the ususal equations for identity and associativity - i.e. for $f:A\rightarrow B$, $g:B\rightarrow C$ and $h:C\rightarrow D$ $$f1_a=f=1_Bf,\space\space (hg)f=h(gf)$$