The step to the next number class

By convention (since Cantor), the first number class is the set of natural numbers (or finite ordinals), the second is the set of ordinals which are at most countable (i.e. have cardinal at most that of the set of natural numbers), the third is the set of ordinals which have cardinal less than or equal to the set of countable ordinals, and so on.

In a typed calculus, the number classes can be represented by the following series of least fixed points:

How do we get rid of the ... here and define the step from one number class to the next in a uniform way? (I am not interested here in dependent types, but only in simple types with no dependency. Nor do I care if the `first' number class turns out to be the second or the third -- it is only a matter of convention.)

The answer is to define instead the sequence of functors whose least fixed points are the various number classes. That is, we define a higher type operation:

    Phi F X  = F X + X^(mu F)
and then consider the least fixed points of the series of functors Id, Phi(Id), Phi^2(Id), .... Here Id stands for the identity functor id(X) = X.

Then the first number class is 0 = mu Id, which is the empty set. The second is the least fixed point of X |-> Id(X) + X^0, ie the set of natural numbers. The third is the set of countable ordinals, and so on.

The successive functors, and their initial algebras are as follows:

        Functor B_n(X)            Initial algebra Omega_n = mu B_n 
        -------                   ---------------
        Id X = X                  0 = Empty set
        Maybe X = Id X + X^0      w = Natural numbers, first number class
        B X = Id X + X^0 + X^w    W = Brouwer ordinals, second number class
        ...                       ...

I'd quite like to find a general description of this kind of construction in type-theory (particularly to look at collapsing functions from each number class starting at the third to its predecessor), and also to push beyond the finite number classes.

To make a start on this, try to define a collapsing function theta_n : Omega_{n+1} -> Omega_n for n > 1. The idea is essentially this:

      theta a = something like 1 + a
      theta (L f) = (theta . f)^w (succ zero)
One needs the destination type to be at least the countable ordinals, so that one can define w-iteration of functions over it. Some pretty properties of theta are (not rigorously checked):
  theta(Omega.a + b) = w^a + b 
  theta(Omega^(1+a).(1+b)) = phi_a b
provided we take the Veblen hierarchy phi to be based on phi_0 b = w^(1+b). The collapsing function is order preserving on terms in Cantor Normal form to the base Omega. It is remarkable the way theta "lifts" multiplication to exponentiation, and exponentiation to iteration of the derivative operation.

Since Omega_n = mu B_n, we can reason:

      theta_n : Omega_{n+1} -> Omega_n 
              = mu B_{n+1} -> mu B_n 
              = (mu X. B_n X + X^Omega_n) -> Omega_n
We can define theta_n to be the catamorphism iter f arising from an algebra f : B_n (Omega_n) + Omega_n ^ Omega_n, and the most obvious inhabitant of that type is [ constructors of Omega_n, omega-iteration]. However, that is not quite what we want. We want to do something interesting with `zero', which is in a way a distinguished constructor.

To begin, maybe one should define some simple things.

      emb_n : Omega_n -> Omega_{n+1}
      emb_n = iterate (f : B_n Omega_{n+1} -> Omega_{n+1})
               where f = cons_{n+1} . in_L
      sup_n : (Omega_n -> Omega_{n+1}) -> Omega_{n+1}
      sup_n = cons_{n+1} . in_R 

      lift_n : X -> B_n(X) 
      lift_0 = identity
      lift_{n+1} = in_L . lift_n 

Now we can define the sequence of initial ordinals -- for example 0, w = the first infinite ordinal, and "Church-Kleene" w_1 = the first uncountable ordinal. One simply takes for w_n : Omega_{n+1} the supremum sup_{n+1} . emb_n. Note that zero exists in every successor number-class, whereas successor exists in all number classes.

The problem now is to somehow break out "both ends" of the functors B_n. One wants to treat the first case (zero), and the last case (the new kind of supremum operation) specially in the definition of theta.

The idea of a universe of "higher order" functors, as opposed to a universe of sets is not new. Some other examples: universes of predicates over a fixed set of states, universes of relations or predicate transformers, universes of families, etc.

Peter Hancock
Last modified: Wed Jun 19 16:20:51 BST 2002