Not all Kripke models of $\mathsf{HA}$ are locally $\mathsf{PA}$

Abstract

Let $\mathbf{K}$ be an arbitrary Kripke model of Heyting Arithmetic, $\mathsf{HA}$. For every node $k$ in $\mathbf{K}$, we can view the classical structure of $k$, ${\mathfrak{M}}_k$ as a model of some classical theory of arithmetic. Let $\mathsf{T}$ be a classical theory in the language of arithmetic. We say $\mathbf{K}$ is locally $\mathsf{T}$, iff for every $k$ in $\mathbf{K}$, ${\mathfrak{M}}_k\models \mathsf{T}$. One of the most important problems in the model theory of $\mathsf{HA}$ is the following question: {\it Is every Kripke model of $\mathsf{HA}$ locally $\mathsf{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 $\mathbf{K}⊩\mathsf{HA}+\mathsf{EC}{\mathsf{T}}_0$ ($\mathsf{EC}{\mathsf{T}}_0$ stands for Extended Church Thesis). The characterization says that for every arithmetical structure $\mathfrak{M}$, there exists a rooted Kripke model $\mathbf{K}⊩\mathsf{HA}+\mathsf{EC}{\mathsf{T}}_0$ with the root $r$ such that ${\mathfrak{M}}_r=\mathfrak{M}$ iff $\mathfrak{M}\models {\mathbf{Th}}_{{\Pi }_2}(\mathsf{PA})$. One of the consequences of this characterization is that there is a rooted Kripke model $\mathbf{K}⊩\mathsf{HA}+\mathsf{EC}{\mathsf{T}}_0$ with the root $r$ such that ${\mathfrak{M}}_r/\models \mathbf{I}{\Delta }_1$ and hence $\mathbf{K}$ is not even locally $\mathbf{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 $\mathsf{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 $\mathbf{K}⊩\mathsf{T}$ with the root $r$ such that ${\mathfrak{M}}_r=\mathfrak{M}$.

References in corpus (1)

• The provably total recursive functions and the MRDP theorem in Basic Arithmetic and its extensions