Categorical proof theory of classical propositional calculus
type: Item
instance of: scholarly article
title: Categorical proof theory of classical propositional calculus
zbMATH Open document ID: 1121.03086
author: Gianluigi Bellin
author: Christian Urban
author: Martin Hyland
author: Edmund P. Robinson
published in: Theoretical Computer Science
publication date: 2007-01-09T00:00:00Z
review text: ``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 ident…
reviewed by: Michel Eytan
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 03F07
Mathematics Subject Classification ID: 03B05
Mathematics Subject Classification ID: 18B99
Mathematics Subject Classification ID: 18C15
zbMATH DE Number: 5083492
zbMATH Keywords: classical logic
zbMATH Keywords: semantics
zbMATH Keywords: classical proof
zbMATH Keywords: sequent calculus
zbMATH Keywords: polycategory
zbMATH Keywords: \(*\)-polycategory
zbMATH Keywords: \(*\)-autonomous category
zbMATH Keywords: guarded transformation/category/functor
zbMATH Keywords: coherence diagrams
zbMATH Keywords: normal form
MaRDI profile type: Publication
full work available at URL: j.tcs.2006.08.002
OpenAlex ID: W2156159683
cites work: Q4440826
cites work: Natural deduction and coherence for weakly distributive categories
cites work: Duplication of directed graphs and exponential blow up of proofs
cites work: Weakly distributive categories
cites work: Q4842975
cites work: Order-enriched categorical models of the classical sequent calculus
cites work: Linear logic
cites work: The duality of computation
cites work: Proof theory in the abstract
cites work: Computer Science Logic
cites work: Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads
cites work: Typed Lambda Calculi and Applications
cites work: Classical proofs as programs: How, what and why
cites work: Q4255509
cites work: Premonoidal categories as categories with algebraic structure
cites work: Proof Nets for Classical Logic
cites work: Non-commutative logic. I: The multiplicative fragment
cites work: Control categories and duality: On the categorical semantics of the lambda-mu calculus
cites work: Polycategories
cites work: Strong normalisation of cut-elimination in classical logic
cites work: Call-by-value is dual to call-by-name
DOI: 10.1016/J.TCS.2006.08.002
description: scientific article; zbMATH DE number 5083492