Classical and intuitionistic models of arithmetic (Q1355126)

A Kripke model of a theory \(T\), in a language \(L\), is a structure \({\mathbb{K}}=(K,\leq, (A_\alpha)_{\alpha\in K})\), where \((K,\leq)\) is a partial order, called the frame of \(\mathbb{K}\), and the structures \(A_\alpha\), for \(\alpha\in K\), are classical \(L\)-structures satisfying certain monotonicity conditions with respect to \(K\). \({\mathbb{K}}\) is locally \(T\) if all structures \(A_\alpha\) are classical models of \(T\). \textit{D. van Dalen, H. Mulder, E. C. Krabbe} and \textit{A. Visser} proved [Notre Dame J. Formal Logic 27, 528-532 (1986; Zbl 0632.03048)] that Kripke models of Heyting Arithmetic (HA) over finite frames are locally PA. Using the technique of pruning of van Dalen et al. [loc. cit.], the author shows that Kripke models of HA over the frame \((\omega,\leq)\) are locally PA. This result is then extended to some other types of infinite frames. The paper also presents other results concerning the conjecture: all Kripke models of HA are locally PA.