Categorical proof theory of classical propositional calculus

DOI10.1016/J.TCS.2006.08.002MaRDI QIDQ860833zbMATH OpenOpenAlexFDO

Authors Gianluigi Bellin, Christian Urban, Martin Hyland, Edmund P. Robinson

Publication date 9 January 2007

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2006.08.002

zbMATH Keywords

normal formsemanticssequent calculusclassical logicpolycategory\(*\)-autonomous category\(*\)-polycategoryclassical proofcoherence diagramsguarded transformation/category/functor

Mathematics Subject Classification ID

Classical propositional logic (03B05) Structure of proofs (03F07) Categorical logic, topoi (03G30) Special categories (18B99) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15)

Recommendations

• Proof theory in the abstract
• Computer Science Logic
• Typed Lambda Calculi and Applications
• Proof-theoretical coherence
• Lambek's categorical proof theory and Läuchli's abstract realizability

Cites work

• 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?)
• 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
• 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

Cited in

(16)

• The classification of propositional calculi
• The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
• Proof theory in the abstract
• Computer Science Logic
• Towards Hilbert's 24th Problem: Combinatorial Proof Invariants
• The three dimensions of proofs
• Assertions, Hypotheses, Conjectures, Expectations: Rough-Sets Semantics and Proof Theory
• Proof-theoretical coherence
• Algebra of proofs
• A mathematical theory of resources
• Typed Lambda Calculi and Applications
• Generality of proofs and its Brauerian representation
• On categorical models of classical logic and the Geometry of Interaction
• scientific article; zbMATH DE number 7715469 (Why is no real title available?)
• A categorical semantics for polarized MALL
• Classical proof forestry

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)