English

Localizing Finite-Depth Kripke Models

Logic 2017-10-25 v1

Abstract

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. αAρMαA \alpha\Vdash A^\rho \Leftrightarrow \mathfrak{M}_\alpha\models A. We introduce some applications of this fact. We extend the result of [Ardeshir and Hessam 2002] and show that semi-narrow Kripke models of Heyting Arithmetic HA {\sf HA} are locally PA {\sf PA} .

Keywords

Cite

@article{arxiv.1710.08730,
  title  = {Localizing Finite-Depth Kripke Models},
  author = {Mojtaba Mojtahedi},
  journal= {arXiv preprint arXiv:1710.08730},
  year   = {2017}
}
R2 v1 2026-06-22T22:23:57.494Z