Generalizing realizability and Heyting models for constructive set theory
type: Item
instance of: scholarly article
title: Generalizing realizability and Heyting models for constructive set theory
zbMATH Open document ID: 1267.03055
author: Albert Ziegler
published in: Annals of Pure and Applied Logic
publication date: 2011-12-12T00:00:00Z
review text: Is there a common generalization of Heyting models and realizability models for the case of predicative constructive set theory CZF? As is well known, CZF includes the axioms of empty set, extensionality, pairing union, strong infinity, bounded separation, strong collection, subset collection. The main result of this interesting paper is to offer a positive solution to the problem, by introducing in Section 2 the notion of applicative topology. Roughly, an applicative topology consists of a pair of structures, that is: (i) a formal topology \(S\) which is a poset with a covering relation; (ii) a subset \(\nabla\) of \(S\) which essentially forms a partial combinatory algebra, where the equality relation is approximated by the covering relation. The core of the paper is Section 3: there a realizability universe \(V(S)\) is inductively generated -- provably in CZF -- which crucially depends on the applicative topology \(S\); if \(e \in S\), this allows one to define the relation \(e \Vdash\varphi\), which makes use of the covering relation \(\triangleleft\). Subsequently, the author shows that the realized formulas are closed under intuitionistic logical deducibility (Theorem 2), while the main theorem asserts that all CZF-axioms are realized. The proof requires the verification of suitable lemmata (3 through 6), the most difficult steps being those dealing with strong collection and subset collection. In addition to more efficient proofs of results that are accessible via Rathjen's realizability method, the author states in the conclusive section that his own method yields additional interesting results, e.g., that realizability with applicative topologies allows one to check the absoluteness of the so-called regular extension axiom REA.
reviewed by: Andrea Cantini
Mathematics Subject Classification ID: 03F25
Mathematics Subject Classification ID: 03E35
Mathematics Subject Classification ID: 03E70
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03F65
zbMATH DE Number: 5987971
zbMATH Keywords: constructive set theory
zbMATH Keywords: CZF
zbMATH Keywords: realizability
zbMATH Keywords: Heyting models
zbMATH Keywords: formal topology
zbMATH Keywords: applicative topology
MaRDI profile type: Publication
full work available at URL: j.apal.2011.06.025
OpenAlex ID: W2032794985
cites work: Q3762311
cites work: Q3214890
cites work: Heyting-valued interpretations for constructive set theory
cites work: Q3852176
cites work: Relativized realizability in intuitionistic arithmetic of all finite types
cites work: Ordered partial combinatory algebras
cites work: Q4010362
cites work: Q3222842
cites work: Q3481701
cites work: Q5477363
cites work: Q5718561
cites work: Constructivism in mathematics. An introduction. Volume I
DOI: 10.1016/J.APAL.2011.06.025
Recommended article: Q5477363
Recommended article: The semantics of realizability for the constructive set theory based on hyperarithmetical predicates
Recommended article: Extensional realizability for intuitionistic set theory
Recommended article: Heyting-valued interpretations for constructive set theory
Recommended article: Realisability for infinitary intuitionistic set theory
Recommended article: Realizability and Existence Property of a Constructive Set Theory with Types
Recommended article: Q5718562
Recommended article: The generalised type-theoretic interpretation of constructive set theory
Recommended article: Realizability and recursive set theory
Recommended article: Models of intuitionistic set theory in subtoposes of nested realizability toposes
description: scientific article; zbMATH DE number 5987971