|Authors:||Marković, Zoran||Affiliations:||Mathematical Institute of the Serbian Academy of Sciences and Arts||Title:||On the structure of kripke models of heyting arithmetic||Journal:||Mathematical Logic Quarterly||Volume:||39||Issue:||1||First page:||531||Last page:||538||Issue Date:||1-Jan-1993||ISSN:||0942-5616||DOI:||10.1002/malq.19930390154||Abstract:||
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 , ,  and . Here we present some results in the same direction, announced in . 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.
|Keywords:||Heyting arithmetic | Kripke model | Peano arithmetic|
Show full item record
checked on Sep 17, 2022
checked on Sep 15, 2022
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.