β Scribed by Morteza Moniri
No coin nor oath required. For personal study only.
This paper proves some independence results for weak fragments of Heyting arithmetic by using Kripke models. We present a necessary condition for linear Kripke models of arithmetical theories which are closed under the negative translation and use it to show that the union of the worlds in any linear Kripke model of HA satisfies PA. We construct a twoβnode PAβnormal Kripke structure which does not force iΞ£~2~. We prove iβ~1~ β¬ iβ~1~, iβ~1~ β¬ iβ~1~, iΞ ~2~ β¬ iΞ£~2~ and iΞ£~2~ β¬ iΞ ~2~. We use Smorynski's operation Ξ£β² to show HA β¬ lΞ ~1~.
π SIMILAR VOLUMES
The purpose of this note is to show that the independence results for sharply bounded arithmetic of Takeuti [4] and Tada and Tatsuta [3] can be obtained and, in case of the latter, improved by the model-theoretic method developed by the author in [2].
## Abstract A basic result in intuitionism is Ξ ^0^~2~βconservativity. Take any proof __p__ in classical arithmetic of some Ξ ^0^~2~βstatement (some arithmetical statement β__x__.β__y__.__P__(__x, y__), with __P__ decidable). Then we may effectively turn __p__ in some intuitionistic proof of the same