Läuchli's completeness theorem from a topos-theoretic perspective
From MaRDI portal
Publication:969688
DOI10.1007/s10485-008-9124-9zbMath1211.03103MaRDI QIDQ969688
Publication date: 7 May 2010
Published in: Applied Categorical Structures (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10485-008-9124-9
intuitionistic logic; topos theory; intuitionistic predicate calculus; Läuchli's completeness theorem
03G30: Categorical logic, topoi
18B25: Topoi
03B20: Subsystems of classical logic (including intuitionistic logic)
Cites Work
- Cocomplete toposes whose exact completions are toposes
- Sheaves in geometry and logic: a first introduction to topos theory
- The fibrational formulation of intuitionistic predicate logic. I: Completeness according to Gödel, Kripke, and Läuchli. Part 1
- Some free constructions in realizability and proof theory
- Linear Läuchli semantics
- Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels
- Lambek's categorical proof theory and Läuchli's abstract realizability
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item