Classical provability of uniform versions and intuitionistic provability

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 .