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

chains, etc & announcement on intuitionistic Tarski theorem

Date: Thu, 28 Nov 91 15:17:04 GMT

Several people have referred to the equivalence between chains, ordinals and
directed sets. Lest anyone think there is anything mysterious about this,
let me remind you of the proof.

We need the concept of [CO]FINALITY. [The "co" does not refer to dual
categories - the whole word just means "having the same limit"; the prefix
got dropped in the generalisation to categories.] A subset of a directed set
is cofinal if given any point of the larger set there is a point of the
smaller beyond it - cf one of the orders on powerdomains. For the categorical
definition, see Mac Lane. The point is that cofinal diagrams in ANY poset or
category have the same join or colimit.

Now, given a countable (ie enumerated) directed set, we can choose an
increasing sequence in it which is cofinal. Easy exercise.
>From this it is a very easy exercise to show that for ANY POSET WHATEVER
(algebraicity is, as usual, a complete red herring) every countable
increasing sequence has a join iff every countable directed set has a join,
and a function preserves all joins of one kind iff it preserves all joins
of the other kind.

Now, this raises several points.

(1) The process of choosing this sequence is completely IRRELEVANT to the
applications. It is a lemma to be forgotten, just as you forget the inner
workings of your computer. Working with chains is, as I said, like working
with Kleene indices. To prove, for instance, the continuity of the fixed
point operator, you need to take a product of diagrams; this presents no
problem with directed sets, but if you insist on working with chains you
have to perform the irrelevant operation of choosing the diagonal chain from
the square.

(2) I deliberately emphasised that countable meant enumerated. Otherwise,
you have to CHOOSE the enumeration.

(3) The uncountable case is more complicated and depends on the AXIOM OF CHOICE.
The result can be proved by induction on cardinals:  assuming that the given
directed set actually has bounds within itself not just of pairs but of sets
smaller than the cardinal under consideration, we can choose a transfinite
increasing cofinal sequence.

Now, I assume that the reason why John Mitchell and others on types should be
interested in this is with a view to understanding semantics of programming
languages, a subject which lies within CONSTRUCTIVE mathematics. They have,
therefore, no business to be using the AXIOM OF CHOICE.

With respect to Achim Jung [and I have a very high opinion of him both
mathematically and as a friend] it is not relevant to cite his work on this
question. That was concerned with settling the "largest ccc" problem, and
in particular he needed to sweep out those dusty corners where semantics
[per se] never goes but in which might lurk some ghoulish counterexample.
This is most often what the AXIOM OF CHOICE gets used for in mathematics.
I rather suspect that John Mitchell had no intention of visiting such places.

[Exercises for those interested in such things: using the method above for
the uncountable case show that:
  i) Given a directed subset with no join in a poset (of smallest cardinality
     with this property), construct a monotone endofunction of the poset
     which fixes all bounds for the directed set but nothing else, and in
     particular acts as the successor on a cofinal sequence. Hence show that
     a poset in which every monotone function has a least fixed point has a
     bottom and joins for all directed sets.
 ii) Given two points in a cpo which fail to have a complete set of minimal
     upper bounds, construct a continuous endofunction which fixes bottom and
     the two points, acts as the successor on a descending ordinal subset
     and has this and the three points as image. Show that the function space
     of the image is not algebraic (or continuous or locally compact) and
     hence neither is that of the original cpo.
The latter is the first result towards the largest ccc classification.]

As I have said, in theoretical computer science - being part of constructive
mathematics - we have no business using the Axiom of Choice. Nor do we have
any business using EXCLUDED MIDDLE, though those who insist on proving simple
constructive results [which the largest ccc problem is not] in domain theory
by bit-picking rely on it all the time.

Here, then, is an ANNOUNCEMENT OF A RESULT.

				THEOREM
		In higher order INTUITIONISTIC type theory,
	TARSKI's THEOREM holds for monotone endfunctions of a cpo.

By considering the smallest set closed under arbitrary joins and application
of the function, it is not difficult to prove Tarksi's theorem for complete
lattices intuitionistically. [Somebody will probably tell me that's what
Tarski did (?)]

Using ordinals (zero goes to bottom, apply the function at successors and
take directed joins at limits) it is also quite easy to prove the result for
cpos.

However the theory of ordinals as usually presented depends on excluded middle.

Here is the definition of ordinal which makes transfinite induction work
constructively.

WELL-FOUNDEDNESS is defined using the induction scheme, not minimal elements
of non-empty sets or descending chains.

An ORDINAL is a set (type) X with a WELL FOUNDED, TRANSITIVE, EXTENSIONAL
binary relation (<) such that X is CLOSED UNDER "UNIONS" in the sense that
  for all x and y in X,
  there is a (unique) z in X such that
  for all w in X, w<z iff w<x or w<y

The SUCCESSOR of an ordinal is the set of lower union-closed subsets; the
order on it is defined by considerations of a set-theoretical kind.
(There is no simple connection between the well-founded and hence irreflexive
relation < and the reflexive containment relation.)

This result forms one of the four chapters so far written of my book, but
there are a lot more to go.

Paul Taylor.