Abstract
Tao’s notion of metastability is classically equivalent to the well-known ‘epsilon delta’ definition of Cauchy sequence, but the former has much nicer computational properties than the latter. In particular, results from the proof mining program suggest that metastability gives rise to highly uniform and computable results under very general conditions, in contrast to the non-uniform and/or non-computable rates of convergence emerging from basic convergence theorems involving the definition of Cauchy sequence. As a trade-off for these high levels of uniformity, metastability only provides information about a finite but arbitrarily large domain. In this paper, we apply this ‘metastability trade-off’ to basic theorems of mathematics, i.e. we introduce in the latter finite domains in exchange for high(er) levels of uniformity. In contrast to the aforementioned effective results from proof mining, we obtain functionals of extreme computational hardness. Thus, our results place a hard limit on the generality of the metastability trade-off and show that metastability does not provide a ‘king’s road’ to computable mathematics. Perhaps surprisingly, we shall make use of Nonstandard Analysis (NSA) to establish the aforementioned results (which do not involve NSA).
S. Sanders—This research was supported by the Alexander von Humboldt Foundation and LMU Munich (via the Excellence Initiative).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
- 2.
Unless explicitly stated otherwise, we work in classical mathematics.
- 3.
Heine-Borel theorem in Reverse Mathematics deals with countable covers ([26, IV.1]).
- 4.
The acronym \(\textsf {ZFC} \) stands for Zermelo-Fraenkel set theory with the axiom of choice.
- 5.
The superscript ‘fin’ in (I) means that x is finite, i.e. its number of elements is bounded by a natural number.
- 6.
The language of \(\textsf {E-PA}_{{st}}^{\omega *}\) contains a symbol \({st}_{\sigma }\) for each finite type \(\sigma \), but the subscript is essentially always omitted. Hence \(\mathcal {T}^{*}_{{st}}\) is an axiom schema and not an axiom..
- 7.
A term is called closed in [3] if all variables are bound via lambda abstraction. Thus, if \(\underline{x}, \underline{y}\) are the only variables occurring in the term t, the term \((\lambda \underline{x})(\lambda \underline{y})t(\underline{x}, \underline{y})\) is closed while \((\lambda \underline{x})t(\underline{x}, \underline{y})\) is not. The second axiom in Definition 2.3 thus expresses that \({st}_{\tau }\big ((\lambda \underline{x})(\lambda \underline{y})t(\underline{x}, \underline{y})\big )\) if \((\lambda \underline{x})(\lambda \underline{y})t(\underline{x}, \underline{y})\) is type \(\tau \). We shall omit lambda abstraction.
- 8.
Note that \(\textsf {IVT} _{\textsf {ns} }\) looks fairly close to \(\textsf {IVT} ^{\mathrm{{{st}}}}\), and the latter is provable in \({\textsf {P}}_{0}\). Nonetheless, \(\textsf {IVT} _{\textsf {ns} }\) turns out to be equivalent to \(\textsf {STP} \) from Sect. 2.4. Furthermore, an obvious mistake is to apply Transfer to the conclusion of \(\textsf {IVT} _{\textsf {ns} }\) and conclude there is a standard intermediate value. Indeed, the function f from \(\textsf {IVT} _{\textsf {ns} }\) need not be standard, making application of the Transfer axiom illegal, following Nelson [17].
- 9.
References
Avigad, J., Dean, E.T., Rute, J.: A metastable dominated convergence theorem. J. Log. Anal. 4, 1–19 (2012)
Beeson, M.J.: Foundations of Constructive Mathematics: Metamathematical Studies. Ergebnisse der Mathematik und ihrer Grenzgebiete, vol. 6. Springer, Heidelberg (1985)
van den Berg, B., Briseid, E., Safarik, P.: A functional interpretation for nonstandard arithmetic. Ann. Pure Appl. Logic 163, 1962–1994 (2012)
Bishop, E., Bridges, D.S.: Constructive Analysis, Grundlehren der Mathematischen Wissenschaften, vol. 279. Springer, Berlin (1985)
Cousin, P.: Sur les fonctions de n variables complexes. Acta Math. 19(1), 1–61 (1895)
Hurd, A.E., Loeb, P.A.: An Introduction to Nonstandard Real Analysis, Pure and Applied Mathematics, vol. 118. Academic Press Inc., Orlando (1985)
Ishihara, H.: Reverse mathematics in Bishop’s constructive mathematics. Philosophia Scientiae (Cahier Spécial) 6, 43–59 (2006)
Ishihara, H.: Continuity properties in constructive mathematics. JSL 57, 557–565 (1992)
Ishihara, H.: Continuity and nondiscontinuity in constructive mathematics. JSL 56, 1349–1354 (1991)
Keisler, H.J.: Nonstandard arithmetic and reverse mathematics. Bull. Symb. Log. 12, 100–125 (2006)
Kohlenbach, U., Koutsoukou-Argyraki, A.: Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators. J. Math. Anal. Appl. 423(2), 1089–1112 (2015)
Kohlenbach, U.: Applied Proof Theory: Proof Interpretations and Their Use in Mathematics. Springer Monographs in Mathematics. Springer, Berlin (2008)
Kohlenbach, U.: Higher order reverse mathematics. In: Reverse mathematics 2001. Lecture Notes in Logistics, vol. 21, pp. 281–295. ASL (2005)
Kohlenbach, U.: Foundational and mathematical uses of higher types. Lecture Notes in Logistics, vol. 15, pp. 92–116. ASL (2002)
Lietz, P., Streicher, T.: Realizability models refuting Ishihara’s bound- edness principle. Ann. Pure Appl. Log. 163(12), 1803–1807 (2012)
Longley, J., Normann, D.: Higher-Order Computability. Theory and Applications of Computability. Springer, Heidelberg (2015)
Nelson, E.: Internal set theory: a new approach to nonstandard analysis. Bull. Am. Math. Soc. 83(6), 1165–1198 (1977)
Normann, D.: The extensional realizability model of continuous functionals and three weakly non-constructive classical theorems. Log. Methods Comput. Sci. 11, 1–27 (2015)
Normann, D., Sanders, S.: Nonstandard analysis, computability theory, and their connections (2017, submitted). https://arxiv.org/abs/1702.06556
Normann, D.: Nonstandard analysis, computability theory, and metastability (2017)
Sanders, S.: The Gandy-Hyland functional and a hitherto unknown computational aspect of Nonstandard Analysis. Computability, arXiv: http://arxiv.org/abs/1502.03622 (2015)
Sanders, S.: Grilliot’s trick in Nonstandard Analysis. Logical Methods in Computer Science, Special Issue for CCC15 (2017)
Sanders, S.: The unreasonable effectiveness of Nonstandard Analysis (2015). http://arxiv.org/abs/1508.07434
Sanders, S.: To be or not to be constructive, Indagationes Mathematicae, p. 69, arXiv: https://arxiv.org/abs/1704.00462 2017
Sanders, S.: The refining of the taming of the Reverse Mathematics zoo. Notre Dame J. Formal Log. (2016). http://arxiv.org/abs/1602.02270
Stephen, G.: Simpson, Subsystems of Second Order Arithmetic. Perspectives in Logic, 2nd edn. CUP, Cambridge (2009)
Simpson, S.G., Yokoyama, K.: A nonstandard counterpart of WWKL. Notre Dame J. Form. Log. 52(3), 229–243 (2011)
Tao, T.: Structure and randomness, pp. xii+298. American Mathematical Society, Providence, RI (2008)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this paper
Cite this paper
Sanders, S. (2018). Metastability and Higher-Order Computability. In: Artemov, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2018. Lecture Notes in Computer Science(), vol 10703. Springer, Cham. https://doi.org/10.1007/978-3-319-72056-2_19
Download citation
DOI: https://doi.org/10.1007/978-3-319-72056-2_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-72055-5
Online ISBN: 978-3-319-72056-2
eBook Packages: Computer ScienceComputer Science (R0)