Reverse Mathematics and Computability Theory of Domain Theory

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.

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-free⁴ 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$:

$$\begin{aligned} (\forall x^{\sigma })(\exists y^{\tau })A(x, y)\rightarrow (\exists Y^{\sigma \rightarrow \tau })(\forall x^{\sigma })A(x, Y(x)),\qquad \qquad \; ({\mathsf{QF}\text {-}\mathsf{AC}}^{\sigma ,\tau }) \end{aligned}$$

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:

$$\begin{aligned} \textstyle (\forall k\in {\mathbb {N}})(\exists d\in D)(|x-x_{d}|<\frac{1}{2^{k}}), \end{aligned}$$

(A.2)

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

$$ (\forall n\in {\mathbb {N}})(\exists m\in {\mathbb {N}})\big [ f(\overline{g}n)>0 \rightarrow f(\overline{h}m)\ge f(\overline{g}n) \big ], $$

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$