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
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
forcing
0 references
Heyting algebra
0 references
Kripke-Joyal semantics
0 references