General synthetic domain theory – a logical approach

Synthetic domain theory (SDT) is a version of Domain Theory where ‘all functions are continuous’. Following the original suggestion of Dana Scott, several approaches to SDT have been developed that are logical or categorical, axiomatic or model-oriented in character and that are either specialised towards Scott domains or aim at providing a general theory axiomatising the structure common to the various notions of domains studied so far.In Reus and Streicher (1993), Reus (1995) and Reus (1998), we have developed a logical and axiomatic version of SDT, which is special in the sense that it captures the essence of Domain Theory à la Scott but rules out, for example, Stable Domain Theory, as it requires order on function spaces to be pointwise. In this article we will give a logical and axiomatic account of a general SDT with the aim of grasping the structure common to all notions of domains.As in loc.cit., 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 (such as, for example, complete and well-complete S-spaces (Longley and Simpson 1997)), define the appropriate notion of domain and verify the usual induction principles of domain theory.Although each domain carries a logically definable ‘specialization order’, we avoid order-theoretic notions as much as possible in the formulation of axioms and theorems. The reason is that the order on function spaces cannot be required to be pointwise, as this would rule out the model of stable domains à la Berry.The consequent use of logical language – understood as the internal language of some categorical model of type theory – avoids the irritating coexistence of the internal and the external view pervading purely categorical approaches. Therefore, the paper is aimed at providing an elementary introduction to synthetic domain theory, albeit requiring some knowledge of basic type theory.