I'm trying to get a deeper understanding of Buss's version of Gödel's speedup proof. In short, if we assume that $Z_0$ is first-order arithmetic, $Z_1$ is second-order arithmetic, and so on, then for $i>0$, $Z_{i+1}$ exhibits speedup over $Z_i$. But on page 11, he says this without citing it:

Using a truth-definition for (i+1)-st order formulas, $Z_{i+1}$ can prove the consistency of $Z_i$, i.e., $Z_{i+1}$ can prove $(\forall_x)Con_{z_i}(x).$

Here, $Con_{z_i}(x)$ means: $Z_i$ is consistent up to all proofs in $Z_i$ which have symbol lengths $\leq x$ (using some fixed encoding of proof length). Clearly, this is decidable: just list all $Z_i$-proofs up to size $x$ and make sure they don't prove any inconsistencies.

But here's where I'm lost. From Gödel's second incompleteness theorem, second-order arithmetic cannot prove its own consistency:

$\neg (Z_1 \vdash (\forall_x)Con_{z_1}(x))$

But according to Buss's statement, third-order arithmetic can prove:

$Z_2 \vdash (\forall_x)Con_{z_1}(x)$

And since second-order logic can express anything that higher-order logics can, this means:

$Z_1 \vdash (\forall_x)Con_{z_1}(x)$

I'm sure that I'm missing some nuance here. So here are my questions:

1. Is there a definitive citation for the claim that for all $i\geq 0$, $Z_{i+1} \vdash (\forall_x)Con_{z_i}(x)$? I know you can do this for $Z_0$ by expressing the Tarskian conditions for a truth predicate in $Z_1$, but it's not clear to me you can do that with higher-order logics as well.

2. Is there a definitive citation for the claim that $Z_1$ can express anything that $Z_2$, $Z_3$, ... can?

3. What am I missing in my apparent contradiction above?

I'm trying to get a deeper understanding of Buss's version of Gödel's speedup proof. In short, if we assume that $Z_0$ is first-order arithmetic, $Z_1$ is second-order arithmetic, and so on, then for $i>0$, $Z_{i+1}$ exhibits speedup over $Z_i$. But on page 11, he says this without citing it:

Using a truth-definition for (i+1)-st order formulas, $Z_{i+1}$ can prove the consistency of $Z_i$, i.e., $Z_{i+1}$ can prove $(\forall_x)Con_{z_i}(x).$

Here, $Con_{z_i}(x)$ means: $Z_i$ is consistent up to all proofs in $Z_i$ which have symbol lengths $\leq x$ (using some fixed encoding of proof length). Clearly, this is decidable: just list all $Z_i$-proofs up to size $x$ and make sure they don't prove any inconsistencies.

But here's where I'm lost. From Gödel's second incompleteness theorem, second-order arithmetic cannot prove its own consistency:

$\neg (Z_1 \vdash (\forall_x)Con_{z_1}(x))$

But according to Buss's statement, third-order arithmetic can prove:

$Z_2 \vdash (\forall_x)Con_{z_1}(x)$

And since second-order logic can express anything that higher-order logics can, this means:

$Z_1 \vdash (\forall_x)Con_{z_1}(x)$

I'm sure that I'm missing some nuance here. So here are my questions:

1. Is there a definitive citation for the claim that for all $i\geq 0$, $Z_{i+1} \vdash (\forall_x)Con_{z_i}(x)$? I know you can do this for $Z_0$ by expressing the Tarskian conditions for a truth predicate in $Z_1$, but it's not clear to me you can do that with higher-order logics as well.

2. Is there a definitive citation for the claim that $Z_1$ can express anything that $Z_2$, $Z_3$, ... can?

3. What am I missing in my apparent contradiction above?

EDIT: I'm now convinced that my understanding of the expressive power of second-order logic was indeed where the flaw was, as SOL can in fact express whatever third- and higher-order logics can (in the sense of mutual validity), but that SOL can not necessarily capture whatever third- and higher-order logics can. But part of my original question is still unanswered: does anyone have a citation or proof of Buss's claim I quoted above (that second-order arithmetic can prove the consistency of first-order arithmetic, third-order arithmetic can prove the consistency of second-order arithmetic, etc.)?