Reverse Mathematics and computability theory of domain theory

Sam Sanders, University of Leeds. Part of the Logic Seminar Series.

This talk deals with the foundations of mathematics and computer science and with the following questions in particular:

(Q1) As part of the program Reverse Mathematics, which axioms are needed to prove basic results in domain theory?

(Q2) How hard it is to compute, in the sense of Kleene's S1-S9, the objects in basic results in domain theory?

Now, domain theory is formulated using the fundamental notion of nets (aka Moore-Smith sequences), which yields intuitive definitions of the associated Scott and Lawson topologies, among others.  Regarding (Q1), we study the monotone convergence theorem for nets, which is implicit in the definition of Scott domain.  Even for the basic case of nets in the unit interval and indexed by Baire space, this theorem is extremely hard to prove, relative to the usual hierarchy of comprehension axioms, namely requiring full second-order arithmetic.  Regarding (Q2), it turns out that the limit in the monotone convergence theorem is also extremely hard to compute, but we moreover show that more general index sets (definable in the finite type hierarchy) yield a hierarchy including n-th order arithmetic for any n.  Finally, we show that using nets rather than sequences obviates the use of the the Axiom of Choice, a foundational concern in domain theory.