| T.R | Title | User | Personal
Name | Date | Lines |
|---|
| 1327.1 | Terminology check | VMSDEV::HALLYB | The Smart Money was on Goliath | Wed Nov 07 1990 12:56 | 4 |
| Can someone explain this a bit more? What is "sum plus exponential"
notation?
John (who still says "1-1" and "onto")
|
| 1327.2 | | GUESS::DERAMO | Dan D'Eramo | Wed Nov 07 1990 15:45 | 47 |
| Let the initial number be 11.
In the first step, you subtract 1 (getting 10) and
write this as
10 = 2^3 + 2^1 = 2^(2^1 + 2^0) + 2^(2^0)
= 2^(2^(2^0) + 2^0) + 2^(2^0)
Now you replace the 2's with 3's to get
3^(3^(3^0) + 3^0) + 3^(3^0)
= 3^(3^1 + 1) + 3^1
= 3^4 + 3
= 84
and subtract one and write in this style (using 3 as a base
instead of 2). This might be faster if you forget about
crunching it down to 84 and just evaluate the last term of
the sum, subtract one from it and convert that back. Here
that gives leading terms + 3^1 - 1 = leading terms + 2
= leading terms + 3^0 + 3^0, for
First step: 11
Second step: 10 = 2^(2^(2^0) + 2^0) + 2^(2^0)
Third step: 3^(3^(3^0) + 3^0) + 3^0 + 3^0 (happens to be 83)
continuing would give
Fourth step: 4^(4^(4^0) + 4^0) + 4^0 (happens to be ???)
Fifth step: 5^(5^(5^0) + 5^0)
Sixth step: Here, the complicated leading term is the last term...
The fifth step value was 5^(5^1 + 1) = 5^6 = 15625,
so the sixth step is 15624 written in the above notation
using 6 as the base, which is
7776 + 7776 + 73
6^5 + 6^5 + 6^2 + 6^2 + 6^0
6^(6^0 + 6^0 + 6^0 + 6^0 + 6^0)
+ 6^(6^0 + 6^0 + 6^0 + 6^0 + 6^0) + 6^(6^0 + 6^0)
+ 6^(6^0 + 6^0) + 6^0
Seventh step: it is easy to subtract the one this time, yielding
7^(7^0 + 7^0 + 7^0 + 7^0 + 7^0)
+ 7^(7^0 + 7^0 + 7^0 + 7^0 + 7^0) + 7^(7^0 + 7^0)
+ 7^(7^0 + 7^0)
etc.
Dan
|
| 1327.3 | | GUESS::DERAMO | Dan D'Eramo | Wed Nov 07 1990 17:36 | 35 |
| If at each stage you replace the base number (of the two
numbers you can use in the representation, the one that
isn't zero) with omega (I'll use the symbol "w") then you
get, starting from the (what .-1 labels the) second step
w^(w^w^0 + w^0) + w^w^0
w^(w^w^0 + w^0) + w^0 + w^0
w^(w^w^0 + w^0) + w^0
w^(w^w^0 + w^0)
w^(w^0 + w^0 + w^0 + w^0 + w^0) + w^(w^0 + w^0 + w^0 + w^0 + w^0)
+ w^(w^0 + w^0) + w^(w^0 + w^0) + w^0
w^(w^0 + w^0 + w^0 + w^0 + w^0) + w^(w^0 + w^0 + w^0 + w^0 + w^0)
+ w^(w^0 + w^0) + w^(w^0 + w^0
etc.
(That's ordinal exponentiation, by the way.)
This is a descending sequence of ordinals less than
epsilon = lim w, w^w, w^(w^w), w^(w^(w^w)), ...
0
= the least fixed point of x -> w^x
and as a descending sequence from a well-ordered set it is finite.
So the process stops, but takes so long that you can't prove it
stops in PA.
Dan
|
| 1327.4 | Your basic non-intuitive problem, I'd say | VMSDEV::HALLYB | The Smart Money was on Goliath | Thu Nov 08 1990 11:43 | 9 |
| Thanks for the explanation, Dan. Looks like the arithmetic is a
tiny bit more complicated than the hailstone ("3N+1") problem.
0
I assume by "terminate" they mean you end up with an expression N = 1
at some point. It's a bit hard for me to see how that could happen.
In fact, it's hard to believe the sequence ever decreases, given the
simple example 11, 83, 1025, 15625 in .2
John
|
| 1327.5 | | GUESS::DERAMO | Dan D'Eramo | Thu Nov 08 1990 13:11 | 40 |
| >> In fact, it's hard to believe the sequence ever decreases, given the
>> simple example 11, 83, 1025, 15625 in .2
If you write out the expressions largest to smallest like
in .2, you see that:
a) the base increasing by one each time doesn't
affect the form of the expression
b) except for the substitution of a base that is
one larger, each step either drops the last
term (when it is base^0) or reduces the complexity
of the last term, as in .2 going from the fifth
to the sixth step:
5^(5^(5^0) + 5^0)
(the leading term is raised to a power which
itself contains nested exponentiations)
6^(6^0 + 6^0 + 6^0 + 6^0 + 6^0)
+ 6^(6^0 + 6^0 + 6^0 + 6^0 + 6^0) + 6^(6^0 + 6^0)
+ 6^(6^0 + 6^0) + 6^0
(the leading terms are raised to a power
which is a simple sum of base^0 terms)
The increasing base merely causes later steps to include
increasingly longer sums when they break a complicated
term down. For example, say, 16 with base two is 2^4 = 2^(2^2)
= 2^(2^(2^1)) = 2^(2^(2^(2^0))), but in base three is
16 = 3^2 + 3 + 3 = 1 = 3^(3^0 + 3^0) + 3^(3^0) + 3^(3^0) + 3^0,
which is "simpler" (less nested) but has more of those
simpler terms added in. With base twenty it would be even
longer, a sum of sixteen 20^0 terms. All these extra
little terms get chopped off one at a time, serving only
to increase the base each time and delaying when you get
to break down a more complicated term.
Dan
|
| 1327.6 | correction to my earlier replies | GUESS::DERAMO | Dan D'Eramo | Fri Nov 09 1990 22:37 | 94 |
| The way I worked the example out in .2 was incorrect.
>> .0
>> Consider the following procedure: take a number. rewrite it in "sum
>> plus exponential" notation in terms only of 0's and 2's. Subtract one
>> from this expression, writing the result in 0's and 2's. Replace all
>> 2's with 3's. Evaluate this new (possibly larger) expression.
>> Subtract 1. Rewrite in "sum and exponential" notation, using only 0's
>> and 3's. replace all 3's with 4's. Continue.
>> .2
>> Let the initial number be 11.
>>
>> In the first step, you subtract 1 (getting 10) and
>> write this as
>>
>> 10 = 2^3 + 2^1 = 2^(2^1 + 2^0) + 2^(2^0)
>> = 2^(2^(2^0) + 2^0) + 2^(2^0)
>> [...]
Well, actually, starting with 11 the first step had you writing
11 as 8 + 2 + 1 = 2^3 + 2^1 + 2^0 = 2^(2 + 1) + 2^(2^0) + 2^0
= ... = 2^(2^(2^0) + 2^0) + 2^(2^0) + 2^0. Then subtracting
one just dropped the last term. Showing the steps this way, you
can do most of the work symbolically, only needing to evaluate
the last term when there are no more base^0 terms to chop off,
or if you want to see what the numbers actually are. I did that
afterwards for some of them and put the results after the exclamation
points below:
11 ==> The initial number must be broken down symbolically
(as shown above), the result was
2^(2^(2^0) + 2^0) + 2^(2^0) + 2^0 ! 11
subtract one ==> 2^(2^(2^0) + 2^0) + 2^(2^0) ! 10
increment base ==> 3^(3^(3^0) + 3^0) + 3^(3^0) ! 84
subtract one ==> The trailing term is 3^(3^0) = 3^1 = 3, subtracting
one leaves 2, which must be broken down symbolically
as before and appended to the leading terms, yielding
3^(3^(3^0) + 3^0) + 3^0 + 3^0 ! 83
increment base ==> 4^(4^(4^0) + 4^0) + 4^0 + 4^0 ! 1026
subtract one ==> 4^(4^(4^0) + 4^0) + 4^0 ! 1025
increment base ==> 5^(5^(5^0) + 5^0) + 5^0 ! 15626
subtract one ==> 5^(5^(5^0) + 5^0) ! 15625
increment base ==> 6^(6^(6^0) + 6^0) ! 279936
subtract one ==> Here the last term is the only term and
evaluates to 6^7. Subtracting one leaves
(6^6 + 6^5 + ... 6 + 1) * 5, where the "* 5"
is expressed by adding in that term 5 times.
6^6 is 6^(6^0), 6^5 is 6^(6^0 + ... 6^0), etc.,
which when put all together yields
6^(6^0) + [four more of those]
+ 6^(6^0 + 6^0 + 6^0 + 6^0 + 6^0) + [four more of those]
+ 6^(6^0 + 6^0 + 6^0 + 6^0) + [four more of those]
+ 6^(6^0 + 6^0 + 6^0) + [four more of those]
+ 6^(6^0 + 6^0) + [four more of those]
+ 6^(6^0) + [four more of those]
+ 6^0 + [four more of those] ! 279935
etc.
Since there are five trailing 6^0 terms the next couple of
"subtract one" steps will be simple, consisting of dropping
trailing 7^0, 8^0, 9^0, 10^0, and 11^0 terms. Then the
next step after that will involve subtracting one from
the fifth 12^(12^0) term. That is 12^(12^0) = 12^1 = 12,
so the subtraction will result in
==> 12^(12^0) + [four more of those]
+ 12^(12^0 + 12^0 + 12^0 + 12^0 + 12^0) + [four more of these]
+ 12^(12^0 + 12^0 + 12^0 + 12^0) + [four more of these]
+ 12^(12^0 + 12^0 + 12^0) + [four more of these]
+ 12^(12^0 + 12^0) + [four more of these]
+ 12^(12^0) + [three more of these]
+ 12^0 + [ten more of these]
The next eleven "subtract one" steps will drop off trailing
13^0, 14^0, ..., and 23^0 terms before having to subtract one
from the last of four 24^(24^0) terms. That will leave
twenty-three trailing 24^0's, so the next twenty-three "subtract
one" steps will drop off a trailing 25^0, ..., 47^0. There follows
a subtraction from the last of three 48^(48^0) terms, ..., a
subtraction from the last of two 96^(96^0) terms, ..., a subtraction
from the only 192^(192^0) term, ..., a subtraction from the
fifth 384^(384^0 + 384^0) term. That will leave at the end
383 terms of 384^(384^0) followed by 383 terms of 384^0. After
grinding through all of that there will still be four more
n^(n^0 + n^0) terms to deal with, before you get to the five
n^(n^0 + n^0 + n^0) terms. Etc.
The numbers will get very large, but you can see that progress
is being made (albeit more and more slowly) and the process will
eventually terminate.
Dan
|
| 1327.7 | | GUESS::DERAMO | Dan D'Eramo | Fri Nov 09 1990 23:29 | 73 |
| Path: ryn.esg.dec.com!shlump.nac.dec.com!bacchus.pa.dec.com!wsl.dec.com!heiney
From: [email protected] (Bob Heiney)
Newsgroups: sci.math
Subject: Re: George Boolos' Mistake
Message-ID: <[email protected]>
Date: 9 Nov 90 16:45:43 GMT
References: <[email protected]> <[email protected]>
Sender: [email protected] (News)
Reply-To: [email protected] (Bob Heiney)
Organization: DEC US Worksystem Sales
Lines: 59
Another example of a theorem of arithmetic that cannot
be proven arithmetically (i.e. a theorem about finite
integers that can't be proven by PA) is Goodstein's Theorem.
What I'll sketch below was proven to be true be Goodstein
in 1944 using infinite ordinals in the proof. In 1981,
Kirby and Paris proved that Goodstein's Theorem implies
the consistency of PA, thus by Goedel's Second Incompleteness
Theorem, PA can't prove Goodstein's Theorem.
The presentation below is taken from [Henle]
First, let's define "superbase 2". Take a number and write it
in base 2. Take 23 as an example
23 (base 10) = 10111 (base 2)
The base 2 representation is shorthand for the sum
(1) 2^4 + 2^2 + 2^1 + 2^0
In superbase 2, all numbers greater than 2 in a sum like above
must be rewritten as a sum of powers of two. So (1) becomes
(2) 2^(2^2) + 2^2 + 2^1 + 2^0
Note this can get nastier:
514 = 2^9 + 2
= 2^(2^3+1) + 2
= 2^(2^(2+1)+1) + 2
[note: this isn't the same as
I had been doing it. -- Dan]
Now, the same principle applies to superbase 3, 4, etc.
Theorem (Goodstein, Kirby, Paris):
Take any natural number, m, and write it in
superbase 2.
Replace all the '2's with '3's. Subtract 1.
Rewrite in superbase 3.
Replace all the '3's with '4's. Subtract 1.
Rewrite in superbase 4.
...
For every m, there is a natural number n, such
that after n iterations of the above process, you
will reach zero. (!).
Warning: Don't try this on your computer! It will work OK
for m<=4, but although it takes 5 steps to get 3 to go
to zero, it takes something like
3 * 2^(402653211)-2 steps
[presumably for m=5 -- Dan]
[Henle86]: Henle, James M, "An Outline of Set Theory",
Springer-Verlag, 1986. A "prove it yourself" approach
to ZF set theory and Goodstein's theorem in particular.
|
| 1327.8 | almost the same result for 5 as .-1 | GUESS::DERAMO | Dan D'Eramo | Sun Nov 11 1990 00:41 | 184 |
| 1 ==> 2^0 ! 1
subtract one ==> 0 ! 0
2 ==> 2^(2^0) ! 2
subtract one ==> 2^0 ! 1
increment base ==> 3^0 ! 1
subtract one ==> 0 ! 0
3 ==> 2^(2^0) + 2^0 ! 3
subtract one ==> 2^(2^0) ! 2
increment base ==> 3^(3^0) ! 3
subtract one ==> 3^0 + 3^0 ! 2
increment base ==> 4^0 + 4^0 ! 2
subtract one ==> 4^0 ! 1
increment base ==> 5^0 ! 1
subtract one ==> 0 ! 0
4 ==> 2^(2^(2^0)) ! 4
subtract one ==> 2^(2^0) + 2^0 ! 3
increment base ==> 3^(3^0) + 3^0 ! 4
subtract one ==> 3^(3^0) ! 3
increment base ==> 4^(4^0) ! 4
subtract one ==> 4^0 + 4^0 + 4^0 ! 3
increment base ==> 5^0 + 5^0 + 5^0 ! 3
subtract one ==> 5^0 + 5^0 ! 2
increment base ==> 6^0 + 6^0 ! 2
subtract one ==> 6^0 ! 1
increment base ==> 7^0 ! 1
subtract one ==> 0 ! 0
5 ==> 2^(2^(2^0)) + 2^0 ! 5
subtract one ==> 2^(2^(2^0)) ! 4
increment base ==> 3^(3^(3^0)) ! 27
subtract one ==> 3^(3^0 + 3^0) + 3^(3^0 + 3^0) ! 26
+ 3^(3^0) + 3^(3^0) + 3^0 + 3^0
increment base ==> 4^(4^0 + 4^0) + 4^(4^0 + 4^0) ! 42
+ 4^(4^0) + 4^(4^0) + 4^0 + 4^0
subtract one ==> 4^(4^0 + 4^0) + 4^(4^0 + 4^0) ! 41
+ 4^(4^0) + 4^(4^0) + 4^0
increment base ==> 5^(5^0 + 5^0) + 5^(5^0 + 5^0) ! 61
+ 5^(5^0) + 5^(5^0) + 5^0
subtract one ==> 5^(5^0 + 5^0) + 5^(5^0 + 5^0) ! 60
+ 5^(5^0) + 5^(5^0)
increment base ==> 6^(6^0 + 6^0) + 6^(6^0 + 6^0) ! 84
+ 6^(6^0) + 6^(6^0)
subtract one ==> 6^(6^0 + 6^0) + 6^(6^0 + 6^0) ! 83
+ 6^(6^0) + 6^0 + 6^0 + 6^0 + 6^0
+ 6^0
increment base ==> 7^(7^0 + 7^0) + 7^(7^0 + 7^0) ! 110
+ 7^(7^0) + 7^0 + 7^0 + 7^0 + 7^0
+ 7^0
subtract one ==> 7^(7^0 + 7^0) + 7^(7^0 + 7^0) ! 109
+ 7^(7^0) + 7^0 + 7^0 + 7^0 + 7^0
increment base ==> 8^(8^0 + 8^0) + 8^(8^0 + 8^0) ! 140
+ 8^(8^0) + 8^0 + 8^0 + 8^0 + 8^0
subtract one ==> 8^(8^0 + 8^0) + 8^(8^0 + 8^0) ! 139
+ 8^(8^0) + 8^0 + 8^0 + 8^0
increment base ==> 9^(9^0 + 9^0) + 9^(9^0 + 9^0) ! 174
+ 9^(9^0) + 9^0 + 9^0 + 9^0
subtract one ==> 9^(9^0 + 9^0) + 9^(9^0 + 9^0) ! 173
+ 9^(9^0) + 9^0 + 9^0
increment base ==> 10^(10^0 + 10^0) + 10^(10^0 + 10^0) ! 222
+ 10^(10^0) + 10^0 + 10^0
subtract one ==> 10^(10^0 + 10^0) + 10^(10^0 + 10^0) ! 221
+ 10^(10^0) + 10^0
increment base ==> 11^(11^0 + 11^0) + 11^(11^0 + 11^0) ! 254
+ 11^(11^0) + 11^0
subtract one ==> 11^(11^0 + 11^0) + 11^(11^0 + 11^0) ! 253
+ 11^(11^0)
increment base ==> 12^(12^0 + 12^0) + 12^(12^0 + 12^0) ! 300
+ 12^(12^0)
subtract one ==> 12^(12^0 + 12^0) + 12^(12^0 + 12^0) ! 299
+ 12^0 + 12^0 + 12^0 + 12^0 + 12^0
+ 12^0 + 12^0 + 12^0 + 12^0 + 12^0
+ 12^0
.
.
.
increment base ==> 24^(24^0 + 24^0) + 24^(24^0 + 24^0) ! 1152
subtract one ==> 24^(24^0 + 24^0) + 24^(24^0) ! 1151
+ 24^(24^0) + 24^(24^0) + 24^(24^0)
+ 24^(24^0) + 24^(24^0) + 24^(24^0)
+ 24^(24^0) + 24^(24^0) + 24^(24^0)
+ 24^(24^0) + 24^(24^0) + 24^(24^0)
+ 24^(24^0) + 24^(24^0) + 24^(24^0)
+ 24^(24^0) + 24^(24^0) + 24^(24^0)
+ 24^(24^0) + 24^(24^0) + 24^(24^0)
+ 24^(24^0) + 24^0 + 24^0 + 24^0
+ 24^0 + 24^0 + 24^0 + 24^0 + 24^0
+ 24^0 + 24^0 + 24^0 + 24^0 + 24^0
+ 24^0 + 24^0 + 24^0 + 24^0 + 24^0
+ 24^0 + 24^0 + 24^0 + 24^0 + 24^0
.
.
.
increment base ==> 48^(48^0 + 48^0) + 48^(48^0) ! 3408
+ 48^(48^0) + 48^(48^0) + 48^(48^0)
+ 48^(48^0) + 48^(48^0) + 48^(48^0)
+ 48^(48^0) + 48^(48^0) + 48^(48^0)
+ 48^(48^0) + 48^(48^0) + 48^(48^0)
+ 48^(48^0) + 48^(48^0) + 48^(48^0)
+ 48^(48^0) + 48^(48^0) + 48^(48^0)
+ 48^(48^0) + 48^(48^0) + 48^(48^0)
+ 48^(48^0)
subtract one ==> 48^(48^0 + 48^0) + 48^(48^0) ! 3407
+ 48^(48^0) + 48^(48^0) + 48^(48^0)
+ 48^(48^0) + 48^(48^0) + 48^(48^0)
+ 48^(48^0) + 48^(48^0) + 48^(48^0)
+ 48^(48^0) + 48^(48^0) + 48^(48^0)
+ 48^(48^0) + 48^(48^0) + 48^(48^0)
+ 48^(48^0) + 48^(48^0) + 48^(48^0)
+ 48^(48^0) + 48^(48^0) + 48^(48^0)
+ 48^0 + 48^0 + 48^0 + 48^0 + 48^0
+ 48^0 + 48^0 + 48^0 + 48^0 + 48^0
+ 48^0 + 48^0 + 48^0 + 48^0 + 48^0
+ 48^0 + 48^0 + 48^0 + 48^0 + 48^0
+ 48^0 + 48^0 + 48^0 + 48^0 + 48^0
+ 48^0 + 48^0 + 48^0 + 48^0 + 48^0
+ 48^0 + 48^0 + 48^0 + 48^0 + 48^0
+ 48^0 + 48^0 + 48^0 + 48^0 + 48^0
+ 48^0 + 48^0 + 48^0 + 48^0 + 48^0
+ 48^0 + 48^0
.
.
.
increment base ==> 96^(96^0 + 96^0) + 96^(96^0) ! 11328
+ 96^(96^0) + 96^(96^0) + 96^(96^0)
+ 96^(96^0) + 96^(96^0) + 96^(96^0)
+ 96^(96^0) + 96^(96^0) + 96^(96^0)
+ 96^(96^0) + 96^(96^0) + 96^(96^0)
+ 96^(96^0) + 96^(96^0) + 96^(96^0)
+ 96^(96^0) + 96^(96^0) + 96^(96^0)
+ 96^(96^0) + 96^(96^0) + 96^(96^0)
.
.
.
increment base ==> 201326592^(201326592^0 + 201326592^0) ! 40532396847661056
+ 201326592^(201326592^0)
subtract one ==> 201326592^(201326592^0 + 201326592^0) ! 40532396847661055
+ 201326592^0 [201326591 times]
.
.
.
increment base ==> 402653184^(402653184^0 + 402653184^0) ! 162129586585337856
subtract one ==> 402653184^(402653184^0) ! 162129586585337855
[402653183 times] + 402653184^0 [402653183 times]
Let's pause here, and rewrite this as
increment base ==> (3 * 2^27)^((3 * 2^27)^0 + (3 * 2^27)^0)
subtract one ==> (3 * 2^27)^((3 * 2^27)^0) [3 * 2^27 - 1 times]
+ (3 * 2^27)^0 [3 * 2^27 - 1 times]
.
.
.
increment base ==> (3 * 2^28)^((3 * 2^28)^0) [3 * 2^27 - 1 times]
subtract one ==> (3 * 2^28)^((3 * 2^28)^0) [3 * 2^27 - 2 times]
+ (3 * 2^28)^0 [3 * 2^28 - 1 times]
.
.
.
increment base ==> (3 * 2^29)^((3 * 2^29)^0) [3 * 2^27 - 1 times]
subtract one ==> (3 * 2^29)^((3 * 2^29)^0) [3 * 2^27 - 2 times]
+ (3 * 2^29)^0 [3 * 2^29 - 1 times]
.
.
.
increment base ==> (3 * 2^(27 + 3 * 2^27))^((3 * 2^(27 + 3 * 2^27))^0)
(3 * 2^402653211)^((3 * 2^402653211)^0)
! 3 * 2^402653211
subtract one ==> (3 * 2^402653211)^0 [3 * 2^402653211 - 1 times]
! 3 * 2^402653211 - 1
At this point, all of the terms are n^0, so we finish
rapidly, dropping the last term each time.
.
.
.
increment base ==> (3*2^402653212)^0 ! 1
subtract one ==> 0 ! 0
The sequence starting with 6 is left to the reader.
Dan
|
| 1327.9 | ?? !!! ?? | CHOVAX::YOUNG | The OOL's are not what they seem. | Sun Nov 11 1990 18:54 | 7 |
| Re .7:
Dan, how on earth does Goodsteins theorem implie the consistency of
Peano's Axioms? I find this to be, by far, the most suprising
statement in the whole topic.
-- Barry
|
| 1327.10 | usenet correction | GUESS::DERAMO | Dan D'Eramo | Mon Nov 12 1990 09:25 | 40 |
| Path: ryn.esg.dec.com!shlump.nac.dec.com!bacchus.pa.dec.com!wsl.dec.com!heiney
From: [email protected] (Bob Heiney)
Newsgroups: sci.math
Subject: Re: George Boolos' Mistake
Keywords: typo
Message-ID: <[email protected]>
Date: 10 Nov 90 01:45:38 GMT
References: <[email protected]> <[email protected]> <[email protected]>
Sender: [email protected] (News)
Reply-To: [email protected] (Bob Heiney)
Organization: DEC US Worksystem Sales
Lines: 27
I want to clarify the last bit of my posting on
Goodstein's theorem. I was interrupted from my posting
by my job ( :-) ) and didn't finish the last bit correctly.
What I wrote:
>Warning: Don't try this on your computer! It will work OK
> for m<=4, but although it takes 5 steps to get 3 to go
> to zero, it takes something like
>
> 3 * 2^(402653211)-2 steps
What I meant:
Warning: Don't try this on your computer! It will work OK
for m<4, because although it takes 5 steps to get m=3 to go
to zero, it takes something like
3 * 2^(402653211)-2 steps
to get m=4 to go to zero.
As Henle points out, this is a very large number. :-).
/Bob
|
| 1327.11 | | GUESS::DERAMO | Dan D'Eramo | Mon Nov 12 1990 09:51 | 53 |
| >> Dan, how on earth does Goodsteins theorem implie the consistency of
>> Peano's Axioms? I find this to be, by far, the most suprising
>> statement in the whole topic.
>>
>> -- Barry
I am kind of hazy on this stuff, as I don't have any of the
four sources I am remembering this from, but read them in a
library, the most recent maybe two or three years ago, the
least recent ten to twelve years ago.
Gentzen's proof of the consistency of Peano Arithmetic showed
(1) how to assign to each proof from PA an ordinal number less than
"\epsilon \sub 0", which is the least fixed point of the map
x -> \omega ^ x (ordinal exponentiation), equivalently it is
the limit of \omega, \omega ^ \omega, \omega ^ (\omega ^ \omega), ....
(2) that to each proof of a contradiction from PA, there is another
proof to which is assigned a smaller ordinal number
Thus a proof of a contradiction from PA would imply an infinite
descending sequence of ordinals, which is impossible. Therefore
PA is consistent.
The proof shows that "\epsilon \sub 0" is a measure of the
"strength" of the axioms of PA. The well-ordering of that
ordinal cannot be expressed in PA in a way that PA proves
induction over well-ordered sequences of that length ...
otherwise PA would prove its own consistency, which by Godel's
second theorem it cannot do (if it is consistemt). Smaller
ordinals can be handled by PA. For example, the induction
scheme deals with the ordinal \omega, and you can define a
relation such as
x R y iff x is odd and y is even, or (x and y
have the same parity and x < y)
defining \omega * 2 and prove in PA every instance of induction over
R, i.e., (\forall x (\forall y (y R x ==> P(y)))) ==> \forall x P(x)
But you can't do this for the well-ordering \epsilon \sub 0.
PA can capture Gentzen's proof to the extent that a proof of
a contradiction yields another proof of a contradiction with a
smaller ordinal number. Apparently Goodstein's sentence + PA
can now prove that descending sequences from \epsilon \sub 0
are finite, which is enough to contradict the existence of an
infinite sequence of proofs (of a contradiction) with decreasing
ordinal tags, thus showing Con PA (but of course, by Godel's
second theorem, Goodstein's sentence + PA if it is consistent
cannot prove Con (Goodstein's sentence + PA).
Dan
|
| 1327.12 | | JARETH::EDP | Always mount a scratch monkey. | Tue Nov 13 1990 08:12 | 10 |
| Re .9:
I would think proving Peano's Axioms consistent would be simple:
Suppose the Peano Axioms are inconsistent. By the definition of
inconsistency, there is some statement P for which P and ~P. Since
this is a contradiction, the supposition must be false. QED. :-)
-- edp
|
| 1327.13 | Yes and No. | CHOSRV::YOUNG | The OOL's are not what they seem. | Tue Nov 13 1990 11:42 | 6 |
| re .12:
Tsk, tsk. You are assuming your conclusion. Contradictory statements
are perfectly acceptable in inconsistent systems.
-- Barry
|