 providing that in the case of I being a cut with cut formula A we also have \(\lvert A\rvert &lt;k\). We will write \({\PA_{\omega} \stile{\alpha}{k} \Gamma} \Rightarrow \Delta\) to convey that there exists a \(\PA_{\omega}\)-deduction \({\cD\stile{\alpha}{k} \Gamma}\Rightarrow \Delta\). The ordinal analysis of PA proceeds by first unfolding any PA-deduction into a \(\PA_{\omega}\)-deduction: 