Let $K$ be a kripke model and $k$ be one of its node, then $\mathcal{M}_k$ is classical structure of $k$.
What is the strongest theory of arithmetic like $T$ such that for every kripke model $K\Vdash HA$ and for every nodes of it like $k$, $\mathcal{M}_k\models T$?.
It is not hard to see that $T\vdash I\Delta_0$, because $HA$ proves least number principle for $\Delta_0$ formulas.
I found two paper that partially answered this question:
Finite Kripke models of HA are locally PA
Every Rooted Narrow Tree Kripke Model of HA is Locally PA
I want to know is there any other results on this question? Also can $T$ be a stronger theory than $I\Delta_0$ like $I\Sigma_1$?