From: wgd@zurich.ai.mit.edu (Bill Dubuque)
Newsgroups: sci.math
Subject: Re: Goedel's theorem: about anything in real world?
Date: 11 Dec 95 02:34:50
From: "Kenneth A. Regas"
Date: 10 Dec 1995 21:17:14 GMT
... What I'm getting at here is that G [Godel's undecidable
sentence] is not the kind of sentence that one would come up
against and be obliged to evaluate in the world of physical
phenomena. It seems to be purely a product of "formal systems."
It is my layman's understanding that Goedel's proof relies
upon constructing a proposition like G. In that case,
does Goedel's theorem have anything to say about "old
mathematics" the kind that scientists and engineers are
taught, wherein which "statements" such as G don't come up?
Yes, recent discoveries yield a number of so-called 'natural
independence' results that provide much more natural examples
of independence than does Godel's contrived example based upon
the liar paradox. See the bibliography below. In particular,
your question is essentially the title of Gina Kolata's
article "Does Godel's theorem matter to mathematics?",
referenced below.
As an example of such results, I'll sketch a simple example due
to Goodstein of a concrete number theoretic theorem whose proof
is independent of formal number theory (following [Sim]).
Let b be a positive integer >= 2. Any nonnegative integer n
can be written uniquely in base b representation:
n n
1 k
n = c b + ... + c b
1 k
where k >= 0, 0 < c < b, n > ... > n >= 0, for i = 1, ..., k.
i 1 k
For example the base 2 representation of 266 is
8 3
266 = 2 + 2 + 2
We may extend this by writing each of the exponents n , ..., n
1 k
in base b notation, then doing the same for each of the exponents
in the resulting representations, ... until the process stops.
This yields the so-called 'hereditary base b representation of n'
For example the hereditary base 2 representation of 266 is
2 + 1
2 2 + 1
266 = 2 + 2 + 2
Let B[b](n) be the nonnegative integer which results if we take the
hereditary base b representation of n and then syntactically replace
each b by b+1, i.e. B[b] is a base change operator that 'Bumps the Base'
from b up to b+1. For example bumping the base from 2 to 3 in the above
equation yields
3 + 1
3 3 + 1
B[2](266) = 3 + 3 + 3
Consider a sequence of integers obtained by repeatedly applying
the operation: bump the base then subtract one from the result.
For example, iteratively applying this operation to 266 yields
2 + 1
2 2 + 1
266[0]:= 2 + 2 + 2 = 266
3 + 1
3 3 + 1
266[1] = 3 + 3 + 3 - 1 = B[2](266[0]) - 1
3 + 1
3 3 + 1
= 3 + 3 + 2
4 + 1
4 4 + 1
266[2] = 4 + 4 + 1 = B[3](266[1]) - 1
5 + 1
5 5 + 1
266[3] = 5 + 5 = B[4](266[2]) - 1
6 + 1 .
6 6 + 1 .
266[4] = 6 + 6 - 1 .
7
using 6 - 1 = 10000000 - 1 = 5555555 in base 6
6 + 1
6 6 5
= 6 + 5 6 + 5 6 + ... + 5 6 + 5
7 + 1
7 7 5
266[5] = 7 + 5 7 + 5 7 + ... + 5 7 + 4
.
.
.
266[k+1] = ... = B[k+2](266[k]) - 1
In general, if we start this procedure at the integer n then
we obtain what is known as the Goodstein sequence starting at n.
More precisely, for each nonegative integer n we recursively define
a sequence of nonnegative integers n[0], n[1], ..., n[k], ... by
n[0] := n
[ B[k+2](n[k]) - 1 if n[k] > 0
n[k+1] := |
[ 0 if n[k] = 0
for all k >= 0.
If we examine the above Goodstein sequence for 266 numerically
we find that the sequence initially increases quite rapidly:
2^2^(2+1)+2^(2+1)+2 ~= 2^2^3 ~= 3 10^2
3^3^(3+1)+3^(3+1)+2 ~= 3^3^4 ~= 4 10^38
4^4^(4+1)+4^(4+1)+1 ~= 4^4^5 ~= 3 10^616
5^5^(5+1)+5^(5+1) ~= 5^5^6 ~= 3 10^10921
6^6^(6+1)+5*6^6+5*6^5+..+5*6+5 ~= 6^6^7 ~= 4 10^217832
7^7^(7+1)+5*7^7+5*7^5+..+5*7+4 ~= 7^7^8 ~= 1 10^4871822
8^8^(8+1)+5*8^8+5*8^5+..+5*8+3 ~= 8^8^9 ~= 2 10^121210686
9^9^(9+1)+5*9^9+5*9^5+..+5*9+2 ~= 9^9^10 ~= 5 10^3327237896
10^10^(10+1)+5*10^10+5*10^5+..+5*10+1 ~= 10^10^11 ~= 1 10^100000000000
Nevertheless, despite appearances, it can be proved that this
sequence converges to 0. In other words, 266[k] = 0 for all
sufficiently large k. This surprising result is due to Goodstein
(1944) who actually proved the same result for *all* Goodstein
sequences:
GOODSTEIN'S THEOREM. For all n there exists k such that n[k]=0.
In other words every Goodstein sequence converges to 0.
The secret underlying Goodstein's theorem is that the hereditary
expression of n in base b mimicks an ordinal notation for
ordinals less than eps[0]. For such ordinals, the base bumping
operation leaves the ordinal fixed whereas the subtraction of
one decreases the ordinal. But these ordinals are well-ordered
and this allows us to conclude that a Goodstein sequence
eventually converges to zero. Goodstein actually proved his
theorem for a general increasing base-bumping function f:N->N
(vs. f(b)=b+1 above) and he showed that convergence of all such
f-Goodstein sequences is equivalent to transfinite induction
below the ordinal eps[0].
One of the primary measures of strength for a system of logic is
the size of the largest ordinal for which transfinite induction
holds. It is a classical result of Gentzen that the consistency
of PA (Peano arithmetic, or formal number theory) can be proved
by transfinite induction on ordinals below eps[0]. But we know
from Godel's second incompleteness theorem that the consistency
of PA cannot be proved in PA. It follows that neither can
Goodstein's theorem be proved in PA. Thus we have an example of
a very simple concrete number theoretical statement in PA whose
proof is nonetheless independent of PA.
Another way to see Goodstein's theorem cannot be proved in PA
is to note that the sequence takes too long to terminate, e.g.
4[k] first reaches 0 for k = 3*(2^402653211-1) ~= 10^121210695
In general, if 'for all n there exists k such that P(n,k)' is
provable, then it must be witnessed by a provably computable
choice function F: 'for all n: P(n,F(n))'. But the problem
is that F(n) grows too rapidly to be provably computable in PA,
see [Smo] 1980 for details.
Goodstein's theorem was one of the first examples of so-called
'natural independence phenomena', which are considered by most
logicians as more natural than the metamathematical
incompleteness results first discovered by Godel. Other finite
combinatorial examples were discovered around the same time,
e.g. a finite form of Ramsey's theorem, and a finite form of
Kruskal's tree theorem, see [KiP], [Smo] and [Gal]. [Kip]
presents the Hercules vs. Hydra game which provides an
elementary example of a finite combinatorial tree theorem
closely related to the Goodstein example above.
Kruskal's tree theorem plays a fundamental role in computer
science because it is one of the main tools for showing that
certain orderings on trees are well-founded. These orderings
play a crucial role in proving the termination of rewrite rules
and the correctness of the Knuth-Bendix equational completion
procedures. See [Gal] for a survey of results in this area.
See the references below for further details, especially
Smorynski's papers. Start with Rucker's book if you know no
logic, then move on to Smorynski's papers, and then the others,
which are original research papers. For more recent work, see
the references cited in Gallier, especially to Friedman's school
of 'Reverse Mathematics', and see [JSL].
-Bill
[Gal] Gallier, Jean
What's so special about Kruskal's theorem and the ordinal Gamma[0]?
A survey of some results in proof theory, Ann. Pure and Applied Logic,
53 (1991) 199-260.
[HFR] Harrington, L.A. et.al. (editors)
Harvey Friedman's Research on the Foundations of Mathematics,
Elsevier 1985.
[KiP] Kirby, Laurie, and Paris, Jeff
Accessible independence results for Peano arithmetic, Bull. London
Math. Soc., 14 (1982), 285-293.
[JSL] The Journal of Symbolic Logic, v. 53, no. 2, 1988
This issue contains papers from the Symposium "Hilbert's
Program Sixty Years Later".
[Kol] Kolata, Gina
Does Godel's theorem matter to mathematics?, Science 218 11/19/1982,
779-780; reprinted in [HFR]
[Ruc] Rucker, Rudy
Infinity and The Mind, 1995, Princeton Univ. Press.
[Sim] Simpson, Stephen G.
Unprovable theorems and fast-growing functions,
Contemporary Math. 65 1987, 359-394.
[Smo] Smorynski, Craig (all three papers are reprinted in [HFR])
Some rapidly growing functions, Math. Intell., 2 1980, 149-154.
The Varieties of Arboreal Experience, Math. Intell., 4 1982, 182-188.
"Big" News from Archimedes to Friedman, Notices AMS, 30 1983, 251-256.
[Spe] Spencer, Joel
Large numbers and unprovable theorems,
Amer. Math. Monthly, Dec 1983, 669-675.