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

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}$.