I recently happened upon a paper that provides some great background on a topic relevant for our discussion of termination analysis, namely “The Art of Ordinal Analysis” by Michael Rathjen (abstract and download information below).
I am not the first blog writer (see, for example, Logic Matters of a couple years back) to notice this really helpful paper, but I’ll recommend it a bit more expansively. For termination analysis, background knowledge of proof theory is quite helpful. Ordinal analysis is a highly technical branch of proof theory, which can appear completely inscrutable even to readers who are comfortable with intricate theoretical matters. Very crudely, the idea is to identify the ordinal needed to show (by proof-theoretic means) that a logical system is consistent. Proof-theoretic consistency proofs work by showing how to transform proofs in the proof system in question into ones in a simpler system, where it can be easily shown that it is impossible to derive a contradiction. The critical problem is to prove that this transformation of proofs is a total function. A typical way to prove that any function is total is to define some measure on its inputs, and show that this measure is decreased at every recursive call to the function. Of course, the measure must be decreased in some well-founded ordering, and that is where ordinals come in. An ordinal is a canonical set-theoretic representative of an order-isomorphism class of well-founded orderings. I recommend the sections on ordinals in Wolfram Pohlers “Proof Theory: an Introduction”, although they are dense, and require very patient slow reading to get through. But you will be rewarded with a better understanding of ordinals.
To return to the paper by Rathjen: the thing I like about it so much is that it so elegantly and simply surveys the dizzying technical landscape of ordinal analysis. I have always been baffled when I’ve tried to get into that literature, because there are so many acronyms for different proof systems of interest. Rathjen succinctly explains what many of these acronyms are, and why the corresponding systems are of interest. The effort is much appreciated, since the reader can start to get a better grip on what these proof theorists are working on, and what the state of the field is.
How relevant is all this for Computer Science, and particularly type theory? I don’t really know, because for type theory, we really are mostly interested in strong normalization (all reduction sequences are finite for every term: it is not possible to find a nondeterministic execution that runs forever) — or maybe even just weak normalization (there is a single finite reduction sequence for every term, although there might still be infinite ones for some terms). For these theorems, ordinal analysis does not appear to be needed (at least in many important cases). The reducibility method of Tait, extended to reducibility candidates by Girard, suffices to show strong normalization of 2nd-order intuitionistic logic (“System F”), a so-called impredicative system. We’re getting a little ahead of ourselves with all this — and we will return to these topics later (or see also the discussion in Rathjen’s paper) — but suffice it to say that for ordinal analysis, it seems (from Rathjen’s article) that analyzing impredicative 2nd-order systems is at the limits of what can be done presently. I do not know how System F relates to those other systems, nor do I know if there is an ordinal analysis of System F: even though Girard’s proof shows strong normalization, it does not — and this is surely a feature, if all one cares about is strong normalization — make use of ordinals. These are “novice” questions from the point of view of proof theory, I’m sure; yet another indication of the depth of the field.
Anyhow, take a look at the Rathjen article for a glimpse into this proof-theoretic world.
The art of ordinal analysis
Michael Rathjen (1)
(1) Department of Mathematics, Ohio State University, 231 W 18th Avenue, OH 43210, COLUMBUS, UNITED STATES
Ordinal analysis of theories is a core area of proof theory whose origins can be traced back to Hilbert’s programme – the aim of which was to lay to rest all worries about the foundations of mathematics once and for all by securing mathematics via an absolute proof of consistency. Ordinal-theoretic proof theory came into existence in 1936, springing forth from Gentzen’s head in the course of his consistency proof of arithmetic. The central theme of ordinal analysis is the classification of theories by means of transfinite ordinals that measure their ‘consistency strength’ and ‘computational power’. The so-called proof-theoretic ordinal of a theory also serves to characterize its provably recursive functions and can yield both conservation and combinatorial independence results.
This paper intends to survey the development of “ordinally informative” proof theory from the work of Gentzen up to more recent advances in determining the proof-theoretic ordinals of strong subsystems of second order arithmetic.
Proceedings of the International Congress of Mathematicians
Madrid, August 22–30, 2006