FOM: Intuitionism (Tait)

[Miguel A. Lerma]

Sean C Stidd wrote:

 > Among those who thought this seems to have been Godel himself, who
 > included the following in the original 1931 proof:
 >
 > "From the remark that [R(q);q] says about itself that it is not provable
 > it follows at once that [R(q);q] is true, for [R(q);q] is indeed
 > unprovable (being undecidable).  Thus, the proposition that is
 > undecidable in the system PM still was decided by metamathematical
 > considerations."

I think it is often forgotten that the result is conditioned to
the consistency of the formal system in which we are working. 
For instance if we work in PA and if Con(PA) is the arithmetic
sentence "saying" that PA is consistent, then Godel arguments
prove that Con(PA) implies [R(q);q]. On the other hand metamathematical
considerations do not tell us that [R(q);q] is true, but that if
PA is consistent then [R(q);q] is true. We will never know whether
[R(q);q] is actually true more that we "know" that PA is consistent.


Miguel A. Lerma