FOM: Books, foundations, intuitionism, NF
wtait at ix.netcom.com
Tue Mar 10 13:09:58 EST 1998
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.
More information about the FOM