 As a result, if \({\PA_{\omega} \stile{\alpha}{n} \Gamma}\Rightarrow \Delta\), we may apply the previous theorem n times to arrive at a cut-free deduction \({\PA_{\omega} \stile{\rho}{0} \Gamma} \Rightarrow \Delta\) with \(\rho=\omega^{\omega^{\iddots^{\omega^{\alpha}}}}\), where the stack has height n. Combining this with the result from \((\ref{einbett})\), it follows that every sequent \(\Gamma\Rightarrow \Delta\) deducible in PA has a cut-free deduction in \(\PA_{\omega}\) of length \(&lt;\varepsilon_0\). Ruminating on the details of how this result was achieved yields a consistency proof for PA from transfinite induction up to \(\varepsilon_0\) for elementary decidable predicates on the basis of finitist reasoning (as described below).