Classical consequences of continuous choice principles from intuitionistic analysis (Q2443117)

The central result of this paper shows that provability of certain theorems in an intuitionistic system implies provability of sequential variants in a classical system. Corollary 4.9 states that for certain formulas \(B(X)\) and \(A(X,Y)\), if EL+WKL+GC\(_L\)+CN\(_L\) proves \(\forall X ( B(X) \to \exists Y A (X,Y))\), then RCA+WKL proves \(\forall X ( \forall n B(X_n) \to \exists Y \forall n A(X_ n,Y_n))\). Here, RCA and WKL have their usual reverse mathematics meanings, EL denotes an intuitionistic restriction of RCA, GC is Troelstra's generalized continuity principle, and CN is a subclass of consequences of the law of the excluded middle. This result differs from those of \textit{J. L. Hirst} and \textit{C. Mummert} [Notre Dame J. Formal Logic 52, No. 2, 149--162 (2011; Zbl 1225.03083)] in the class of theorems addressed, extending allowed formula structures while restricting variable types. The result holds when \(B(X) \to \exists Y A (X,Y)\) is in the class \(\Gamma_L\), which allows more options for the structure of \(B(X)\) than the classes used in Hirst and Mummert's results [loc. cit.]. The expansion of this class arises from the use of the Lifschitz variant of Kleene realizability of \textit{J. van Oosten} [J. Symb. Log. 55, No. 2, 805--821 (1990; Zbl 0704.03040)].