On Applications of Forcing in Domain Theory

Question

An interesting feature of domain theory is to use partial orders in order to provide a mathematical model for the computational approximation in a potentially infinite computational process (e.g. computing all digits of $\pi$) that lies beyond the power of our finite-resource computers.

Roughly speaking, from a domain-theoretic perspective, the pieces of information in a computational process form a partial order. Under certain conditions, an infinite set of compatible pieces of partial information may converge to the ultimate answer beyond the computer's computational power.

So the computer will never know the final answer (e.g. all digits of $\pi$) but it deals with its approximations. For instance, at a certain point it finds out that $\pi\in I=[3.14, 3.15]$ and after a few more steps of computing it comes up with the fact that $\pi\in J=[3.141, 3.142]$. So the interval $J$ can be viewed as a piece of information that extends its predecessor $I$ via inverse inclusion order, $J\subseteq I$.

This approach may sound quite familiar to the set theorists as it reminds the way they deal with conditions in a forcing notion. The ultimate object is the generic filter (and whatever made out of it) which lives in the forcing extension but not in the ground model. However, people living in the ground model have a degree of access to such a "transcendental" object through its approximations that exist in their world.

Based on the presented analogy, one may expect forcing and domain theory to share some similar concepts and techniques. But my search didn't reveal that much along these lines, except a master thesis of Håkon Briseid (under the supervision of Dag Normann), titled "Generic Functions in Scott Domains". Its abstract reads as:

In this thesis we will apply forcing to domain theory. When a Scott domain represents a function space, each function will be a filter in the basis of the domain. By using partially ordered basis as the forcing relation, each generic filter $G$ yields a model of $ZFC$ in which $G$ is a function, given some other model of $ZFC$ containing this basis. Such generic functions are the main concern of this thesis. ...

My question is about the existence of possibly deeper connections between these two branches of mathematical logic.

Question. What are other examples of papers and theses relating set theory and domain theory through applying forcing in domain theoretic theorems and constructions?

Answer 1

It may not be well known outside domain theory that there are several different groups who work in domain theory for different reasons. People interested in domains as modeling partial information in computations are often computer scientists, and they may not be particularly interested in the maximal elements of the domain, which will contain infinitely much info. Their interest is often specifically in the partial elements, although the dcpo aspect of domains guarantees there will be maximal elements.

People interested in the topology of the set of maximal elements of a domain are often topologists who are interested in the space of all maximal elements. Neither of these groups, in my experience, seems to be especially interested in generic maximal elements.

There have been some applications of set-theoretic games and determinacy in domain theory, however. The first paper on those lines was Keye Martin, "Topological Games in Domain Theory", Topology and Its Applications, 2003. (MR1961398) Martin showed that the space of maximal points of a domain, among other things, has the strong Choquet completeness property. The problem of characterizing the spaces that are domain representable is still open in the general case, as are various questions about special kinds of winning strategies in the Choquet game. One recent paper along these lines is by Fleissner and Yengulalp, "From subcompact to domain representable", Topology and its Applications, 2015. (MR3414883)

Answer 2

Note that forcing techniques are frequently used in computability theory, e.g., to establish the existence of degrees with certain properties. I refer the reader to Odifreddi's Handbook of Computability Theory Volume 2 chapter XII or his paper series "Forcing and Reducibilities" parts 1 and 2 (part 3 is mostly about set theory) . Or simply search for "1-generic Turing degrees." This has also been used in complexity theory to build sets/languages with certain complexity theoretic properties.

Some of these uses could be formalized in domain theory but that, as the other answer points out, the reasons for using domain theory rather than just working more informally as one does in computability theory have to do with the intended applications and most of the applications domain theory is used for are less concerned with the kind of properties of the infinite object one could prove using forcing methods.

In particular, forcing arguments can be thought of as applications of (a version of) the Baire Category Theorem. The space F of maximal compatible sets of forcing conditions can be thought of as a topological space with the basic open sets given by the conditions which (on reasonable assumptions) is a Baire space letting us infer that there is an element G of F meeting any countable collection of dense sets of conditions. If we need G to be definable/computable in some fashion we restrict our attention to sufficiently definable dense sets of conditions. In either case what we demonstrate is that it's possible to build an infinitary object that meets some countable collection of conditions when we already know we can meet any finite collection of those conditions. As such a forcing argument is necessarily about establishing some infinitary property of G and not the usual concerns about domain theory involving reasoning about the correctness of the program.

For instance, I'm sure one could recast the trivial forcing argument building a language outside of $P$ (force with finite partial functions and considering dense sets that are $P$-time decidable) as an argument in domain theory if one viewed a chain through the partial order from domain theory as determining the language but I just don't see why one would want to bother with the domain theory part.