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?