FOM: Books, foundations, intuitionism, NF

[wtait@ix.netcom.com]

Torkel Franzen (torkel at sm.luth.se) 3/10 writes

>  I can't see that Godel rejects the absolute notion of proof in those
>papers. He argues that an intuitionistic interpretation does
>not yield a *finitary* consistency proof, since finitarily, "any"
>must be restricted to totalities generated by a rule, whereas the
>(assumed) totality of proofs is not generated by a rule. 

I agree, except that the issue is not `finitary', since what Goedel was 
considering was possible satisfactory extensions of finitism for 
Hilbert's program. E.g. his consistency proof for PA using the 
impredicative primitive recursive functions of finite type (which he 
seems to have had in mind in these early papers, at least as a project) 
is not finitist.

Bill Tait