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
    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

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references