[FOM] Attack/defense on Godel

[Karlis Podnieks]

----- Original Message -----
From: "Harvey Friedman" <friedman at math.ohio-state.edu>
To: <fom at cs.nyu.edu>
Sent: Saturday, May 03, 2003 10:21 AM
Subject: [FOM] Attack/defense on Godel

...
> *If PA is consistent then PA does not prove that PA is consistent.
> Furthermore, this is proved within a very weak fragment of PA.*
>
> The attack goes like this.
>
> #Godel shows that some particular formal sentence A that is clearly
> related to the assertion that PA is consistent, is not provable in PA.
...


I would propose to refine these statements by separating the pure
mathematical contents of Godel's proof.

Godel's second theorem (for PA) depends:

a) On some natural number coding of PA-formulas. Let us use _F_ to denote
the code of the formula F.

b) On some formula Pr(x), which satisfies the well-known Hilbert-Bernays
derivability conditions:

For any PA-formulas F, G:

H1) If PA proves F, then PA proves Pr(_F_).

H2) PA proves Pr(_F_) -> Pr(_Pr(_F_)_).

H3) PA proves Pr(_F_) & Pr(_F->G_) -> Pr(_G_).

G o d e l ' s  s e c o n d  t h e o r e m (provable in a very weak fragment
of PA). There is an algorithm, allowing, for any such coding, and any such
formula Pr(x), to convert any PA-proof of the formula ~Pr(_0=1_) into a
PA-proof of a contradiction.

Thus, the only point to attack seems to be:

If we had a "finite" consistency proof for PA, could we derive from it a
PA-proof of the formula ~Pr(_0=1_)?

Karlis Podnieks
www.ltn.lv/~podnieks
Institute of Mathematics and Computer Science
University of Latvia