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
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.
Keywords: Heyting arithmetic | Kripke model | Peano arithmetic

Show full item record


checked on Sep 17, 2022

Page view(s)

checked on Sep 15, 2022

Google ScholarTM




Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.