Premium
Weak Arithmetics and Kripke Models
Author(s) -
Moniri Morteza
Publication year - 2002
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/1521-3870(200201)48:1<157::aid-malq157>3.0.co;2-3
Subject(s) - mathematics , kripke structure , equivalence (formal languages) , bounded function , section (typography) , forcing (mathematics) , path (computing) , kripke semantics , combinatorics , discrete mathematics , model checking , modal , modal logic , mathematical analysis , algorithm , computer science , chemistry , polymer chemistry , programming language , operating system
In the first section of this paper we show that i Π 1 ≡ W⌝⌝lΠ 1 and that a Kripke model which decides bounded formulas forces iΠ 1 if and only if the union of the worlds in any (complete) path in it satisflies IΠ 1 . In particular, the union of the worlds in any path of a Kripke model of HA models IΠ 1 . In the second section of the paper, we show that for equivalence of forcing and satisfaction of Π m ‐formulas in a linear Kripke model deciding Δ 0 ‐formulas it is necessary and sufficient that the model be Σ m ‐elementary. This implies that if a linear Kripke model forces PEM prenex , then it forces PEM. We also show that, for each n ≥ 1, iΦ n does not prove ℋ(IΠ n 's are Burr's fragments of HA.