Categorical proof theory of classical propositional calculus

AbstractWe investigate semantics for classical proof based on the sequent calculus. We show that the propositional connectives are not quite well-behaved from a traditional categorical perspective, and give a more refined, but necessarily complex, analysis of how connectives may be characterised abstractly. Finally we explain the consequences of insisting on more familiar categorical behaviour