Axioms and (counter)examples in synthetic domain theory Original Research Article

An axiomatic treatment of synthetic domain theory is presented, in the framework of the internal logic of an arbitrary topos. We present new proofs of known facts, new equivalences between our axioms and known principles, and proofs of new facts, such as the theorem that the regular complete objects are closed under lifting (and hence well-complete). In Sections 2–4 we investigate models, and obtain independence results. In Section 2 we look at a model in de Modified realizability Topos, where the Scott Principle fails, and the complete objects are not closed under lifting. Section 3 treats the standard model in the Effective Topos. Theorem 3.2 gives a new characterization of the initial lift-algebra relative to the dominance. We prove that in the standard case it is not the internal colimit of the chain 0→L(0)→L2(0)→⋯ . The models in Sections 2 and 3 compare via an adjunction. Section 4 discusses a model in a Grothendieck topos. A feature here is that N is not well-complete (where N is the natural numbers object), whereas 2 is.