FOM: Goedel and the rejection of intuitionism

[Charles Parsons]

>
>I don't know about *any* aspect; but Goedel did reject something that he
>believed to be a presupposition of intuitionistic logic, and that is the
>absolute notion of proof. (See his unpublished papers *1933o and *1938a in
>Volume III.) [I actually think that he was wrong here and that
>intuitionism no more presupposes the absoute notion of proof than his
>interpretation of arithmetic using functionals of higher type presupposes
>the absolute notion of function of a given type.]
>
>Bill Tait

Although this may not have been intended, Tait suggests that Goedel in the
two papers cited regarded an absolute notion of proof as an illegitimate
notion. But in both these papers, the focus is on the Hilbert program. What
is claimed about the notion of proof in *1933o is just that it "violates
the principle ... that the word 'any' can be applied only to those
totalities for which we have a finite procedure for generating their
elemments" (Works III 53). So that it wouldn't be admissible in the
"strictest form of constructive mathematics" (ibid. 51).

In *1938a, to be sure, Goedel's language is more severe, no doubt more
unguarded because it was a talk given to a private circle. But the stress
is still on constructivity; the objection to absolute proof is that it
violates requirements of constructivity. Still, he evidently thinks it
possible to set up plausible axioms for it and to prove theorems on the
basis of them, as in his own modal-logical interpretation of intuitionistic
logic (ibid. 100-01 or 1933f in Works I). And in the 1946 Princeton
remarks, he shows positive interest in an absolute notion of provability in
the classical context, although he doesn't explore it very far (Works II
151).

Harvey Friedman cites Goedel's post-war philosophical writings to argue
that he rejected intuitionism. Certainly, Goedel was no constructivist and
his philosophy was rather far from that of those who were, in particular
Brouwer. But one can press this too far. Goedel was not a constructivist in
the 1930's, but I want to say that he wasn't arguing that the intuitionist
notion of proof is illegitimate or meaningless, just that it doesn't offer
a constructive foundation for mathematics. And he didn't lose interest in
exploring intuitionist ideas later, in his interpretation of intuitionist
arithmetic by functionals of finite type and subsequent comments on that
interpretation. He may not have agreed with Vaughan Pratt that
intuitionistic logic is "no less meaningful a logic than classical", but I
think he did think there was an intuitive conception behind it that could
be developed and explored.

Charles Parsons