Sheaf toposes and chain-complete posets

[Andrej Bauer <andrej.bauer@andrej.com>]

Dear categorists,

I am trying to wrap my mind around the concept of an (internal)
chain-complete poset in a sheaf topos. I am failing to come up with an
example of a poset that is chain-complete but is not complete. The
precise definitions of "chain-complete" in the internal language are
as follows.

Suppose (P, <=) is a poset in a topos. For C in Omega^P, let chain(C)
be the statement

  forall x, y : P, (x in C and y in C) ==> (x <= y or y <= x)

Then P is chain-complete if

  forall C : Omega^P, chain(C) ==> exists x : P, x is the supremum of C

where "x is the supremum of C" means the usual thing.

So what does a chain-complete poset which isn't complete look like?

Since I am used to arguing intuitionistically, it would help a lot if
there were some (possibly infinitary) logical principle or schema that
is typical of sheaf toposes -- something expressing the local nature
of validity. Such a principle ought to be invalid in realizability
toposes, so perhaps it should express or imply cocompleteness (with
respect to Set). But would that be of any help for arguing in the
internal language?

With kind regards,

Andrej Bauer


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]