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
| 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
| 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 .
| 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 )
| 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.
| 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 -> Setare defined inductively, and
| S : Ord -> Set , | _[_] : (Pi Ord) S a -> Ordare 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.
(U,T) . Given such a
family we can consider functions of type:
| fam (U,T) U -> fam (U,T) Uwhich have the typical form
| \(A,B)->(phi(A,B),psi(A,B))where
| phi : ( Pi A : U ) (T(A) -> U) -> U | psi : ( Pi A : U, B : T(A) -> U ) T(phi(A,B)) -> USuch 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.