[FOM] Gödel's Incompleteness Theorems (Ken Kubota)

[Dana Scott]

My feeling is that Ken Kubota has perhaps misunderstood a basic feature 
of Gödel's proof.  His method of arithmetization using Gödel numbers shows 
that his proof can be carried out in PA = first-order arithmetic.  That is
surely a part of standard mathematics.

PA allows us to define primitive recursive functions and prove properties
by induction.  Gödel realized that by using Gödel numbers for syntax he
could define all typical languages AND their deduction rules using
primitive recursive functions.  Of course provability and consistency
need an extra quantifier (EXISTS for the first and ALL for the second).
In his second theorem he proved that the formal version of consistency
of PA cannot be proved in PA.  Later work shows that this fact needs a
stronger induction scheme on a transfinite well ordering relation on the 
natural numbers of order type epsilon_0.

The work of Paulson in no way in my opinion casts any doubt on these
results or contains any mistake.