Finite Kripke models of HA are locally PA (Q1095140)
From MaRDI portal
| This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Finite Kripke models of HA are locally PA |
scientific article; zbMATH DE number 4027462
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Finite Kripke models of HA are locally PA |
scientific article; zbMATH DE number 4027462 |
Statements
Finite Kripke models of HA are locally PA (English)
0 references
1986
0 references
In a Kripke model for Heyting arithmetic the nodes carry classical models of (subsystems of) Peano arithmetic. It is not known which theories hold for these local models in general. In the present paper it is established that in finite Kripke models the local models are models of full Peano arithmetic. The method used in the paper is a model theoretic version of the Friedman translation [\textit{H. Friedman}, Lect. Notes Math. 669, 21-27 (1978; Zbl 0396.03045)].
0 references
Heyting arithmetic
0 references
Peano arithmetic
0 references
local models
0 references
finite Kripke models
0 references