Heyting-valued interpretations for constructive set theory

DOI10.1016/J.APAL.2005.05.021MaRDI QIDQ2575769zbMATH OpenOpenAlexWikidataFDO

Authors Nicola Gambino

Publication date 6 December 2005

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

Full work available at URL https://doi.org/10.1016/j.apal.2005.05.021

zbMATH Keywords

constructive set theoryformal topologyframeHeyting algebraHeyting-valued modelsindependencepointfree topologyrelative consistency

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Other constructive mathematics (03F65)

Recommendations

• Generalizing realizability and Heyting models for constructive set theory
• Concepts and aims of functional interpretations: Towards a functional interpretation of constructive set theory
• The formulae-as-classes interpretation of constructive set theory

Cites work

• An extension of the Galois theory of Grothendieck
• Applications of sheaves. Proceedings of the research symposium on applications of sheaf theory to logic, algebra and analysis, Durham, July 9--21, 1977
• Forcing in intuitionistic systems without power-set
• Harvey Friedman's research on the foundations of mathematics
• scientific article; zbMATH DE number 5919711 (Why is no real title available?)
• scientific article; zbMATH DE number 4012604 (Why is no real title available?)
• scientific article; zbMATH DE number 3664922 (Why is no real title available?)
• scientific article; zbMATH DE number 3724439 (Why is no real title available?)
• scientific article; zbMATH DE number 3754682 (Why is no real title available?)
• scientific article; zbMATH DE number 3775591 (Why is no real title available?)
• scientific article; zbMATH DE number 3787631 (Why is no real title available?)
• scientific article; zbMATH DE number 192927 (Why is no real title available?)
• scientific article; zbMATH DE number 3577208 (Why is no real title available?)
• scientific article; zbMATH DE number 2085163 (Why is no real title available?)
• scientific article; zbMATH DE number 1420782 (Why is no real title available?)
• scientific article; zbMATH DE number 3346319 (Why is no real title available?)
• scientific article; zbMATH DE number 2247251 (Why is no real title available?)
• Inaccessibility in constructive set theory and type theory
• Inductively generated formal topologies.
• Intuitionistic choice and classical logic
• La logique des topos
• Pretopologies and a uniform presentation of sup-lattices, quantales and frames
• Sheaves in geometry and logic: a first introduction to topos theory
• Some points in formal topology.
• The point of pointless topology
• The strength of some Martin-Löf type theories
• Type theories, toposes and constructive set theory: Predicative aspects of AST
• Wellfounded trees in categories

Cited in

(23)

• Heyting valued considerations on some fundamental existence theorems in modern analysis
• ZF between classicality and non-classicality
• Kripke models for subtheories of \textsf{CZF}
• Regular universes and formal spaces
• A parametrised functional interpretation of Heyting arithmetic
• On Tarski’s fixed point theorem
• Lawvere–Tierney sheaves in Algebraic Set Theory
• On some peculiar aspects of the constructive theory of point-free spaces
• scientific article; zbMATH DE number 3916267 (Why is no real title available?)
• Derived rules for predicative set theory: an application of sheaves
• Topological inductive definitions
• ABSTRACT INDUCTIVE AND CO-INDUCTIVE DEFINITIONS
• Induced morphisms between Heyting-valued models
• Homotopy type-theoretic interpretations of constructive set theories
• Separating the fan theorem and its weakenings. II
• Sublocales in formal topology
• A cumulative hierarchy of sets for constructive set theory
• The generalised type-theoretic interpretation of constructive set theory
• Lifschitz realizability as a topological construction
• Generalizing realizability and Heyting models for constructive set theory
• Very large set axioms over constructive set theories
• The associated sheaf functor theorem in algebraic set theory
• Aspects of predicative algebraic set theory. I: Exact completion

This page was built for publication: Heyting-valued interpretations for constructive set theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2575769)