Structure of Kripke Models of Heyting Arithmetic

摘要

Partial answers to the following questions were obtained in referenced papers.Since in Heyting Arithmetic (HA) all atomic formulas are decidable, a Kripke model for HA may be regarded classically as a collection of classical structures for the language of arithmetic, partially ordered by the submodel relation. The obvious question are the following: are these classical structures models of Peano Arithmetic (PA); and if a collection of models of PA, partially ordered by the submodel relation, is regarded as a Kripke model, is it a model of HA Some results in the same direction are presented. In particular, it is proved that the classical structures at the nodes of Kripke model of HA must be models of I(delta(sub 1))(PA(sup -) with induction for provably Delta(sub 1) formulas) and that the relation between these classical structures must be that of a Delta(sub 1) elementary submodel.