@user21820 You may find this thing I came up with recently to be amusing (though it seems I wasn't the first to come up with it)
Let $i,k,n$ denote natural numbers and $F_0$ be the set of $\mathbb N\mapsto\mathbb N$ functions and $F_{k+1}$ be the set of $F_k\mapsto F_k$ functions. Let $f_i$ denote an element of $F_i$.
Define $\operatorname{Iterate}_k$ as an element of $F_k$ as follows:
Let $\operatorname{Iterate}_0=n\mapsto n+1$ be the successor function.
For $k\ne0$, let $\operatorname{Iterate}_k=f_{k-1}\mapsto f_{k-2}\mapsto\dots\mapsto f_1\mapsto f_0\mapsto n=f_{k-1}^n(f_{k-2})\dots(f_…
Let $i,k,n$ denote natural numbers and $F_0$ be the set of $\mathbb N\mapsto\mathbb N$ functions and $F_{k+1}$ be the set of $F_k\mapsto F_k$ functions. Let $f_i$ denote an element of $F_i$.
Define $\operatorname{Iterate}_k$ as an element of $F_k$ as follows:
Let $\operatorname{Iterate}_0=n\mapsto n+1$ be the successor function.
For $k\ne0$, let $\operatorname{Iterate}_k=f_{k-1}\mapsto f_{k-2}\mapsto\dots\mapsto f_1\mapsto f_0\mapsto n=f_{k-1}^n(f_{k-2})\dots(f_…
Actually there is a much simpler 'reason':
$
\def\nn{\mathbb{N}}
$
(1) "$\forall n \in \nn\ ( T \vdash P(n) )$" expands to "$\forall n \in \nn\ \exists q \in Strings\ ( \text{$q$ is a proof over $T$ of $P(n)$} )$".
(2) "$T \vdash \forall n ( P(n) )$" expands to "$\exists q \in Strings\ (...
