[Prev][Next][Index][Thread]

ordinals and Tarski's theorem

Date: Mon, 2 Dec 91 18:51:51 GMT

I am grateful to Jim Lipton for pointing out the following reference:
	R.J. Grayson, "Heyting-values models for intuitionistic set theory",
	in "Appplications of Sheaves" (proceedings of a meeting in Durham,
	editted by M.P. Fourman, C.J. Mulvey & D.S. Scott), Springer LNM 753.
This paper investigates (briefly) intuitionistic ordinals and set theory.

Well-foundedness is defined as the induction scheme:
	all x.   [all x'<x. P(x')]  =>  P(x)
	------------------------------------
		all x. P(x)
extensionality is (as usual)
	all z.  z<x  <=>  z<y
	---------------------
		x=y
Grayson (following Powell, JSL 40 (1975) 221-9) defines an ordinal to be
a set with a well founded extensional transitive relation.

This definition is sufficient to prove Tarski's theorem for *complete lattices*,
but that's easy to do using closure conditions in the way I mentioned. 
Classically one can show, making *very* heavy use of excluded middle, that
such an ordinal is trichotomous (linearly or totally ordered) and hence
(except for zero) directed. Intuitionistically, directedness may fail.

We need to revise the definition as follows. [I mis-typed this in my flame
last week.]
	all x,y.  exists (unique) u.
		all z.  z<x  ->  z<u
	and	all z.	z<y  ->  z<u
	and	all z.  x<z and y<z  ->  u<z
[Jim Lipton or others may have an opinion on whether I should retain the
weaker meaning for "ordinal" and call this "directed ordinal" (or something)
or re-use the term in the stronger sense.  I prefer the latter, since I've
always thought of ordinals as being directed.]

Grayson's definition of the successor is X+1=X union {X}, which, as is remarked
in that paper, fails to satisfy
	x subset y element z -> x element z
and there are more [constructible] ordinals of rank 2 than elements of his
ordinal 2.

This problem is solved by an idea I got from synthetic domain theory:
	X+1 is the set of binary-directed lower subsets of X
(cf functions to Sigma, which, in the case of the finite ordinals constructed
in my LiCS 91 paper, always preserve binary meets & joins.) We need some more
explicitly set-theoretic ideas to define the well founded (irreflexive) order
on the successor. IZF suffices, but being a categorical atheist I don't believe
in transsubstantiation and much of my text is devoted to the development of
extensional well founded relations from a type-theoretic foundation (just as
we do with domains or any other mathematical structure apart, traditionally,
>from sets). Subset inclusion turns out to be characterised as a *fibration*.

We also have to revise the definition of cpo to mean having joins of sets
which are directed in only the binary sense, although I think there's a hack
to adapt the result to bottom + (nullary+binary)-directed joins.

Proof of Tarski's theorem.

Then given a cpo D with a monotone endofunction f:D->D, there is a unique
[class] function  g:On->D such that
	g(0) = bottom
	g(x+1) = f(g(x))
	g preserves binary-directed joins
In fact,
	g(x)=join{f(g(y)):y<x}		the join being binary-directed

It remains to show that the process of applying f and taking directed joins
terminates. Classically this is done using Hartogs' Lemma: for any set D there
is an ordinal X with no 1-1 function X->D whatever. The ordinal X is simply
the set of ordinals which do have 1-1 functions to D.

Intuitionistically this is not quite enough.
However, taking X to be a successor (wlog), we can define a continuous
closure operation c:X->X such that  c;g=g  and the restriction of g to
the image of c is 1-1. This image is an ordinal (wrt the restricted order)
and so, by Hartogs' construction, an element of X, and (by the universal
property of g) the image is in fact a lower set. It has a greatest
element, whose successor is in X, and this is the fixed point.

End of Proof

Addendum to my flame:

(4) The whole concept of cardinality, upon which so much of the discussion
relies, is unconstructive. It relies on the *non-existence* of functions
(bijective, surjective, injective according to formulation).  Since 1963
(Cohen's proof of the independence of the continuum hypothesis using what
was then called forcing and is now called basic topos theory) its fragility
has been obvious: you can embed one model in another in such a way as to
preserve everything of genuine constructive interest but making sets have
the same cardinality where previously they were very different. Cardinality
("omega-algebraic" etc) just clutters up the subject.