Heyting-valued interpretations for constructive set theory

DOI10.1016/j.apal.2005.05.021zbMath1077.03038OpenAlexW2002542640WikidataQ59904134 ScholiaQ59904134MaRDI QIDQ2575769

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

independenceframeHeyting algebraconstructive set theoryformal topologypointfree topologyrelative consistencyHeyting-valued models

Mathematics Subject Classification ID

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

Related Items (16)

Sublocales in formal topology ⋮ ABSTRACT INDUCTIVE AND CO-INDUCTIVE DEFINITIONS ⋮ On Tarski’s fixed point theorem ⋮ Derived rules for predicative set theory: an application of sheaves ⋮ Topological inductive definitions ⋮ Generalizing realizability and Heyting models for constructive set theory ⋮ A cumulative hierarchy of sets for constructive set theory ⋮ The associated sheaf functor theorem in algebraic set theory ⋮ Aspects of predicative algebraic set theory. I: Exact completion ⋮ On some peculiar aspects of the constructive theory of point-free spaces ⋮ Kripke models for subtheories of \textsf{CZF} ⋮ SEPARATING THE FAN THEOREM AND ITS WEAKENINGS II ⋮ The generalised type-theoretic interpretation of constructive set theory ⋮ Lawvere–Tierney sheaves in Algebraic Set Theory ⋮ Regular universes and formal spaces ⋮ LIFSCHITZ REALIZABILITY AS A TOPOLOGICAL CONSTRUCTION

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Harvey Friedman's research on the foundations of mathematics
• Sheaves in geometry and logic: a first introduction to topos theory
• Applications of sheaves. Proceedings of the research symposium on applications of sheaf theory to logic, algebra and analysis, Durham, July 9--21, 1977
• Inaccessibility in constructive set theory and type theory
• The strength of some Martin-Löf type theories
• Inductively generated formal topologies.
• Some points in formal topology.
• Wellfounded trees in categories
• Intuitionistic choice and classical logic
• Pretopologies and a uniform presentation of sup-lattices, quantales and frames
• An extension of the Galois theory of Grothendieck
• La logique des topos
• Forcing in intuitionistic systems without power-set
• The point of pointless topology
• Type theories, toposes and constructive set theory: Predicative aspects of AST

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