by Venanzio on December 15, 2012.
Tagged as: Lunches.
Today is the 100th anniversary of the birth of Reuben Goodstein. It's a very young age for someone immortalized by his voyages into the transfinite realm. A few months ago I talked about his theorem during an FP lunch. After some wait, here is a blog post about it.
Every natural number \(x\) can be put in Cantor normal form with respect with any base \(b\). First we write \(x\) in base \(b\), as a sum of powers of \(b\) multiplied by coefficients smaller than \(b\), for example, if \(x=68630377369258\) and \(b=3\) we have \[ 68630377369258 = 3^{29} + 3^7\cdot 2 + 1 \] We recursively write the exponents in the same base: \[ 29 = 3^3+2 = 3^{3^1}+2, \quad 7 = 3\cdot 2 +1 = 3^1\cdot 2+1 \] Thus the Cantor normal form of 68630377369258 in base 3 is: \[ 68630377369258 = 3^{3^{3^1}+2} + 3^{3^1\cdot 2+1}\cdot 2 + 1 \] So a Cantor normal form in base b expresses a number x as \(x = b^{c_0} \cdot a_0 + b^{c_1} \cdot a_1 + \cdots + b^{c_n} \cdot a_n\) where \(c_0\), ..., \(c_n\) are themselves Cantor normal forms.
Abstractly, generalizing over the base, it's a list of pairs of coefficients and exponents, which are themselves Cantor normal forms. Here it is expressed as a Haskell data type with functions converting between it and naturals with respect to a given base.
data Cantor = Cantor [(Integer, Cantor)]
deriving Show
-- (cantNum c b) computes the number with CNF c in base b
cantNum :: Cantor -> Integer -> Integer
cantNum (Cantor l) = cantNumL l
cantNumL :: [(Integer,Cantor)] -> Integer -> Integer
cantNumL [] _ = 0
cantNumL ((i,c):cs) base = i*base^(cantNum c base) + cantNumL cs base
-- (numCant b x) computes the CNF of x in base b
numCant :: Integer -> Integer -> Cantor
numCant base = Cantor . map (\(c,n) -> (c,numCant base n)) . (inBase base)
iLog :: Integer -> Integer -> Integer
iLog base n = iLogAux 0 1
where iLogAux i k = if (k*base)>n then i else iLogAux (i+1) (k*base)
inBase :: Integer -> Integer -> [(Integer,Integer)]
inBase base 0 = []
inBase base n = (n `div` k,i) : inBase base (n `rem` k)
where i = iLog base n
k = base^iNow take a Cantor normal form (CNF), change the base and recompute the number. For example, earlier we had the CNF of \(68630377369258\) in base 3. If we change the base to 4 we obtain \[ \begin{array}{l} 3^{3^{3^1}+2} + 3^{3^1\cdot 2+1}\cdot 2 + 1 \leadsto 4^{4^{4^1}+2} + 4^{4^1\cdot 2+1}\cdot 2 + 1\\ = 21452492687908155359318439997129353803966985312947829\\ \quad 40435769830995482244811767516288299887706704548430405\\ \quad 09730983776813660062124991145119142938384097869825. \end{array} \] The number has become much bigger, so let's make it smaller by subtracting one! \[ \begin{array}{l} 21452492687908155359318439997129353803966985312947829\\ 40435769830995482244811767516288299887706704548430405\\ 09730983776813660062124991145119142938384097869825 - 1 \\ = 21452492687908155359318439997129353803966985312947829 \\ \quad 40435769830995482244811767516288299887706704548430405 \\ \quad 09730983776813660062124991145119142938384097869824. \end{array} \] This is one step of the Goodstein procedure: find the Cantor normal form of a number \(x\) with respect to a base \(b_1\), change the base to \(b_2\), recompute the number and subtract one. The Goodstein sequence associated with a number is obtained by iterating the step increasing the base by one every time.
-- (goodstep b1 b2 n) first finds the CNF of n in base b1
-- then recomputes it in base b2 and subtracts 1
goodstep :: Integer -> Integer -> Integer -> Integer
goodstep base1 base2 n = cantNum (numCant base1 n) base2 - 1
-- Given a list of bases and a number n
-- we iterate the Goodstein step on n using all the bases
goodsteinGen :: [Integer] -> Integer -> [Integer]
goodsteinGen _ 0 = []
goodsteinGen (b1:b2:bs) n = n : goodsteinGen (b2:bs) (goodstep b1 b2 n)
goodstein :: Integer -> [Integer]
goodstein = goodsteinGen [2..]Let's compute a few:
*Main> goodstein 1
[1]
*Main> goodstein 2
[2,2,1]
*Main> goodstein 3
[3,3,3,2,1]Now do what I did: run it on 4 on your university's server and enjoy the screams of frustration of your colleagues when everything hangs up.
Although computing the Goodstein sequence for 4 is not feasible in practice, one can prove that it terminates.
The Goodstein procedure terminates on every starting number.
Although the theorem has a simple formulation and a short elegant proof, it cannot be proved in Peano Arithmetic: it essentially needs transfinite induction. It is probably the simplest result that is undecidable in PA.
The proof consists in associating an ordinal to every CNF, proving that every step in the process reduces this ordinal and therefore concluding that the process terminates by well-foundedness of the ordinal numbers.
Given a CNF, just compute it using the ordinal \(\omega\) (the ordinal associated to the natural numbers) as a base. The example that we've seen earlier gives: \[ \omega^{\omega^{\omega^1}+2} + \omega^{\omega^1\cdot 2+1}\cdot 2 + 1 \] (Addition and multiplication of transfinite ordinals are not commutative; to get the correct result the coefficients must be multiplied on the right and the terms must be in decreasing order.)
Now it is very easy to see that every step reduces the ordinal. If the CNF contained a non-zero term with the base raised to the power zero (that is, if the number is not divisible by the base) then the associated ordinal is a successor an the step will just give its predecessor. Otherwise there is a bigger decrease in the ordinal (depending on the base used).
In any case, we get a decreasing sequence of ordinals that will eventually reach zero. This proves the theorem.
Since every tower of exponentiation of the base is a valid CNF, we get that every ordinal smaller that \(\epsilon_0\) can occur: \[ \epsilon_0 = \sup \{\omega, \omega^\omega, \omega^{\omega^\omega}, \ldots\}. \] So we are doing \(\epsilon_0\)-induction, which goes beyond elementary arithmetic.