FOM: applications of proof theory

[wtait@ix.netcom.com]

Concerning Steve Simpson's (4/9)
>(i) The deemphasis of consistency proofs is not only my opinion.
>Feferman and other eminent proof-theorists have expressed similar
>opinions.  Indeed, are there any proof-theorists who still take the
>traditional view?  (By the traditional view, I mean the view that
>consistency proofs are a principal reason to be interested in
>Gentzen-style ordinal analysis.)
>
>Would some of the other proof-theorists on the FOM list (Tait,
>Rathjen, Friedman, Pohlers, Takeuti, Sommer, Sieg, Buss, Kohlenbach,
>Pfeiffer, Fine, ...) care to commment on this matter?

I refer to my (3/31), where I expressed the problem for the extended 
Hilbert program (as I understood it) as: 

>to find a constructive interpretation (in some loose sense, an extension 
>of finitistic mathematics) of parts of classical mathematics.

Of course, understood this way, the motivation for proof theory depended 
on the belief that constructive methods are, in some sense, superior. 

Concerning Steve's
>In my posting of 1 Apr 1998 12:27:29, I wrote:
> > the ordinal analysis itself ... is very complicated and
> > therefore unconvincing with respect to consistency of the systems
> > considered.

I wrote

>**So for me, it wasn't the well-orderedness of the ordering of the natural 
>numbers which carried constructive conviction; it was the constructive 
>theory of iterated inductive definition and, in particular, the 
>constructive higher number classes. 


Bill Tait