Finite Kripke models of HA are locally PA (Q1095140)

In a Kripke model for Heyting arithmetic the nodes carry classical models of (subsystems of) Peano arithmetic. It is not known which theories hold for these local models in general. In the present paper it is established that in finite Kripke models the local models are models of full Peano arithmetic. The method used in the paper is a model theoretic version of the Friedman translation [\textit{H. Friedman}, Lect. Notes Math. 669, 21-27 (1978; Zbl 0396.03045)].