An Independence Result for Intuitionistic Bounded Arithmetic.
Saved in:
| 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 |
| FullText | Links: – Type: pdflink Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 44441453 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: An Independence Result for Intuitionistic Bounded Arithmetic. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Moniri%2C+Morteza%22">Moniri, Morteza</searchLink><relatesTo>1</relatesTo><i> ezmoniri@ipm.ir</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Journal+of+Logic+%26+Computation%22">Journal of Logic & Computation</searchLink>. Apr2006, Vol. 16 Issue 2, p199-204. 6p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Arithmetic%22">Arithmetic</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+arithmetic+%26+logic+units%22">Computer arithmetic & logic units</searchLink><br /><searchLink fieldCode="DE" term="%22Intuitionistic+mathematics%22">Intuitionistic mathematics</searchLink><br /><searchLink fieldCode="DE" term="%22Polynomials%22">Polynomials</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+formulas%22">Mathematical formulas</searchLink><br /><searchLink fieldCode="DE" term="%22Sentences+%28Grammar%29%22">Sentences (Grammar)</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+models%22">Mathematical models</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+logic%22">Mathematical logic</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>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.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=44441453 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1093/logcom/exi085 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 6 StartPage: 199 Subjects: – SubjectFull: Arithmetic Type: general – SubjectFull: Computer arithmetic & logic units Type: general – SubjectFull: Intuitionistic mathematics Type: general – SubjectFull: Polynomials Type: general – SubjectFull: Mathematical formulas Type: general – SubjectFull: Sentences (Grammar) Type: general – SubjectFull: Mathematical models Type: general – SubjectFull: Mathematical logic Type: general Titles: – TitleFull: An Independence Result for Intuitionistic Bounded Arithmetic. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Moniri, Morteza IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 04 Text: Apr2006 Type: published Y: 2006 Identifiers: – Type: issn-print Value: 0955792X Numbering: – Type: volume Value: 16 – Type: issue Value: 2 Titles: – TitleFull: Journal of Logic & Computation Type: main |
| ResultId | 1 |
