A Mechanizable First-Order Theory of Ordinals

Abstract

We present a first-order theory of ordinals without resorting to set theory. The theory is implemented in the KeY program verification system which is in turn used to prove termination of a Java program computing the Goodstein sequences.

1 Introduction

A number of automated reasoning systems have been put to the task to prove theorems about ordinal numbers. Here is a fair selection of pertinent papers: [4, 5, 9, 15] for the Isabelle proof assistent, [6, 8] for Coq, [3] for OTTER. All these efforts have in common that they start with a semantic definition of ordinals as sets with special properties. Of a different flavor are the papers [13, 14], that present algorithms implemented in the ACL2 system for solving problems in ordinal arithmetic working on a normal form representation.

In this paper, we will present a first-order theory $Th_{Ord}$ of ordinals. The models of $Th_{Ord}$ are of the form $\mathcal {M} =(U, \dot{0}, \dot{\omega }, \dot{+1}, \dot{<})$ with universe U, constants $\dot{0}$, and $\dot{\omega }$, the unary successor function $\dot{+1}$ and the order relation $\dot{<}$. The logic itself contains the binary operator $sup_{x<n} m$ binding variable x. Its interpretation in $\mathcal {M}$ is the supremum of $\{ m^{\mathcal {M}}(\alpha )\mid \alpha \in U \text { and } \alpha \dot{<} n^{\mathcal {M}}\}$. Typically, the term m will contain the free variable x and $t^{\mathcal {M}}(\alpha )$ stands for the evaluation of m in $\mathcal {M}$ with x instantiated to the element $\alpha \in U$. The operator $sup_{x<n}m$ is the only construct in our axiomatization with a set theoretic flavor. This operator is, however, definable in the standard first-order logic; a proof of this result for variable-binders in general is available in Ulbrich’s PhD thesis [22].

Already in 1965 Gaisi Takeuti presented in [20] a first-order theory $\mathcal {O}$ of ordinal numbers. His interest were in proof theoretic properties. The theory $\mathcal {O}$ allows to define an inner model of Zermelo-Fraenkel (ZF) set theory. Thus, a formula $\phi$ is derivable from $\mathcal {O}$ iff a canoncial translation of $\phi$ is derivable in ZF set theory. The vocabulary of $\mathcal {O}$ is much richer than ours: it contains e.g., already in its axiomatic basis coding and decoding functions for pairs of ordinals. As a consequence the theory $\mathcal {O}$ is not very well suited as the basis for automated reasoning on ordinals.

It is well-known that the Peano axioms, PA, for the natural numbers are incomplete. This did and does not cause much alarm since the examples of true statements not derivable in PA were consider too arcane to be of any pratical relevance. This is beginning to change as these examples get more and more accessible. We present, based on [10], a Java program with less than 20 lines of code, computing the Goodstein sequences, such that termination of one of its two methods cannot be proved in PA. Still, there is no reason to be alarmed since termination can be proved in $Th_{Ord}$, which is a simple, plausible extension of PA as can be seen by scrutinizing the axioms in Fig. 1 below.

Fig. 1.

The axioms of the core theory

The first automatic termination proof for Goodstein sequences was recorded in [23]. In that paper a finite rewrite system is presented whose termination encodes the termination of these sequences and termination of the rewrite system is proved. A termination proof using the higher-order logic proof assistant Coq can be downloaded from [7] as part of the Coq project on ordinal notation [6]. Hereditary multisets, a variant of nested multisets, offer a convenient representation of ordinals below $\epsilon _{0}$. A formalization of hereditary multisets in the Isabelle/HOL proof assistant is available from the Archive of Formal Proofs [5] also containing a termination proof for Goodstein sequences. A corresponding publication is pending [4]. The theory $Th_{Ord}$ has been implemented in KeY, a first-order theorem proving and program verification system based on the sequent calculus [1]. This implementation has been put to use to obtain a machine assisted termination proof of the Java program mentioned above. This seems to be the first termination proof for Goodstein sequences using a first-order reasoning system.

2 A Theory of Ordinals

In the first subsection, we start out with a very simple core theory $Th_{Ord}^{0}$. This plays the same role here as Peano’s theory for the arithmetic of natural number. In the next subsection, the final theory $Th_{Ord}$ is obtained as a definitional extension of $Th_{Ord}^{0}$.

2.1 The Core Theory

The vocabulary $\varSigma _{Ord}^{0}$ of the core theory contains the following symbols

$\begin{array}{ll@{}l} \mathbf{predicate } &{} < &{} \text {binary}\\ \mathbf{functions } &{} +1 &{} \text {unary}\\ &{} 0, \omega &{} \text {constants} \\ \end{array}$

Terms and formulas are defined as usual in first-order logic with the exception that we include a term building operator sup:

if n, m are terms and x is a variable that does not occur free in n, then

$$\begin{aligned} sup_{x<n}m \end{aligned}$$

is a term.

Two operations, (1) start with 0 and (2) add one, suffice to generate all finite ordinals. We use $x+1$ to denote the immediate successor of x to avoid the introduction of an additional symbol. In set theory, a third operation is added to generate all transfinite ordinals: (3) for any set X of ordinals, there is a least ordinal not less than all $\alpha \in X$. Here we avoid set theory and restrict this operation to sets X that can be obtained as instances of one term m, where furthermore only instantiations up to a bound n are allowed. This motivates the term constructor $sup_{x<n}m$. The term m will typically contain the variable x.

In most presentations of Peano arithmetic, the order relation < is not part of the core theory, but it is later added as a definitional extension. It would have been extremely cumbersome to do so in our setting. So, we sacrificed on minimality and included < from the outset.

The intended meaning of symbols in $\varSigma _{Ord}^{0}$ is fixed by the axioms in Fig. 1.

We thus see that < is to be interpreted as a strict, total, order relation. We use $x\le y$ as a shorthand for $x\doteq y \vee x < y$. From the axioms, we see that 0 is the least element with respect to < and $\omega$ is the first infinite ordinal. Without the two axioms 5 and 6 for $\omega$, the natural numbers with strict order and successor would be a model of the remaining axioms and nothing would have been gained over Peano’s theory. Axioms 8 and 9 establish the intended meaning of the supremum operator as explained in the introduction. We use the notation m[z / x] to denote the term that arises from m by replacing x by z everywhere. Note that the way we defined sup, the formulas $sup_{x<0}m \doteq 0$ and $sup_{x < 1}m \doteq m[0/x]$ can be derived.

The last and most powerful axiom is the axiom scheme of transfinite induction that is an extension the course-of-value induction scheme in finite arithmetic. Let $\phi$ be a formula that typically would contain x as a free variable and let $\phi (y)$ stand for the formula obtained from $\phi$ by replacing x by y (assuming of course that y does not occur in $\phi$, neither free nor bound). If we can prove for every x the transfinite induction step $\forall y(y<x \rightarrow \phi (y))\rightarrow \phi$, then we conclude that $\phi$ is true for all x.

One could ask whether the sup operator should have been omitted from the core vocabulary and added later as a definitional extension. The answer is no! Since we follow the usual set-up of first-order logic all functions are total. Consequently, inclusion of a function symbol in the vocabulary already implies an implicit existence axiom: the function values exist for all arguments. Adding sup is not a definitional extension since the associated existence claim could not be proved in the theory without sup.

An alternative would have been to include the following axiom scheme instead of the two parts of the definition of sup

$$\forall y(\exists z(\forall x(x<y \rightarrow t\le z)))$$

A possible instantiation could be $\forall y(\exists z(\forall x(x<y \rightarrow \omega ^{x}\le z)))$. Then, it would have been possible to show, using transfinite induction, that adding the sup operator is a definitional extension of this version of the core theory. The adopted approach is more straightforward.

2.2 The Full Theory

The full vocabulary $\varSigma _{Ord}$ of the theory $Th_{Ord}$ is shown in Fig. 2.

Fig. 2.

The full vocabulary $\varSigma _{Ord}$

The axioms of $Th_{Ord}$ are $Th_{Ord}^{0}$ plus the definitions of the new symbols in Figs. 3 and 5.

Fig. 3.

Definitional extension: axioms for auxiliary predicates

The three axioms in Fig. 3 define the auxiliary symbols $\le$ and max plus the important concept of a limit ordinal. In contrast to other presentations, 0 is not a limit ordinal in our set-up.

Figure 4 shows a sample of lemmas that can already be derived at this point from the axioms considered so far. The lemmas are grouped together according to the syntactical symbols involved. This does not reflect the order in which the lemmas can or need to be proved.

Fig. 4.

Some lemmas derivable from the axioms considered so far

Lemma 1 in Fig. 4 is the least number principle, a well known equivalent to the induction axiom scheme. It is instructive to figure out why this lemma is true even if x does not occur as a free variable in $\phi$. Lemma 2 in Fig. 4 is the equivalent rephrasing of the transfinite induction scheme 10 in Fig. 1 that is most frequently employed: If a formula $\phi$ with free variable x is true for $x=0$ (base case), if for all z we can prove that $\phi [z+1]$ follow from $\phi [z]$ (successor induction step), and if we can prove for every limit ordinal $\lambda$, when $\phi [z/x)$ is true for all $z < \lambda$ then $\phi [\lambda /x]$ follows (limit induction step), then we have proved $\forall x\phi$.

Lemma 3 could be rephrased as: if x is a limit ordinal then x is the least ordinal that is greater or equal than all ordinals that are strictly less than x. This is not true for successor ordinals x. In this case, we have $sup_{y < x+1}~y \doteq x$ instead. Lemma 4 is useful in proving statements involving the sup operator via induction. Lemma 5 helps to show that two suprema are equal especially in the case when equality between $t_{1}$ and $t_{2}$ is not obvious.

For the purpose of this paragraph we look at a term t that contains z as a sequence $t_{z}$. We say that a sequence $t_{z < x_{1}}$ is confinal in $s_{z < x_{2}}$ if for every $x < x_{1}$ there is $y < x_{2}$ with $t[x/z]\le s[y/z]$. If two sequences are mutually confinal in one another, then they share the same supremum. This is Lemma 6 in Fig. 4. Note, that we get equality of two suprema with different bounds $x_{1}$, and $x_{2}$. Lemma 7 gives an alternative definition of a limit ordinal.

Fig. 5.

Definitional extension: axioms for arithmetic operations

The second installment of the axioms extending $Th_{Ord}^{0}$ to $Th_{Ord}$ is listed in Fig. 5. They give the usual recursive definitions of ordinal addition, multiplication and exponentiation.

2.3 Derived Lemmas

In this subsection, we will in Figs. 6, 7, 8 and 9 list and comment on a selection of lemmas derivable from $Th_{Ord}$.

Fig. 6.

Lemmas involving addition and order relations

Figure 6 lists lemmas that are needed as intermediate stepping stones in the proofs of the properties of ordinal arithmetic.

Lemma 1 in Fig. 6 extends the axiom $\forall x(x < x+1)$ from Fig. 1 where we now add on the right side an arbitrary number greater than or equal to 1 instead of just 1. This is, of course, proved via transfinite induction. Lemma 2 is an easy variant of Lemma 1. Addition of ordinals is not commutative, so we cannot conclude from Lemma 1 that $\forall x,y(x\ne 0 \rightarrow y<x+y)$. Indeed, $y=\omega , x=1$ is a counterexample. But the version for $\le$ instead of < is provable. This is Lemma 3. Lemma 4 is also proved using transfinite induction. We remark that $\forall x,y,z(x<y \rightarrow x+z < y+z)$ is not true, as can be seen by the instantiation 0 for x, 1 for y, and $\omega$ for z. But the relaxed version with $\le$ instead of < is derivable. This is Lemma 5. Lemma 6 is the reverse of Lemma 4.

Fig. 7.

Lemmas on addition

Figure 7 gives lemmas on ordinal addition. Since ordinal addition is in general not commutative Lemma 1 in Fig. 7 may not be immediately obvious, but it can be easily proved using ordinal induction. Lemma 3 is a fact on ordinal addition that we have referred to already above. Lemma 4 is a useful lemma formalizing the intuition that the property of being a limit ordinal is determined by the right end part of the ordinal regardless of what comes before. Lemma 5 gives a first general representation theorem for ordinals. In [21, Theorem 8.13] it is proved using set comprehension. This is not available in our setting. Fortunately, it turned out that there is a much simpler proof using ordinal induction. Lemma 6 required the most complex proof so far. The basic idea, however, is quite simple. As a witness for z take b, the least ordinal such that $y\le x+b$. It can easily be seen that such a number exists by the least number principle (Lemma 1 in Fig. 4). Then, a case distinction $b=0, b\doteq b_{0}+1$ for some $b_{0}$, or lim(b) leads to success. Lemma 7 is the wellknown associative law. Lemmas 8 and 9 correspond to the Peano axioms for the natural numbers, which say that 0 is not a successor and the successor function is injective. Lemma 10 shows that addition on the right, with fixed left summand, is injective. Lemma 11 resisted for a while all my attempts to prove it. Since I could also not find it in [21], I was, at some point, even in doubt wether it is true at all. The inequality, $sup_{z< x}~(i+t) \le i + sup_{z < x}~t$ is simple. For the reverse inequality a proof by contradiction turned out to be the right way of attack. So assume $sup_{z< x}~(i+t)< i + sup_{z < x}~t$ and try to find a contradiction. The key to the solution was the case distinction $sup_{z< x}~(i+t) < i$ or $i \le sup_{z < x}~(i+t)$. Notice that in the first case, we arrive at the contradiction $i \le i+t[0/z]< sup_{z< x}~(i+t) < i$. Here also the assumption $x>0$ comes in. In the second case, there is by Lemma 5 an ordinal k such that $i+k \doteq sup_{z < x}~(i+t)$. By the proof-by-contradiction assumption, this yields $i+k< i+sup_{z < x}~t$ and further by Lemma 7 in Fig. 6 $k< sup_{z < x}~t$. By the definition of sup there, is $\lambda < x$ with $k\le t[\lambda /z]$. This leads to the contradiction $i+k \le i+ t[\lambda /z]< sup_{z < x}~(i+t)$. The commuted version of Lemma 11, i.e., $sup_{z< x}~(t+i) \doteq (sup_{z < x}~t) + i$, provided z does not occur in i and $x>0$, is – as you would have expected –not true: $\omega \doteq sup_{z< \omega }~(z + 1) \doteq (sup_{z < \omega }~z) + 1 \doteq \omega + 1$. Lemma 12 shows a dramatic failure of commutativity for ordinal addition: A left finite ordinal summand is simply absorbed if the right summand is infinite. We found it helpful to split the proof of Lemma 12 in the cases $\omega \doteq j$ and $\omega < j$.

Fig. 8.

Lemmas on multiplication

Figure 8 shows derivable properties of ordinal multiplication. Lemma 1 shows that the strict order relation is preserved by multiplication on the left, provided that the left multiplyer is not 0. Multiplication on the right only preserves $\le$, as Lemma 4 shows. Lemma 2 is the reverse implication from Lemma 1. Lemma 3 states that multiplication on the right, with a fixed multiplicand on the left, is an injective function. Lemma 7 is crucial for the proof of distributivity (Lemma 8) and multiplicative associativity (Lemma 9).

After all the preparations the proof of multiplicative associativity is now straightforward. Let us for once give a detailed proof sketch in this exemplary case. We use ordinal induction (Lemma 2 in Fig. 4) on the variable k. The base case is trivial. The successor induction step is proved as follows:

$$ \begin{array}{lclr} i*(j*(k+1)) &{} \doteq &{} i*(j*k + j) &{} \text {definition of } *\\ &{} \doteq &{} i*(j*k) + i*j &{} \quad \text {distributivity (Lemma 8)}\\ &{} \doteq &{} (i*j)*k + i*j &{} \text {induction hypothesis}\\ &{} \doteq &{} (i*j)*(k+1) &{} \text {definition of } *\\ \end{array} $$

The induction step in the limit case is shown next. We us $\lambda$ instead of k to signal that k is a limit ordinal:

$$ \begin{array}{lclr} i*(j*\lambda ) &{} \doteq &{} i*sup_{x<\lambda }j*x &{} \text {definition of } *\\ &{} \doteq &{} sup_{x<\lambda }i*(j*x) &{} \text {Lemma 7}\\ &{} \doteq &{} sup_{x<\lambda }(i*j)*x &{} \quad \text {induction hypothesis}\\ &{} \doteq &{} (i*j)*\lambda &{} \text {definition of } *\\ \end{array} $$

Lemma 10 (we are still talking about Fig. 8) is a strengthening of Lemma 6: multiplicative absorbtion on the left of finite ordinals not only holds for $\omega$, but for any limit ordinal. Lemma 11 states when addition of two ordinals is less than their product. The restrictions are necessary as can be seen by the following simple examples:

$$ \begin{array}{rcl} j = 0+j &{} \not \le &{} 0*j = 0\\ 1+j &{} \not \le &{} 1*j = j\\ i = i+0 &{} \not \le &{} i*0 = 0 \\ i+1 &{} \not \le &{} i*1 = i \\ \end{array} $$

Fig. 9.

Lemmas on exponentiation

Finally, we turn to the lemmas on exponentiation in Figure 9. Note that the restriction on x in Lemma 1 is necessary since by definition $0^{0} \doteq 1$. Also the restrictions in Lemma 2, which says that exponentiation is strictly increasing in the left argument, are necessary as can be seen by the following examples $2\not< 2^{0} \doteq 1, 2\not< 2^{1} \doteq 2, 0\not < 0^{2} \doteq 0$, and $1\not < 1^{2} \doteq 1$. It is only weakly increasing on the right, Lemma 3. The strict inequality is far from being true, as Lemma 4 shows. Exponentiation is also strictly monotone in the second argument, as Lemma 5 shows. The reverse implication is also true, as stated by Lemma 7. In the first argument exponention is only weakly monotone, as stated by Lemma 7. A counterexample to strict monotonicity is given by the instantiations $x_1 = 2, x_2 = 3$, and $y=\omega$. Lemmas 8 and 9 show how the property of being a limit ordinal is propagated by exponentiation. Lemmas 10 and 11 are laws of exponentiation familiar from finite arithmetic. Lemma 12 is in fact a lemma scheme. Note that in typical applications x is a free variable in j. It states an indispensable continuity property for exponentiation.

The theory $Th_{Ord}$ has been implemented in the KeY system. Interactive proof for over 170 lemmas found in the set theory textbooks [2, 11, 12, 21] have been obtained documenting the strength of $Th_{Ord}$.

3 Termination of Goodstein Sequences

The sequences under investigation were first introduce by Goodstein in [18]. In fact, Goodstein considered in his paper more general sequences involving a non-decreasing function $f:\mathbb {N}\rightarrow \mathbb {N}$ as a parameter. The Goodstein sequences considered here, these are the same as the ones considered by Kirby and Paris, are obtained by the choice $f(i) = i+2$. Kirby and Paris showed in their highly acclaimed paper [10] that termination of Goodstein sequences cannot be proved in Peano arithmetic, stronger principles, like e.g., ordinal induction, are needed. We will use ordinal induction, as provided by the theory $Th_{Ord}$ presented in Sect. 2, to prove termination of a Java program computing the Goodstein sequences in Subsect. 3.3.

3.1 Injecting Natural Numbers

The termination proof in Subsect. 3.3 will be done using the program verification system KeY. KeY employs a many-sorted first-order logic. For ease of presentation the theory $Th_{Ord}$ was formulated in Sect. 2 as a one-sorted theory. In the implementation of $Th_{Ord}$ within the KeY prover, Ord is used to name the sort of ordinals. Among the other sorts present in the KeY prover, there are mathematical integers int. It is essential for the intended proof to relate non-negative integers to the finite ordinals. To this end, we add a function $onat: int \rightarrow Ord$.

Figure 10 shows an axiomatisation of the function $onat: int \rightarrow Ord$ that maps the non-negative integers into corresponding ordinals less than $\omega$. Obviously, onat is a partial function. The KeY system deals with partial function by underspecification. That means that onat is a total function, but the axioms do not include any commitment on the values for negative arguments.

Fig. 10.

Positive integers as ordinals

Figure 10 also shows useful derived lemmas. We use in this figure and also later on overloaded syntax. Thus, whether 0 denotes an integer or an ordinal, whether $+$ is ordinal addition or addition of non-negative integers can be found out by looking at the type information.

3.2 Definition of Goodstein Sequences

We start with an informal explanation. First, the auxiliary concept of a hereditary base-n notation is needed. This makes only sense for $n\ge 2$. The hereditary base-n notation for a natural number m is obtained from its ordinary base-n notation

$$\begin{aligned} m = m_{k}\cdot n^{k} + m_{k-1}\cdot n^{k-1} + \ldots m_{1}\cdot n + m_{0}, \quad 0\le m_{i} < n, m_{k}\ne 0 \end{aligned}$$

by also writing the exponents $k, k-1$, ...in base-n notation and again the thus arising exponents, and so on.

Example 1

$\begin{array}[t]{l@{}lcl} \text{ base- }2 &{} 35 &{} = &{} 2^{5} + 2^{1} + 2^{0}\\ \text{ hereditary } \text{ base- }2 &{} 35 &{} = &{} 2^{2^{2}+1} + 2 + 1\\ \text{ base- }3 &{} 100 &{} = &{} 3^4 + 2\cdot 3^2 + 3^0\\ \text{ hereditary } \text{ base- }3 &{} 100 &{} = &{} 3^{3+1} + 2\cdot 3^2 + 1. \\ \end{array}$

The Goodstein sequence $G_{k}(m)$ with initial value m is computed as follows

$\begin{array}{lcl} G_{1}(m) &{}=&{} m \\ G_{2}(m) &{}=&{} \text {in the hereditary base-} 2\text { representation of } m \\ &{}&{} \text {replace every occurence of } 2 \text { by } 3 \text { and subtract }1\\ \cdots &{}&{} \\ G_{k}(m) &{} = &{} \text {in the hereditary base-}k \text { representation of } G_{k-1}(m) \\ &{}&{} \text {replace every occurence of } k \text { by } k+1 \text { and subtract } 1\\ \end{array}$

Example 2

The Goodstein sequence for $m=3$

Example 3

Initial part of the Goodstein sequence for $m=4$

  $\begin{array}[t]{|l|l|l|l|} \hline &{} &{} 4 &{}\\ \hline 2^{2^{1}} &{} 3^{3^{1}}-1 &{} 26 &{} \omega ^{\omega }\\ \hline 3^{2}*2 + 3^{1}*2 + 2 &{} 4^{2}*2 + 4^{1}*2 + 2 -1 &{} 41 &{} \omega ^{2}*2 + \omega *2 +2 \\ \hline 4^{2}*2 + 4^{1}*2 +1 &{} 5^{2}*2 + 5^{1}*2 +1 -1 &{} 60 &{} \omega ^{2}*2 + \omega *2 +1\\ \hline 5^{2}*2 + 5^{1}*2 &{} 6^{2}*2 + 6^{1}*2 -1 &{} 83 &{} \omega ^{2}*2 + \omega *2 \\ \hline 6^{2}*2 + 6^{1}*1 + 5 &{} 7^{2}*2 + 7^{1}*1 + 5 -1 &{} 109 &{} \omega ^{2}*2 + \omega + 5\\ \hline 7^{2}*2 + 7^{1}*1 + 4 &{} 8^{2}*2 + 8^{1}+1 + 4 -1 &{} 139 &{} \omega ^{2}*2 + \omega + 4\\ \hline 8^{2}*2 + 8^{1}*1 +3 &{} 9^{2}*2 + 9^{1}*1 +3 -1 &{} 173 &{} \omega ^{2}*2 + \omega + 3\\ \hline 9^{2}*2 + 9^{1}*1 + 2 &{} 10^{2}*2 + 10^{1}*1 + 2 -1 &{} 211 &{} \omega ^{2}*2 + \omega + 2\\ \hline 10^{2}*2 + 10^{1}*1 +1 &{} 11^{2}*2 + 11^{1}*1 +1 -1 &{} 253 &{} \omega ^{2}*2 + \omega + 1\\ \hline 11^{2}*2 + 11^{1}*1 &{} 12^{2}*2 + 12^{1}*1 -1 &{} 299 &{} \omega ^{2}*2 + \omega \\ \hline 12^{2}*2 + 11 &{} 13^{2}*2 + 10 &{} 348 &{} \omega ^{2}*2 + 11\\ \hline &{} &{} &{} \\ \hline &{} &{} 1058 &{} \\ \hline 23^{2}*2 &{} 24^{2}*2 -1 &{} 1151 &{} \omega ^{2}*2 \\ \hline 24^{2} + 24*23 + 23 &{} 25^{2} + 25*23 + 23 -1 &{} 1222 &{} \omega ^{2} + \omega *23 + 23\\ \hline \end{array}$

Example 3 shows the Goodstein sequence with initial value 4 upto its 25-th term. The last column should be ignored on first reading. We will come back to it in the next subsection. Also $G_{k}(4)$ will eventually reach 0, but for k in the order of magnitude of $10^{121210700}$.

The following mathematical formalization of these informal explanations differ in detail greatly from those in the paper [10]. Intuitively the value of the function ${\text {oHNf}}(n,m)$ is obtained by computing the hereditary base-n representation of m and replacing all occurences of n by $n+1$. This is turned into the following recursive definition:

Definition 1

( ${\text {oHNf}}(n.m)$ ). For $n\ge 2, m\ge 0$

$$\begin{aligned} {\text {oHNf}}(n,m) = \left\{ \begin{array}{l@{}l} m &{} if\,\, m< n \\ (n+1)^{{\text {oHNf}}(n,k)}*a + {\text {oHNf}}(n,c) &{} if\,\, m = n^{k}*a + c \,\,with\\ &{} 1 \le k \wedge 0< a< n \wedge c < n^{k} \end{array} \right. \end{aligned}$$

This is a complete definition since we can easily prove:

  $\begin{array}{ll} \forall m,n (2\le n \wedge n \le m \rightarrow \exists r, a, c &{} (m = n^{r}*a + c \quad \wedge \\ &{} \quad 1\le r \wedge 0< a \wedge a< n \wedge c < n^{r} \wedge 0 \le c))\\ \end{array}$

Definition 2

( $G_{n}(m)$ ). For $n\ge 2$ and $m\ge 0$

$\begin{array}{lcl} G_{1}(m) &{} = &{} m \\ G_{k}(m) &{} = &{} {\text {oHNf}}(k,G_{k-1}(m)) - 1\\ \end{array}$

3.3 Termination Proof

Close inspection showed that the original termination proof of Goodstein sequences in [10] is more complicated than necessary. We follow instead the idea of a short proof of the termination of general Goodstein sequences from [16, 17]. Figure 11 shows the Java program to be verified. Since in the default setting the KeY system treats Java integers as mathematical integers this is what we need. Running this program, however, would yield wrong results as soon as is reached. Since exponention is not part of the Java language, the method had to be implemented. Since this is a standard task, the code is not shown here.

Fig. 11.

Goodstein program for verification

We do not assume that every reader is familiar with program verification and will complement the code with explaining comments. Figure 11 contains the Java code plus annotations in the Java Modeling Language (JML). A lucid introduction to JML can be found in [1, Chap. 7]. The following comments should, we hope, be sufficient to provide the reader with a clear understanding of the central points. JML annotations needed to guide the system but not essential for the casual human reader have been omitted, i.e., replaced by ....

JML allows to add specifications enclosed between special comments to a Java program. Formal verification then provides a mathematical proof that the code meets its JML specifications.

JML provides method contracts. These are placed immediately before the method code. The crucial method in Listing 11 is in lines 5–14. Its method contract spans lines 2–4. The clause states a precondition that must be met to guarantee the postcondition. Here the precondition requires the initial value for the Goodstein sequence to be strictly positive. The postcondition is - in this case - hidden in the keyword . This says that the method terminates and no uncaught exceptions are thrown. The code of the method consists of a simple loop computing the Goodstein sequence and breaking out when 0 is reached. Now, a second type of JML contracts comes into play namely, loop contracts. The first part of the loop contract in lines 7–11 requires that the formula be true before entering the loop and after each iteration of the loop body. This is easy. The crucial part of the loop contract is the clause that gives a quantity in some well-founded ordering that is strictly decreased with every loop iteration. Here in line 10 the function ${\text {oGS}}(n,m)$ provides an ordinal for this purpose. The KeY prover knows about the function ${\text {oGS}}$, but it is by no means part of standard JML. The escape sequence triggers the JML parser to pass ${\text {oGS}}$ directly to the underlying logic. The same applies for the functions ${\text {oHNf}}$ and pow. In line 19 the JML keyword $\backslash result$ for the first time. It denotes the return value of the method the annotation belong to, in this case the return value of .

The definition of ${\text {oGS}}(n,m): int \times int \rightarrow Ord$ lies at the very heart of the termination argument. Informally, ${\text {oGS}}(n,m)$ is computed by replacing in the hereditary base-n expansion of m every occurence of n by $\omega$.

Definition 3

For $n\ge 2$, $m\ge 0$

$$ {\text {oGS}}(n,m) = \left\{ \begin{array}{l@{}l} onat(m) &{} if\,\, m< n \\ (\omega )^{{\text {oGS}}(n,k)}*onat(a) + {\text {oGS}}(n,c) &{} if\,\, m = n^{k}*a + c \,\,with \\ &{} 1 \le k \wedge 0< a< n \wedge c < n^{k} \end{array} \right. $$

Examples of ${\text {oGS}}$ for an initial segment of the Goodstein sequence with initial value 4 are displayed in the last column in Example 3. The next lemma lists the crucial properties of ${\text {oGS}}$, that have also been interactively verified with the KeY prover.

Lemma 1

• 1. $\forall n, m_{1}, m_{2}(2\le n \wedge 0\le m_{1}< m_{2} \rightarrow {\text {oGS}}(n,m_{1}) < {\text {oGS}}(n,m_{2}))$

• 2. $\forall n, m (2\le n \wedge 0\le m \rightarrow {\text {oGS}}(n,m) = {\text {oGS}}(n+1,{\text {oHNf}}(n,m)))$

We conclude the subsection by revealing the plan to prove that ${\text {oGS}}$ decreases. An arbitrary loop iteration starts with ${\text {oGS}}(base,m)$. After normal termination of the loop body, the decreasing function evaluates to ${\text {oGS}}(base+1,\backslash result - 1)$, where $\backslash result$ is the return value of the call to method in line 13. The method contract for guarantees that ${\text {oGS}}(base,m)$ and ${\text {oGS}}(base+1,\backslash result)$ are equal (line 20). By Lemma 1(1), oSG is strictly monotone in its second argument. Thus, ${\text {oGS}}(base+1,\backslash result - 1)$ is strictly smaller than ${\text {oGS}}(base+1,\backslash result)$ in the ordinal ordering. Bingo.

In this argument, we have made use of the method contract for , but we also need to establish it. It turns out that for this we need to know that the return value is ${\text {oHNf}}(oldBase,m)$, Line 19 and Lemma 1(2) will come into play at this point.

4 Concluding Remarks

What are the limits of $Th_{Ord}$? Let $\epsilon _{0}$ be the first epsilon ordinal, i.e., the least ordinal $\epsilon$ with $\omega ^{\epsilon } = \epsilon$. Let $\mathcal {M}_{\epsilon _{0}}$ be the structure with all ordinals less than $\epsilon _{0}$ as universe and the standard interpretation of $\varSigma _{Ord}$. It can be easily checked that $\mathcal {M}_{\epsilon _{0}}$ is a model of $Th_{Ord}$. Closure under sup is the crucial part. This shows that $\exists x(\omega ^{x} = x)$ cannot be derived in $Th_{Ord}$. It can furthermore be shown that for a model $\mathcal {M}$ of $Th_{Ord}$ that does not contain nonstandard natural numbers $\mathcal {M}_{\epsilon _{0}}$ is a substructure of $\mathcal {M}$. In a way, $Th_{Ord}$ is the analogon of Peano arithmetic for $\mathcal {M}_{\epsilon _{0}}$. Precise formulations of these claims and complete proofs can be found in the technical report [19].

If we had only intended to present a machine assisted proof of the mathematical theorem that all Goodstein sequences terminate, this could already have been obtained from Lemma 1. We wanted – however – to make the point that there are simple Java programs whose termination cannot be proved in Peano arithmetic, but $Th_{Ord}$ is strong enough to prove it.

Runable Java code, saved proofs and the version of the KeY system needed can be downloaded or “webstarted” from https://www.key-project.org/papers/ordinal-numbers/.