A WALK WITH GOODSTEIN

Abstract

Goodstein’s principle is arguably the first purely number-theoretic statement known to be independent of Peano arithmetic. It involves sequences of natural numbers which at first appear to diverge, but eventually decrease to zero. These sequences are defined relative to a notation system based on exponentiation for the natural numbers. In this article, we provide a self-contained and modern analysis of Goodstein’s principle, obtaining some variations and improvements. We explore notions of optimality for notation systems and apply them to the classical Goodstein process and to a weaker variant based on multiplication rather than exponentiation. In particular, we introduce the notion of base-change maximality, and show how it leads to far-reaching extensions of Goodstein’s result. We moreover show that by varying the initial base of the Goodstein process, one readily obtains independence results for each of the fragments $\mathsf {I}\Sigma _n$ of Peano arithmetic.

1 Introduction

Ever since Gödel’s first incompleteness theorem [9], we know that Peano arithmetic ( $\mathsf {PA}$ ) cannot prove every true arithmetical statement. However, Gödel’s proof is based on a specifically constructed statement that can be argued to be artificial from the perspective of mainstream mathematics. Since then, several facts of a purely combinatorial or number-theoretic nature have been shown to be independent from $\mathsf {PA}$ [4, 5, 12–14, 18], but the oldest example is a theorem of Goodstein [10], although it was only shown to be independent much later by Kirby and Paris [15]; see [19] for a historical overview. Goodstein’s result will be the focus of this work.

Informally, one writes a natural number m in hereditary base $2$ , meaning that m is represented in base $2$ in the usual way, then so is each exponent that appears, and so on. A precise definition will be given later, but for example, $m=20$ would be written as $2^{2^2} + 2^2 $ . The Goodstein process based on m is a sequence $(\mathrm {G}_{i}(m))_{i <\alpha }$ with $\alpha \leq \infty $ , such that $\mathrm {G}_{0}(m) = m$ and, if $\mathrm {G}_{i}(m)$ is defined and positive, $\mathrm {G}_{{i+1}}(m)$ is obtained by first writing $ \mathrm {G}_{i}(m) $ in hereditary base $i+2$ , then replacing every instance of $i+2$ by $i+3$ , and finally subtracting $1$ . The sequence terminates if it reaches zero. Thus, for example,

$$\begin{align*}\mathrm{G}_{1}(20) = 3^{3^3} +3^3 - 1 = 3^{3^3} + 3^2\cdot 2 + 3\cdot 2 +2.\end{align*}$$

This number is already large enough to be rather cumbersome to write out and, in fact, the sequence will grow very rapidly for some time. This should make Goodstein’s principle quite surprising: for any m that we start with, there will be a value of i such that $\mathrm {G}_{i}(m)=0$ . The proof uses transfinite induction, and Kirby and Paris showed that this was, in a precise sense, unavoidable, leading to unprovability in $\mathsf {PA}$ [15].

A natural question to ask is if this particular way of writing natural numbers is ‘canonical’ in some way. For example, we could just as well have written $20=2^{2^2} + 2 + 2 $ . This would lead to a different candidate for $\mathrm {G}_{1}(20)$ ; namely, $3^{3^3} + 3 + 2 $ . Is there some sense in which the standard representation of $20$ is preferable? Will the Goodstein process still terminate if we choose a different representation of each natural number?

Remarkably, the answer to both of these questions is ‘yes’. In fact, the two questions are intimately connected, as we will see throughout the paper. Regarding the first question, we identify two potential criteria for a canonical system of normal forms: first, it could be norm minimizing, meaning that we use the least possible number of symbols to write a number. Second, it could be base-change maximal, which roughly states that $\mathrm {G}_{i+1}(m)$ will be as large as possible given $\mathrm {G}_{i}(m)$ . While the first property is arguably more intuitive, the second turns out to be surprisingly useful. In particular, termination for a Goodstein process based on a base-change maximal notation system implies that any other notation system (based on the same primitive functions) will also yield a terminating Goodstein process.

As we will see, the hereditary exponential normal form for natural numbers enjoys both norm minimization and base-change maximality. This tells us that every Goodstein walk is finite, by which we mean every sequence of numbers $(m_i)_{i=0}^{\alpha }$ , where $m_{i+1}$ is obtained by writing $m_i$ in an arbitrary fashion using addition and base- $(i+2)$ exponentiation, then replacing every instance of $i+2$ by $i+3$ and subtracting one. We may even use multiplication, which is not needed for Goodstein’s original theorem, even though norm minimality fails when multiplication is involved. We will formalize and prove these results in Section 8.

We also consider some variants of Goodstein’s principle of lower proof-theoretic strength. For each $n\geq 1$ , recall that $\mathsf {I}\Sigma _n$ is the fragment of $\mathsf {PA}$ where induction is restricted to $\Sigma _n$ formulas. First, we consider notations based on addition and multiplication, but not exponentiation. This leads to an independence result for $\mathsf {I}\Sigma _1$ ; see Section 4 for details. Finally, we show that by varying the initial base (i.e., rather than writing m in hereditary exponential base $2$ , we use a different base $r\geq 2$ ) but restricting m, we may obtain a parametrized version of Goodstein’s principle which provides independence results for each $\mathsf {I}\Sigma _n$ with $n\geq 1$ . These parametrized Goodstein principles are detailed in Section 9. Meskens and Weiermann [17] have also shown independence results for $\mathsf { I}\Sigma _n$ based on Goodstein principles, albeit our approach is quite different: we consider Goodstein processes where only the initial base is modified, while they consider sequences with slowly changing bases. Our presentation is mostly self-contained, so that in particular Goodstein’s original theorem and its independence from Peano arithmetic are obtained via our methods.

Layout.

In Section 2 we review Goodstein’s classical result and set up an abstract framework which sets the stage for generalizations. Section 3 then introduces the notions of norm minimality and base-change maximality, which will be a focus of the paper. With these notions in mind, the following sections study various Goodstein processes: Section 4 considers a weakened Goodstein principle, Section 5 studies the optimality of hereditary exponential normal forms, and Section 6 shows that base-change maximality holds even if we extend the notation system to include multiplication. Section 7 then compares the termination time of Goodstein processes to Hardy functions, from which termination and independence is obtained. The optimality results obtained are used in Section 8 to provide generalizations of Goodstein’s theorem in terms of Goodstein walks, and Section 9 parametrizes Goodstein’s result to obtain provability phase transitions for each $\mathsf {I}\Sigma _n$ .

2 The classical Goodstein process

Let us discuss the original Goodstein principle from an abstract perspective, which will be useful in the rest of the text. A notation system is a family of function symbols ${\mathcal F}$ so that each $f\in {\mathcal F}$ is equipped with an arity $n_f>0$ and a function $|f| \colon {\mathbb N}^{n_f} \to {\mathbb N}$ . For a function symbol $f(x_0,\ldots ,x_{n})$ of arity $n+1$ , the parameter $x_0$ will be regarded as a ‘base’ and usually denoted k or $\ell $ .

Given fixed $k\geq 2$ , the set of (closed) base k terms, $\mathbb T^{{\mathcal F}}_k$ , is defined inductively so that if $\tau _1,\ldots ,\tau _n \in \mathbb T^{{\mathcal F}}_k$ are terms and f is a function symbol with arity $n+1$ , then $f(k,\tau _1,\ldots ,\tau _n ) \in \mathbb T^{{\mathcal F}}_k$ . We write $\mathbb T^{{\mathcal F}}$ for $\bigcup _{k=2}^{\infty } \mathbb T^{{\mathcal F}}_k$ ; note that $\mathbb T^{{\mathcal F}}$ contains terms of all bases, but each term has a unique base. ¹ The value of a term $\tau = f(k,\tau _1,\ldots ,\tau _n)$ is defined recursively by $|\tau | = |f| (k,|\tau _1|,\ldots ,|\tau _n|)$ . The norm of $\tau $ is defined inductively by $\|\tau \| = 1 + \sum _{i = 1}^n\|\tau _i\|$ ; note that function symbols that depend only on k have norm one. In practice, we may also include constant symbols c, but for theoretical purposes these will be regarded as function symbols f of arity one such that $|f|(k)\equiv c$ . Similarly, operations such as addition might not display k but a term $\tau +\sigma $ is ‘officially’ $f(k,\tau ,\sigma )$ for some symbol f with $|f|(k,x,y)=x+y$ .

It is important to make a conceptual distinction between function symbols and the functions they represent, as for example we can do induction on the complexity of a term, independently of its numerical value. However, often we will not make a notational distinction and omit $|\cdot |$ ; whether an expression should be treated as a value or a term will be made clear from context. For the classical Goodstein process, we will work with the functions/function symbols $0,x+y$ and $k^x$ ; we denote this notation system by ${\mathcal E}$ for ‘exponential’, and write $\mathbb E_k$ instead of $\mathbb T^{\mathcal E}_k$ and $\mathbb E$ instead of $\mathbb T^{\mathcal E}$ .

It is not required that each natural number has a single notation, but a canonical one may be chosen nonetheless. A normal form assignment for a notation system ${\mathcal F}$ is a function such that and for all $k\geq 2$ and n. A notation system equipped with a normal form assignment is called a normalized notation system. In the case of $\mathbb E_k$ , the normal form for $n\in {\mathbb N}$ is defined as follows. Set . For $n>0$ , assume that is defined for all $m<n$ . Let r be the unique natural number such that $k^r\leq n < k^{r+1}$ , and $ b = n - k^r$ . Then set .

Finally, we need a base-change operation to define the Goodstein process. Given $k\leq \ell $ and $\tau \in \mathbb T^{{\mathcal F}}_k$ , we define $ {\uparrow ^{\ell } } \tau $ recursively by

$$\begin{align*}{\uparrow ^{\ell} } f(k,\tau_1,\ldots,\tau_n) = f(\ell, {\uparrow ^{\ell} } \tau_1 ,\ldots, {\uparrow }{^{\ell}}\tau_n ).\end{align*}$$

If a normal form assignment is given, we can extend operations on terms to natural numbers by first computing their normal form. In particular, we define and . To ease notation, we will sometimes write $ {\uparrow } n $ instead of $ {\uparrow ^{\ell }_{k} } n $ , when k and $\ell $ are made clear. We may also write instead of .

Definition 2.1. Let ${\mathcal F}$ be a normalized notation system and $m\in {\mathbb N}$ . We define the ${\mathcal F}$ -Goodstein sequence beginning at m with initial base r to be the unique sequence $( m_i )_{i <\alpha }$ , where $\alpha \leq \infty $ , so that:

1. 1. $m_0=m$ ,

2. 2. $m_{i+1} = {\uparrow ^{r+i+1}_{r+i} } m_i - 1$ if $m_i> 0 $ ,

3. 3. $\alpha = i+1 $ if $m_i = 0$ ; if there is no such i, then $\alpha = \infty $ .

We write $ \mathrm {G}^{{\mathcal F}}_{i}(m|r):=m_i$ , and we often write $\mathrm {G}^{{\mathcal {F}}}_{i}(m)$ instead of $\mathrm {G}^{{\mathcal F}}_{i}(m|2)$ .

With this, we can state Goodstein’s principle within our general framework.

Theorem 2.2 (Goodstein).

For every $m\in {\mathbb N}$ , there is $i\in {\mathbb N}$ such that $\mathrm {G}^{{\mathcal {E}}}_{i}(m) = 0$ .

This theorem is a consequence of Theorem 7.16, which we will state and prove later. Note that in Definition 2.1, the normal forms used are essential when computing $ {\uparrow ^{r+i+1}_{r+i} } m_i $ , and Goodstein sequences based on different normal forms may have wildly different behaviour. However, as we will see in Section 8, Theorem 2.2 is remarkably robust and holds true for any choice of normal forms. The proof of this uses base-change maximality, a notion of ‘optimality’ of normal forms, as we discuss next.

3 Optimality criteria for normal forms

For a given notation system ${\mathcal F}$ , there may be many ways to assign normal forms to natural numbers. The question thus arises: is there an ‘optimal’ way to define normal forms? The following two criteria could help answer this question. We say that a normal form assignment nf is:

• • norm minimizing if whenever $k\geq 2$ and $\tau \in \mathbb T^{{\mathcal F}}_k$ , it follows that ;

• • base-change maximal if whenever $k\geq 2$ and $\tau \in \mathbb T^{{\mathcal F}}_k$ , it follows that for all $\ell \geq k$ .

The motivation for norm minimizing normal forms should be clear, as these provide the most succinct way to represent natural numbers. Base-change maximality is perhaps a less obvious criterion, although the intuition is that we are using the fastest-growing functions available in order to represent numbers; from this perspective, one may expect that the two notions will often coincide (although not always). Moreover, as we will see, base-change maximal normal forms are rather useful. For one thing, under some mild assumptions, they satisfy a natural monotonicity property.

Proposition 3.1. Let ${\mathcal F} $ be a normalized notation system which includes addition and a term $1$ which does not depend on k. Suppose that ${\mathcal F} $ is base-change maximal. Then, whenever $2\leq k<\ell $ and $m<n $ , it follows that $ {\uparrow ^{\ell }_{k} } m < {\uparrow ^{\ell }_{k} } n $ .

Proof Working inductively, we may assume that $n=m+1$ . Then, we have that , and by base-change maximality,

In fact, this monotonicity property is crucial for proving that Goodstein processes terminate, and Proposition 3.1 tells us that we have this property for free, given base-change maximality.

Remark 3.2. Note that Proposition 3.1 can also be applied ‘locally’: if we know that ${\mathcal F} $ is base-change maximal whenever $|\tau |<N$ for some fixed value of N, then from $m<n<N$ we can deduce that $ {\uparrow ^{\ell }_{k} } m < {\uparrow ^{\ell }_{k} } n $ . This restricted version will be useful in inductive arguments.

In the sequel, we will evaluate various Goodstein-like processes according to these criteria. We begin by considering a weak variant of Goodstein’s original result.

4 A weak Goodstein principle

In this section we apply our framework to a weak Goodstein principle based on the ‘multiplicative’ notation system $\mathcal M$ , whose functions are $0,1,+$ and $kx$ (which we may also denote $k\cdot x$ ). We will write $\mathbb M_k$ instead of $\mathbb T^{\mathcal M}_k$ . For ease of notation, we will omit parentheses around addition and treat terms $(\sigma +\tau )+\rho $ and $\tau +(\sigma +\rho )$ as identical; this will not be an issue, as all of the properties we consider are invariant under associativity. For $q\in {\mathbb N}$ , we define a term $\bar q$ by setting $\bar 0 = 0$ and, for $q>0$ , $\bar q= 1+ 1 + \cdots +1$ (q times); note that $\|\bar q\| = 2q-1$ in this case. For $k\geq 2$ , define $m=_{k} k\cdot p + q$ if $p,q$ are the unique positive integers such that $q<k$ and $m = k\cdot p + q$ . If $p=0$ , set , and if $p>0$ , define inductively . Note that $\|m\|_k {\kern-1pt}={\kern-1pt} \|p\|_k {\kern-1pt}+{\kern-1pt} 2 q{\kern-1pt}+{\kern-1pt}1$ . Throughout this section, all notation (e.g., , $\|\tau \|$ , etc.) will refer exclusively to this representation of natural numbers.

Lemma 4.1. If $m\in {\mathbb N}$ and $\ell> k\geq 2$ , then

Proof This is clear since $q<k$ yields $q<\ell $ .

This normalized notation system satisfies both optimality properties, as we see next.

4.1 Norm minimality

Let us begin by showing that our multiplicative notation system satisfies the norm minimality property.

Theorem 4.2. If $\tau \in \mathbb M_k$ , then .

Proof Write $m = |\tau |$ . The claim is proven by induction on m, considering several cases. We treat the most interesting case, which is that of a term $\tau = k\cdot \sigma + \bar n$ . Write $n = k\cdot p + q$ with $q<k$ , so that $m=_{k} k\cdot |\sigma + \bar p| + q$ . By the induction hypothesis, $\||\sigma + \bar p|\|_k \leq \| \sigma + \bar p\| =\|\sigma \| + 2 p $ . Hence,

$$ \begin{align*} \|m\|_k &\leq \|| \sigma+p|\|_k + 2 q +1 = \|\sigma\| + 2 (p + q) + 1 \\ & \leq \|\sigma\| + 2 n + 1 = \|k\cdot \sigma + \bar n\|.\\[-35pt] \end{align*} $$

4.2 Maximality of base change

Recall that our second optimality criterion was optimality under base change. We will show that multiplicative normal forms also enjoy this property. This will follow from the next lemma.

Lemma 4.3. If $m = k\cdot r+s$ and $\ell \geq k$ , then

$$\begin{align*}{\uparrow ^{\ell}_{k} } m \geq \ell \cdot {\uparrow ^{\ell}_{k} } r +s,\end{align*}$$

and equality holds if and only if $m =_{k} k\cdot r+s$ .

Proof In this proof, we write $ {\uparrow } x $ instead of $ {\uparrow ^{\ell }_{k} } x $ . Proceed by induction on m. If $m=0$ , then $r=s=0$ and $ {\uparrow } 0 = 0 = \ell \cdot {\uparrow } 0 +0$ , so we assume $m>0$ . Write $s=_k k\cdot p + q$ (with p or q possibly zero), so that $m=_k k\cdot (r+p) +q$ . Write $r = ku+v$ in normal form. Then, the induction hypothesis yields

Hence,

$$ \begin{align*} {\uparrow } m & = \ell \cdot {\uparrow } (r+p) +q \geq \ell \cdot {\uparrow } r {} + \ell p+q \geq \ell \cdot {\uparrow } r {} +s, \end{align*} $$

and the last inequality is strict unless $p = 0$ , so that $m =_{k} kr+s$ .

In view of Lemma 4.3, a simple induction on term complexity yields the following.

Theorem 4.4. If $\tau \in \mathbb M_k$ , $\ell> k \geq 2$ , and $m=|\tau |$ , then

$$\begin{align*}{\uparrow ^{\ell}_{k} } m \geq | {\uparrow ^{\ell} } \tau |.\end{align*}$$

5 Optimality of exponential normal forms

Now we turn our attention to the original Goodstein process. In this setting, it is already known that the process terminates [11], and that this fact is independent of Peano arithmetic [15]. We will show that the notation system used satisfies our optimality criteria. We begin by establishing some useful basic properties.

5.1 Properties of normal forms

Recall that ${\mathcal E}$ has as primitive functions $0$ , $x+y$ , and $ k^x$ (with $k\geq 2$ ), and is equipped with normal forms as defined in Section 2. We will treat terms modulo associativity of addition and hence omit parentheses. However, we will not treat term addition as commutative. With this in mind, it is easy to check that $k^{\rho _0} + \cdots + k^{\rho _{n-1}}$ is in normal form if and only if each $\rho _i$ is in normal form, $\rho _i \geq \rho _{i+1}$ whenever $i + 1 < n $ , and $\rho _i> \rho _{i+k-1}$ whenever $i+k-1 < n$ . We will extend the notation $=_k$ to write $m=_k \tau (k,a_1,\ldots ,a_{n })$ , where $a_i\in {\mathbb N}$ , if ; for example, we may write $15=_2 2^3+ 2^2 + 3$ or $12=_2 8 + 2^2$ but not, say, $15=_2 7 + 2^3$ . Sums should be read from right to left, i.e., $\sum _{i=0}^{n } \tau _i = \tau _n + \cdots + \tau _0$ . Multiplication is used as a shorthand: $p\cdot \tau = \tau +\ldots + \tau $ (p times).

With this notation at hand, the following is easily checked.

Lemma 5.1. Fix $k\geq 2$ , $m\in {\mathbb N}$ , and $ \sigma ,\tau \in \mathbb E_k$ .

1. 1. If $\sigma + \tau $ is in normal form, then $\sigma $ and $\tau $ are each in normal form.

2. 2. If $m =_k k^a$ and $b < a$ , then $m-k^b =_k \sum _{i= b}^{a-1} (k-1) k ^{i}$ .

3. 3. If $m = a + k^b$ and $n = k^c + d$ are in normal form with $b>c$ , then $m+n$ is in normal form.

5.2 Norm minimality

In this subsection, we will show that the hereditary exponential notation satisfies norm minimality. We begin with some useful inequalities.

Lemma 5.2. If $k\geq 2$ and $m\in {\mathbb N}$ , then $\|m+1\|_k \leq \|m\|_k+3$ .

Proof Write $m+1 =_k a+k^b$ . If $b = 0$ , then $ m = a$ and $\|m+k^0\|_k = \|m\|_k + 3$ (we add one for the term $0$ , one for $+$ and one for $k^\cdot $ ). Otherwise, using Lemma 5.1, we see that $m =_k a + \sum _{i=0}^{b-1} (k-1) k^i$ , and

With this in mind, the following useful inequality is proven by induction on m; details are left to the reader.

Lemma 5.3. If $m= k^a + b$ , then $\|m\|_k \leq \|a\|_k + \|b\|_k + 2$ .

In particular, if $m=_k k^p+q$ and $k^a+b=m$ , then we have that $ \|p\|_k +\|q\|_k+2= \|m\|_k\leq \|a\|_k+\|b\|_k +2 $ . From this and an easy induction on term complexity, we obtain that ${\mathcal E}$ is norm minimal.

Theorem 5.4. If $\tau \in \mathbb E_k$ and $m=|\tau |$ , then $\|m\|_k \leq \|\tau \|$ .

5.3 Maximality of base change

We have seen that hereditary exponential notation satisfies norm minimality. Let us now show that it is base-change maximal as well. This will follow from the next lemma. If ${\mathcal F}$ is a normalized notation system, say that ${\mathcal F}$ is base-change maximal below $m\in {\mathbb N}$ if, whenever $\tau \in \mathbb T^{{\mathcal F}}_k$ and $|\tau | < m$ , it follows that . Recall from Remark 3.2 that, if ${\mathcal F}$ is base-change maximal below m, then whenever $x<y<m$ , we may conclude that $ {\uparrow ^{\ell }_{k} } x < {\uparrow ^{\ell }_{k} } y $ . As we wish to appeal to this property in the proof of the following lemma, we will assume inductively that hereditary exponential notation is base-change maximal below m.

Lemma 5.5. Fix $\ell> k \geq 2$ and write $ {\uparrow } x $ instead of $ {\uparrow ^{\ell }_{k} } x $ . Suppose that the normalized notation system ${\mathcal E}$ is base-change maximal below m. If $m=k^a+b$ , then

$$\begin{align*}{\uparrow } m \geq \ell^{ {\uparrow } a } + {\uparrow } b .\end{align*}$$

Proof Write $m =_{k} k^p + q$ . The proof proceeds by induction on m; here we treat the critical case, where $ a < p$ and $ b < k ^p$ . We note that in this case $q < k^a$ , and thus

$$\begin{align*}b = ( k^p - k^a ) + q =_k \sum _{ i = a }^{p-1} (k-1) k^{i} + q, \end{align*}$$

and hence

$$ \begin{align*} {\uparrow } b = (k-1) \sum _{ i = a }^{p-1} \ell^{ {\uparrow } i } + {\uparrow } q = (k-1) \sum _{ i = 1 }^{p-a} \ell^{ {\uparrow } (p-i) } + {\uparrow } q. \end{align*} $$

Since $p<m$ , we may use the assumption that ${\mathcal E}$ is base-change maximal below m to obtain $ {\uparrow } (p-i) {} \leq {\uparrow } p {} -i$ , and hence

$$\begin{align*}\sum _{ i = 1 }^{p - a} \ell^{ {\uparrow } (p - i) } \leq \sum _{ i = 1 }^{p - a } \ell^{ {\uparrow } p - i} = \dfrac{\ell^{ {\uparrow } p }(\ell^{p - a } - 1)}{\ell^{p - a }(\ell-1)} < \dfrac{\ell^{ {\uparrow } p } }{ \ell-1 } \leq \frac { \ell^{ {\uparrow } p }}{k },\end{align*}$$

so .

By monotonicity below m, available due to Remark 3.2, we have that $ {\uparrow } a \leq {\uparrow } p -1 $ , so . Therefore,

$$\begin{align*}\ell^{ {\uparrow } a } + {\uparrow } b < \frac{\ell^{ {\uparrow } p }} k + \frac {(k-1) \ell^{ {\uparrow } p }}{k } + {\uparrow } q = \ell^{ {\uparrow } p } + {\uparrow } q = {\uparrow } m.\\[-42pt] \end{align*}$$

Theorem 5.6. If $2\leq k<\ell $ , $\tau \in \mathbb E_k$ , and $m=|\tau |$ , then $ {\uparrow }{^{\ell }_k}m \geq | {\uparrow ^{\ell } } \tau |$ .

Proof Induction on term complexity using Lemma 5.5.

In view of Proposition 3.1, we immediately obtain monotonicity of the base-change operation.

Corollary 5.7. If $m<n$ and $2\leq k < \ell $ , then $ {\uparrow ^{\ell }_{k} } m < {\uparrow ^{\ell }_{k} } n $ .

From monotonicity, we readily obtain normal form preservation for hereditary exponential normal forms.

Lemma 5.8. If $m\in {\mathbb N}$ and $\ell> k\geq 2$ , then

Proof Write $ {\uparrow } $ for $ {\uparrow ^{\ell }_{k} } $ . It suffices to show that if $k^a+b$ is in normal form then so is $\ell ^{ {\uparrow } a } + { {\uparrow } b }$ , since then the result follows by an easy induction on .

We write $k^a+b = r\cdot k^a+c $ , where $c<k^a$ and $0<r<k$ , and proceed by a secondary induction on $s\leq r $ to prove that $ (s+1)\cdot \ell ^{{\uparrow }^{} _{} a}> s\ell ^{{\uparrow }^{} _{} a }+ {\uparrow }^{} _{} c$ . The claim will then follow, since $b=_{k} (r-1) k^{ {} {}{a} }+ {} {}{c} $ and

$$ \begin{align*} \ell^{{\uparrow}^{} _{} a +1} & = \ell \cdot \ell^{{\uparrow}^{} _{} a } \geq (r+1)\cdot \ell^{{\uparrow}^{} _{} a }\\ &> \ell^{{\uparrow}^{} _{} a }+ (r-1) \ell^{{\uparrow}^{} _{} a }+ {\uparrow}^{} _{} c = \ell^{{\uparrow}^{} _{} a }+ {\uparrow}^{} _{} b, \end{align*} $$

as needed.

For $s=1$ , $c <k^a$ and Corollary 5.7 yields ${\uparrow }^{} _{} c< {\uparrow }^{} _{} k^a = \ell ^{{\uparrow }^{} _{} a} $ Hence, $(1+1)\ell ^{{\uparrow }^{} _{} a}> \ell ^{{\uparrow }^{} _{} a}+ {\uparrow }^{} _{} c$ . Otherwise,

6 Elementary functions

In this section we consider an extension of ${\mathcal E}$ with product and study whether hereditary exponential normal forms are still optimal in this context. Define $\mathcal L = \{0,x+y,x\cdot y,k^x\}$ . Then, for example,

$$ \begin{align*} (5^2+5^1+5^0)\cdot ( 5^1+5^0) & = 5^3+2\cdot 5^2+2\cdot 5^1 + 5^0 \\ &= 5^3+ 5^2+5^2+5^1 + 5^1 + 5^0, \end{align*} $$

although the left-hand side has the smallest norm of the three. This tells us that exponential normal forms no longer give minimal norms, even if we allow for coefficients below k. However, as we will see, we still obtain maximality under base change. Below and throughout this section, denotes the normal form operator for ${\mathcal E}$ , as used in the standard Goodstein theorem.

Theorem 6.1. Let $\ell \geq k\geq 2$ , $m\in {\mathbb N}$ , and $\tau \in \mathcal L_k $ . Then, .

Proof The theorem is proven by induction on $|\tau |$ with a secondary induction on $\|\tau \|$ . Write $ {\uparrow } $ for $ {\uparrow ^{\ell } } $ . The key step is reducing a product to a term in $\mathbb E_k$ . Suppose that $\tau = \sigma \cdot \rho $ , with both terms having non-zero value. Write and . Define $\tau '= k^{\alpha } \cdot \delta + k^{\gamma } \cdot \beta + \beta \cdot \delta $ . Then,

where the first inductive step is by the secondary induction hypothesis on $\|\sigma \|,\|\rho \|<\|\tau \|$ and the second is the primary induction hypothesis on $|\tau '|<|\tau |$ . Note that , and moreover

Thus, by Theorem 5.6,

We conclude that , as required.

Theorem 6.1 might seem surprising, as hereditary exponential normal forms do not involve multiplication, yet they remain base-change maximal even compared to arbitrary elementary terms. Later, we will see that this result leads to a wide generalization of Goodstein’s principle.

7 Termination times of the Goodstein processes

In this section we provide a proof that the Goodstein processes terminate by comparing them to Hardy functions. These are functions defined by transfinite induction up to $\varepsilon _0$ . Our analysis will yield additional information which will also lead to independence results. We begin by reviewing these functions and their properties.

7.1 Hardy functions and independence

Recall that $\varepsilon _0$ is the first fixed point of the function $\xi \mapsto \omega ^{\xi }$ , and by the Cantor normal form theorem, every non-zero $\xi <\varepsilon _0$ can be written in the form $\omega ^{\alpha }+\beta $ with $\alpha ,\beta <\xi < \omega ^{\alpha +1}$ . The Cantor normal form of $0$ is $0$ .

Definition 7.1. For $\xi <\varepsilon _0$ and $n \in {\mathbb N}$ , we define $\xi [n]$ recursively by:

• • $0[ n ] := 1 [ n ] :=0 $ ;

• • $(\omega ^{\alpha }+\beta )[ n ] := \omega ^{\alpha }+\beta [n] $ if $\omega ^{\alpha }+\beta $ is in Cantor normal form and ${\beta }>0$ ;

• • $(\omega ^{\alpha +1}) [ n ] := \omega ^{\alpha } n $ ;

• • $(\omega ^{\alpha }) [ n ] := \omega ^{\alpha [n]}$ if $\alpha $ is a limit.

These fundamental sequences satisfy the essential properties that $\alpha [n]<{\alpha }$ if ${\alpha }\neq 0$ and, if ${\alpha }<\varepsilon _0$ is a limit ordinal, then $({\alpha }[n])_{n<\omega }$ is an increasing sequence converging to ${\alpha }$ . Another key property of these fundamental sequences is the Bachmann property; see [20, 22] for details.

Proposition 7.2 (Bachmann property).

If $\alpha ,\beta < \varepsilon _0$ and $k \in {\mathbb N}$ satisfy $\alpha [k] < \beta < {\alpha }$ , then $\alpha [k] \leq \beta [1]$ .

For example, $\omega ^{\omega }[ 4]=\omega ^ 4$ and $\omega ^4<\omega ^ 6<\omega ^{\omega }$ , while $\omega ^4< \omega ^ 5 = \omega ^6 [1] $ . The intuition here is that if ${\beta }\in (\alpha [k],{\alpha })$ and we iteratively apply fundamental sequences to ${\beta }$ , we will be ‘stuck’ in the interval $(\alpha [k],{\alpha })$ , unless we pass through $\alpha [k]$ . Note that this may fail if we replace $1$ by $0$ , as $\omega ^6[0] = 0< \omega ^{\omega }[4]$ .

We also need to identify conditions under which we can guarantee that $\xi [n]\geq \zeta $ for $\zeta <\xi $ . To this end, define the maximal coefficient of $\zeta $ , $\mathrm {mc}(\zeta )$ , to be the largest natural number appearing in $\zeta $ when written in Cantor normal form. To be precise, $\mathrm {mc}(0)=0$ , and if $\zeta = \omega ^{\alpha } n+\beta $ with $\beta <\omega ^{\alpha }$ , then $\mathrm {mc}(\zeta ) = \max \{n,\mathrm {mc}(\alpha ),\mathrm {mc}(\beta )\}$ . The following is proven in, e.g., [8].

Lemma 7.3. Let $\xi <\varepsilon _0$ and $n\in {\mathbb N}$ . Then,

1. 1. $\mathrm {mc}(\xi [n]) \leq \max \{\mathrm {mc}(\xi ), n\}$ , and

2. 2. if $\zeta <\xi $ and $\mathrm {mc}(\zeta )< n$ then $\zeta \leq \xi [n]$ .

Fundamental sequences can be used to define fast-growing functions on the natural numbers, such as the Hardy functions below.

Definition 7.4. For $x\in \mathbb {N}$ and $\alpha < \varepsilon _0$ , we define:

• • $H_0 (x) = x$ ;

• • $H_{\alpha } (x) = H_{{\alpha }[x]}(x + 1)$ if ${\alpha }\neq 0$ .

The intuition is that each $H_{\alpha }$ is an increasing function, which grows more quickly for larger $\alpha $ .

Theorem 7.5 [3].

1. 1. If $x<y$ and ${\alpha }<\varepsilon _0$ , then $H _{\alpha }(x) < H _{\alpha }(y)$ .

2. 2. If ${\alpha }<{\beta }$ and $x> \mathrm {mc}(\alpha )$ , then $H _{\alpha }(x) < H _{\beta }(x)$ .

The totality of these functions cannot be proven over weak theories. To make this precise, define $\omega _n$ to be a tower of n $\omega $ ’s, i.e., $\omega _0 = 1 $ and $\omega _{n+1} = \omega ^{\omega _n}$ .

Theorem 7.6 [6, 21].

For $n\in {\mathbb N} \setminus \{0\}$ ,

1. 1. $\mathsf {I}\Sigma _n$ proves that $H_{\alpha } $ is total if and only if $\alpha < \omega _{n+1}$ .

2. 2. If f is a provably total computable function in $\mathsf {I}\Sigma _n$ , then there is $N\in {\mathbb N}$ such that for all $x>N$ , $f(x) < H_{ \omega _{n+1}}(x)$ .

Thus a general strategy for proving independence of $\Pi ^0_2$ statements is showing that they require witnesses growing faster than suitable Hardy functions. This approach based on the Hardy function and variants has been used in various classic independence results by, e.g., Cichon [2], Loebl and Nešetřil [16], and, of course, Kriby and Paris’ proof of independence of Goodstein’s theorem [15]. The following is useful in establishing such lower bounds.

Proposition 7.7. Let $x> 0$ , $\xi <\varepsilon _0$ , and $(\xi _n)_{n \leq \ell }$ be a sequence of ordinals below $\varepsilon _0$ such that $:$

1. 1. $\xi [x]< \xi _0 \leq \xi $ ,

2. 2. for all $n < \ell $ , $ {\xi _n}[x+n] \leq \xi _{n+1} \leq \xi _n$ , and

3. 3. $\xi _{\ell } = 0$ .

Then, $\ell + x \geq H_{\xi }(x)$ .

Proof We prove the lemma by induction on $\ell $ . The claim is vacuously true when $\ell = 0$ (i.e., $\xi _0 = 0$ ), so we assume otherwise. Consider two cases.

Case 1 ( $\xi [x] <\xi _1$ ).

Then, the sequence $(\xi _{n+1})_{n \leq \ell -1}$ once again satisfies the assumptions, since ${\xi _{n+1}}[x+n] \leq {\xi _{n+1}}[x+n+1] \leq \xi _{n+2} $ . By induction on $\ell $ , we obtain $\ell - 1 + x \geq H_{\xi }(x)$ .

Case 2 ( $\xi [x] = \xi _1$ ).

Then, the sequence $(\xi _{n+1})_{n \leq \ell -1}$ satisfies the assumptions, but for $\xi $ replaced by $\xi [x]$ and x replaced by $x+1$ , since ${\xi _{n+1}}[(x+1)+n] = {\xi _{n+1}}[x+n+1] \leq \xi _{n+2} $ . Thus we obtain $\ell +x = (\ell - 1)+(x+1) \geq H_{\xi [x]}(x+1) = H_{\xi }(x)$ .

We will also need to establish upper bounds in terms of the Hardy functions. For this, we use the following.

Proposition 7.8. Let $x\in {\mathbb N}$ and $(\xi _n)_{n \leq \ell }$ be a sequence of ordinals below $\varepsilon _0$ such that $ \xi _0 \leq \xi $ , $\xi _{n}>0$ if $n<\ell $ , and for all $n < \ell $ , $ \xi _{n+1} < \xi _n$ and $\mathrm {mc}(\xi _{n+1}) \leq x+n $ . Then, $\ell + x < H_{\xi }(x+1)$ .

Proof If $\xi _0=0$ , then $\ell +x = x <x+1 = H_0(x+1) $ . Otherwise, consider the sequence $(\xi _{n+1})_{n \leq \ell -1}$ ; we claim that it satisfies the assumptions of the proposition, but with $\xi $ replaced by $\xi [x+1]$ and x replaced by $x+1$ . By Lemma 7.3, $\xi _1\leq \xi [x+1] $ , and $\mathrm {mc}(\xi _{n+2}) \leq x+n+1 = (x+1)+n $ . So, induction on $\ell $ yields $(\ell -1)+(x+1) < H_{\xi [x+1]}( x+ 2) = H_{\xi }(x+1) $ , i.e., $\ell +x < H_{\xi }(x+1)$ , as needed.

7.2 Termination of the weak Goodstein process

We now show that the weak Goodstein process terminates in time $H_{\omega ^{\omega }}$ . In this subsection, all notation (e.g., ) refers to the notation system $\mathcal M$ of Section 4. If ${\mathcal F}$ is a normalized notation system and $m\in {\mathbb N}$ , we define $\mathrm {G}^{{\mathcal F}}_{\infty }(m)$ to be the least $\ell $ such that $\mathrm {G}^{{\mathcal F}}_{\ell } (m) = 0$ , and $\mathrm {G}^{{\mathcal F}}_{\infty }(m) = \infty $ if no such $\ell $ exists. More generally, $\mathrm {G}^{{\mathcal F}}_{\infty }(m|r)$ is the least $\ell $ such that $\mathrm {G}^{{\mathcal F}}_{\ell }(m|r)= 0$ , if it exists. We will show that $ \mathrm {G}^{{\mathcal F}}_{\infty }(m|r) \approx H_{{\uparrow }^{\omega } _{r} m}(r) $ , so the left hand is finite since the right hand is.

To make this precise, we need to introduce an ordinal assignment for terms. We note that the operations in $\mathcal M$ are well-defined on the ordinals, and as such we can consider expressions with base $\omega $ . For $\tau \in \mathbb M_k$ , we define ${\uparrow }^{\omega } _{{}} \tau $ to be the result of replacing every occurrence of k by $\omega $ , i.e., ${\uparrow }^{\omega } _{{}} 0 =0$ , ${\uparrow }^{\omega } _{{}} (\tau +\sigma ) ={\uparrow }^{\omega } _{{}} \tau + {\uparrow }^{\omega } _{{}} \sigma $ , and ${\uparrow }^{\omega } _{{}} k\tau = \omega {\uparrow }^{\omega } _{{}} \tau $ . If $m\in {\mathbb N}$ , then .

To continue, we need to calculate the normal form of $m-1$ . The following is easy to check.

Lemma 7.9. Suppose that $0 < m =_{k} k p+r$ and $k\geq 2$ .

1. 1. If $r>0$ , then $m-1 =_{k} k p+(r-1)$ .

2. 2. If $r = 0$ , then $m-1 =_{k} k (p-1)+(k-1)$ .

Inspection on Definition 7.1 then yields the following.

Lemma 7.10. For every $m\in {\mathbb N}$ and $k\geq 2$ ,

$$\begin{align*}{\uparrow}^{\omega} _{k} (m-1) = ({\uparrow}^{\omega} _{k}m) [k-1] .\end{align*}$$

Below, we note that $ {\uparrow ^{\omega } } \tau $ is defined according to the base of $\tau $ ; if $\tau \in \mathbb M_k$ , then $ {\uparrow ^{\omega } } \tau $ is obtained by replacing every occurrence of k by $\omega $ , and if $\tau \in \mathbb M_{\ell }$ , then $ {\uparrow ^{\omega } } \tau $ is obtained by replacing every occurrence of $\ell $ by $\omega $ . A routine induction on term complexity shows that if $\tau \in \mathbb T^{\mathcal M}_k$ and $\ell> k$ , then $ {\uparrow ^{\omega } } {\uparrow ^{\ell } } \tau = {\uparrow ^{\omega } } \tau .$ From this, we readily obtain the following.

Proposition 7.11. If $2\leq k < \ell $ , then $ {\uparrow ^{\omega }_{\ell } } {\uparrow } {^{\ell }_{k} }m = {\uparrow } {^{\omega }_{k}}m.$

Proof Write . By Lemma 5.8, . Hence,

$$\begin{align*}{\uparrow } {^{\omega}_{k}}m = {\uparrow ^{\omega} } \tau = {\uparrow }{^{\omega}} {\uparrow ^{\ell} } \tau = {\uparrow ^{\omega}_{\ell} } {\uparrow } {^{\ell}_{k} }m.\\[-35pt] \end{align*}$$

Theorem 7.12. For every $m\in {\mathbb N}$ and $k\geq 2$ , $\mathrm {G}^{\mathcal M}_{\infty }(m|k)$ is finite and

$$\begin{align*}\mathrm{G}^{\mathcal M}_{\infty}(m|k) +k = H_{{\uparrow}^{\omega} _{k} m} (k ). \end{align*}$$

Proof We use transfinite induction below $\omega ^{\omega }$ on ${\uparrow }^{{\omega }} _{{k}} m$ . The base case, where $m=0$ , yields $k $ on both sides. Otherwise, we use Lemma 7.10 to see that

where we are justified in using the induction hypothesis since

$$\begin{align*}{\uparrow}^{\omega} _{{k+1}} {({\uparrow}^{{k+1}} _{{k }} m-1 )} = ({\uparrow}^{\omega} _{k} {\uparrow}^{{k+1}} _{{k }} m )[k-1 ] = ({\uparrow}^{\omega} _{k} m )[k-1 ] < {\uparrow}^{\omega} _{k} m.\\[-35pt] \end{align*}$$

Corollary 7.13. $\mathsf {I}\Sigma _1$ does not prove that for every $m\in {\mathbb N}$ , $\mathrm {G}_{\infty }^{\mathcal M} (m)$ is finite.

Proof Let $a_{x} = 2^{2x }$ . Then it is not hard to check that ${\uparrow }^{\omega } _{2} a_{x} = \omega ^{2x }$ , and $H_{\omega ^{2x }}(2)> H_{\omega ^{x }}(x+1) = H_{\omega ^{\omega }}(x)$ . But then, by Theorem 7.12, $\mathrm {G}_{\infty }^{\mathcal M} (a_x) + 2> H_{\omega ^{\omega }}(x)$ . It follows from the second item of Theorem 7.6 that $\mathsf {I}\Sigma _1$ does not prove that $\mathrm { G}_{\infty }^{\mathcal M} (a_x)$ is finite for all x.

7.3 Termination of the classic Goodstein process

Now we turn our attention to the classic Goodstein process based on ${\mathcal E}$ . Recall that in this context, $r\cdot \tau $ is shorthand for $\tau +\cdots +\tau $ , r times.

Lemma 7.14. If $k\geq 2$ and $\tau $ is in base k normal form, then $\mathrm {mc}({\uparrow }^{\omega } _{k} \tau )<k$ .

Proof It suffices to observe that $r\cdot k^a + b$ cannot be in normal form for any $r\geq k$ , since otherwise

$$\begin{align*}r\cdot k^a + b \geq k^{a+1}. \end{align*}$$

With this and an easy induction on term complexity, we see that no term in normal form may contain coefficients greater than or equal to k.

The following may readily be checked by induction on m, by writing $m = k^a+b$ in normal form and comparing ${\uparrow }^{\omega } _{k} (m -1) $ to $({\uparrow }^{\omega } _{{k}} m)[k-1]$ according to Definition 7.1.

Lemma 7.15. If $k\geq 2$ and $0< m\in {\mathbb N}$ , then

$$\begin{align*}({\uparrow}^{\omega} _{{k}} m )[k-1] \leq {\uparrow}^{\omega} _{k} (m -1) < {\uparrow}^{\omega} _{k} m.\end{align*}$$

Note that in contrast to Lemma 7.10, we do not always obtain equality on the left, but this is enough to obtain a lower bound. It is also worth remarking that ${\uparrow }^{\omega } _{k} (m -1) < {\uparrow }^{\omega } _{k} m$ for all $m>0$ is equivalent to the statement that if $n<m$ , then ${\uparrow }^{\omega } _{k} n < {\uparrow }^{\omega } _{k} m$ and thus the $\omega $ -base change is monotone, just as the finitary ones. This lemma will allow us to compare Hardy hierarchies with the length of the standard Goodstein process.

Theorem 7.16. For all $m\in {\mathbb N}$ and $x\geq 2$ ,

$$\begin{align*}H_{{\uparrow}^{\omega} _{x} m}(x ) \leq \mathrm{G}^{{\mathcal E}}_{\infty}(m|x) +x \leq H_{{\uparrow}^{\omega} _{x} m}(x+1 ). \end{align*}$$

Proof The upper bound is immediate from Lemmas 7.14 and 7.15 and Proposition 7.8, while the lower bound follows from Lemma 7.15 and Proposition 7.7.

Corollary 7.17. $\mathsf {PA}$ does not prove that for every $m\in {\mathbb N}$ , $\mathrm {G}_{\infty }^{{\mathcal E}} (m)$ is finite.

Proof If this were provable in $\mathsf {PA}$ , it would be provable in $\mathsf {I}\Sigma _n$ for some n. For $k>0$ , it would follow that the function f given by $f(x) = \mathrm {G}_{\infty }^{{\mathcal E}} (2_{n+x+1})+2$ is total, where $x_y$ denotes the superexponential function. But $ {\uparrow ^{\omega }_{2} } 2_{n+x+1} = \omega _{n+x+1}$ , and it is easy to check using Theorem 7.5 and an easy induction that $H_{\omega _{n+x+1}}(2)> H_{\omega _{n+1}}(x)$ , so $f(x)>H_{\omega _{n+1}}(x)$ , contradicting the second item of Theorem 7.6.

8 Goodstein walks

In this section we introduce and study Goodstein walks. These are Goodstein-like processes which are defined independently of a normal form representation; natural numbers may be written in an arbitrary way using the functions from ${\mathcal F}$ . Aside from this, the definition is analogous to that of standard Goodstein processes.

Definition 8.1. Fix a notation system ${\mathcal F}$ . A Goodstein walk (for ${\mathcal F}$ ) is a sequence $(m_i)_{i <\alpha }$ , where $\alpha \leq \infty $ , such that for every $i<\alpha $ , there is a term $\tau _i \in \mathbb T^{{\mathcal F}}_{i+2}$ with $|\tau _i| = m_i$ and $m_{i+1} = {\uparrow ^{i+3} } \tau - 1$ .

Theorem 8.2. Let ${\mathcal F}$ be a normalized notation system with $+$ and $1$ . Suppose that ${\mathcal F}$ is base-change maximal, and that for every $m\in {\mathbb N}$ there is $i\in {\mathbb N}$ such that $\mathrm {G}^{{\mathcal F}}_i (m) = 0$ . Then, every Goodstein walk for ${\mathcal F}$ is finite.

Proof Let ${\mathcal F}$ satisfy the assumptions of the theorem and $(m_i)_{i=0}^{\alpha }$ be a Goodstein walk for ${\mathcal F}$ . Let $m = m_0$ . By induction on i, we check that $m_i \leq \mathrm {G}^{{\mathcal F}}_i (m)$ . For the base case this is clear. Otherwise, $m_{i+1} = | {\uparrow ^{i+3} } \tau _i | - 1$ for some term $\tau _i \in \mathbb T^{{\mathcal F}}_{i+2}$ , and thus

where the second inequality uses Proposition 3.1 and the assumption that ${\mathcal F}$ is base-change maximal. Thus if we choose i such that $\mathrm {G}^{{\mathcal F}}_i (m) =0 $ , we must have $\alpha \leq i $ .

As a corollary, we obtain the following extension of Goodstein’s theorem.

Theorem 8.3. Any Goodstein walk for $\mathcal M$ , ${\mathcal E}$ , or $\mathcal L$ is finite.

Example 8.4. Consider alternative normal forms based on $\mathcal L$ as follows. Let $k\geq 2$ and $m\geq 0 $ . First, set . For $m> 0$ , let $p_ 1 \cdots p_n$ be the decomposition of m into prime factors. If $n\leq 1 $ , we write $m = k^r + b $ with $m<k^{r+1}$ (as in the exponential normal forms) and set . Otherwise, set .

These normal forms do not have the natural structural properties that are useful in a direct proof of termination. For example, $7 =_{3} 3^1 + 3^1 + 1$ and $8 =_{3} 2\cdot 2\cdot 2$ . It follows that $ {\uparrow ^{4}_{3} } 7 = 4^1 + 4^1 + 1 = 9 $ and $ {\uparrow ^{4}_{3} } 8 = 2\cdot 2\cdot 2 \,{=}\, 8 $ . Thus the base-change operator is not monotone, in the sense that the analogue of Corollary 5.7 fails. Similarly, the natural ordinal assignment would not be monotone, as it would yield $ {\uparrow ^{\omega }_{3} } 7 = \omega \cdot 2 + 1 $ and $ {\uparrow ^{\omega }_{3} } 8 = 8$ . Without these monotonicity properties, a termination proof as given in Section 4 would not go through. Nevertheless, the Goodstein process based on these normal forms is terminating by Theorem 8.3, and such a direct proof is not needed.

9 Phase transitions

We have defined general Goodstein sequences $\mathrm {G}_{i}(m|r)$ , where $r\geq 2$ is the base of the first term. In this section, we aim to find weakenings of this statement provable in $\mathsf {I}\Sigma _n$ . The strategy is to bound the value of n, but for any fixed r and N, the statement $\forall m<N (\mathrm { G}^{\mathcal {{\mathcal E}}}_{\infty }(m|r)<\infty )$ is provable in $\mathsf {I}\Sigma _1$ (or even weaker systems) since it can be proved by checking finitely many instances. Instead, we may let r vary, and moreover have N depend on r. Specifically, we will set $N=r_k$ , where we recall that $x_y$ denotes the superexponential function. The provability of the termination of such restricted Goodstein processes in $\mathsf {I}\Sigma _n$ depends on whether $k\leq n$ .

Theorem 9.1. For $k\geq 1$ , let $\varphi _k$ be the statement

For every $r\geq 2$ and every $m<r_k$ , $\mathrm {G}^{{\mathcal E}}_{\infty }(m|r)$ is finite.

Then, for every $n,k\geq 1$ , $\mathsf {I}\Sigma _n\vdash \varphi _k$ if and only if $k \leq n $ .

Proof Fix $n,k\geq 1$ . Let $r \geq 2$ and $m<r_k$ . By Lemma 7.15, ${\uparrow }^{\omega } _{r} m < {\uparrow }^{\omega } _{r} r_k = \omega _k$ .

By Theorems 7.16 and 7.5, along with $\mathrm {mc}( {\uparrow }^{\omega } _{r} m)<r$ by Lemma 7.14, $\mathrm {G}^{{\mathcal E}}_{\infty }(m|r)<H_{ {\uparrow }^{\omega } _{r} m } (r+1) < H_{\omega _k}(r+1 )$ . Moreover, we established these inequalities using elementary means, so they are provable in $\mathsf {I}\Sigma _n$ . If $k \leq n $ , from the provable totality of $H_{\omega _k}$ in $\mathsf {I}\Sigma _n$ (Theorem 7.6), we conclude that $\varphi _k$ is provable in $\mathsf {I}\Sigma _n$ .

If $k>n $ , let $m=(r+1)_{k}-1$ . Note that $H_{\omega _k}(r)=H_{\omega _k[r] }(r+1) $ . By Lemma 7.15, ${\uparrow }^{\omega } _{r+1} m \geq \omega _k[r] = \omega _k r$ . Since $\mathrm {mc}(\omega _k r)=r$ , in view of Theorems 7.5 and 7.16, it follows that $H_{\omega _k[r]}(r ) < H_{ {\uparrow ^{\omega }_{r+1} } m }(r+1)\leq \mathrm {G}^{{\mathcal E}}_{\infty }(m|r+1) +r+1$ . Thus the function

$$\begin{align*}r\mapsto \mathrm{G}^{{\mathcal E}}_{\infty}((r+1)_k-1| {r+1})+r+1\end{align*}$$

grows faster than $H_{\omega _{n + 1}}(r )$ ; hence, once again by Theorem 7.6, the statement $\forall r \ \big ( \mathrm {G}^{{\mathcal E}}_{\infty }(r_{k}-1| {r})<\infty \big )$ is not provable in $\mathsf { I}\Sigma _n$ . Since clearly $ {r_{k}-1}<r_k$ , neither is $\varphi _k$ .

10 Concluding remarks

We have explored two notions of ‘optimality’ for notations for Goodstein processes. The first, norm minimality, is naturally motivated, but we have seen that it may fail for some otherwise well-behaved normal forms; specifically, for the notation system $\mathcal L$ and the standard Goodstein normal forms. The second, base-change maximality, is perhaps more subtle but leads to some very interesting consequences: most notably, it allows for ‘normal form-free’ Goodstein processes. In the context of $\mathcal M$ and ${\mathcal E}$ , normal forms are simple enough that the benefit of eliminating them is debatable. However, already for elementary terms we have that the standard normal forms are not norm-minimizing, and it is unclear if norm-minimizing terms will lead to a Goodstein process with a natural ordinal interpretation. Thus it is surprising that such an ordinal interpretation—or even identifying norm-minimizing normal forms to begin with—is not needed to establish the termination of any Goodstein processes based on this notation system.

However, for more powerful notation systems, the elimination of normal forms becomes more pressing, and here the base-change maximality technique is crucial. For notation systems based on the Ackermann function [1], normal forms are already quite cumbersome, so normal form-free Goodstein principles would lead to substantially more accessible independent statements. We have already applied base-change maximality to fast-growing hierarchies [7], where once again normal forms can be quite complex. We believe that, going forward, the analysis of norm-minimality and, especially, base-change maximality will become an essential ingredient in the study of new and ever-more-powerful Goodstein principles.