FOM: applications of proof theory

[Stephen G Simpson]

Bill Tait 9 Apr 98 11:11:03:
 > >to find a constructive interpretation (in some loose sense, an extension 
 > >of finitistic mathematics) of parts of classical mathematics.

OK.  But then, do you view such an interpretation as a consistency
proof?  My point is that it seems better to view it as a
proof-theoretic reduction and to formulate the result as a
conservation theorem.  Do you agree?  Or, how would you formulate it?

For example, you said:
 > >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. 

and I would like it better if you had stated a conservativity result,
along the lines of "classical ID_{<omega} is conservative over
intuitionistic ID_{<omega} for a certain class of sentences."  (I'm
not sure exactly what the right class of sentences is.)  Don't you
agree that this kind of formulation is more informative?

I guess my real point is that proof theory qua search for finitistic
consistency proofs a la Hilbert is dead and buried, as a result of
G"odel's 2nd incompleteness theorem.  So we need to look elsewhere for
foundationally significant applications of technical work in proof
theory.  My favorite places to look are: (1) combinatorial
independence results, (2) reductions formulated as conservation
theorems.  What are your favorite places to look?

-- Steve