FOM: Re: your FOM posting on proof theory
avigad at cmu.edu
Fri Jul 17 09:59:58 EDT 1998
> 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
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
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
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
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.
More information about the FOM