The proof theoretic ordinal of a formal system such as a type-theory is a measure of how complicated an interaction can be expressed as a program in the system. It is a "least common denominator" measure which allows comparision between systems of very different kinds; it wouldn't however be sensible to use it as a guide to something like resource consumption.
What kind of programs are these, and when is it possible to regard a formal system as a language for writing interactive programs? I am thinking of extremely stylised call-response programs. In these, the program makes a call, and the run-time environment responds with some value that may influence the subsequent evolution of the program. Calls are limited to one of the following:
In a type-theory such as Godel's T, one may directly implement such a program as an expression, or more precisely an expression in the extension of T with a new ground type Prog, and new constants:
To run a program represented as above, the expression is reduced to head normal form. This must be one of
An complete execution of a program is a sequence of calls terminating with a Stop call. One way to set an upper bound on how complicated a pattern of interaction that can be is with a term in some `natural' notation system for an initial segment of the countable ordinals, which defines a fundamental sequence for each limit notation. Such a term represents a program: a successor term represents a program that begins with a Wait, and a limit term represents a program that begins with a Read. The ordinal bounds the program if each complete execution of the program is the same as some descending chain from the ordinal.
The pioneer in the mathematical analysis of the concept of well-foundedness was Cantor, in publications from around 1880. He studied linear (i.e. total) well-founded binary relations on a set, up to isomorphism. An order type is an equivalence class of well-founded relations. Well-foundedness rules out infinite descending chains, and requires accessibility from beneath. Cantor's investigations were particularly remarkable, because he was constantly dicing with the distinction between class (property) and set (thing representing a property). A long time later (1927) von Neumann gave the definition of ordinal in set theory that most people nowadays accept, choosing a canonical representative for each order-type: a set on which the epsilon (i.e. membership) relation is the linear well-ordering.
I have a great admiration for Cantor. He was a towering genius, responsible for huge progress in securing the foundations of mathematics. He seems also rather charmingly eccentric, at least if the letters from him quoted in Bertrand Russell's autobiography are to be believed. He encountered a lot of hostility and derision. (See Cantor, Georg (1845 - 1918)). Among Frege's writings (Posthumous Writings, Blackwell 1979) there is a draft of a witheringly sarcastic review of Cantor's more philosophical writings. (It should be mentioned that E.T. Bell's influental book `Men of mathematics' is unreliable, not to say irresponsible, perhaps even anti-semitic as an account of Cantor's life. See `Georg Cantor, His Mathematics and Philosophy of the Infinite' by J.W. Dauben, Princeton University Press.)
Among other things, Cantor invented his famous `normal form' for ordinals. Basically, any ordinal which is not a fixed point of exp_w = \ a -> omega ^ a can be uniquely expressed as a sum a = exp_w a1 + .. + exp_w ak. where (a1,...,ak) is a non-decreasing sequence of ordinals less than a. This leads to a decidable well-order on certain kinds of "hereditarily sorted" finitary trees. The trees can be used as ordinal notations up to the first fixed point of exp_w, known as epsilon zero. Cantors construction makes use of addition, (subtraction), multiplication, (division), exponentials and logarithms. Epsilon zero is the first ordinal not describable from below in Cantor-normal form, i.e. with addition, multiplication, and exponentiation of ordinals to the base omega, starting with zero.
There are various links between formal systems (like Peano Arithmetic) and ordinal numbers. The first to make such a link was Gentzen in 1936, with his proof of the consistency of first order arithmetic. In the proof, the only principle used beyond methods available in primitive recursive arithmetic, was induction on epsilon zero. Gentzen also showed certain results about the extent to which transfinite induction can be proved in first order arithmetic.
The link Gentzen made was immediately reinforced by Ackermann, who proved the consistency of a version of arithmetic formulated using Hilbert's so called epsilon, or choice symbol. Ackermann used completely different methods from Gentzen, although the crux of his results was again termination of a certain procedure, demonstrated using Cantor-style ordinal notations. So began the branch of proof theory known as ordinal analysis. I find it beautiful and mysterious. Yet I have never seen a formulation of what the subject is about that seems completely satisfactory. Anyway, there are plenty of strange and beautiful phenomena.
Since Gentzen and Ackermann, major (and various) contributions to the subject were made by many people, most of them German. As areas in logic go, ordinal analysis and the development of ordinal notation systems has a notably high burn-out rate. By anecdote, several people who contributed important notions abandoned the subject altogether to become deck-chair attendants, business tycoons, teachers, or other normal members of society.
A particularly important development was Veblen's investigations at the beginning of the century into normal (continuous and strictly increasing) functions and their derivatives. The derivative of a normal function is another normal function whose range consists of the fixed points of the first. For any countable sequence of successively derivative normal functions, there is a normal function which exhausts exactly their common fixed-points. This leads to a hierarchy, or binary operation which for describing ordinals going beyond Cantor normal form. Veblen, Ackermann and Schutte pursued various generalisations of this hierarchy.
It is a matter which gives scope for great pedantry, but the proof-theoretic ordinal (or for short, just `the ordinal') of a formal system is the least upper bound of the order-types of finite notation systems which can be proved within the system to be well-orderings. The intention is to have an absolute measure of strength in proving things, i.e. of `how much' can be constructed, defined or proved within the system. Here are some match-ups:
It is comparatively easy to set a lower bound on the proof-theoretic ordinal of a system - it is just a matter of exploiting the principles formalised in the system to construct sufficiently large well-founded structures. On the other hand, to get an exact bound is much harder. The method which has proved most successful involves embedding the system in an *infinitary* formal system (with infinite formulas or types, and proofs or terms).
My opinion is that there must be a simple semantical method for establishing upper bounds on the proof-theoretic ordinals, that remains to be found. I hope someone will find it before I'm too senile to understand it.