Bibliographic Details
| Title: |
An Independence Result for Intuitionistic Bounded Arithmetic. |
| Authors: |
Moniri, Morteza1 ezmoniri@ipm.ir |
| Source: |
Journal of Logic & Computation. Apr2006, Vol. 16 Issue 2, p199-204. 6p. |
| Subjects: |
Arithmetic, Computer arithmetic & logic units, Intuitionistic mathematics, Polynomials, Mathematical formulas, Sentences (Grammar), Mathematical models, Mathematical logic |
| Abstract: |
It is shown that the intuitionistic theory of polynomial induction on positive Π1b (coNP) formulas does not prove the sentence ¬¬∀x, y∃z ≤ y(x ≤ |y| → x = |z|). This implies the unprovability of the scheme ¬¬PIND(∑1b+) in the mentioned theory. However, this theory contains the sentence ∀x, y¬¬∃z ≤ y(x ≤ |y| → x = |z|). The above independence result is proved by constructing an ω-chain of submodels of a countable model of S2 + Ω3 + ¬exp such that none of the worlds in the chain satisfies the sentence, and interpreting the chain as a Kripke model. [ABSTRACT FROM PUBLISHER] |
|
Copyright of Journal of Logic & Computation is the property of Oxford University Press / USA and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| Database: |
Engineering Source |
