[FOM] Godel's Theorems
Andrew Boucher
Helene.Boucher at wanadoo.fr
Sat May 3 17:28:05 EDT 2003
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.
More information about the FOM
mailing list