[FOM] Godel's Theorems

[Andrew Boucher]

Harvey Friedman wrote:

> I looked at
>
> On Floyd and Putnam on Wittgenstein on Godel,  
> http://www.nd.edu/~tbays/papers/
>
> and
>
> http://staff.washington.edu/dalexand/Putnam%20Readings/Notorious.pdf
>
> I have some specific questions. Let PA be the usual Peano Arithmetic.
> Consider the claim
>
> *) there is a true sentence in the language of PA which is not 
> provable in PA.
>
> 1. Conventional wisdom is that this is now a fully established
> theorem of mathematics (or ordinary mathematics as currently
> practiced by the overwhelming majority of mathematicians). Is there
> agreement on this?
>
> 2. For those who do not agree, do they believe that *) is not a
> mathematical statement capable of mathematical proof? E.g., this
> could be on the grounds that they do not accept the usual
> mathematical definition of "true sentence in the language of PA".
>
> 3. For those who believe that *) is a mathematical statement capable
> of mathematical proof, but do not agree with 1. Do you see a flawed
> step in the mathematical proof of *)? E.g., that it uses some
> questionable inductions and/or definitions by recursion.

Perhaps a more unconventional view will be of interest.

I think it can be held that there is a distinction between PM and PA.  I 
would say that, while Godel's proof goes through for PA as normally 
understood, it needs a (minor?) addition to go through for PM. 
 Moreover, if one were to make a slight modification to PA, the proof 
would need a similar addition to go through as well.  That is, under a 
certain case, the Godel proposition may in fact be provable in PA even 
if PA (or something very much like PA) is consistent.  However, in this 
case *another* true proposition is unprovable.  So the theorem that 
there is *some* true, unprovable theorem still holds (for both PM and PA).

To clarify these assertions, note that PA is part of first-order logic, 
which is usually defined supposing the Ad Infinitum principle - there 
exists an always next of something (be it numbers, wffs, or proofs). 
 So, if A and B are wffs, the following are also supposed to be wffs: 
 (not A), (A and B), etc.  Thus e.g. (not A), (not (not A)), (not (not 
(not A))), ... ad infinitum are all wffs.  Similarly for terms and proofs.

However, it is easy to see that one can define PA in a modified 
first-order logic where Ad Infinitum is not pre-supposed.  One could 
say:  if A is a wff and (not A) exists, then (not A) is a wff. Or one 
could phrase it in the other direction:  A is a wff if there exists B 
such that A is (not B), or there exists B and C such that A is (B and 
C), etc.

PM never did define what a wff was, so its construction cannot be said 
to pre-suppose Ad Infinitum.  This is what distinguishes it from the 
normal specification of PA.  However, as just pointed out, PA can be 
modified so that it keeps its normal axioms, but now in a first-order 
language which is defined without supposing Ad Infinitum.

Now a Godel-type argument produces a proposition G, which can be held to 
say, "There does not exist a number representing a proof of G."  Or: 
 "For all numbers x, x is not a proof of G."  Write this as (x) ! 
Proof(x,g), where g represents the proposition G in PA.  (I have cut a 
corner here concerning g, but hopefully any troubled reader sees how to 
remedy this.)

Surely it is possible that:  G is true but there is a proof of G.  Godel 
reasoning, which says that it is not possible, goes as follows.  If 
there is a proof of G, then there is a number p (or just a term x'''..., 
where there are p apostrophes after the x) such that |- Proof(p,g).  But 
|- ! Proof(p,g).  Hence PA is inconsistent.

Evidently, the proof, at least as stated (but perhaps there is a fix?) 
relies on Ad Infinitum.  Just because there is a proof of G (with length 
n) does not, at least without Ad Infinitum, imply that there must exist 
the much bigger number (or the much bigger term) which Godel uses to 
code the proof.  So rather than conclude that PA is inconstent, one may 
alternatively conclude that Ad Infinitum is not true.

So strictly Godel has left out the case where Ad Infinitum does not 
hold, where there are bounds to existence, such as a maximum number M. 
 There are perhaps many ways of handling this, but one reasonable way 
would be to suppose that there are wffs, propositions and proofs so long 
as they are of length M or less; otherwise not.  In any case, supposing 
this is so, then it is trivial to construct a proposition of length as 
close to M as possible consisting of numerous repeated conjunctions of 
"0 = 0".  Then this proposition cannot be proven in PA under our 
supposition, because any proof would have to have length much bigger 
than M, contradicting its maximality.  But clearly the statement is true.

So incompleteness still holds, but perhaps our view of the result should 
change a little.