Intuitionistic weak arithmetic (Q1423636)

The paper is devoted to the study of some weak fragments of Heyting arithmetic and Kripke models of them. \(\omega\)-framed Kripke models of \(i \forall_{1}\) and \(i \Pi_{1}\) are constructed none of whose worlds satisfies \(\forall x\;\exists y (x=2y \vee x=2y+1)\) and \(\forall x, y\;\exists z \text{ Exp}(x,y,z)\), respectively. This enables the author to show that \(i \forall_{1}\) does not prove \(\neg \neg \forall x\;\exists y (x=2y \vee x=2y+1)\) and \(i \Pi_{1}\) does not prove \(\neg \neg \forall x, y\;\exists z \text{ Exp}(x,y,z)\). Therefore, \(i \forall_{1} \nvdash \neg \neg \text{ lop}\) and \(i \Pi_{1} \nvdash \neg \neg i \Sigma_{1}\). It is also shown that \(\text{HA} \nvdash l \Sigma_{1}\).