Categorical proof theory of classical propositional calculus

DOI10.1016/J.TCS.2006.08.002zbMATH Open1121.03086OpenAlexW2156159683MaRDI QIDQ860833FDOQ860833

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

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

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)

Cites Work

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

Cited In (16)

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

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)