I'm trying to get a deeper understanding of Buss's version of [Gödel's speedup proof][1]. 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][2], 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?


  [1]: https://www.math.ucsd.edu/~sbuss/ResearchWeb/godelone/paper.pdf
  [2]: https://www.quora.com/Is-true-that-math-theories-in-higher-than-Second-order-logic-can-be-reduced-to-Second-order-logic

**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.)?