FOM: applications of proof theory
wtait at ix.netcom.com
Thu Apr 9 12:11:03 EDT 1998
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.
>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.
>**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.
More information about the FOM