Heyting-valued interpretations for constructive set theory

Annals of Pure and Applied Logic 137 (1-3):164-188 (2006)
  Copy   BIBTEX

Abstract

We define and investigate Heyting-valued interpretations for Constructive Zermelo–Frankel set theory . These interpretations provide models for CZF that are analogous to Boolean-valued models for ZF and to Heyting-valued models for IZF. Heyting-valued interpretations are defined here using set-generated frames and formal topologies. As applications of Heyting-valued interpretations, we present a relative consistency result and an independence proof

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,261

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

On Kreisel's notion of validity in post systems.Dov M. Gabbay - 1976 - Studia Logica 35 (3):285 - 295.
Syntax and Semantics of the Logic.Carsten Butz - 1997 - Notre Dame Journal of Formal Logic 38 (3):374-384.
Henselian valued fields: a constructive point of view.Hervé Perdry - 2005 - Mathematical Logic Quarterly 51 (4):400-416.
Closed fragments of provability logics of constructive theories.Albert Visser - 2008 - Journal of Symbolic Logic 73 (3):1081-1096.
Predicate Logics of Constructive Arithmetical Theories.Albert Visser - 2006 - Journal of Symbolic Logic 71 (4):1311 - 1326.
Generalizing realizability and Heyting models for constructive set theory.Albert Ziegler - 2012 - Annals of Pure and Applied Logic 163 (2):175-184.
MV and Heyting Effect Algebras.D. J. Foulis - 2000 - Foundations of Physics 30 (10):1687-1706.

Analytics

Added to PP
2013-12-31

Downloads
36 (#446,058)

6 months
8 (#370,225)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Sublocales in Formal Topology.Steven Vickers - 2007 - Journal of Symbolic Logic 72 (2):463 - 482.

View all 17 citations / Add more citations

References found in this work

The strength of some Martin-Löf type theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
Inductively generated formal topologies.Thierry Coquand, Giovanni Sambin, Jan Smith & Silvio Valentini - 2003 - Annals of Pure and Applied Logic 124 (1-3):71-106.
Boolean-Valued Models and Independence Proofs in Set Theory.J. L. Bell & Dana Scott - 1981 - Journal of Symbolic Logic 46 (1):165-165.
Boolean-Valued Models and Independence Proofs in Set Theory.J. L. Bell & Dana Scott - 1986 - Journal of Symbolic Logic 51 (4):1076-1077.

View all 13 references / Add more references