>>219
>証明可能性述語の具体的構成なんて不要だけどね。

後から考えればそうだけどね

要するに
Σ1(帰納的枚挙可能)述語　を
Δ1(計算可能)述語　に
潰すことはできないのが本質

証明チェック述語が原始的帰納関数として記載できる
というのはそれはそれで立派な成果
（ただのプログラミングではあるが・・・まあパイオニアですから）