ある再帰的関数 \(f\) があって，任意の文 \(\varphi\) について，\(T \vdash \varphi\) ならば \(f(\varphi)\) 以下に \(T\) における \(\varphi\) の証明があると仮定する． このとき与えられた文 \(\varphi\) に対して \(f(\varphi)\) を計算し，\(f(\varphi)\) 以下の各 \(k\) が \(T\) における \(\varphi\) の証明かどうかをチェックする． もしその中に \(T\) における \(\varphi\) の証明があれば \(T \vdash \varphi\) であり，なければ \(T \nvdash \varphi\) である． したがって \(T\) は決定可能であり，\({\sf Q}\) が本質的決定不可能（Theorem 1.2）であることに反する． つまり各再帰的関数 \(f\) に対してある文 \(\varphi\) があって，\(T \vdash \varphi\) であり，かつ \(f(\varphi)\) 未満に \(T\) における \(\varphi\) の証明はない．