FOM: Re: your FOM posting on proof theory

[Jeremy Avigad]

> I liked your posting on proof theory very much.
> To mak eit even more accessible to non-proof-theorists, perhaps you could 
> have explained exactly what a proof-theoretic ordinal is?
> Neil Tennant

Dear Neil,

Thanks for your kind words. There are a number of different definitions of
"proof-theoretic ordinal" that coincide in normal cases, but each
definition has problems that one can elicit with cooked-up
counterexamples. Explaining this fully would take a small essay; if I ever
expand my present essay to something more formal, I will elaborate on
this. 

Proof-theoretic ordinals are, by definition, recursive, which means that
you can think of them as given by concrete notations with a computable
order relation. For example, "omega times 5 + 3" denotes an ordinal less
that is less than the ordinal denoted by "omega times 7 + 9".

Epsilon_0 is the supremum of the sequences of ordinals

   omega, omega^omega, omega^(omega^omega), ...

Roughly speaking, saying that the proof-theoretic ordinal
of PA is epsilon_0 means all of the following:

1) PA proves transfinite induction principles up to anything less than
epsilon_0, but not epsilon_0 itself

2) primitive recursive arithmetic (or even weaker theories), together with  
open transfinite induction up to epsilon_0, proves the consistency of PA

3) any recursive function whose totality is provable in PA can be computed
using a schema of transfinite primitive recursion below epsilon_0, or by a
procedure that "counts down" from an ordinal below epsilon_0; any such
function is dominated by a fast-growing function in the Wainer hierarchy
below epsilon_0

4) If PA can prove a well-ordering principle for *any* recursive ordering
(you have to add free set variables to PA to be able to express this
precisely) then that recursive ordering has order type less than
epsilon_0

Modern proof theorists like 4, because it refers to the "real" epsilon_0,
and not a specific notation system. There are natural modifications of the
definitions if the theory is in the language of second-order arithmetic or
set theory. For example, 4 usually translates to to measuring the sup of
the "norms" of the theory's provable Pi^1_1 sentences (second-order
arithmetic) or determining the minimal Sigma_1 model (set theory). 

The idea is this: the stronger a theory is, the more recursive ordinals it
"knows about," i.e. the more powerful the transfinite induction
principles it can derive. So determining this ordinal measures, in a
sense, the strength of the theory.

Pohlers' LNM volume 1407 is a nice introduction to ordinal analysis, as
well as his survey in "Proof Theory," Aczel, Simmons, Wainer eds. There's
a little bit of a discussion in sections 4 and 6 of a paper I wrote with
Rick Sommer, "A model theoretic approach to ordinal analysis,"  Bulletin
of Symbolic Logic 3 (1997) 17-52, also available on my web page,
http://macduff.andrew.cmu.edu. Sam Buss tells me that the new handbook on
proof theory has just been published, and that will also provide helpful
introductions to the subject. 

Jeremy