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.
展开▼
