Lambek's categorical proof theory and Läuchli's abstract realizability

DOI10.2307/2275186zbMath0765.03027OpenAlexW2029971057MaRDI QIDQ4008758

Victor Harnik, Michael Makkai

Publication date: 27 September 1992

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2275186

zbMATH Keywords

propositional logicabstract realizabilityintroduction to categorical proof theory

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items (9)

The shuffle Hopf algebra and noncommutative full completeness ⋮ Completeness results for intuitionistic and modal logic in a categorical setting ⋮ A categorical semantics for polarized MALL ⋮ Linear Läuchli semantics ⋮ Embedding of a free cartesian-closed category into the category of sets ⋮ Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels ⋮ The Deduction Theorem (Before and After Herbrand) ⋮ Generalized sketches as a framework for completeness theorems. I-III ⋮ Läuchli's completeness theorem from a topos-theoretic perspective

Cites Work

• Intuitionism. An introduction
• Two-dimensional monad theory
• Atomic toposes
• Deductive systems and categories
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Lambek's categorical proof theory and Läuchli's abstract realizability