[FOM] Discussion of Gödel's beliefs

[Colin McLarty]

> On 05/18/2011 07:14 PM, Martin Davis wrote:
>>  .... (with much else) ...
>> Discussion of Gödel's beliefs should take note of the fact that he himself offered another proof of con(PA) via the equivalent con(HA) - his "Dialecta" interpretation.
>>

Richard Heck <rgheck at brown.edu>

wrote this (and much else) in a reply:

> Presumably Gödel thought, then, that we had some other way of knowing that HA is consistent?

No, I think he did not.  He thought it interesting to explore
intuitionism formally.  Here he showed a genuinely interesting
relation: intuitionistic arithmetic formalized as HA is equiconsistent
with PA.

In terms of foundations, Brouwer sometimes (though not always) claimed
his intuituitionism was safer from contradiction than what he
(sometimes) called formalism.  Godel took his result to show this is
not true on the level of arithmetic if the intuitionist accepts HA.

best, Colin