Abstract

It is assumed that a Kripke–Joyal semantics \({\mathcal{A} = \left\langle \mathbb{C},{\rm Cov}, {\it F},\Vdash \right\rangle}\) has been defined for a first-order language \({\mathcal{L}}\) . To transform \({\mathbb{C}}\) into a Heyting algebra \({\overline{\mathbb{C}}}\) on which the forcing relation is preserved, a standard construction is used to obtain a complete Heyting algebra made up of cribles of \({\mathbb{C}}\) . A pretopology \({\overline{{\rm Cov}}}\) is defined on \({\overline{\mathbb{C}}}\) using the pretopology on \({\mathbb{C}}\) . A sheaf \({\overline{{\it F}}}\) is made up of sections of F that obey functoriality. A forcing relation \({\overline{\Vdash}}\) is defined and it is shown that \({\overline{\mathcal{A}} = \left\langle \overline{\mathbb{C}},\overline{\rm{Cov}},\overline{{\it F}}, \overline{\Vdash} \right\rangle }\) is a Kripke–Joyal semantics that faithfully preserves the notion of forcing of \({\mathcal{A}}\) . That is to say, an object a of \({\mathbb{C}Ob}\) forces a sentence with respect to \({\mathcal{A}}\) if and only if the maximal a-crible forces it with respect to \({\overline{\mathcal{A}}}\) . This reduces a Kripke–Joyal semantics defined over an arbitrary site to a Kripke–Joyal semantics defined over a site which is based on a complete Heyting algebra