A Reduction Theorem for the Kripke–Joyal Semantics: Forcing Over an Arbitrary Category can Always be Replaced by Forcing Over a Complete Heyting Algebra

摘要

It is assumed that a Kripke–Joyal semantics ({mathcal{A} = leftlangle mathbb{C},{rm Cov}, {it F},Vdash rightrangle}) 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}} = leftlangle overline{mathbb{C}},overline{rm{Cov}},overline{{it F}}, overline{Vdash} rightrangle }) 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.