Classical consequences of continuous choice principles from intuitionistic analysis (Q2443117): Difference between revisions

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)].