FOM: Intuitionism (Tait)

[Sean C Stidd]

C. Silver wrote:

>Frequently it is thought that the proof that neither Godel's sentence G
>("I am not provable") is provable nor is Not-G provable is *itself* a
>"proof" of G (namely that G is not provable).   The argument is that G
>*says* it's not provable, which is true.   (Not-G says it's provable, 
>which is false).

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."

Whether or not my being able to observe the truth of this sentence proves
that I'm not a machine - being inconsistent, I'm an uninteresting one in
any case - accepting this argument would seem to lead to broad questions
about what a proof is. For instance: if this argument is a proof, does
that mean the concept of proof-in-a-formal-system of suitable strength
can't capture some 'intuitive' notion of proof that transcends it? Or if
proof just is proof-in-a-system, does being able to 'observe' the truth
of this argument show that we have some kind of access to mathematical
truth that outstrips the reach of proof?

I don't think any of this is exactly relevant to the incompleteness
result proper, since you don't need to know that the sentence is true for
the semantics-syntax disconnect. (Because you've assumed bivalence &
excluded middle either the sentence or its negation will be true and
unprovable.) But two questions seem worth answering: (1) If Godel's
'metamathematical demonstration' cited above is one we ought to accept as
valid, what are the philosophical and/or mathematical consequences, if
any, beyond those of the incompleteness theorem of doing so? (2) If this
argument is not one we ought to accept, what is its principled dismissal?