So I was reading about Goodstein Sequences:
https://en.wikipedia.org/wiki/Goodstein%27s_theorem
where it is given as an example of a theorem that is not decidable in PA but decidable in second order arithmetic.
So now my question, can one generate a 2-dimensional list of theorems $X_{i,j}$ where $X_{i,j}$ can be stated in $i^{th}$ order arithmetic, but whose proof requires $j^{th}$ order arithmetic?
Getting something where the separation between $i$ and $j$ is greater than 1 seems to be very hard.
Ideas for $X_{2,3}$
So in the same vein as the Goodstein sequences we can define "minimal-hereditary-hyperoperator-form" of a natural number $X$ with respect to a base $b$.
Before we do this we introduce hyperoperator-forms:
Observe that $X$ has a unique base $b$ representation of the form
$$ a_0 b^0 + a_1 b^1 + ... a_kb^k $$
where $0 < a_i < b$, but now suppose the $k$ were very large. We can compress these expressions further by using tetration:
$$ a_0 b^0 + a_1 b^1 + ... a_k(b\uparrow \uparrow c)\uparrow d $$
And likewise, suppose that $c$ was extremely large, it too can be compressed further by considering
$$ a_k (((b \uparrow \uparrow \uparrow c_1) \uparrow \uparrow c_2) \uparrow c_3 )$$
Now we generalize: take a number $X$, find the largest m such that
$$ b \uparrow^m c < X, c > 1$$
Then find the largest $c_1, c_2 ... c_{M-1} $ such that
$c_k$ is maximal given $c_1 ... c_{k-1}$ and
$$ b\uparrow ^m c \uparrow^{m-1} c_1 \uparrow^{m-2} c_2 ... \uparrow^{m-k} c_k < X \forall k \in \lbrace 1 ... m \rbrace $$
Then we can collect terms of the form
$$ b\uparrow ^m c \uparrow^{m-1} c_1 \uparrow^{m-2} c_2 ... \uparrow c_{M-1} $$
And subtract them from $X$ repeatedly, sorting them ascending order of magnitude, summed together (collecting like terms with multiplication) to express $X$ uniquely in this extended hyperoperator notation.
Now we can consider the hereditary version of this, by re-expressing any numbers not equal to $b$ or $0$ into this form, repeatedly. Giving us hereditary hyper operator notation.
Consider now the following "Meta-Goodstein Sequence", we start with base $b=2$ and an initial value $X$. As we switch to higher bases, replace every $b$ with $b+1$ and subtract 1, re-expressing in hereditary hyper operator notation.
Claim, for all initial $X$ this goes to 0.
In the traditional goodstein example we are changing the numbers but the "form" of the numbers is steadily decreasing (using the $\omega$ argument). Now even the "form" is apparently increasing but the "form of the form" is decreasing so in third order arithmetic, one can show that this too is a sequence that goes to 0. While this problem itself requires use of functions, so must require at least second arithmetic or higher for it to be posed.
The statement "$n$th-order arithmetic is consistent" is expressible in first-order arithmetic, but not provable in $n$th-order arithmetic; and this is true for every $n$ (EDIT: and provable in $(n+1)$th order arithmetic, as per Carl's comment). We can similarly leap outside finite-order arithmetic in this way.
A more natural example: The statement "There is a structure which computes its own jump" is expressible in second-order arithmetic but not provable in $n$th-order arithmetic for any $n$; see https://arxiv.org/pdf/1106.0908.pdf.
And "Every Borel game is determined" is naturally expressible in third-order arithmetic, but not provable in any limited-order arithmetic at all; see Friedman's paper http://www.sciencedirect.com/science/article/pii/0003484371900180.
Re: the idea in your post, since every computable function can be defined in first-order arithmetic, your meta-Goodstein sentence is expressible in first-order arithmetic. And I don't see any reason why anything beyond $Z_2$ should be needed to prove it. In fact, I think it - and all similar ideas - still won't get you past $ATR_0$, a small fragment of second-order arithmetic.