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

Intuitionistic Sets and Ordinals (paper by FTP)


		Intuitionistic Sets and Ordinals
			Paul Taylor

In December 1991 I wrote to "types" claiming to have proved Tarski's
fixed point theorem for montone functions on a cpo intuitionistically,
without further assumption such as the axiom of collection.

That claim I have to withdraw, but I have now fully worked out the
intuitionistic theory of ordinals on which it was based.

The following paper has been submitted to the special issue of
"Mathematical Structures in Computer Science" to record the conference
"Category Theory and Computer Science 5" held at CWI, Amsterdam, Sept 1993.
(The work was also presented at the Category Theory meeting in July 1992.)

It is also available in dvi and compressed P*stScr*pt form by
anonymous FTP:
	ftp theory.doc.ic.ac.uk   (IP address 146.169.2.27)
	login: ftp
	password: (your email address)
	cd theory/papers/Taylor
	bin          (DVI and compressed files are binary)
	hash
	get ordinals.dvi

By the way, our archive now mirrors those of many of our colleagues in
theoretical computer science and category theory. If you would like us
to include your site, or if there is anything in your directory here
which shouldn't be, please email me with the details.

ABSTRACT

Powell defined \emph{ordinals} intuitionistically as transitive
extensional \emph{well founded} relations and showed that they admit
\emph{transfinite induction}.  However these ordinals are not
\emph{directed} and their successor operation is poorly behaved,
leading to~problems of functoriality.

By strengthening transitivity to \emph{plumpness}, we clarify
the traditional development of~successors and unions, and make it
\emph{intuitionistic}; even the (classical) proof of~\emph{trichotomy}
is made simpler.  Unfortunately, as their name suggests, the plump
ordinals grow very rapidly.

Directedness must be defined \emph{hereditarily}.  It~is orthogonal
to the other four conditions, and the \emph{lower powerdomain}
construction is shown to be the universal way of imposing it.

Our set theory is similar to Osius' \emph{transitive set objects},
but presents \emph{Mostowski's theorem} as a reflection of categories.
Set-theoretic union is a corollary of the \emph{adjoint functor theorem}.

Each notion of set or ordinal is a \emph{free algebra} for one of
the theories discussed by Joyal and Moerdijk, namely joins of certain
arities together with an operation $s$ satisfying conditions
such as $x\leq s x$, monotonicity or $s(x\lor y)\leq sx\lor sy$.

This work originally aimed to prove the \emph{fixed point theorem}
for a monotone endofunction $s$ of a poset with least element
and directed joins.  We show that there is a point $x$ for which
$\lnot\lnot(x=s(x))$ and explain why it is unlikely that any
notion of ordinal can improve on this if it obeys the induction
scheme for arbitrary predicates.