証明可能性述語の具体的構成なんて不要だけどね。
理論Tの論理式φと証明図τがそれぞれ任意に与えられたときにτはTにおけるφの証明図であるという関係を述語Proof(τ,φ)で表す。φがTで証明可能であることは∃xProof(x,φ)で与えられる。
証明図は有限長だからTが再帰的ならProof(τ,φ)の真偽は有限時間で判定可能なのでProof(x,y)はΣ1論理式、よって∃xProof(x,φ)もΣ1論理式。よってTの定理全体の集合はΣ1集合。
これだけの情報があれば不完全性定理の証明に十分。
尚、ゲーデル文Gは T|-(G⇔¬∃xProof(x,G)) を満たす閉論理式。