Premium
On the structure of kripke models of heyting arithmetic
Author(s) -
Marković Zoran
Publication year - 1993
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.19930390154
Subject(s) - mathematics , peano axioms , relation (database) , decidability , kripke semantics , kripke structure , arithmetic , pure mathematics , discrete mathematics , model checking , algorithm , computer science , intermediate logic , theoretical computer science , database , description logic
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 is then: are these classical structures models of Peano Arithmetic (PA)? And dually: 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 partial answers to these questions were obtained in [6], [3], [1] and [2]. Here we present some results in the same direction, announced in [7]. In particular, it is proved that the classical structures at the nodes of a Kripke model of HA must be models of IΔ 1 (PA ‐ with induction for provably Δ 1 formulas) and that the relation between these classical structures must be that of a Δ 1 ‐elementary submodel. MSC: 03F30, 03F55.