Localizing Finite-Depth Kripke Models

TL;DR

This paper demonstrates that in finite-depth Kripke models, classical truth aligns with non-classical Kripke truth via Friedman's translation, with applications to Heyting Arithmetic models.

Contribution

It establishes an equivalence between classical and Kripke semantics for finite-depth models using Friedman's translation, extending previous results.

Findings

Classical truth in finite-depth models equals Kripke truth of Friedman's translation.

Semi-narrow Kripke models of HA are locally PA.

Provides applications for model localization techniques.

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. $ \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 $ {\sf HA} $ are locally $ {\sf PA} $.