FOM: Intuitionism (Tait)

[Neil Tennant]

On Tue, 18 Jun 2002, charles 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).   However, this is not a "proof," where "proof" is defined as a
> certain sequence of patterns inside a well-defined formal system.
> (Incidentally, this insight {that the undecidability of G constitutes a
> "proof of G outside the system"}has led a number of philosophers to draw
> various conclusions about the relationship between humans and formal
> systems.)

The proof that the Godel-sentence G for a formal system S is true (or: the
proof of the Godel-sentence G for a formal system S) is of course
formalizable in a suitable (proper) extension (call it S*) of S. It is an
interesting question what principles not in S are to be added so as to
obtain S*, with an eye to proving, in S*, a formal proof recognizably
preserving the structure of the informal proof of G as given in the
so-called "semantical argument" for the truth of G. In the following paper
I make the case that the best new principle to adopt is the uniform
reflection principle for S for primitive recursive sentences, and show
that the resulting S*-proof of G makes no use of a truth-predicate, and
hence is acceptable to the deflationist.

'Deflationism and the Godel-Phenomena', Mind Vol. 111, 443, July 2002,
pp. 551-582.

Neil Tennant