Classical provability of uniform versions and intuitionistic provability
Makoto Fujiwara, Ulrich Kohlenbach · Mathematical logic quarterly · 2015
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 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 in all finite types but also nonconstructive principles such as Kőnig's lemma and uniform weak Kőnig's lemma . Our result is applicable to many mathematical principles whose sequential versions imply .