Conference rusure::math

    Can someone explain this a bit more?  What is "sum plus exponential"
    notation?
    
      John (who still says "1-1" and "onto")

	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

	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

    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

>>    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

	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

Path: ryn.esg.dec.com!shlump.nac.dec.com!bacchus.pa.dec.com!wsl.dec.com!heiney
From: heiney@wsl.dec.com (Bob Heiney)
Newsgroups: sci.math
Subject: Re: George Boolos' Mistake
Message-ID: <1990Nov9.084543@wsl.dec.com>
Date: 9 Nov 90 16:45:43 GMT
References: <45100038@uxa.cso.uiuc.edu> <45100040@uxa.cso.uiuc.edu>
Sender: news@wrl.dec.com (News)
Reply-To: heiney@dec.com (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.

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

    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

Path: ryn.esg.dec.com!shlump.nac.dec.com!bacchus.pa.dec.com!wsl.dec.com!heiney
From: heiney@wsl.dec.com (Bob Heiney)
Newsgroups: sci.math
Subject: Re: George Boolos' Mistake
Keywords: typo
Message-ID: <1990Nov9.174538@wsl.dec.com>
Date: 10 Nov 90 01:45:38 GMT
References: <45100038@uxa.cso.uiuc.edu> <45100040@uxa.cso.uiuc.edu> <1990Nov9.084543@wsl.dec.com>
Sender: news@wrl.dec.com (News)
Reply-To: heiney@dec.com (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

>>    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

    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

    re .12:
    
    Tsk, tsk.  You are assuming your conclusion.  Contradictory statements
    are perfectly acceptable in inconsistent systems.
    
    --  Barry