Generalizing realizability and Heyting models for constructive set theory (Q651324)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Generalizing realizability and Heyting models for constructive set theory |
scientific article |
Statements
Generalizing realizability and Heyting models for constructive set theory (English)
0 references
12 December 2011
0 references
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.
0 references
constructive set theory
0 references
CZF
0 references
realizability
0 references
Heyting models
0 references
formal topology
0 references
applicative topology
0 references