The Synthetic Plotkin Powerdomain

Wesley Phoa Paul Taylor

1990

Abstract
Plotkin [1976] introduced a powerdomain construction on domains in order to give
semantics to a non-deterministic binary choice constructor, and later [1979] characterised
it as the free semilattice. Smyth [1983] and Winskel [1985] showed that it could be
interpreted in terms of modal predicate transformers and Robinson [1986] recognised it
as a special case of Johnstones [1982] Vietoris construction, which itself generalises the
Hausdorff metric on the set of closed subsets of a metric space. The domain construction
involves a curious order relation known as the Egli-Milner order.
In this paper we relate the powerdomain directly to the free semilattice, which in a
topos is simply the finite powerset, i.e. the object of (Kuratowski-)finite subobjects of an
object. We show that the Egli-Milner order coincides (up to ) with the intrinsic
order induced by a family of observable predicates.
This problem originally arose in the context of the Effective topos, in which the observ-
able predicates are the recursively enumerable subsets. However we find that the results
of this paper hold for any elementary topos, and so by considering a (pre)sheaf topos
(which the Effective topos is not) we may compare them with the classical approach.

Important Note: Much of the credit for the work in this paper is due to Wesley
Phoa and Martin Hyland, but I take the blame for its presentation. Comments on it are
most welcome. When it is finished it will be submitted as a joint paper with Wesley Phoa,
and an announcement will be made on types.

1 Introduction
1.1 The Plotkin powerdomain
Plotkin [1976] introduced his powerdomain construction in order to extend denotational se-
mantics in the Scott style to languages involving a binary choice, or. The behaviour of a
program in such a language may be that:

it always diverges;

it always terminates, and with the same output value;

it always terminates, but there are several (but finitely many) possible output values;

it sometimes converges and sometimes diverges;

and so to express its denotation we must consider the set of possible outputs. Divergence
must be mentioned explicitly as a value if it occurs in order to distinguish the third and
fourth cases. The set must be nonempty since there must be some behaviour divergence

1
if nothing else. Incidentally, by Konigs lemma, if there are infinitely many possible output
values, then divergence must also be possible.
By analogy with the powerset, X , one might suppose that the powerdomain would be
of the form T X for some truthvalues domain T . There are two objections to this: First,
the class of admissible subobjects would then be closed under inverse images, so including
infinite subobjects. Second, the subobjects themselves would be upwards-closed (on the
reasonable assumption that the generic such set is a maximal element of T ), but we want {}
to be admissible.
The central theme of denotational semantics is that each program constructor should
correspond to an algebraic operation in the domain. In particular since or is a conjunction of
nondeterministic behaviours, it must correspond to a binary operation d on the domain. In the
natural understanding, this must be commutative, associative, idempotent and computable,
so the nondeterministic domain must be a semilattice (A, d) in the category of domains.
Moreover since every deterministic program is nondeterministic in a trivial way, there is an
inclusion of the deterministic domain X into the nondeterministic one. Indeed Hennessy and
Plotkin [1979] argued that (A, d) has to be the free semilattice on X.
There is another approach to semantics, which is axiomatic: we argue about the properties
of programs. We have already informally said that a program may or must diverge: these
are modalities on propositions concerning its actual behaviours in any particular run. Smyth
[1983] showed how a program p (in particular a non-deterministic one) can be interpreted
as a predicate transformer from post-conditions to the weakest corresponding pre-condition.
Winskel [1985] characterised the powerdomain in terms of the properties it could express in
a logic which includes these transformers [p] and hpi as unary operators. Robinson [1986]
did something slightly different: he treated the modal predicates  and as abstract
symbols and showed that they generate the topology (i.e. the lattice of properties) on the
powerdomain A as ranges over the open sets of the base domain X. In fact the point of
Robinsons paper was to show that the powerdomain is a special case of Johnstones [1982]
Vietoris monad, which had already been generalised from a construction on metric spaces due
originally to Hausdorff.
These axiomatic and topological approaches are very significant in the literature, but for
two reasons we have not attempted to make use of them in this paper. First, Johnstone
showed that the Vietoris construction and the free semilattice agree only in special cases
(admittedly including all those of interest in classical domain theory), and our problem is
likely to be as difficult as his. Secondly, the analogy with topology is not strict (in particular
we do not assume all joins), so it is not yet clear what a -frame should be.

1.2 Synthetic domain theory

(To be written)

1.3 The synthetic Plotkin powerdomain

Throughout we shall use the word set to mean an object of a given elementary topos, E.
We suppose that we have a category C of predomains which is a full reflective subcategory of
the category of sets. Then

arbitrary limits of predomains exist (which is not true of most of the classical categories
of domains) and are constructed set-theoretically

2
 we may perform some type construction with sets (for instance, in our case the Plotkin
powerdomain is the free semilattice) and turn the result into a predomain.

Definition 1.1 A semilattice is a set A E together with a (global) element } A and a

binary operation d : A A A which is
idempotent: a d a = a,
commutative: a d b = b d a,
associative: a d (b d c) = (a d b) d c, and
} is the unit: a d } = a = } d a.
We shall find that } is an inessential part of the structure, so we define a binary semilattice
to be an algebra (A, d) without the unit.
It is easy to see that
def
a b b a d b = b
defines a partial order (reflexive, transitive antisymmetric relation), and in fact d is the join
for this. However it is important not to consider (A, d) as specifically a join-semilattice (or as
a meet-semilattice), because b is not what we shall mean by the intrinsic order on
the set A (see section 2): it is intrinsic to the semilattice, not to the set.
The definition of a semilattice can be expressed in any category with finite products, so
we write SL() for the category of semilattices in any such. Then we have forgetful functors
V - C
SL(C)
..
..6
..
..
U T ... a U
..
K ..
.
?  ................................ ?
SL(E) - E
V
two of which (we shall show) have left adjoints (indicated by dotted arrows). From K and T ,
it is a simple categorical argument to derive the other two adjoints.

Proposition 1.2 The left adjoint to SL(C) SL(E) is given by the reflector T : E C.
Proof Explicitly, if (A, d) is a (binary) semilattice, then the free C-semilattice on it is
(T A, T d). To make this meaningful we need

TA TA
= T (A A)
i.e. T preserves finite products: itself is unambiguous because products in a reflective sub-
category are always calculated as in the larger category. By functoriality this is a C-semilattice.
If f : (A, d) (B, d0 ) is a homomorphism into a C-semilattice then the underlying map has
a lifting f : T A B and this is a homomorphism because d0 (f f) and f T d both serve
as the unique lifting of d0 (f f ) = f T d, again using the fact that T preserves binary
products. The argument for the unit, }, is similar, using the terminal object. 

Theorem 1.3 The left adjoint to SL(C) C is given by T K U .

3
Proof Let X C and (A, d) SL(C). We have to show a natural bijection between maps
f : X A and homomorphisms T (K(X), ) (A, d); it doesnt matter whether we work in
C or E because the former is a full subcategory of the latter. But T K a V U . 
So in order to construct the synthetic Plotkin powerdomain it suffices

to define our categories of sets and domains, and show that the latter is a full reflective
subcategory of the former and that the reflector preserves finite products,

to show that the finite powerset affords the free semilattice in the category of sets.

These two topics will be the subject of sections 2 and 3 respectively.

This abstract nonsense, however, tells us little about the concrete structure of the power-
domain, and the main purpose of the paper is to show that the Egli-Milner order is (almost)
the intrinsic order relation on it. In other words, the synthetic construction is the same as
the concrete one. Section 4 shows one implication, and with the help of modal operators
(section 5) we prove a weak form of the converse in section 6.

2 The intrinsic order

As usual, we use to denote the object of truth values in E, and we shall also assume given
a sublattice whose elements we shall think of as computable predicates. In section 6
we shall need to assume that these predicates are -closed, i.e. .
If we look at a parametric case it will become more reasonable to the intuition why is a
very complex object, much larger than the set 2 = {true, false} of decidable truthvalues or
even than a typical choice of . A map : N is a predicate (n) on natural numbers, and
as such it may perhaps be primitive recursive, recursively decidable, recursively enumerable,
02 or worse. In fact the parameter is irrelevant and so using the Kleene bracket notation we
can define
= { : n.({n}(0) )}
the object of recursively enumerable predicates.
Although this is the intended application, it is easier to grasp the intuition if you think of
open instead of computable predicates. For this purpose the reader is invited to apply the
op
following definitions to the topos SetC where C is the category of countably based algebraic
lattices and Scott-continuous maps and is (the representable functor on) the two-point
lattice. In this case a sieve (i.e. a subobject of a representable) is generated by the inclusion
of an open set iff its characteristic function factors through .
Given , we can define the intrinsic order:

Definition 2.1 For any object X E and x, y X, write

def
x v y X .(x) (y)

This says that every computable property possessed by x is shared by y, so y is more de-
fined than x. Clearly v is reflexive and transitive, but it need not be antisymmetric.

Examples 2.2

if = then this order is discrete, i.e. x v y x = y.

4
 if = {>, } then the (pre)order is the finest decidable equivalence relation on X.

in the topological example, (the externalisation of) v is exactly the specialisation order
(on generalised points of representables).

v > in [spell out]

Lemma 2.3 Every function is monotone with respect to this order. 

I
Unfortunately it is difficult to deduce very much about v on a power X from the order
on X without additional assumptions, but we do have the expected result for binary product:

Lemma 2.4 For x1 , x2 X and y1 , y2 Y , we have hx1 , y1 i v hx2 , y2 i in X Y iff x1 v x2

in X and y1 v y2 in Y . 
Traditional domain theory begins with posets sets with an imposed order relation
and then considers extra conditions such as bottom and joins of chains. The idea here is
to follow the same course, but starting from the intrinsic order relation on all sets, which is
automatically preserved by all functions. Domains are then just special sets but with ordinary
functions.
This point of view is analogous to the topological approach to domain theory, for which
Vickers [1989] is an excellent introduction. A map X plays the role of an open set
of X and v is antisymmetric iff X is T0 in this topology. The point is characterised as
being in no open set save the whole space, and sobriety is analogous to (but stronger than)
directed-completeness. Note, however, that the class of -subsets is in general not closed
under arbitrary unions.

Definition 2.5 A -space is an object X for which v is antisymmetric; it is focal 1 if it has

a least element in this order.

Examples 2.6
If = , every object is a -space, but only the terminal object is focal.

If = {>, }, an object is a -space iff (the equality predicate on) it is decidable, and
again only the terminal object is a focal -space.

In a Scott topos, every representable object is a -space, and is focal iff it has a bottom
in the specialisation order.

In the Effective topos, all -spaces are modest sets (but not conversely) and hence
definable by partial equivalence relations on N.
It is not difficult to see that X is a -space iff the map
X
X : X by x 7 f.f x

is mono. This suggests forming the epi-mono factorisation of X : we shall show that this does
in fact give the reflection of X into the full subcategory of -spaces.

Lemma 2.7 Let p : X Y . Then

1
For topological spaces, this term is due to Peter Freyd.

5
 the induced map p : Y X is split epi iff p factors into X .

if p is mono and X is focal then Y is focal and p preserves . 

pX e X
Proposition 2.8 Let X TX X
be the epi-mono factorisation of X . Then T defines
the reflection into the full subcategory of -spaces, and also preserves the property of being
focal. 
In order to be able to construct the powerdomain we need another property:

Proposition 2.9 T preserves finite products. 

So much for the synthetic analogue of posets; for (pre)domains we need some kind of
either directed-completeness or sobriety. There are several different candidates for this, some
of which are considered by the first author in [1990], but in this paper we prefer not to
be drawn into this discussion. However in the proofs of the previous results the important
property was being epi with respect to maps into , and by isolating this we obtain easily a
good notion, due to Martin Hyland, which suffices for our purposes (in fact we shall make no
further use of it).

Definition 2.10 p : X Y is called -epi if it induces a mono p : Y X and -

anodyne if this is an isomorphism. The object X is -replete if the only -anodyne maps
p : X Y are isomorphisms.

Proposition 2.11 Every object X has a -replete reflection, SX, and S preserves finite
products. 
In the topological example, a representable is -replete iff it is sober, and in this case the
specialisation order has directed joins.In the Effective Topos -replete also implies that -
sequences have joins, although the proof makes crucial use of Markovs Principle and Churchs
Thesis.

3 The finite powerset

In order to construct free algebras it is in general necessary to assume that the topos E has
free model). However the powerset X of a
a natural numbers object N (since that is itself a S
set X E is already the free internally-complete -semilattice on X, even when E itself fails
to have infinitary colimits or a natural numbers object.
Since X has I-indexed joins for all I E, in particular it has nullary and binary ones,
usually written and U V respectively, so it is a (finitary) -semilattice.

Notation 3.1 Let K(X) X denote the smallest subset which

contains the empty set X

contains the singletons {} : X , X and

is closed under binary unions : X X X .

So,

6
 to prove properties of K(X) we consider the class L K(X) of sets which possess
the property and show that it includes and singletons and is closed under binary
unions.

If U K(X) for some X, we say U is Kuratowski-finite. On the assumption that

the topos E has a natural numbers object N, a set is Kuratowski-finite iff locally2 it has an
enumeration
U = {x1 , . . . , xn }
possibly including repetitions for some n N, i.e. there is a surjection [n]  U . Hence the
class of Kuratowski-finite sets is closed under quotients, although not under subobjects. For
an account of this characterisation, the reader is referred to Johnstone [1977]. Although it
is useful intuition, we prefer not to make our proofs rely on it as it is more complicated to
express categorically.

Proposition 3.2 K(X) is the free semilattice on X.

Proof Let (A, d, }) be any semilattice; we are going to construct the structure map :
K(A) A. Consider the set

C = hU, ai A A : (u U.u b a) b A.(u U.u b b) a b b



and let
D = U A : a A.hU, ai C


Then by antisymmetry of b, the projection 0 : C  D is an isomorphism; also

h{} , idi : A A A factors through C,

h, }i C and

if hU, ai, hV, bi C then hU V, a d bi C

Hence K(A) D and the components of
1
: K(A) D
= C A A A

are semilattice homomorphisms. Moreover {} = id because

{a} = 1 h{a} , ai = a

Hence if we are given any function f : X A we may factor it through {} : X , K(X) by

the semilattice homomorphism
def def
f == K(f ) where K(f )(U ) == {f (u) : u U }

(so essentially f(U ) = {f (u) : u U }). This factorisation is unique, since given two such
S
we may form their equaliser E K(X), which is a sub-semilattice containing X and hence
the whole. 
2
The number n is not a constant, but is parametrised by v V , where V is some supported object (see next
footnote). The indices i of the enumeration are similarly functions i : V N such that v.1 i(v) n(v).
For example if E = SetG for some group G, any finite set with a G-action is Kuratowski-finite, but (constant)
numerals [n] and their quotients carry the trivial action.

7
 The following simple but important result is true of the free functor of any finitary alge-
braic theory:

Lemma 3.3 The functor K : E E preserves surjectivity.

Proof Let f : Y  X in E, i.e.

x X.y Y.f (y) = x

Consider the set

L = {U K(X) : V K(Y ).K(f )(V ) = U }

It contains the singletons because for U = {x} we are given y Y.f (y) = x, so put
V = {y} and then K(f )(V ) = {f y} = U .

It contains the empty set because K(f )() =

It is closed under unions because if U1 = K(f )(V1 ) and U2 = K(f )(V2 ) then U1 U2 =
K(f )(V1 ) K(f )(V2 ) = K(f )(V1 V2 ).

and so L = K(X), i.e. U K(X).V K(Y ).K(f )(V ) = U . 

Corollary 3.4 (Weak Axiom of Finite Choice) Let U X be finite (i.e. U K(X)) and
let (x, f ) be a predicate on X F such that

u U.f F.(u, f )

Then there is a finite set of pairs V U F such that

u U.f F.hu, f i V and hu, f i V.(u, f )

Proof Apply the Proposition to the projection

0 : {hu, f i U F : (u, f )}  U

and consider U K(U ). 

Notation 3.5 Let K+ (X) X be generated by the singletons and (not ). By a binary
semilattice we mean an algebra (A, d) with an idempotent, commutative and associative
binary operation (but no unit).

Proposition 3.6

K+ (X) is the free binary semilattice on X,

any U K+ (X) is supported,3 i.e. u U.>, and

K(X) = K+ (X) + {} (the disjoint union).

3
Being supported is the internal way of saying that a set has an element; diagrammatically, U  1. It need
not be inhabited, i.e. have a global element 1 U .

8
Proof The first part is exactly similar to what we did before. The subset L K+ (X) of
supported sets includes the singletons and is closed under so is all of it. Finally K+ (X)+{}
carries a (d, })-semilattice structure, so there are mediators K(X)  K+ (X) + {}; the
universal properties (coproduct and free semilattice) make these mutually inverse. 
So the finite powerset, like the Hausdorff and Vietoris constructions but unlike the full
powerset X , falls into two parts. This means that, given a Kuratowski-finite set, there
is a constructive procedure to determine whether it is empty or inhabited. The Plotkin
construction only defined the larger part anyway because the empty set of process behaviours
is not meaningful in denotational semantics.

4 The Egli-Milner order

Since the order on A A is pointwise, we have

Lemma 4.1 If a1 v a2 and b1 v b2 in a semilattice (A, d) then a1 d b1 v a2 d b2 . 

Here it is important to remember the distinction between the two order relations: the
similar result for b is trivial.
Let S be a Kuratowski-finite set; informally, we can think of it as the word s1 ds2 d dsn
for some n N (where the si are not necessarily distinct). Now suppose that T is another
finite set and the relation



s S.t T.s v t t T.s S.s v t

holds; this is called the Egli-Milner order, written S vEM T . Then for each i we have some
t0i T with si v t0i . Similarly T is the word t1 d d tm and we have s0j v tj with s0j S.
Then

(s1 d d sn ) = (s1 d d sn ) d (s01 d d s0m ) v (t01 d d t0n ) d (t1 d d tm ) = (t1 d d tm )

using the semilattice equations for the equalities and v-monotonicity of d for the inequality.
Now each of the authors who have discussed the Egli-Milner order have given motivations
for it (from Computer Science), which one may or may not find convincing. However a little
consideration of pure category theory shows how it is forced upon us. For each object X E
we have
def
[v] == {hs, ti X X : s v t}
which internalises the order relation. We write p, q : [v] X for the projections, and of
course one is pointwise less than the other.
Now apply the functor K. What is this order4 K[v] KX? An instance of it is a finite
set V of pairs hs, ti with s v t; then let
def
S == K(p)(V ) = {s X : t X.hs, ti V }

and
def
T == K(q)(V ) = {t X : s X.hs, ti V }
4
In fact K[v] K(X) K(X) is not mono, but this doesnt matter; shortly we shall show that its image
is [vEM ].

9
so we have S vEM T . We shall now give a purely categorical proof that it implies the -
order. The first result (like preservation of surjectivity) is true of the free functor of any
finitary algebraic theory.

Lemma 4.2 The functor K preserves the (pointwise) v relation.

Proof We are given p, q : Y X satisfying y Y.p(y) v q(y). Consider the set

L = {V K(Y ).K(p)(V ) v K(q)(V )}

Then
K(p)({y}) = {py} v {qy} = K(q)({y}) by monotonicity of {} : X K(X),

K(p)() = = K(q)() and

if K(p)(V1 ) v K(q)(V1 ) and K(p)(V2 ) v K(q)(V2 ) then using the Corollary,

K(p)(V1 V2 ) = K(p)(V1 ) K(p)(V2 ) v K(q)(V1 ) K(q)(V2 ) = K(q)(V1 V2 )

so L = K(Y ), i.e. V K(Y ).K(p)(V ) v K(q)(V ). 

Lemma 4.3 If S, T K(X) with S vEM T then there is some V K[v] with K(p)(V ) = S
and K(q)(V ) = T .
Proof We use the weak axiom of finite choice with the finite set S and the predicate s v t
on S T to find V1 K(S T ) with

s S.t T.hs, ti V1

and similarly V2 K(S T ) with

t T.s S.hs, ti V2

Then V1 , V2 K[v] with

K(p)(V2 ) K(p)(V1 ) = S and K(q)(V1 ) K(q)(V2 ) = T

Finally put V = V1 V2 . 

Proposition 4.4 For S, T K(X), if S vEM T then S v T in K(X). 

Corollary 4.5 v is not necessarily antisymmetric, but if X has a least element in this
order then K+ (X) has a least element {}.
Proof
Let X = and consider the finite sets
def def
S == {h, i, h>, i, h>, >i} and T == {h, i, h, >i, h>, >i}

Then we have both S vEM T and T vEM S, so by the Proposition S v T and T v S in

K(X). However neither is a subset of the other, so theyre certainly not equal.

Any T K+ (X) is supported, i.e. y T. v y, so {} vEM T and hence {} v T . 

10
5 Modalities
We want to derive a property of v on X (which is defined in terms of maps : X )
from v on K(X) (which is defined in terms of : K(X) ). Therefore we need a way of
generating computable properties of finite sets from those of elements.

Lemma 5.1 Let (x) be a -predicate in x X. Then

def def
(U ) == u U.(u) and  (U ) == u U.(u)

are -predicates in U K(X).

Proof Treating as respectively an - and an -semilattice, these predicates are the
mediators from K(X), the free semilattice, of the maps : X . 
 concerns inevitable behaviour of a process (containment in Johnstones topological
setting, where he writes t()) and possible behaviour (non-empty intersection, m()).
In the rest of our discussion of the modal operators, the predicates to which they are applied
are not necessarily computable, unless explicitly stated. In fact we shall simply find S a
convenient abbreviation for s S, and similarly S , T and T , but this notation already
illustrates that when we use the modal operators for several variables, we more or less end
up using quantifiers anyway.
W W
Lemma 5.2  > = >, ( ) =   and iI i = iI i . 

Definition 5.3 A family {i : i I} of predicates is directed if

i I.>,

i, j I.k I.i k j k .

In this case we write  i for their join5 . These two axioms are of course the nullary and
W
binary forms of the more general

U K(I).j I.i U.i j

which is shown to be equivalent by the same methods as before.

Lemma 5.4  is continuous, i.e. if {i : i I} is a directed family of predicates then

_ _
  i =   i
iI iI
Proof ( follows from monotonicity of .) For U K(X) we must show

u U.i I.i (u) ` j I.u U.j (u)

i.e. a uniformity result. For this we use the weak axiom of finite choice to obtain a finite
set V U I such that

u U.i I.hu, ii V and hu, ii V.i (u)

5
Not necessarily a -predicate.

11
So by the general statement of directedness of I we have j I with

hu, ii V.i j

So j I.u U.j (u) as required. 

Remark 5.5 It seems that the dual result, cocontinuity of , can only be proved by contra-
diction. This is a pity, because it is what we really want to use.
Finally there are two properties which relate the two modalities:

Lemma 5.6  ( ) and ( )  .

Proof The first is obvious; for the second show that the set of finite sets satisfying it
contains and the singletons and is closed under . 
Johnstone defines the Vietoris locale V(A) of an arbitrary locale A as the free frame
generated by symbols { a, a : a A} subject to these six relations. He shows that this is
part of a monad defined on the category of locales, and that every algebra for this monad
carries a (localic) semilattice structure. However the correspondence between the Vietoris
and free semilattice constructions is only exact in special cases, so we do not expect it to hold
in our setting.

Lemma 5.7 K+ (X) K(X) is characterised by the imposition of either of the equivalent
additional relations
 = or > = >
Proof The second is x U.>, which is just the definition of being inhabited, whilst the
first, x U., is clearly equivalent. 
In the context of locales or -predicates we do not consider negation, but of course it is
defined for general predicates and we need to know how the modal operators relate to it. It
is an easy exercise in natural deduction to show that ( ) () ().

Lemma 5.8  and   .

Proof The first follows immediately from the definitions as quantifiers, whilst the second
holds because  is really finite conjunction. Let L K(X) be the class of finite sets U for
which  (U )  (U ). Then L contains , singletons and binary unions. 

6 Sigma implies not not Egli-Milner

As we said in section 2, we need an additional assumption:

every is -closed, i.e.

In the Effective Topos, where is of the form n.f (n) = 1 for some f : N 2, this assumption
is precisely Markovs principle; intuitively, it says that if a process doesnt diverge then
eventually it converges. Although forcing all predicates to be -closed makes
Boolean, this condition does not even make Boolean.6
6
The reader is invited to find a lattice of regular (pinhole-free) open subsets of R.

12
 The converse argument is beset with negations, and the best way to understand them is
by introducing a relation which says positively that not every property of s is shared by t:
def
x v| t X .(s) (t)

Clearly we have s v| t (s v t), but in fact

Lemma 6.1 s v t iff (s v| t).

def 
Proof It is convenient to introduce N (s) == X : (s) , the set of neighbourhoods or

properties of s. Then the right hand side is

N (s).(t)

which, since , is just

N (s).(t)
But (t) and is by hypothesis -closed, so this is just s v t. 

Corollary 6.2 v is -closed, i.e. (S v T ) S v T . 

Hence the best converse of section 4 we can expect is S v T (S vEM T ). It is
convenient to show this in the form (S vEM T ) (S v T ): a classical argument by
contradiction. Incidentally, all functions reflect v,
| but the best transitivity result we have is

x v| z y.(x v| y y v
| z)

We introduce
def
S 6vEM T s S.t T.s v
| t t T.s S.s v
| t

Suppose informally that the first disjunct holds for a particular s S. Writing T =
{t1 , . . . , tm }, there are computable predicates j X such that j (s) but j (tj ). Then
with = 1 m we have (s) but t T.(t). Then = is satisfied by S but
not by T . The other part is similar, with as the disjunction and  . More formally,

Lemma 6.3 If S 6vEM T then S v| T .

Proof The first predicate (fixing s) is
_ _ _
T  (T )  T (T )  T (T )
N (s) N (s) N (s)

by continuity of  and then  . Recall that the former used the weak axiom of finite
choice, and it is easy to check that N (s) is a filter. Then

X .s S.(s) (T )

whence the result follows by putting = .

Using the ideal
def 
M (t) == X .(t)

13
the second predicate (fixing t) is
_ _
S  (S)  S (S)
M (t) M (t)

Then
X .t T.(t) S (S)
from which we deduce  (T )  (S), so we put =  . 
A classical argument would now be complete, but we have to reason constructively, and
negation is a delicate thing, so there is more work to be done and we must be careful. The
negated Egli-Milner relations do not behave quite as well as v,
| but we do have

Lemma 6.4 (S 6vEM T ) iff (S vEM T ).

Proof (S 6vEM T ) is of the form

S T s v
| t T S s v
| t

whilst, by the first lemma, we have already expressed (S vEM T ) in the form

S T s v
| t T S s v| t

Then
        
from the relationships between modal operators and negation.7 

Theorem 6.5 S v T iff (S vEM T ).

Proof We have shown that

S v T (S v
| T ) (S 6vEM T ) (S vEM T ) (S v T ) S v T

7 Bibliography
J.L. Bell Toposes and local set theories, Oxford logic guides 14, Oxford University Press,
1988.
M.P. Fourman, The Logic of Topoi, in: J. Barwise, ed., Handbook of Mathematical Logic,
North-Holland, 1977, 10531090.
M. Hennessy and G.D. Plotkin, Full Abstraction for a Simple Parallel Programming Lan-
guage, in J. Becvar, ed., Proc. MFCS, Lecture Notes in Computer Science 74, Springer, 1979,
108120.
R. Hindley and J. Seldin, eds., To H.B. Curry: essays in combinatory logic, lambda
calculus and formalisms, Academic Press, 1980
J.M.E. Hyland, The effective topos, in: A.S. Troelstra & D. van Dalen,, eds., Brouwer
centenary symposium, North Holland, 1982.
7
This formula, though terse and unorthodox, precisely captures the active part of the argument.

14
 J.M.E. Hyland, P.T. Johnstone and A.M. Pitts, Tripos theory, Proc. Camb. Philos. Soc.
88 (1980) 205232.
P.T. Johnstone, Topos Theory, Acedemic Press, 1977.
P.T. Johnstone, Stone Spaces, Cambridge studies in advanced mathematics 3, Cambridge
University Press, 1983.
P.T. Johnstone, The Vietoris Monad on the Category of Locales, in: R.-E. Hoffmann, ed.,
Continuous Lattices and Related Topics, Universitat Bremen Mathematik-Arbeitspapier 27
(1982) 162179.
A. Kock, Synthetic differential geometry, LMS lecture notes, Cambridge University Press,
1981.
J. Lambek, From -calculus to cartesian closed categories, in: Hindley & Seldin.
J. Lambek and P.J. Scott, Introduction to higher order categorical logic, Cambridge stud-
ies in advanced mathematics 7, Cambridge University Press, 1986.
M. Makkai and G. Reyes, First order categorical logic, Lecture notes in Mathematics 611,
Springer, 1977.
W.K.-S. Phoa, Effective Domains and Intrinsic Structure, in: Logic in Computer Science
(Philadelphia, 1990), to appear.
G.D. Plotkin, A Powerdomain Construction, SIAM J. Comp. 5 (1976) 452487.
G.D. Plotkin, Dijkstras predicate transformers and Smyths powerdomain, in: D. Bjrner,
ed., Abstract Software, Lecture Notes in Computer Science 86, Springer, 1979.
E.P. Robinson, A Modal Language for Power-Domains, manuscript.
E.P. Robinson, Powerdomains, Modalities and the Vietoris Monad, Cambridge University
Computer Laboratory Technical Report 98, 1986.
G. Rosolini, Continuity and effectiveness in topoi, Ph. D. thesis, Carnegie-Mellon Univer-
sity, 1986.
G. Rosolini, Categories and effective computation, in: D. Pitt, ed., Category Theory and
Computer Science (Edinburgh, 1987), Lecture Notes In Computer Science 240, Springer, 1987.
D.S. Scott, Relating theories of the -calculus, in Hindley & Seldin.
M.B. Smyth, Powerdomains and Predicate Transformers: a Topological view, in: J.
Diaz, ed., Automata, Languages and Programming, Lecture Notes in Computer Science 154,
Springer, 1983, 662675.
S.J. Vickers, Topology via Logic, Cambridge University Press, 1989.
G. Winskel, Note on Powerdomains and Modality, Theor. Comp. Sci. 36 (1985) 127137.

15