Categorical proof theory of classical propositional calculus (Q860833)

``The questions \textit{`What is a proof?'} and \textit{`When are two proofs the same?'} are fundamental for proof theory. But for the most prominent logic, Boolean (or classical) propositional logic, we still have no satisfactory answers.'' [\textit{L. Strassburger}, Theory Appl. Categ. 18, 536--601, electronic only (2007; Zbl 1122.03066)] Section 1: Introduction. The authors propose to describe semantics for a classical proof along Gentzen's sequent calculus. They look for analogues of the correspondence beween deductions in minimal logic and terms of a typed lambda calculus. There arise, however, some problems: term languages for classical proofs are either incompatible with the symmetries in the sequent calculus or accepting that symmetry makes evaluations deterministic. This leads to reducing classical proofs to constructive proofs via the double-negation translation. The term calculi are associated directly with the sequent calculus [\textit{C. Urban}, Classical logic and computation. Ph.D. Dissertation, University of Cambridge (2000)], but formulating criteria for identity of terms is not clear. Section 2 of the paper, Modelling classical proofs, recalls the definition of Szabo's polycategories and defines \(*\)-polycategories (duality between propositions and proofs). Rules of inference are then given and naturality is discussed as well as logical rules and structural rules. Section 3, Categorical formulation, defines guarded categories (resp. functors, transformations) and proves that all these data define a 2-category. The authors then extend the connectors of classical logic on objects to maps that are not functorial but guarded functorial. Furthermore, units and associations are equipped with the analogue of structures familiar for tensor products. They satisfy the Mac Lane pentagon and unit conditions; this also holds for the Mac Lane hexagon and unit conditions. One can define a symmetry on the \(*\)-polycategory that satisfies the standard braid identities. One then goes on to prove that linear distributivities are guarded transformations and that the coherence diagrams for weak distributivities hold. All this leads to the definition of a categorical model for classical proofs. Section 4, Explanation and comparison, examines the groupoid enriched functors \(\text{SPoly} : \mathbf{*Aut} \to \text\textbf{*Poly}\) and \(\text{SAut} : \mathbf{*Poly} \to \text\textbf{*Aut}\), where \textbf{*Poly} is the obvious 2-category of \(*\)-polycategories and \textbf{*Aut} that of \(*\)-autonomous categories. This gives rise to a groupoid enriched adjunction \(\text{SAut} \dashv \text{SPoly}\). For this we have Theorem 4.1., which says that the unit \(\mathcal P \to \text{SPoly}\,\text{SAut}\) is full and faithful for any \(*\)-polycategory \(\mathcal P\). A model \(\mathcal C\) for classical proof theory can be proved to satisfy equivalent conditions between identity conditions, full functoriality of \(\wedge\) and \(\top\), representability of polymaps by \(\wedge\), \(\top\) and \(\vee\), \(\bot\) (Theorem 4.2.). In sum, Theorem 4.4., if \(\mathcal C\) is a model for classical proof theory freely generated by a category, then the quotient \(\widehat{\mathcal{C}}\) is a model in the Führmann-Pym sense. Section 5, Provisional conclusions, discusses guiding principles and further issues.