Metastability and Higher-Order Computability

  • Sam SandersEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10703)


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


Metastability Higher-order computability Nonstandard analysis 


  1. 1.
    Avigad, J., Dean, E.T., Rute, J.: A metastable dominated convergence theorem. J. Log. Anal. 4, 1–19 (2012)MathSciNetzbMATHGoogle Scholar
  2. 2.
    Beeson, M.J.: Foundations of Constructive Mathematics: Metamathematical Studies. Ergebnisse der Mathematik und ihrer Grenzgebiete, vol. 6. Springer, Heidelberg (1985)CrossRefzbMATHGoogle Scholar
  3. 3.
    van den Berg, B., Briseid, E., Safarik, P.: A functional interpretation for nonstandard arithmetic. Ann. Pure Appl. Logic 163, 1962–1994 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Bishop, E., Bridges, D.S.: Constructive Analysis, Grundlehren der Mathematischen Wissenschaften, vol. 279. Springer, Berlin (1985)Google Scholar
  5. 5.
    Cousin, P.: Sur les fonctions de n variables complexes. Acta Math. 19(1), 1–61 (1895)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Hurd, A.E., Loeb, P.A.: An Introduction to Nonstandard Real Analysis, Pure and Applied Mathematics, vol. 118. Academic Press Inc., Orlando (1985)zbMATHGoogle Scholar
  7. 7.
    Ishihara, H.: Reverse mathematics in Bishop’s constructive mathematics. Philosophia Scientiae (Cahier Spécial) 6, 43–59 (2006)CrossRefGoogle Scholar
  8. 8.
    Ishihara, H.: Continuity properties in constructive mathematics. JSL 57, 557–565 (1992)MathSciNetzbMATHGoogle Scholar
  9. 9.
    Ishihara, H.: Continuity and nondiscontinuity in constructive mathematics. JSL 56, 1349–1354 (1991)MathSciNetzbMATHGoogle Scholar
  10. 10.
    Keisler, H.J.: Nonstandard arithmetic and reverse mathematics. Bull. Symb. Log. 12, 100–125 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Kohlenbach, U.: Applied Proof Theory: Proof Interpretations and Their Use in Mathematics. Springer Monographs in Mathematics. Springer, Berlin (2008)zbMATHGoogle Scholar
  13. 13.
    Kohlenbach, U.: Higher order reverse mathematics. In: Reverse mathematics 2001. Lecture Notes in Logistics, vol. 21, pp. 281–295. ASL (2005)Google Scholar
  14. 14.
    Kohlenbach, U.: Foundational and mathematical uses of higher types. Lecture Notes in Logistics, vol. 15, pp. 92–116. ASL (2002)Google Scholar
  15. 15.
    Lietz, P., Streicher, T.: Realizability models refuting Ishihara’s bound- edness principle. Ann. Pure Appl. Log. 163(12), 1803–1807 (2012)CrossRefzbMATHGoogle Scholar
  16. 16.
    Longley, J., Normann, D.: Higher-Order Computability. Theory and Applications of Computability. Springer, Heidelberg (2015)CrossRefzbMATHGoogle Scholar
  17. 17.
    Nelson, E.: Internal set theory: a new approach to nonstandard analysis. Bull. Am. Math. Soc. 83(6), 1165–1198 (1977)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Normann, D.: The extensional realizability model of continuous functionals and three weakly non-constructive classical theorems. Log. Methods Comput. Sci. 11, 1–27 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Normann, D., Sanders, S.: Nonstandard analysis, computability theory, and their connections (2017, submitted).
  20. 20.
    Normann, D.: Nonstandard analysis, computability theory, and metastability (2017)Google Scholar
  21. 21.
    Sanders, S.: The Gandy-Hyland functional and a hitherto unknown computational aspect of Nonstandard Analysis. Computability, arXiv: (2015)
  22. 22.
    Sanders, S.: Grilliot’s trick in Nonstandard Analysis. Logical Methods in Computer Science, Special Issue for CCC15 (2017)Google Scholar
  23. 23.
    Sanders, S.: The unreasonable effectiveness of Nonstandard Analysis (2015).
  24. 24.
    Sanders, S.: To be or not to be constructive, Indagationes Mathematicae, p. 69, arXiv: 2017
  25. 25.
    Sanders, S.: The refining of the taming of the Reverse Mathematics zoo. Notre Dame J. Formal Log. (2016).
  26. 26.
    Stephen, G.: Simpson, Subsystems of Second Order Arithmetic. Perspectives in Logic, 2nd edn. CUP, Cambridge (2009)zbMATHGoogle Scholar
  27. 27.
    Simpson, S.G., Yokoyama, K.: A nonstandard counterpart of WWKL. Notre Dame J. Form. Log. 52(3), 229–243 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Tao, T.: Structure and randomness, pp. xii+298. American Mathematical Society, Providence, RI (2008)Google Scholar

Copyright information

© Springer International Publishing AG 2018

Authors and Affiliations

  1. 1.Center for Advanced Studies and Munich Center for Mathematical PhilosophyLMU MunichMunichGermany

Personalised recommendations