FOM: to doctor Simpson (others please delete)

[reply to: adriano.palma@usa.net]

to prof; Simpson, I would appreciate it if you can repost or resend the
phone number and the codes for ordering Feferman's collections (called
"lights of logic")
due to a computer crash I lost the message (posted yesterday) with the
relevant information.
thank you



























||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||


  Ratio, enim, nisi judex universalis esse deberet, frustra singulis datur. 
 
  [ _Questiones Naturales_, Adelard of Bath ] 


On Fri, 17 Jul 1998, Jeremy Avigad wrote:

> Date: Fri, 17 Jul 1998 09:59:58 -0400 (Eastern Daylight Time)
> From: Jeremy Avigad <avigad at cmu.edu>
> To: fom at math.psu.edu
> Cc: Neil Tennant <neilt at mercutio.cohums.ohio-state.edu>
> Subject: FOM: Re: your FOM posting on proof theory
> 
> 
> > 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
> 
> 
> 
> 
>