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)

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.