Vrftsjtryk

A weak Goodstein sequence starting at $m>0$ is a sequence $m_0,m_1,cdots$ of natural numbers defined by $m_0=m$. To obtain $m_{k+1}$ form $m_k$ (as long as $m_kneq 0$), write $m_k$ in base $k+2$, increase the base by $1$ (to $k+3$), and subtract $1$. For example, the weak Goodstein sequence starting at $m=21$ is as follows:

$m_0=21=2^4+2^2+2^0$

$m_1=3^4+3^2+3^0-1=90$

$m_2=4^4+4^2-1=271$

$m_3=5^4+5^1cdot 3+5^0cdot 3-1=642$

Theorem: For each $m>0$, the weak Goodstein sequence starting at $m$ eventually terminates with $m_n=0$ for some $n$.

Does my attempt look fine or contain logical flaws/gaps? Any suggestion is greatly appreciated. Thank you for your help!

My attempt:

Let $m_0,m_1,cdots$ be the weak Goodstein sequence starting at $m$. Its $a^{rm th}$ term is written in base $a+2$: $$m_a=(a+2)^{b_1}k_1+cdots+(a+2)^{b_n}k_n$$

Consider the ordinal $alpha_a=omega^{b_1}cdot k_1+cdots+omega^{b_n}cdot k_n$ obtained by replacing $a+2$ by $omega$. We have $$begin{align}m_{a+1}&=(a+3)^{b_1}k_1+cdots+(a+3)^{b_n}k_n-1\&=(a+3)^{b_1}k_1+cdots+(a+3)^{b_{n-1}}k_{n-1}+left((a+3)^{b_n}k_n-1right)\&=(a+3)^{b_1}k_1+cdots+(a+3)^{b_{n-1}}k_{n-1}+(a+3)^{b'_n}k'_nend{align}$$ where $(a+3)^{b_n}k_n-1=(a+3)^{b'_n}k'_n$.

It follows that $b_n>b'_n$ and that $alpha_a>alpha_{a+1}=omega^{b_1}cdot k_1+cdots+omega^{b_{n-1}}cdot k_{n-1}+omega^{b'_n}cdot k'_n$. Then $alpha_0>alpha_1>cdots>alpha_a>cdots$ is a decreasing sequence of ordinals.

If $(m_a mid ainBbb N)$ did not go to $0$, it would not terminate and thus be infinite. Consequently, $(alpha_amid ain Bbb N)$ would be infinite. This contradicts the fact that $<$ is a well-founded relation on ordinals.

For each $m>0$, the Goodstein sequence starting at $m$ eventually terminates with $m_n=0$ for some $n$.

When $m_a$ is written in pure base $a+2$, we get an ordinal $alpha_a$ by replacing each $a+2$ by $omega$. Then we can define a similar decreasing sequence of ordinals. By similar reasoning, the Goodstein sequence must terminate.