Not all Kripke models of $\sf HA$ are locally $\sf PA$

TL;DR

This paper demonstrates that not all Kripke models of Heyting Arithmetic are locally models of Peano Arithmetic, introducing new constructions to characterize arithmetical structures at the roots of such models.

Contribution

It introduces two novel Kripke model constructions that characterize arithmetical structures at roots, showing some models are not locally PA.

Findings

Existence of rooted Kripke models with non-PA structures at the root.

Characterization of arithmetical structures that can be roots of models satisfying HA+ECT_0.

Conditions for the existence of models with given arithmetical structures at the root.

Abstract

Let ${\bf K}$ be an arbitrary Kripke model of Heyting Arithmetic, ${\sf HA}$. For every node $k$ in ${\bf K}$, we can view the classical structure of $k$, ${\mathfrak M}_k$ as a model of some classical theory of arithmetic. Let ${\sf T}$ be a classical theory in the language of arithmetic. We say ${\bf K}$ is locally ${\sf T}$, iff for every $k$ in ${\bf K}$, ${\mathfrak M}_k\models{\sf T}$. One of the most important problems in the model theory of ${\sf HA}$ is the following question: {\it Is every Kripke model of ${\sf HA}$ locally ${\sf PA}$?} We answer this question negatively. We introduce two new Kripke model constructions to this end. The first construction actually characterizes the arithmetical structures that can be the root of a Kripke model ${\bf K}\Vdash{\sf HA}+{\sf ECT_0}$ (${\sf ECT_0}$ stands for Extended Church Thesis). The characterization says that for every arithmetical structure ${\mathfrak M}$, there exists a rooted Kripke model ${\bf K}\Vdash{\sf HA}+{\sf ECT_0}$ with the root $r$ such that ${\mathfrak M}_r={\mathfrak M}$ iff ${\mathfrak M}\models{\bf Th}_{\Pi_2}({\sf PA})$. One of the consequences of this characterization is that there is a rooted Kripke model ${\bf K}\Vdash{\sf HA}+{\sf ECT_0}$ with the root $r$ such that ${\mathfrak M}_r\not\models{\bf I}\Delta_1$ and hence ${\bf K}$ is not even locally ${\bf I}\Delta_1$. The second Kripke model construction is an implicit way of doing the first construction which works for any reasonable consistent intuitionistic arithmetical theory ${\sf T}$ with a recursively enumerable set of axioms that has the existence property. We get a sufficient condition from this construction that describes when for an arithmetical structure ${\mathfrak M}$, there exists a rooted Kripke model ${\bf K}\Vdash {\sf T}$ with the root $r$ such that ${\mathfrak M}_r={\mathfrak M}$.