[FOM] Attack/defense on Godel
Karlis Podnieks
Karlis.Podnieks at mii.lu.lv
Mon May 5 03:17:35 EDT 2003
----- 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
More information about the FOM
mailing list