(G) \({\sf Q} \vdash \varphi \leftrightarrow \neg {\rm Pr}_T(\varphi)\)
を満たす \(\Pi_1\) 文 \(\varphi\) について,PR 論理式 \(\delta(x)\) を \(\neg {\rm Prf}_T(\varphi, x)\) と定めると,\({\sf Q} \vdash \forall x \delta(x) \leftrightarrow \varphi\) なので Theorem 1 より \(T \nvdash \forall
x \delta(x)\) である.
- \(\delta(x)\) は PR 論理式なので \(T \vdash \delta(x) \to {\rm Pr}_T(\delta(\dot{x}))\) である.
- 一方 \(T \vdash \neg \delta(x) \to {\rm Prf}_T(\varphi, x)\) なので \(T \vdash\neg \delta(x) \to {\rm Pr}_T(\varphi)\) である. \(T \vdash \varphi \to \delta(x)\) なので \(T \vdash {\rm Pr}_T(\varphi)
\to {\rm Pr}_T(\delta(\dot{x}))\) であり,\(T \vdash \neg \delta(x) \to {\rm Prf}_T(\delta(\dot{x}))\) となる.
したがって \(T \vdash {\rm Pr}_T(\delta(\dot{x}))\) つまり \(T \vdash \forall x{\rm Pr}_T(\delta(\dot{x}))\) が成り立つ.