\(\delta_g(x, y)\) を，\(g\) を \(T\) において define する \(\Sigma_1\) 論理式とし，\(\Pi_1\) 文 \(\psi_0\) と \(\psi_1\) を \[ T \vdash \psi_0 \leftrightarrow \forall y, z({\rm Prf}^\mu(\psi_0 \lor \psi_1, y)
\land \exists v(\delta_g(y, v) \land z \leq v) \land {\rm Prf}(\psi_0, z) \to \exists u < z {\rm Prf}(\psi_1, u)), \] \[ T \vdash \psi_1 \leftrightarrow \forall y, z({\rm Prf}^\mu(\psi_0 \lor
\psi_1, y) \land \exists v(\delta_g(y, v) \land z \leq v) \land {\rm Prf}(\psi_1, z) \to \exists u \leq z {\rm Prf}(\psi_0, u)), \] を満たすものとしてとる．
- 理論 \(T + \neg \psi_0\) において議論し，\(\psi_1\) を示す： \(\neg \psi_0\) より，\({\rm Prf}^\mu(\psi_0 \lor \psi_1, y)\) を満たす \(y\) と \(\delta_g(y, v)\) を満たす \(v\) があって，\(z \leq v\) となるある \(z\) に対して \({\rm
Prf}(\psi_0, z)\) かつ \(\forall u < z \neg {\rm Prf}(\psi_1, u)\) となる． いま \({\rm Prf}^\mu(\psi_0 \lor \psi_1, y)\) を満たす \(y\) と \(\delta_g(y, v)\) を満たす \(v\)，\({\rm Prf}(\psi_1, w)\) となる \(w
\leq v\) をとれば，このような \(y\) と \(v\) の一意性より\(w \geq z\) となる． したがって \(z \leq w\) で \({\rm Prf}(\psi_0, z)\) となるものがとれる． 以上より \(\psi_1\) が成り立つ． つまり \(T \vdash \psi_0 \lor \psi_1\) が成り立つことが示せた．
\(T\) における \(\psi_0 \lor \psi_1\) の最小の証明を \(p\) とする． このとき \[ T \vdash \psi_0 \leftrightarrow \forall z \leq g(p)({\rm Prf}(\psi_0, z) \to \exists u < z {\rm Prf}(\psi_1, u)), \] \[ T
\vdash \psi_1 \leftrightarrow \forall z \leq g(p)({\rm Prf}(\psi_1, z) \to \exists u \leq z {\rm Prf}(\psi_0, u)), \] となる．
- \(\psi_0\) か \(\psi_1\) が \(g(p)\) 以下に \(T\) における証明をもつと仮定する． 例えば \(\psi_0\) が \(\psi_1\) より小さい証明をもてば，\(T \vdash \exists z \leq g(p)({\rm Prf}(\psi_0, z) \to \forall u< z \neg {\rm
Prf}(\psi_1, u))\) なので \(T \vdash \neg \psi_0\) となるためおかしい． \(\psi_1\) が \(\psi_0\) より小さい証明をもつときも同様におかしくなる．
したがって \(\psi_0\) も \(\psi_1\) も \(g(p)\) 以下に \(T\) における証明をもたない．
- よって \(i = 0, 1\) に対して \(T \vdash \forall z \leq g(p) \neg {\rm Prf}(\psi_i, z)\) なので \(T \vdash \psi_i\) となる．