Conceptual completeness for first-order intuitionistic logic: An application of categorical logic

DOI10.1016/0168-0072(89)90007-9zbMath0665.03048OpenAlexW2068932960MaRDI QIDQ1115868

Andrew M. Pitts

Publication date: 1989

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(89)90007-9

zbMATH Keywords

categoriesfunctorsinterpretationclassifying Heyting pretoposfirst order theories in intuitionistic logic and their modelsgeometric morphisms of Grothendieck toposeslogostopos of filters

Mathematics Subject Classification ID

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

Related Items

2000 Annual Meeting of the Association for Symbolic Logic, Saturated models of intuitionistic theories, Model completions and r-Heyting categories, Strong conceptual completeness for first-order logic, Unnamed Item, Partial hyperdoctrines: categorical models for partial function logic and Hoare logic, Ultrasheaves and double negation, Generalising canonical extension to the categorical setting, Unnamed Item

Cites Work

• Amalgamation and interpolation in the category of Heyting algebras
• An application of open maps to categorical logic
• Open maps of toposes
• Completeness results for intuitionistic and modal logic in a categorical setting
• Seminar of algebraic geometry du Bois-Marie 1963--1964. Topos theory and étale cohomology of schemes (SGA 4). Vol. 1: Topos theory. Exp. I--IV
• An extension of the Galois theory of Grothendieck
• La logique des topos
• Fibered categories and the foundations of naive category theory
• Introduction to bicategories
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item