w, ww, www

W refers to Martin-Lof's W type operator, WW to a natural embellishment of it defined below, and WWW to something defined by abandoning myself to the formal seduction of notation. Today is Christmas, and I am indulging myself. (There is a slightly serious section at the end.)

I define a holy trinity:

|  w : Fam Set -> Set 
|  ww : (PI (A,B) : Fam Set) w(A,B) -> Set 
|  www : (PI (A,B) : Fam Set, t : w(A,B))ww(A,B) t -> Fam Set 

General definitions

Various notions of powerset.
|   Fam, Pow :: Type -> Type,
|   Fam A = (SIGMA I : Set)I -> A, 
|   Pow A = A -> Set 
|   fam : Fam Set -> Set -> Set 
|   fam (A,B) S = (SIGMA a : A)B a -> S 


Martin-Löf's "W type".
|   W : Fam Set -> Set 
|   W (A,B) = mu S : Set. 
|                S = fam (A,B) S  
where mu stands for a fixed point operator. So we have:
|          W(A,B) = fam(A,B) (W(A,B)) 
I write W(A,B) or (W x : A)B x .


A set-valued function defined on a W type.
|   WW : (PI (A,B) : Fam Set) W(A,B) -> Set 
|   WW (A,B) = mu F : W(A,B) -> Set .
|                 F(a,f) = W (B a) (F . phi) 
where `.' stands for function composition. So we have:
|          WW(A,B) (a,phi) = (W x : B a) WW(A,B) (phi x) 
I write WW(A,B) :: W(A,B) -> Set, etc.

Note that

|   \(A,B)->(W(A,B),WW(A,B)) : Fam Set -> Fam Set
As with any other operator of the same type, we may reasonably postulate (see `Mahlo' below) that there is a family of sets which is closed under `W,WW'. (It is not easy to see what the family is in this case! )

An afterthought: One may get a more interesting construction if one pre- or post- composes `W,WW' with the following construction, which is an analogue of von-Neumann successor on families.

|      (A,B)^+ = ( 1 + A,
|                  \ a' : 1 + A -> 
|                    case a' of inl 0 -> A
|                               inr a -> B a )


What is WWW? On aesthetic grounds (though I would prefer a recursive definition):
|  WWW : (PI (A,B) : Fam Set, t : W(A,B)) WW(A,B) t -> Fam Set 
|  WWW (A,B) (a,phi) (b,psi) 
|     =  LET F = WW(A,B) . phi : B a -> Set 
|        IN ( F b, WW (B a, F) . psi ) 
I hasten to add that I have little idea what this means. But damn it's pretty! Here is how it looks in half . What can we do with this monster? In effect, it gives us a function of type:
|  \(A,B)->(W(A,B),    \t  ->
|          (WW(A,B) t, \t' -> 
|          WWW(A,B) t t')) 
|  : Fam Set -> Fam^3 Set  
We have thus an interactive system over the large type of families of sets (usually, the base of an interactive system is a set). Perhaps we can assign to a family of sets the set of Petersson-Synek trees determined by this structure?? Here is surely a deep, dark forest in which one might find a little cottage made of ginger-bread...!!

Of course, as it stands, it may simply be nonsense.

PS: the ordinals

In this vein, it seems one can define the ordinals, as a transition system:
|        Ord : Set
|        Ord = 1 + (Sigma a : Ord) R a -> Ord  
|        R : Ord -> Set
|        R a = 1 + (Sigma s : S a) R (a[s]) -> R a 
|        S : Ord -> Set
|        S 0 = { }   -- empty set
|        S (a,phi) = (Sigma r : R a) 1 + S (phi r)
|        \a,s->a[s] : (Pi a : Ord) S a -> Ord
|        (a,phi)[r,0]     = phi r 
|        (a,phi)[r,inr s] = (phi r)[s]
The idea is that one starts with 0, and takes the least strict upper bound of a family of ordinals indexed by a `regular'. A regular reflects this closure property of the ordinals, with respect to smaller regulars, these being given by a transition structure \a : On ->(S a : Set,\s->a[s] : S a -> On) on the ordinals. For a : On, I think of the family { a[s] | s : S a } as `exhausting' the predecessors of a, ie. the segment of ordinals below a.

There must be something wrong with it! (Or several things. I have not succeeded in typechecking this using half. Perhaps it can be tackled with Agda?) Is it a definition in any sense, or even having any sense? I am trying to define simultaneously Ord, together with a transition structure of type : Ord -> Fam Ord . There is an auxiliary `predicate': R : On -> Set . It is as if

|        Ord : Set, 
|          R : Ord -> Set 
are defined inductively, and
|          S : Ord -> Set ,
|       _[_] : (Pi Ord) S a -> Ord
are defined recursively, with everything simultaneous. This is not an inductive recursive definition in the sense of Setzer and Dybjer, I'm assured.

How can it be that Ord is a set?? Surely the ordinals are a (large) type? Is there a non-terminating term here somewhere? If this is some kind of definition, what are these ordinals? Where do they run out of steam? Somehow, there are no stronger closure properties than are implied by being able to index regular ordinals. So maybe Ord is something like the least inaccessible (assuming it is anything at all).

IF the definition is good, or can be made good, then one would like to pick out the `real' ordinals as being those which are hereditarily transitive, or well-behaved in some way; then to define the basic comparision relations between ordinals, then investigate their arithmetic, and so on.

The theory of ordinals in traditional classical set-theory is in my opinion of spine-chilling beauty. It seems sad that there is no general computational theory of ordinals, comparable to that in classical set theory. There are the `Brouwer' ordinals, and analogues of the higher number classes, but actually trying to use them nudges at the limits of human toleration. In classical set theories, there are the von-Neumman ordinals, each the linearly ordered set of its predecessors. As it were, they form the (chilly) spine of the set theoretical universe (or the skewer on which the set theoretical universe is kebabed).

In the classical theory of ordinals, everything is splendid. To begin with, the ordinals are linearly ordered. Not only that, but each ordinal has a unique representation in Cantor normal form to a given base > 1; this is something assumed for example everywhere in work on proof-theoretical ordinals. It isn't obvious how to interpret these basic amenities of set-theoretical life computationally, at least without talking about representation systems rather than ordinals, which is very sordid.

It is interesting that principal components in the machinery of CNF representation are the partial operations of subtraction, division and logarithm. These operations are even nicer in Conway's arithmetic, in which ordinals can be identified with special positions for a certain kind of 2-player perfect-information terminating game. Who knows, there may be a constructive treatment of Conway's games, in which CNF holds?

The work in recent years on universe principles in type theory by Anton Setzer, Michael Rathjen, Ed Griffor, Erik Palmgren (any others?) may point towards a computational theory of ordinals. Maybe the work of Paul Taylor (JSL Vol 61, No. 3, Sept 1996 "Intuitionistic Sets and Ordinals) bears on this. There is also work coming from category theory (Joyal and Moerdijk: Algebraic set theory, LMS 220), which may be relevant. In another vein, there are constructive set theories of the kind formulated by Peter Aczel. It seems that reformulations of parts of the classical theory of ordinals can be developed in such set theories; but also that the notion of ordinal (hereditarily transitive set) plays a less central role than in classical set theory. It isn't true that every set has a least rank. Moreover, general induction over the membership relation is more useful than induction over just the ordinals.


What does `Mahlo' mean? The notion was introduced into type theory by Anton Setzer. (Mahlo was a gent who wrote about 1911 some papers about hierarchies of inaccessibles astonishing for the insight and technical virtuousity they exhibit, especially in view of the date.) It is a closure property of families of sets (U,T) . Given such a family we can consider functions of type:
|       fam (U,T) U -> fam (U,T) U
which have the typical form
|       \(A,B)->(phi(A,B),psi(A,B)) 
|       phi : ( Pi A : U ) (T(A) -> U) -> U
|       psi : ( Pi A : U, B : T(A) -> U ) T(phi(A,B)) -> U
Such a function is in effect an operator on `small families of small sets', where by a small set we mean a set T(u) for some u : U , and by a small family we mean a family the domain of which is a small set. The Mahlo property requires that (U,T) is closed under an operation which assigns to such a operator a small family of small sets which is closed under the appropriate restriction of the operator.

A more precise description follows. Given (U,T) and (phi,psi) as above, define the following family of small sets (V,S) : Fam U .

|   V : Set,     S : V -> U 
|   V   =   ...      {- some other constructions -}
|        + ( SIGMA A : V ) (T.S)(A) -> V                    
|        + ( SIGMA A : V, B : (T.S)(A) -> V ) T(phi(A,B))
|   S ...     = ...  
|     (A,B)   = phi(S(A),(S.B))
|     (A,B,c) = psi(S(A),(S.B),c) 
[Here I have used f.g to abbreviate \x->f(g(x)) .] Note that this definition is parameterised by (phi,psi) , although I have not shown the parameters explicitly. The Mahlo property is that (V,S) is actually small, which we can express with the following fixed point equation.
|   U   =   ...
|        + ( fam (U,T) U -> fam (U,T) U )
|   T ...                           = ...
|     (\(A,B)->(phi(A,B),psi(A,B))) =  V(phi,psi) 
Of course, in all the above, we may throw in whatever other closure properties we like: under PI , SIGMA , Nat , W , ... what have you.

A number of slight isotopes are essentially equivalent. For example, we may require that any operator on small families of small sets has a closure, which takes such a family to an extension of that family which has universes closed under the operator.

If you're at all the same kind of sick hopeless degenerate as me, and you look at equations like:

|    U = 1 + fam (U,T) U + ( fam (U,T) U  -> fam (U,T) U ) 
|    T 0 = sometype
|    T (a,b) = somequantifier (T a) (T . b)
|    T (\ (a,b) -> (phi(a,b),psi(a,b))) = somethingMahlo-ish (phi,psi)
you will immediately start doodling out another summand like, oh,
|       ... + ( (fam (U,T) U -> fam (U,T) U) 
|                -> fam (U,T) U -> fam (U,T) U )
on the right hand side of the equation for U, and then searching for some pretty clause with which to extend the equations for T. And so on and so forth... . There may be a (distant) relationship/analogy with Palmgren's higher order universe operators, and/or the hierarchies of functionals over the ordinals investigated by Feferman and Aczel in the late 60's. I wish I had time to look into this.

The principle that for any operator on families of sets, there is a family of sets which is closed under it is (to my mind) extremely natural. (This is sometimes called `black' mahlo -- saying that Set is a Mahlo universe. The version above is called `red', on the grounds perhaps that it is `more dangerous': the set U can not be equipped with a recursion principle, on pain of contradiction, and non-normalising terms; this was pointed out by Erik Palmgren: the argument is not substantially different from the observation that one cannot have recursion on an impredicative universe.) I now realise that I have been cheerfully using isotopes of black Mahlo for a long time, without consciously realising it. When you start to think about it, the principle is in fact extremely strong, and rather mysterious. The Mahlo universe is somehow the simplest possible example of a non-monotone inductive definition.

Anton Setzer has been working out a type-theoretic analogue of a Pi-3 reflecting universe. This goes (way?) beyond what one can derive from any autonomous iteration of the notion of Mahlo-ness. I presume that Anton will shortly obtain `universal' analogues of Pi-n reflection. But if you really want to depress yourself, equip yourself with a very large packet of extremely strong asprin, and look at the recent expository papers of Michael Rathjen to see how far proof theorists have got. They've already run out of any sensible vocabulary to name the cardinals they need, and are only encroaching on analyses of Delta-1-3 comprehension. Clearly, advanced proof theory is no place for an amateur! For me, what is most depressing is that one needs to have mastered several subfields of mathematical logic to which I have never paid the slightest attention (on the `soviet' grounds that they obviously could never make any computational sense), and are now forever beyond me.

Peter Hancock
Last modified: Sun Sep 19 22:51:07 BST 1999