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.
Denotational semantics of recursive types in synthetic guarded domain theory