[FOM] Proof "from the book"

[charles silver]

> Somewhere in Gödel's recollections (either in the Wang volumes, or
in the
> Collected Works, or in Feferman's recent book), he says that, in his
train
> of thought in 1930, he found the Indefinability Theorem first, and
then the
> first Incompleteness Theorem came slightly later. I can't remember
exactly
> where this is located. If I remember right, the gist is this. In
studying
> the consistency problem, Gödel wanted initially to give an
interpretation of
> second-order arithmetic within first-order arithmetic, and tried to
find a
> definition of (second-order!) arithmetic truth in the first-order
language.
> He discovered however that even first-order arithmetic truth is not
> arithmetically definable: i.e., what we now call Tarski's
Indefinability
> Theorem. But, as he also discovered, the concept "provable-in-F",
with F
> some fixed formal system, is arithmetically definable. This implies
that
> arithmetic truth is distinct from provable-in-F, for any formal
system F.
> This then gives us the quick proof of Gödel's first incompleteness
theorem.

    An explanation of Godel's thinking along the lines you indicate
can be found in Feferman's "Kurt Godel: Conviction and Caution", in
a book by Shanker, _Godel's Theorem_, 1988.

Charlie Silver