Läuchli's completeness theorem from a topos-theoretic perspective

DOI10.1007/S10485-008-9124-9MaRDI QIDQ969688zbMATH OpenOpenAlexFDO

Authors Matias Menni

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

zbMATH Keywords

intuitionistic logicintuitionistic predicate calculusLäuchli's completeness theoremtopos theory

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Categorical logic, topoi (03G30) Topoi (18B25)

Review text

The aim of this paper is to prove a variant of Läuchli's completeness theorem for intuitionistic predicate calculus.

Recommendations

• The fibrational formulation of intuitionistic predicate logic. I: Completeness according to Gödel, Kripke, and Läuchli. Part 2
• Linear Läuchli semantics
• An intuitionistic completeness theorem for classical predicate logic
• Lambek's categorical proof theory and Läuchli's abstract realizability
• Krivine's intuitionistic proof of classical completeness (for countable languages)

Cites work

• Cocomplete toposes whose exact completions are toposes
• scientific article; zbMATH DE number 2117177 (Why is no real title available?)
• scientific article; zbMATH DE number 937370 (Why is no real title available?)
• scientific article; zbMATH DE number 3222098 (Why is no real title available?)
• scientific article; zbMATH DE number 3370546 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• Lambek's categorical proof theory and Läuchli's abstract realizability
• Linear Läuchli semantics
• Sheaves in geometry and logic: a first introduction to topos theory
• Some free constructions in realizability and proof theory
• Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels
• The fibrational formulation of intuitionistic predicate logic. I: Completeness according to Gödel, Kripke, and Läuchli. Part 1

Cited in

(6)

• Lawvere completeness in topology
• Lascar rank and the finite cover property for complete theories of unars
• Topology and completion in semantics. Workshop, Chartres, France, November 18--20, 1993
• The Skolem-Löwenheim theorem in toposes
• Cohesive Toposes and Cantor's 'lauter Einsen'
• About Grothendieck fibrations

This page was built for publication: Läuchli's completeness theorem from a topos-theoretic perspective

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q969688)