Abstract
This paper deals with the foundations of mathematics and computer science, domain theory in particular; the latter studies certain ordered sets, called domains, with close relations to topology. Conceptually speaking, domain theory provides a highly abstract and general formalisation of the intuitive notions ‘approximation’ and ‘convergence’. Thus, a major application in computer science is the semantics of programming languages. We study the following foundational questions:
-
(Q1)
Which axioms are needed to prove basic results in domain theory?
-
(Q2)
How hard it is to compute the objects in these basic results?
Clearly, (Q1) is part of the program Reverse Mathematics, while (Q2) is part of computability theory in the sense of Kleene. Our main result is that even very basic theorems in domain theory are extremely hard to prove, while the objects in these theorems are similarly extremely hard to compute; this hardness is measured relative to the usual hierarchy of comprehension axioms, namely one requires full second-order arithmetic in each case. By contrast, we show that the formalism of domain theory obviates the need for the Axiom of Choice, a foundational concern.
This research was supported by the John Templeton Foundation grant a new dawn of intuitionism with ID 60842. Opinions expressed in this paper do not necessarily reflect those of the John Templeton Foundation. See also Remark 4.7 below.
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.
By [27, Prop. 3.6], \({{\mathsf{RCA}}_{0}^{\omega }}\) can prove the global equivalence of sequential continuity and epsilon-delta continuity on Baire space, i.e. when those continuity properties hold everywhere on the latter.
- 2.
Simpson mentions in [52] the caveat that e.g. \({\textsf {PRA}}\) and \({\textsf {WKL}}_{0}\) have the same first-order strength, but the latter is strictly stronger than the former.
- 3.
There are some examples of theorems (predating \({\mathsf{HBU}}\) and [41]) that fall outside of the Gödel hierarchy based on inclusion, like special cases of Ramsey’s theorem and the axiom of determinacy from set theory [22, 32]. These are far less natural than e.g. Heine-Borel compactness, in our opinion.
- 4.
To be absolutely clear, variables (of any finite type) are allowed in quantifier-free formulas of the language \({\textsf {\text {L}}}_{\omega }\): only quantifiers are banned.
References
Abramsky, S., Jung, A.: Domain Theory. Handbook of Logic in Computer Science, vol. 3, pp. 1–168. Oxford University Press (1994)
Avigad, J., Feferman, S.: Gödel’s Functional (“Dialectica”) Interpretation. 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. Monthly 62, 551–557 (1955)
Benacerraf, P., Putnam, H.: Philosophy of Mathematics: Selected Readings, 2nd edn. Cambridge University Press, Cambridge (1984)
Bernays, P.: Sur le Platonisme Dans les Mathé matiques. L’Enseignement Mathématique 34, 52–69 (1935)
Bourbaki, N.: Elements of Mathematics. General Topology. Part 2. Addison-Wesley, Boston (1966)
Brown, A., Pearcy, C.: An Introduction to Analysis. Graduate Texts in Mathematics, vol. 154. Springer, Heidelberg (1995). https://doi.org/10.1007/978-1-4612-0787-0
Burgess, J.P.: Fixing Frege. Princeton Monographs in Philosophy. Princeton University Press, Princeton (2005)
Cousin, P.: Sur les fonctions de n variables complexes. Acta Math. 19, 1–61 (1895)
Dorais, F.G.: Classical consequences of continuous choice principles from intuitionistic analysis. Notre Dame J. Form. Log. 55(1), 25–39 (2014)
Dorais, F.G., Dzhafarov, D.D., Hirst, J.L., Mileti, J.R., Shafer, P.: On uniform relationships between combinatorial problems. Trans. Am. Math. Soc. 368(2), 1321–1359 (2016)
Felgner, U.: Models of ZF-Set Theory. LNM, vol. 223. Springer, Heidelberg (1971). https://doi.org/10.1007/BFb0061160
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.: Interpretations, According to Tarski. Interpretations of Set Theory in Discrete Mathematics and Informal Thinking, The Nineteenth Annual Tarski Lectures, vol. 1, p. 42 (2007). http://u.osu.edu/friedman.8/files/2014/01/Tarski1052407-13do0b2.pdf
Fujiwara, M., Yokoyama, K.: A note on the sequential version of \({\varPi ^1_2}\) statements. In: Bonizzoni, P., Brattka, V., Löwe, B. (eds.) CiE 2013. LNCS, vol. 7921, pp. 171–180. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39053-1_20
Fujiwara, M., Higuchi, K., Kihara, T.: On the strength of marriage theorems and uniformity. MLQ Math. Log. Q. 60(3), 136–153 (2014)
Gandy, R.: General recursive functionals of finite type and hierarchies of functions. Ann. Fac. Sci. Univ. Clermont-Ferrand 35, 5–24 (1967)
Gierz, G., Hofmann, K.H., Keimel, K., Lawson, J.D., Mislove, M., Scott, D.S.: A Compendium of Continuous Lattices. Springer, Heidelberg (1980). https://doi.org/10.1007/978-3-642-67678-9
Gierz, G., Hofmann, K.H., Keimel, K., Lawson, J.D., Mislove, M., Scott, D.S.: Continuous Lattices and Domains. Encyclopedia of Mathematics and its Applications, vol. 93. Cambridge University Press (2003)
Goubault-Larrecq, J.: Non-Hausdorff Topology and Domain Theory. New Mathematical Monographs, vol. 22. Cambridge University Press, Cambridge (2013)
Hirschfeldt, D.R.: Slicing the Truth. Lecture Notes Series, Institute for Mathematical Sciences, National University of Singapore, vol. 28. World Scientific Publishing (2015)
Hirst, J.L., Mummert, C.: Reverse mathematics and uniformity in proofs without excluded middle. Notre Dame J. Form. Log. 52(2), 149–162 (2011)
Hunter, J.: Higher-Order Reverse Topology. ProQuest LLC, Ann Arbor, MI, Thesis (Ph.D.)–The University of Wisconsin - Madison (2008)
Kelley, J.L.: General Topology. Springer, Heidelberg (1975). Reprint of the 1955 edition, Graduate Texts in Mathematics, No. 27
Koellner, P.: Large Cardinals and Determinacy. The Stanford Encyclopedia of Philosophy (2014). https://plato.stanford.edu/archives/spr2014/entries/large-cardinals-determinacy/
Kohlenbach, U.: Higher order reverse mathematics. Reverse Mathematics (2001). Lect. Notes Log., vol. 21, ASL, 2005, pp. 281–295
Kreuzer, A.P.: Primitive recursion and the chain antichain principle. Notre Dame J. Form. Log. 53(2), 245–265 (2012)
Li, G., Ru, J., Wu, G.: Rudin’s lemma and reverse mathematics. Ann. Jpn. Assoc. Philos. Sci. 25, 57–66 (2017)
Longley, J., Normann, D.: Higher-Order Computability. Theory and Applications of Computability. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-47992-6
Medvedev, F.A.: Scenes from the History of Real Functions. Science Networks. Historical Studies, vol. 7. Birkhœuser Verlag, Basel (1991)
Montalbán, A., Shore, R.A.: The limits of determinacy in second order arithmetic. Proc. Lond. Math. Soc. (3) 104(2), 223–252 (2012)
Moore, E.H.: Definition of limit in general integral analysis. Proc. Natl. Acad. Sci. U.S.A 1(12), 628–632 (1915)
Moore, E., Smith, H.: A general theory of limits. Am. J. Math. 44, 102–121 (1922)
Moore, E.: General Analysis. Part I. The Algebra of Matrices, vol. 1. Memoirs of the American Philosophical Society, Philadelphia (1935)
Muldowney, P.: A General Theory of Integration in Function Spaces, Including Wiener and Feynman Integration, vol. 153. Longman Scientific & Technical, Harlow, Wiley (1987)
Mummert, C., Simpson, S.G.: Reverse mathematics and \({\varPi ^1_2}\) comprehension. Bull. Symb. Log. 11(4), 526–533 (2005)
Mummert, C.: On the Reverse Mathematics of General Topology. ProQuest LLC, Ann Arbor, MI, Thesis (Ph.D.)–The Pennsylvania State University (2005)
Mummert, C.: Reverse mathematics of MF spaces. J. Math. Log. 6(2), 203–232 (2006)
Mummert, C., Stephan, F.: Topological aspects of poset spaces. Michigan Math. J. 59(1), 3–24 (2010)
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 (2018, submitted). arXiv: https://arxiv.org/abs/1808.09783
Normann, D., Sanders, S.: Representations in measure theory (2019). arXiv: https://arxiv.org/abs/1902.02756
Pu, P.M., Liu, Y.M.: Fuzzy topology. I. Neighborhood structure of a fuzzy point and Moore-Smith convergence. J. Math. Anal. Appl. 76(2), 571–599 (1980)
Sacks, G.E.: Higher Recursion Theory. Perspectives in Mathematical Logic. Springer, Heidelberg (1990)
Sakamoto, N., Yamazaki, T.: Uniform versions of some axioms of second order arithmetic. MLQ Math. Log. Q. 50(6), 587–593 (2004)
Sanders, S.: Reverse Mathematics of topology: dimension, paracompactness, and splittings, p. 17 (2018). arXiv: https://arxiv.org/abs/1808.08785
Sanders, S.: Nets and Reverse Mathematics: Initial Results. Proceedings of CiE19. LNCS, p. 12. Springer, Heidelberg (2019, to appear)
Sanders, S.: Splittings and disjunctions in Reverse Mathematics. Notre Dame J. Formal Log. 18 (2019, to appear). arXiv: https://arxiv.org/abs/1805.11342
Simpson, S.G. (ed.): Reverse Mathematics (2001). Lecture Notes in Logic, vol. 21, ASL, La Jolla, CA (2005)
Simpson, S.G. (ed.): Subsystems of Second Order Arithmetic, 2nd edn. Perspectives in Logic, CUP (2009)
Simpson, S.G. (ed.): The Gödel hierarchy and reverse mathematics., Kurt Gödel. Essays for his centennial, pp. 109–127 (2010)
Stillwell, J.: Reverse Mathematics, Proofs from the Inside Out. Princeton University Press, Princeton (2018)
Swartz, C.: Introduction to Gauge Integrals. World Scientific (2001)
Turing, A.: On computable numbers, with an application to the Entscheidungs-problem. Proc. Lond. Mat. Soc. 42, 230–265 (1936)
Vietoris, L.: Stetige mengen. Monatsh. Math. Phys. 31(1), 173–204 (1921). (German)
Wang, H.: Eighty years of foundational studies. Dialectica 12, 466–497 (1958)
Zadeh, L.A.: Fuzzy sets. Inf. Control 8, 338–353 (1965)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
A Technical Appendix
A Technical Appendix
We provide the full definition of the system \({{\mathsf{RCA}}_{0}^{\omega }}\) in Sect. A.1, while we list some proofs in Sect. A.2.
1.1 A.1 The Base Theory of Higher-Order Reverse Mathematics
We list all the axioms of the base theory \({{\mathsf{RCA}}_{0}^{\omega }}\), first introduced in [27, §2].
Definition A.1
The base theory \({{\mathsf{RCA}}_{0}^{\omega }}\) consists of the following axioms.
-
(a)
Basic axioms expressing that \(0, 1, <_{0}, +_{0}, \times _{0}\) form an ordered semi-ring with equality \(=_{0}\).
-
(b)
Basic axioms defining the well-known \(\varPi \) and \(\varSigma \) combinators (aka K and S in [2]), which allow for the definition of \(\lambda \)-abstraction.
-
(c)
The defining axiom of the recursor constant \(\mathbf {R}_{0}\): For \(m^{0}\) and \(f^{1}\):
$$\begin{aligned} \mathbf {R}_{0}(f, m, 0):= m \text { and } \mathbf {R}_{0}(f, m, n+1):= f(n, \mathbf {R}_{0}(f, m, n)). \end{aligned}$$(A.1) -
(d)
The axiom of extensionality: for all \(\rho , \tau \in \mathbf {T}\), we have:
$$\begin{aligned} (\forall x^{\rho },y^{\rho }, \varphi ^{\rho \rightarrow \tau }) \big [x=_{\rho } y \rightarrow \varphi (x)=_{\tau }\varphi (y) \big ]. \qquad \qquad \quad (\textsf {\text {E}}_{\rho , \tau }) \end{aligned}$$ -
(e)
The induction axiom for quantifier-freeFootnote 4 formulas of \({\textsf {\text {L}}}_{\omega }\).
-
(f)
\({\mathsf{QF}\text {-}\mathsf{AC}}^{1,0}\): The quantifier-free Axiom of Choice as in Definition A.2.
Definition A.2
The axiom \({\mathsf{QF}\text {-}\mathsf{AC}}\) consists of the following for all \(\sigma , \tau \in \mathbf T \):
for any quantifier-free formula A in the language of \({\textsf {\text {L}}}_{\omega }\).
For completeness, we list the following notational convention on finite sequences.
Notation A.3
(Finite sequences). We assume a dedicated type for ‘finite sequences of objects of type \(\rho \)’, namely \(\rho ^{*}\). Since the usual coding of pairs of numbers goes through in \({{\mathsf{RCA}}_{0}^{\omega }}\), we shall not always distinguish between 0 and \(0^{*}\). Similarly, we do not always distinguish between ‘\(s^{\rho }\)’ and ‘\(\langle s^{\rho }\rangle \)’, where the former is ‘the object s of type \(\rho \)’, and the latter is ‘the sequence of type \(\rho ^{*}\) with only element \(s^{\rho }\)’. The empty sequence for the type \(\rho ^{*}\) is denoted by ‘\(\langle \rangle _{\rho }\)’, usually with the typing omitted.
Furthermore, we denote by ‘\(|s|=n\)’ the length of the finite sequence \(s^{\rho ^{*}}=\langle s_{0}^{\rho },s_{1}^{\rho },\dots ,s_{n-1}^{\rho }\rangle \), where \(|\langle \rangle |=0\), i.e. the empty sequence has length zero. For sequences \(s^{\rho ^{*}}, t^{\rho ^{*}}\), we denote by ‘\(s*t\)’ the concatenation of s and t, i.e. \((s*t)(i)=s(i)\) for \(i<|s|\) and \((s*t)(j)=t(|s|-j)\) for \(|s|\le j< |s|+|t|\). For a sequence \(s^{\rho ^{*}}\), we define \(\overline{s}N:=\langle s(0), s(1), \dots , s(N-1)\rangle \) for \(N^{0}<|s|\). For a sequence \(\alpha ^{0\rightarrow \rho }\), we also write \(\overline{\alpha }N=\langle \alpha (0), \alpha (1),\dots , \alpha (N-1)\rangle \) for any \(N^{0}\). By way of shorthand, \((\forall q^{\rho }\in Q^{\rho ^{*}})A(q)\) abbreviates \((\forall i^{0}<|Q|)A(Q(i))\), which is (equivalent to) quantifier-free if A is.
1.2 A.2 Some Proofs
We provide the proofs of some of the above theorems. First of all, the proof of Corollary 3.7 is as follows.
Proof
We only need to prove the reverse implication. To this end, let \(x_{d}:D\rightarrow I\) be an increasing net converging to some \(x\in I\). This convergence trivially implies:
and applying \({\mathsf{QF}\text {-}\mathsf{AC}}^{0, 1}\) to (A.2) yields \(\varPhi :{\mathbb {N}}\rightarrow D\) such that the sequence \(\lambda k^{0}.x_{\varPhi (k)}\) also converges to x as \(k\rightarrow \infty \). Since \({\mathsf{ADS}}\) is equivalent to the statement that a sequence in \({\mathbb {R}}\) has a monotone sub-sequence [28, §3], \({\mathsf{SUB}}_{0}\) follows. \(\square \)
Secondly, the proof of Theorem 4.2 is as follows.
Proof
For the ‘vice versa’ direction, one uses the usual ‘interval halving technique’ where \(\exists ^{4}\) is used to decide whether there is \(e\in E\) such that \(x_{e}\) is in the relevant interval. For the other direction, fix \(F^{3}\), let E be \({\mathbb {N}}^{{\mathbb {N}}}\rightarrow {\mathbb {N}}\) itself, and define ‘\(X\preceq Y \)’ by \(F(X)\ge _{0} F(Y)\) for any \(X^{2}, Y^{2}\). It is easy to show that \((E, \preceq )\) is a directed set. Define the net \(x_{e}:E \rightarrow I\) by 0 if \(F(e)>0\), and 1 if \(F(e)=0\), which is increasing by definition. Hence, \(x_{e}\) converges, say to \(y_{0}\in I\), and if \(y_{0}>2/3\), then there must be \(Y^{2}\) such that \(F(Y)=0\), while if \(y_{0}<1/3\), then \((\forall Y^{2})(F(Y)>0)\). Clearly, this yields a term of Gödel’s T computing \(\exists ^{3}\). \(\square \)
Thirdly, we provide the proof of Theorem 4.3.
Proof
For the ‘vice versa’ direction, one uses the usual ‘interval halving technique’ where \({\mathsf{S}}^{2}\) is used to decide whether there is \(d\in D\) such that \(x_{d}\) is in the relevant interval. For the other direction, fix \(f^{1}\), let D be Baire space, and define ‘\(h\preceq g\)’ by the following arithmetical formula
for any \(h, g\in D\). It is easy to show that \((D, \preceq )\) is a directed set. Define the net \(x_{g}:D \rightarrow I\) by 0 if \((\exists n^{0})(f(\overline{g}n)>0)\), and 1 if otherwise, which is arithmetical and increasing. Hence, \(x_{d}\) converges, say to \(y_{0}\in I\), and if \(y_{0}>2/3\), then there is \(g^{1}\) such that \((\forall n^{0})(f(\overline{g}n)=0)\), while if \(y_{0}<1/3\), then \((\forall g^{1})(\exists n^{0})(f(\overline{g}n)>0)\). Clearly, this provides a term of Gödel’s T computing \({\mathsf{S}}^{2}\). \(\square \)
Fourth, we provide the proof of Corollary 4.4
Proof
Let \((\forall f^{1})\varphi (f, F^{2}, e^{0})\) be the formula expressing that the e-th algorithm with input \(F^{2}\) terminates, i.e. \(\varphi (f, F, e)\) is arithmetical with type two parameters. Let D be Baire space and define ‘\(f\preceq _{D} g\)’ by \(\varphi (f, F,e )\rightarrow \varphi (g, F, e)\), which readily yields a directed set. The net \(x_{d}:D\rightarrow {\mathbb {R}}\) is defined as follows: \(x_{f}\) is 0 if \(\varphi (f, F, e)\), and 1 otherwise. This net is increasing and \({\mathsf{MCT}}_{{\mathsf{net}}}^{\mathbb {S}}\) yields a limit \(y_{0}\in I\); if \(y_{0}>1/3\), then \(\{e\}(F)\) does not terminate, and if \(y<2/3\), then \(\{e\}(F)\) terminates. \(\square \)
Rights and permissions
Copyright information
© 2019 Springer-Verlag GmbH Germany, part of Springer Nature
About this paper
Cite this paper
Sanders, S. (2019). Reverse Mathematics and Computability Theory of Domain Theory. In: Iemhoff, R., Moortgat, M., de Queiroz, R. (eds) Logic, Language, Information, and Computation. WoLLIC 2019. Lecture Notes in Computer Science(), vol 11541. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-59533-6_33
Download citation
DOI: https://doi.org/10.1007/978-3-662-59533-6_33
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-59532-9
Online ISBN: 978-3-662-59533-6
eBook Packages: Computer ScienceComputer Science (R0)