Abstract
In classical computability theory, a recursive counterexample to a theorem shows that the latter does not hold when restricted to computable objects. These counterexamples are highly useful in the Reverse Mathematics program, where the aim of the latter is to determine the minimal axioms needed to prove a given theorem of ordinary mathematics. Indeed, recursive counterexamples often (help) establish the ‘reverse’ implication in the typical equivalence between said minimal axioms and the theorem at hand. The aforementioned is generally formulated in the language of second-order arithmetic and we show in this paper that recursive counterexamples are readily modified to provide similar implications in higher-order arithmetic. For instance, the higher-order analogue of ‘sequence’ is the topological notion of ‘net’, also known as ‘Moore-Smith sequence’. Our results on metric spaces suggest that the latter can only be reasonably studied in weak systems via representations (aka codes) in the language of second-order arithmetic.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
To be absolutely clear, variables (of any finite type) are allowed in quantifier-free formulas of the language \(\textsf {L }_{\omega }\): only quantifiers are banned.
- 2.
An equivalence relation is a binary, reflexive, transitive, and symmetric relation.
References
Avigad, J., Feferman, S.: Gödel’s functional (“dialectica”) interpretation. In: Handbook of Proof Theory. Studies in Logic and the Foundations of Mathematics, vol. 137, pp. 337–405 (1998)
Bartle, R.G.: Nets and filters in topology. Am. Math. Mon. 62, 551–557 (1955)
Brown, D.K.: Notions of closed subsets of a complete separable metric space in weak subsystems of second-order arithmetic. In: Logic and Computation, Pittsburgh, PA (1987). Contemporary Mathematics, vol. 106, pp. 39–50. American Mathematical Society, Providence, RI (1990)
Brown, D.K.: Notions of compactness in weak subsystems of second order arithmetic. In: Simpson, S. (ed.) Reverse Mathematics 2001. Perspectives in Logic, pp. 47–66. Association for Symbolic Logic, Urbana, IL (2005)
Dorais, F.G., Hirst, J.L., Shafer, P.: Reverse mathematics, trichotomy and dichotomy. J. Log. Anal. 4, 14 (2012). Paper 13
Ershov, Y.L.: Theorie der numerierungen III. Z. Math. Logik Grundlagen Math. 23(4), 289–371 (1977)
Ershov, Y.L., Goncharov, S.S., Nerode, A., Remmel, J.B., Marek, V.W. (eds.): Handbook of Recursive Mathematics. Volume 138 of Studies in Logic and the Foundations of Mathematics, Vol. 1. North-Holland, Amsterdam (1998). Recursive Model Theory
Friedman, H.: Some systems of second order arithmetic and their use. In: Proceedings of the International Congress of Mathematicians (Vancouver, B.C., 1974), vol. 1, pp. 235–242 (1975)
Friedman, H.: Systems of second order arithmetic with restricted induction, I & II (abstracts). J. Symb. Log. 41, 557–559 (1976)
Friedman, H., Simpson, S.G., Smith, R.: Countable algebra and set existence axioms. Ann. Pure Appl. Logic 25(2), 141–181 (1983)
Hatzikiriakou, K.: Minimal prime ideals and arithmetic comprehension. J. Symb. Log. 56(1), 67–70 (1991)
Hirst, J.L.: Combinatorics in subsystems of second order arithmetic, Ph.D. thesis, The Pennsylvania State University, ProQuest LLC, Ann Arbor, MI (1987)
Hunter, J.: Higher-order reverse topology, Ph.D. thesis, The University of Wisconsin-Madison, ProQuest LLC, Ann Arbor, MI (2008)
Kelley, J.L.: General Topology. Springer, New York (1975). Reprint of the 1955 edition; Graduate Texts in Mathematics, no. 27
Kohlenbach, U.: Foundational and mathematical uses of higher types. In: Reflections on the Foundations of Mathematics (Stanford, CA, 1998). Lecture Notes in Logic 15, pp. 92–116. Association for Symbolic Logic, Urbana, IL (2002)
Kohlenbach, U.: Higher order reverse mathematics. In: Simpson, S. (ed.) Reverse Mathematics 2001. Perspectives in Logic, pp. 281–295. Association for Symbolic Logic, Urbana, IL (2005)
Mandelkern, M.: Brouwerian counterexamples. Math. Mag. 62(1), 3–27 (1989)
Moore, E.H., Smith, H.: A general theory of limits. Am. J. Math. 44, 102–121 (1922)
Normann, D., Sanders, S.: On the mathematical and foundational significance of the uncountable. J. Math. Log. (2018). https://doi.org/10.1142/S0219061319500016
Normann, D., Sanders, S.: Pincherle’s theorem in Reverse Mathematics and computability theory. arXiv:1808.09783 (2018, submitted)
Rado, R.: Axiomatic treatment of rank in infinite sets. Can. J. Math. 1, 337–343 (1949)
Royden, H.L.: Real Analysis, 3rd edn. Macmillan Publishing Company, New York (1988)
Rudin, W.: Real and Complex Analysis, 3rd edn. McGraw-Hill, New York (1987)
Sanders, S.: Plato and the foundations of mathematics. arxiv:1908.05676, pp. 44 (2019, submitted)
Sanders, S.: Nets and reverse mathematics: a pilot study, to appear in Computability, pp. 34 (2019)
Sanders, S.: Nets and reverse mathematics. In: Manea, F., Martin, B., Paulusma, D., Primiero, G. (eds.) CiE 2019. LNCS, vol. 11558, pp. 253–264. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-22996-2_22
Sanders, S.: Reverse mathematics and computability theory of domain theory. In: Iemhoff, R., Moortgat, M., de Queiroz, R. (eds.) WoLLIC 2019. LNCS, vol. 11541, pp. 550–568. Springer, Heidelberg (2019). https://doi.org/10.1007/978-3-662-59533-6_33
Simpson, S.G.: Subsystems of Second Order Arithmetic. Perspectives in Logic, 2nd edn. Cambridge University Press, Cambridge (2009)
Simpson, S.G., Rao, J.: Reverse algebra. In: Handbook of Recursive Mathematics, Volume 2, Studies in Logic and the Foundations of Mathematics, vol. 139, pp. 1355–1372. North-Holland (1998)
Solomon, D.R.: Reverse mathematics and ordered groups, Ph.D. thesis, Cornell University, ProQuest LLC (1998)
Specker, E.: Nicht konstruktiv beweisbare Sätze der Analysis. J. Symb. Log. 14, 145–158 (1949)
Stillwell, J.: Reverse Mathematics, Proofs from the Inside Out. Princeton University Press, Princeton (2018)
Troelstra, A.S.: Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, vol. 344. Springer, Berlin (1973). https://doi.org/10.1007/BFb0066739
Turing, A.: On computable numbers, with an application to the Entscheidungs-problem. Proc. Lond. Math. Soc. 42, 230–265 (1936)
Vietoris, L.: Stetige Mengen (German). Monatsh. Math. Phys. 31, 173–204 (1921)
Acknowledgement
Our research was supported by the John Templeton Foundation via the grant a new dawn of intuitionism with ID 60842. We express our gratitude towards this institution. We thank Anil Nerode and Paul Shafer for their valuable advice. We also thank the anonymous referees for the helpful suggestions. Opinions expressed in this paper do not necessarily reflect those of the John Templeton Foundation.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Sanders, S. (2020). Lifting Recursive Counterexamples to Higher-Order Arithmetic. In: Artemov, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2020. Lecture Notes in Computer Science(), vol 11972. Springer, Cham. https://doi.org/10.1007/978-3-030-36755-8_16
Download citation
DOI: https://doi.org/10.1007/978-3-030-36755-8_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-36754-1
Online ISBN: 978-3-030-36755-8
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)