Categorical Proof Theory of Classical Propositional Calculus

Remarks by the first author: This four-hand work, praised by a referee as a breakthrough in the problem of finding a categorical semantics for classical logic, takes off from work by the third author and others on proof-nets for classical logic. Giving a fresh look at Gentzen's sequent calculus, we argue against some identifications of proofs suggested by the proof-net model. One consequence of our analysis is that it is not reasonable to regard proofs as equivalent precisely when they give rise to the same set of normal forms.