Technically Exists

Theorem ω\omega-1

This theorem establishes a simple upper bound on the Wainer hierarchy up to ω\omega in terms of hyper operators.

2⋅fα(n)≤2[α+1](2⋅n) for α<ω2⋅fω(n)≤2[n+1](2⋅n)\begin{align*} 2 \cdot f_\alpha(n) &\le 2 [\alpha + 1] (2 \cdot n) \text{ for } \alpha < \omega \\ 2 \cdot f_\omega(n) &\le 2 [n + 1] (2 \cdot n) \\ \end{align*}

The correctness of this bound was originally proven by Deedlit for 1≤α<ω1 \le \alpha < \omega and n≥1n \ge 1. This proof follows the same approach as Deedlit’s proof. It is worth noting that Deedlit has also proven the correctness of a more complicated but tighter upper bound.

Lemma ω\omega-0

In order for 2⋅fm(n)≤gm(2⋅n)2 \cdot f^m(n) \le g^m(2 \cdot n) to hold for all m,n∈N0m, n \in \N_0, it is sufficient for the following conditions to be met.

  1. ff is a function f:N0→N0f : \N_0 \to \N_0
  2. gg is a non-decreasing function g:N0→N0g : \N_0 \to \N_0
  3. 2⋅f(n)≤g(2⋅n)2 \cdot f(n) \le g(2 \cdot n) for all n∈N0n \in \N_0

Proof

Base case:

2⋅f0(n)=2⋅n=g0(2⋅n)\begin{align*} 2 \cdot f^0(n) &= 2 \cdot n \\ &= g^0(2 \cdot n) \\ \end{align*}

Induction step for mm:

2⋅fm(n)≤gm(2⋅n)by the induction hypothesisg(2⋅fm(n))≤g(gm(2⋅n))by conditions 1 and 22⋅f(fm(n))≤g(gm(2⋅n))by condition 32⋅fm+1(n)≤gm+1(2⋅n)\begin{align*} 2 \cdot f^m(n) &\le g^m(2 \cdot n) &&\text{by the induction hypothesis} \\ g(2 \cdot f^m(n)) &\le g(g^m(2 \cdot n)) &&\text{by conditions 1 and 2} \\ 2 \cdot f(f^m(n)) &\le g(g^m(2 \cdot n)) &&\text{by condition 3} \\ 2 \cdot f^{m + 1}(n) &\le g^{m + 1}(2 \cdot n) \\ \end{align*}

Lemma ω\omega-1

2⋅n≤2[m]n2 \cdot n \le 2 [m] n for all m,n∈N0,m≥2m, n \in \N_0, m \ge 2.

Proof

Base cases where m=2m = 2:

2⋅n=2[2]n\begin{align*} 2 \cdot n &= 2 [2] n \\ \end{align*}

Base cases where n=0n = 0 and m≥3m \ge 3:

2⋅0=0<1=2[m]0\begin{align*} 2 \cdot 0 &= 0 \\ &< 1 \\ &= 2 [m] 0 \\ \end{align*}

Base cases where n=1n = 1:

2⋅1=2=2[m]1\begin{align*} 2 \cdot 1 &= 2 \\ &= 2 [m] 1 \\ \end{align*}

Induction step for n≥1n \ge 1, with the assumption that the lemma holds for mm:

2⋅(n+1)=2⋅n+2≤2⋅n+2⋅n=2⋅(2⋅n)≤2⋅(2[m+1]n)by the induction hypothesis≤2[m](2[m+1]n)by assumption=2[m+1](n+1)\begin{align*} 2 \cdot (n + 1) &= 2 \cdot n + 2 \\ &\le 2 \cdot n + 2 \cdot n \\ &= 2 \cdot (2 \cdot n) \\ &\le 2 \cdot (2 [m + 1] n) &&\text{by the induction hypothesis} \\ &\le 2 [m] (2 [m + 1] n) &&\text{by assumption} \\ &= 2 [m + 1] (n + 1) \\ \end{align*}

Performing induction over mm completes the proof.

Lemma ω\omega-2

(2[α+1])m(2[α+2]n)=2[α+2](n+m)(2 [\alpha + 1])^m (2 [\alpha + 2] n) = 2 [\alpha + 2] (n + m) for all m,n,α∈N0m, n, \alpha \in \N_0.

Proof

Base case:

(2[α+1])0(2[α+2]n)=2[α+2]n=2[α+2](n+0)\begin{align*} (2 [\alpha + 1])^0 (2 [\alpha + 2] n) &= 2 [\alpha + 2] n \\ &= 2 [\alpha + 2] (n + 0) \\ \end{align*}

Induction step for mm:

(2[α+1])m+1(2[α+2]n)=2[α+1]((2[α+1])m(2[α+2]n))=2[α+1](2[α+2](n+m))by the induction hypothesis=2[α+2](n+m+1)\begin{align*} (2 [\alpha + 1])^{m+1} (2 [\alpha + 2] n) &= 2 [\alpha + 1] ((2 [\alpha + 1])^m (2 [\alpha + 2] n)) \\ &= 2 [\alpha + 1] (2 [\alpha + 2] (n + m)) &&\text{by the induction hypothesis} \\ &= 2 [\alpha + 2] (n + m + 1) \\ \end{align*}

Proof of Theorem ω\omega-1

Base case:

2⋅f0(n)=2⋅(n+1)=2+(2⋅n)=2[0+1](2⋅n)\begin{align*} 2 \cdot f_0(n) &= 2 \cdot (n + 1) \\ &= 2 + (2 \cdot n) \\ &= 2 [0 + 1] (2 \cdot n) \\ \end{align*}

Induction step for α\alpha:

2⋅fα+1(n)=2⋅fαn(n)≤(2[α+1])n(2⋅n)by the induction hypothesis and Lemma ω-0≤(2[α+1])n(2[α+2]n)by Lemma ω-1=2[α+2](2⋅n)by Lemma ω-2\begin{align*} 2 \cdot f_{\alpha + 1}(n) &= 2 \cdot f_\alpha^n(n) \\ &\le (2 [\alpha + 1])^n (2 \cdot n) &&\text{by the induction hypothesis and Lemma } \omega\text{-0} \\ &\le (2 [\alpha + 1])^n (2 [\alpha + 2] n) &&\text{by Lemma } \omega\text{-1} \\ &= 2 [\alpha + 2] (2 \cdot n) &&\text{by Lemma } \omega\text{-2} \\ \end{align*}

Case where α=ω\alpha = \omega:

2⋅fω(n)=2⋅fω[n](n)=2⋅fn(n)≤2[n+1](2⋅n)by the previous cases\begin{align*} 2 \cdot f_\omega(n) &= 2 \cdot f_{\omega[n]}(n) \\ &= 2 \cdot f_n(n) \\ &\le 2 [n + 1] (2 \cdot n) &&\text{by the previous cases} \\ \end{align*}