Categorical proof theory of classical propositional calculus
``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.
- Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads
- Call-by-value is dual to call-by-name
- Classical proofs as programs: how, what and why
- Computer Science Logic
- Control categories and duality: On the categorical semantics of the lambda-mu calculus
- Duplication of directed graphs and exponential blow up of proofs
- scientific article; zbMATH DE number 1324438 (Why is no real title available?)
- scientific article; zbMATH DE number 2020177 (Why is no real title available?)
- scientific article; zbMATH DE number 786494 (Why is no real title available?)
- Linear logic
- Natural deduction and coherence for weakly distributive categories
- Non-commutative logic. I: The multiplicative fragment
- Order-enriched categorical models of the classical sequent calculus
- Polycategories
- Premonoidal categories as categories with algebraic structure
- Proof Nets for Classical Logic
- Proof theory in the abstract
- Strong normalisation of cut-elimination in classical logic
- The duality of computation
- Typed Lambda Calculi and Applications
- Weakly distributive categories
- The classification of propositional calculi
- Bifibrations of polycategories and classical linear logic
- The three dimensions of proofs
- Generality of proofs and its Brauerian representation
- A mathematical theory of resources
- Proof-theoretical coherence
- A categorical approach to the semantics of argumentation
- Towards Hilbert's 24th Problem: Combinatorial Proof Invariants
- The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
- Assertions, Hypotheses, Conjectures, Expectations: Rough-Sets Semantics and Proof Theory
- Computer Science Logic
- On categorical models of classical logic and the Geometry of Interaction
- Typed Lambda Calculi and Applications
- Proof theory in the abstract
- scientific article; zbMATH DE number 7715469 (Why is no real title available?)
- Classical proof forestry
- The frame problem and the semantics of classical proofs
- Categorical proof-theoretic semantics
- Algebra of proofs
- A categorical semantics for polarized MALL
This page was built for publication: Categorical proof theory of classical propositional calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q860833)
