Premium
Classical provability of uniform versions and intuitionistic provability
Author(s) -
Fujiwara Makoto,
Kohlenbach Ulrich
Publication year - 2015
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.201300056
Subject(s) - mathematics , lemma (botany) , statement (logic) , type (biology) , pure mathematics , discrete mathematics , calculus (dental) , medicine , ecology , poaceae , dentistry , political science , law , biology
Along the line of Hirst‐Mummert [9][J. L. Hirst, 2011] and Dorais [4][F. G. Dorais, 2014], 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 Kőnig's lemma KL and uniform weak Kőnig's lemma UWKL . Our result is applicable to many mathematical principles whose sequential versions imply ACA .