Axioms and (counter)examples in synthetic domain theory

Jaap van Oosten, Alex Simpson

Research output: Contribution to journalArticlepeer-review

Abstract

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.
Original languageUndefined/Unknown
Pages (from-to)233 - 278
Number of pages46
JournalAnnals of Pure and Applied Logic
Volume104
Issue number1?3
DOIs
Publication statusPublished - 2000

Keywords

  • Realizability

Cite this