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.
Type de document :
Communication dans un congrès
Topology, Algebra and Categories in Logic (TACL) 2011, Jul 2011, Marseille, France. 2011
Liste complète des métadonnées

https://hal.inria.fr/inria-00618862
Contributeur : Ivano Alessandro Ciardelli <>
Soumis le : samedi 3 septembre 2011 - 17:35:47
Dernière modification le : jeudi 11 janvier 2018 - 06:20:16
Document(s) archivé(s) le : jeudi 30 mars 2017 - 14:30:38

Fichier

A_canonical_model_for_presheaf...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00618862, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

183

Téléchargements de fichiers

156