General Synthetic Domain Theory - A Logical Approach.

Synthetic Domain Theory (SDT) is a version of Domain Theory where "all functions are continuous". In [14, 12] there has been developed a logical and axiomatic version of SDT which is special in the sense that it captures the essence of Domain Theory `a la Scott but rules out other important notions of domain. In this article we will give a logical and axiomatic account of General Synthetic Domain Theory (GSDT) aiming to grasp the structure common to all notions of domain as advocated by various authors. As in [14, 12] the underlying logic is a sufficiently expressive version of constructive type theory. We start with a few basic axioms giving rise to a core theory on top of which we study various notions of predomains as well-complete and replete S-spaces [9], define the appropriate notion of domain and verify the usual induction principles.