Skip to Main content Skip to Navigation
Conference papers

A Canonical Model for Presheaf Semantics

Abstract : Presheaf models [Osius, 1975, Fourman and Scott, 1979, Moerdijk and Mac Lane, 1992] are a simple generalization of Kripke models and provide one of the most natural semantics for intuitionistic predicate logic. Although a completeness result for this semantics is known, this is usually obtained either non-constructively, by defi ning a canonical Kripke model,or indirectly, e.g. via categorical equivalences with omega-models as in [Troelstra and Van Dalen, 1988]. This paper describes an elementary canonicalmodel construction by means of which completeness is established in a perspicuous, direct and constructive way.
Document type :
Conference papers
Complete list of metadata
Contributor : Ivano Alessandro Ciardelli Connect in order to contact the contributor
Submitted on : Saturday, September 3, 2011 - 5:35:47 PM
Last modification on : Saturday, June 25, 2022 - 10:32:38 AM
Long-term archiving on: : Thursday, March 30, 2017 - 2:30:38 PM


Files produced by the author(s)


  • HAL Id : inria-00618862, version 1



Ivano Alessandro Ciardelli. A Canonical Model for Presheaf Semantics. Topology, Algebra and Categories in Logic (TACL) 2011, Jul 2011, Marseille, France. ⟨inria-00618862⟩



Record views


Files downloads