Classical consequences of continuous choice principles from intuitionistic analysis (Q2443117): Difference between revisions
From MaRDI portal
Removed claim: reviewed by (P1447): Item:Q335001 |
Changed an Item |
||
Property / reviewed by | |||
Property / reviewed by: Jeffry L. Hirst / rank | |||
Normal rank |
Revision as of 07:01, 13 February 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Classical consequences of continuous choice principles from intuitionistic analysis |
scientific article |
Statements
Classical consequences of continuous choice principles from intuitionistic analysis (English)
0 references
4 April 2014
0 references
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)].
0 references
intuitionistic analysis
0 references
second-order arithmetic
0 references
reverse mathematics
0 references
realizability
0 references
choice principles
0 references
Lifschitz
0 references
sequential
0 references
uniformity
0 references