Generalizing realizability and Heyting models for constructive set theory (Q651324): Difference between revisions

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.