On sequential theorems in reverse mathematics
This work in higher-order reverse mathematics uses the base system \(\mathsf{RCA}^\omega_0\) proposed by \textit{U. Kohlenbach} [Lect. Notes Log. 21, 281--295 (2005; Zbl 1097.03053)]. The authors formalize definitions for semi-continuous functions in this setting and prove in \(\mathsf{RCA}^\omega_0\) the equivalence of formulations of the Heine-Borel theorem and bounding principles for semi-continuous functions. Adding the choice principle \(\mathsf{QF}\text{-}\mathsf{AC}^{0,1}\) to the base system, they extend the equivalences to include supremum principles for semi-continuous functions. A new choice principle, \(\mathsf{CIC}\) for choosing elements from sequences of nonempty closed subsets of \([0,1]\) is introduced, and plays a prominent role in the analysis of sequential forms of results for semi-continuous functions. A sequential form of the Heine-Borel theorem is shown to be equivalent to comprehension statements in the \(\mathsf{WKL}_0\) range plus a choice principle \(\mathsf{OC}^{0,0}\) that is not provable from \(\mathsf{CIC}\). The article closes with a discussion of variations of the results involving \(\mathsf{WWKL}_0\), Cousin's lemma, and the Lebesgue number lemma. Semi-continuous functions were previously studied using second-order formalizations by \textit{D. Fernández-Duque} et al. [Sel. Math., New Ser. 26, No. 5, Paper No. 68, 37 p. (2020; Zbl 1467.03006)] and with \textit{David Fernández-Duque} et al. [``Metric fixed point theory and partial impredicativity, Preprint, \url{arXiv:2302.08874}].
- A note on the sequential version of ^1_2 statements
- Approximations of semicontinuous functions with applications to stochastic optimization and statistical estimation
- Big in reverse mathematics: measure and category
- Big in reverse mathematics: the uncountability of the reals
- Brouwer's fan theorem and unique existence in constructive analysis
- Classical consequences of continuous choice principles from intuitionistic analysis
- Connecting real and hyperarithmetical analysis
- Ekeland's variational principle in weak and strong systems of arithmetic
- Higher-order computability
- scientific article; zbMATH DE number 4002093 (Why is no real title available?)
- scientific article; zbMATH DE number 3767656 (Why is no real title available?)
- scientific article; zbMATH DE number 1030714 (Why is no real title available?)
- scientific article; zbMATH DE number 1549895 (Why is no real title available?)
- scientific article; zbMATH DE number 2236640 (Why is no real title available?)
- INDECOMPOSABLE LINEAR ORDERINGS AND HYPERARITHMETIC ANALYSIS
- Necessary use of \(\Sigma ^1_{1}\) induction in a reversal
- On functions of n complex variables.
- On Real-Valued Functions in Topological Spaces
- On robust theorems due to Bolzano, Weierstrass, Jordan, and Cantor
- On the mathematical and foundational significance of the uncountable
- On the reverse mathematics and Weihrauch complexity of moduli of regularity and uniqueness
- On the strength of marriage theorems and uniformity
- On the uncountability of \(\mathbb{R}\)
- On uniform relationships between combinatorial problems
- On uniform weak König's lemma
- On Weierstrass extreme value theorem
- Open sets in computability theory and reverse mathematics
- Pincherle's theorem in reverse mathematics and computability theory
- Representations and the foundations of mathematics
- Representations of Reals in Reverse Mathematics
- Reverse Mathematics
- Reverse mathematics and uniformity in proofs without excluded middle
- Reverse mathematics, trichotomy and dichotomy
- Some characterizations of normal and perfectly normal spaces
- Standard and non-standard analysis in second order arithmetic
- Subsystems of second order arithmetic
- Sur quelques points de la théorie des ensembles.
- The axiom of choice in computability theory and reverse mathematics with a cameo for the continuum hypothesis
- The biggest five of reverse mathematics
- The Dirac delta function in two settings of reverse mathematics
- Theory of relations. Transl. from the French by P. Clote. With an appendix by Norbert Sauer.
- Über halbstetige und unstetige Funktionen.
This page was built for publication: On sequential theorems in reverse mathematics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6857832)
