Categorical proof theory of classical propositional calculus

DOI10.1016/j.tcs.2006.08.002zbMath1121.03086OpenAlexW2156159683MaRDI QIDQ860833

Gianluigi Bellin, Christian Urban, J. M. E. 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 formsequent calculussemanticsclassical logicpolycategory\(*\)-autonomous category\(*\)-polycategoryclassical proofcoherence diagramsguarded transformation/category/functor

Mathematics Subject Classification ID

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

Related Items

A mathematical theory of resources, Classical proof forestry, 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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Weakly distributive categories
• Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads
• Duplication of directed graphs and exponential blow up of proofs
• Natural deduction and coherence for weakly distributive categories
• Premonoidal categories as categories with algebraic structure
• Non-commutative logic. I: The multiplicative fragment
• Order-enriched categorical models of the classical sequent calculus
• Control categories and duality: on the categorical semantics of the lambda-mu calculus
• The duality of computation
• Polycategories
• Proof Nets for Classical Logic
• Classical proofs as programs: How, what and why
• Call-by-value is dual to call-by-name
• Computer Science Logic
• Typed Lambda Calculi and Applications
• Proof theory in the abstract