Classical provability of uniform versions and intuitionistic provability

Makoto Fujiwara, Ulrich Kohlenbach

研究成果: Article

抄録

Along the line of Hirst-Mummert and Dorais , we analyze the relationship between the classical provability of uniform versions Uni(S) of Π2-statements S with respect to higher order reverse mathematics and the intuitionistic provability of S. Our main theorem states that (in particular) for every Π2-statement S of some syntactical form, if its uniform version derives the uniform variant of ACA over a classical system of arithmetic in all finite types with weak extensionality, then S is not provable in strong semi-intuitionistic systems including bar induction BI in all finite types but also nonconstructive principles such as Konig's lemma KL and uniform weak Konig's lemma UWKL. Our result is applicable to many mathematical principles whose sequential versions imply ACA.

元の言語English
ページ(範囲)132-150
ページ数19
ジャーナルMathematical Logic Quarterly
61
発行部数3
DOI
出版物ステータスPublished - 2015 5 1
外部発表Yes

Fingerprint

Finite Type
Lemma
Reverse Mathematics
Proof by induction
Higher Order
Imply
Line
Theorem
Syntax
Form
Relationships

ASJC Scopus subject areas

  • Logic

これを引用

Classical provability of uniform versions and intuitionistic provability. / Fujiwara, Makoto; Kohlenbach, Ulrich.

:: Mathematical Logic Quarterly, 巻 61, 番号 3, 01.05.2015, p. 132-150.

研究成果: Article

Fujiwara, Makoto ; Kohlenbach, Ulrich. / Classical provability of uniform versions and intuitionistic provability. :: Mathematical Logic Quarterly. 2015 ; 巻 61, 番号 3. pp. 132-150.
@article{800f024902244ad787768afb90de61ee,
title = "Classical provability of uniform versions and intuitionistic provability",
abstract = "Along the line of Hirst-Mummert and Dorais , we analyze the relationship between the classical provability of uniform versions Uni(S) of Π2-statements S with respect to higher order reverse mathematics and the intuitionistic provability of S. Our main theorem states that (in particular) for every Π2-statement S of some syntactical form, if its uniform version derives the uniform variant of ACA over a classical system of arithmetic in all finite types with weak extensionality, then S is not provable in strong semi-intuitionistic systems including bar induction BI in all finite types but also nonconstructive principles such as Konig's lemma KL and uniform weak Konig's lemma UWKL. Our result is applicable to many mathematical principles whose sequential versions imply ACA.",
author = "Makoto Fujiwara and Ulrich Kohlenbach",
year = "2015",
month = "5",
day = "1",
doi = "10.1002/malq.201300056",
language = "English",
volume = "61",
pages = "132--150",
journal = "Mathematical Logic Quarterly",
issn = "0942-5616",
publisher = "Wiley-VCH Verlag",
number = "3",

}

TY - JOUR

T1 - Classical provability of uniform versions and intuitionistic provability

AU - Fujiwara, Makoto

AU - Kohlenbach, Ulrich

PY - 2015/5/1

Y1 - 2015/5/1

N2 - Along the line of Hirst-Mummert and Dorais , we analyze the relationship between the classical provability of uniform versions Uni(S) of Π2-statements S with respect to higher order reverse mathematics and the intuitionistic provability of S. Our main theorem states that (in particular) for every Π2-statement S of some syntactical form, if its uniform version derives the uniform variant of ACA over a classical system of arithmetic in all finite types with weak extensionality, then S is not provable in strong semi-intuitionistic systems including bar induction BI in all finite types but also nonconstructive principles such as Konig's lemma KL and uniform weak Konig's lemma UWKL. Our result is applicable to many mathematical principles whose sequential versions imply ACA.

AB - Along the line of Hirst-Mummert and Dorais , we analyze the relationship between the classical provability of uniform versions Uni(S) of Π2-statements S with respect to higher order reverse mathematics and the intuitionistic provability of S. Our main theorem states that (in particular) for every Π2-statement S of some syntactical form, if its uniform version derives the uniform variant of ACA over a classical system of arithmetic in all finite types with weak extensionality, then S is not provable in strong semi-intuitionistic systems including bar induction BI in all finite types but also nonconstructive principles such as Konig's lemma KL and uniform weak Konig's lemma UWKL. Our result is applicable to many mathematical principles whose sequential versions imply ACA.

UR - http://www.scopus.com/inward/record.url?scp=84929664147&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84929664147&partnerID=8YFLogxK

U2 - 10.1002/malq.201300056

DO - 10.1002/malq.201300056

M3 - Article

AN - SCOPUS:84929664147

VL - 61

SP - 132

EP - 150

JO - Mathematical Logic Quarterly

JF - Mathematical Logic Quarterly

SN - 0942-5616

IS - 3

ER -