\section{Fourth Hyperoperation is Tetration Operation}
Tags: Hyperoperation

\begin{theorem}
The '''$4$th hyperoperation''' is the tetration operation restricted to the positive integers:
:$\forall x, y \in \Z_{\ge 0}: H_4 \left({x, y}\right) = x \uparrow \uparrow y$
where $\uparrow \uparrow$ denotes tetration:
:$x \uparrow \uparrow n := \begin{cases}
1 & : n = 0 \\
x \uparrow \left({x \uparrow \uparrow \left({n - 1}\right)}\right) & : n > 0 \\
\end{cases}$
In this context, $x \uparrow y$ is the Knuth notation for powers:
:$x \uparrow y := x^y$
\end{theorem}

\begin{proof}
By definition of the hyperoperation sequence:
:$\forall n, x, y \in \Z_{\ge 0}: H_n \left({x, y}\right) = \begin{cases}
y + 1 & : n = 0 \\
x & : n = 1, y = 0 \\
0 & : n = 2, y = 0 \\
1 & : n > 2, y = 0 \\
H_{n - 1} \left({x, H_n \left({x, y - 1}\right)}\right) & : n > 0, y > 0 \end{cases}$
Thus the $4$th hyperoperation is defined as:
:$\forall x, y \in \Z_{\ge 0}: H_4 \left({x, y}\right) = \begin{cases}
1 & : y = 0 \\
H_3 \left({x, H_4 \left({x, y - 1}\right)}\right) & : y > 0 \end{cases}$
From Third Hyperoperation is Integer Power Operation:
:$(1): \quad \forall x, y \in \Z_{\ge 0}: H_4 \left({x, y}\right) = \begin{cases}
1 & : y = 0 \\
x \uparrow H_3 \left({x, y - 1}\right) & : y > 0 \end{cases}$
The proof proceeds by induction.
For all $y \in \Z_{\ge 0}$, let $P \left({y}\right)$ be the proposition:
:$\forall x \in \Z_{\ge 0}: H_4 \left({x, y}\right) = x \uparrow \uparrow y$
\end{proof}

