Apartness, sharp elements, and the Scott topology of domains

摘要

Working constructively, we study continuous directed complete posets (dcpos) and the Scott topology.Our two primary novelties are a notion of intrinsic apartness and a notion of sharp elements. Beingapart is a positive formulation of being unequal, similar to how inhabitedness is a positive formulationof nonemptiness. To exemplify sharpness, we note that a lower real is sharp if and only if it is located. Ourfirst main result is that for a large class of continuous dcpos, the Bridges–V??tˇa apartness topology and theScott topology coincide. Although we cannot expect a tight or cotransitive apartness on nontrivial dcpos,we prove that the intrinsic apartness is both tight and cotransitive when restricted to the sharp elements ofa continuous dcpo. These include the stronglymaximal elements, as studied by Smyth and Heckmann. Wedevelop the theory of strongly maximal elements highlighting its connection to sharpness and the Lawsontopology. Finally, we illustrate the intrinsic apartness, sharpness, and strong maximality by consideringseveral natural examples of continuous dcpos: the Cantor and Baire domains, the partial Dedekind reals,the lower reals and, finally, an embedding of Cantor space into an exponential of lifted sets.