Intuitionistic weak arithmetic
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}\).
- Weak arithmetics
- Intuitionistic elementary arithmetic
- Weak arithmetical interpretations for the logic of proofs
- On intuitionistic elementary arithmetic
- Weak arithmetic
- scientific article; zbMATH DE number 5862877
- scientific article; zbMATH DE number 2236625
- An arithmetic interpretation of intuitionistic verification
- Intuitionistic Refinement Calculus
- Weak arithmetics and Kripke models
- Weak arithmetics and Kripke models
- scientific article; zbMATH DE number 5364051 (Why is no real title available?)
- Fragments of Heyting arithmetic
- Some weak fragments of HA and certain closure properties
- scientific article; zbMATH DE number 2152688 (Why is no real title available?)
- The strength of replacement in weak arithmetic
- The intuitionistic Robinson arithmetic(s)
This page was built for publication: Intuitionistic weak arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1423636)
