The fibrational formulation of intuitionistic predicate logic. I: Completeness according to Gödel, Kripke, and Läuchli. Part 1
From MaRDI portal
Publication:1317983
DOI10.1305/ndjfl/1093634727zbMath0808.03049OpenAlexW4240266424MaRDI QIDQ1317983
Publication date: 21 April 1994
Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1305/ndjfl/1093634727
completenessintuitionistic predicate logicfibered categoriesfunctorial semanticscategory of sets- equipped-with-a-permutation
Categorical logic, topoi (03G30) Fibered categories (18D30) Preorders, orders, domains and lattices (viewed as categories) (18B35)
Related Items
Homotopies in Grothendieck fibrations, On the semantics of the universal quantifier, Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels, Abstract categorical logic, Fibrations with indeterminates: contextual and functional completeness for polymorphic lambda calculi, Deductive Completeness, Läuchli's completeness theorem from a topos-theoretic perspective, Structural induction and coinduction in a fibrational setting
