Localizing finite-depth Kripke models
Mojtaba Mojtahedi · Logic Journal of IGPL · 2018
We can look at a first-order (or propositional) intuitionistic Kripke model as an ordered set of classical models. In this paper, we show that for a finite-depth Kripke model in an arbitrary first-order language or propositional language, local (classical) truth of a formula is equivalent to non-classical truth (truth in the Kripke semantics) of a Friedman’s translation of that formula, i.e. |$ \alpha \Vdash A^\rho \Leftrightarrow \mathfrak{M}_\alpha \models A$|. We introduce some applications of this fact. We extend the result of Ardeshir and Hesaam (2002, Math. Logic Quart., 48, 391–395) and show that semi-narrow Kripke models of Heyting Arithmetic |$ \textsf{HA} $| are locally |$ \textsf{PA} $|.