>>70
再帰的になるということは、各文献で目にしていますが、確認はしていません。
なので、現在はproof(x,y)が本当に再帰的な述語であるかどうかを確認するため、これを構成する際に必要な諸々の述語を再帰的かどうか確認しています。
とまぁ、この過程で今「ゲーデル数xはPAの項である。」でどんづまっています。