A reduction theorem for the Kripke-Joyal semantics: forcing over an arbitrary category can always be replaced by forcing over a complete Heyting algebra (Q382416)

From MaRDI portal
scientific article
Language Label Description Also known as
English
A reduction theorem for the Kripke-Joyal semantics: forcing over an arbitrary category can always be replaced by forcing over a complete Heyting algebra
scientific article

    Statements

    A reduction theorem for the Kripke-Joyal semantics: forcing over an arbitrary category can always be replaced by forcing over a complete Heyting algebra (English)
    0 references
    0 references
    0 references
    19 November 2013
    0 references
    The authors start with a Kripke-Joyal model \(\mathcal{A} = \langle \mathbb{C}, \mathrm{Cov}, F, \Vdash \rangle\). Taking the collection of cribles on \(\mathbb{C}\), they obtain a complete Heyting algebra \(\overline{\mathbb{C}}\). They define a pretopology \(\overline{\mathrm{Cov}}\) for \(\overline{\mathbb{C}}\), a sheaf \(\overline{F}\) and a forcing \(\overline{\Vdash}\). They obtain a Kripke-Joyal model \(\overline{\mathcal{A}} = \langle \overline{\mathbb{C}}, \overline{\mathrm{Cov}}, \overline{F}, \overline{\Vdash} \rangle\) that forces precisely the same well-formed formulae as \(\mathcal{A}\). Thus, forcing over an arbitrary category can always be replaced by a forcing over a complete Heyting algebra.
    0 references
    0 references
    forcing
    0 references
    Heyting algebra
    0 references
    Kripke-Joyal semantics
    0 references

    Identifiers