I read Aristotelian demonstration as more a making explicit than a proof of truths. The logical expressivism of the author of Making It Explicit (Robert Brandom) does something similar with modern logic. Nonetheless it would be very wrong to conclude that proof theory has no philosophical relevance.

To begin with, proof theory is itself not concerned with proving this or that truth. It is the study of proofs, the beginning of which is to recognize that proofs and proof calculi are themselves mathematical objects. Proofs are functions from premises to conclusions. This has profound consequences.

At an utterly simple level, one small piece of a far larger result is that the notion of an implication A => B is at a certain level formally interchangeable with the notion of a mathematical function A => B. Frege very explicitly treats logical predication as a function as well.

Category theory builds all of mathematics on such morphisms, starting from a single basic operation of composition of arrows. Homotopy type theory suggests that we think of the arrows as paths through spaces. All this is an elaboration and abstraction of the utterly simple but crucial notion of “follows from”, or what Brandom calls subjunctive robustness.

Then an Aristotelian syllogism can be seen on the model of the composition of two predications or functions or morphisms or arrows or paths A => B and B => C around a common type or middle term B that is the output of one and the input of the other. This is not intended to capture a sophisticated result like a mathematical theorem, but rather to express sound reasoning in the simplest, most perspicuous, and most universal way possible.

Next in this series: Reason Relations