Title: "Hilbert, and phi_w(0)"

There's a straighforward coding of (some!) countable ordinals in
Girard's impredicative system F, the idea for which can be traced
back through Church, Wittgenstein, (apparently) Peano, to the dawn
of time. Replacing full impredicative quantification by schemas,
one can even take it as the basis for a clean and natural
definition of provable ordinal in type theories such as Godel's T,
or for systems that can be regarded as type theories in view of
Curry-Howard.  Precisely how this ties up with the somewhat
messier definitions adopted in mainstream ordinal analysis is a
possibly interesting project. (I'll blithely ignore that
question.)
 Among many in the last century who have flirted with some of these
ideas, I was recently surprised to find (actually, it was pointed
out to me) .. Hilbert!  Indeed, the system of "variable types"
mentioned in "On the Infinite" goes a bit beyond Godel's T, in
that (arguably) it uses a universe, or type of types.  He
specifically mentions (on p 477 of van Heijenoort) pushing things
up to the first critical epsilon number.  (phi_2(0), where phi is
the 2-place Veblen function over w^a.)
 This will not be a history talk.  I'll use the history only as a
peg on which to hang some ideas of my own, and show you how to
exploit "variable types" of height w^w to build ordinals up to
phi_w(0). This happens to be the ordinal of primitive recursive
arithmetic over the second number class: quite a respectable
ordinal.
 For those who want to look at the relevant passages in Hilbert, my
copy of van Heijenoort has yellow stickies at pages 385, 468, and
477.