- 98 名前：１３２人目の素数さん mailto:sage [2011/10/31(月) 08:33:10.20 ]
- >>91
g(x)が再帰的関数、P(x,y)が再帰的述語のとき、∃y<g(x) P(x,y) も再帰的述語になるということはご存知ですか？
Prove(x) (⇔ヨyproof(x,y) ) の場合、yを上から抑えるg(x)が存在しません
例えば、論理式Aを証明する過程でむちゃくちゃ長い論理式を経由しなければならない場合もあるかもしれないのです
一方、項の定義では、生成規則は必ず生成前のより生成後の方が記号列の長さが大きくなるように作られています
したがって、項Tを生成する列T1,T2,...,Tnで n≦(Tの長さ)、かつ∀p=1,2,...,n Tp≦Tとなるようなものを具体的に作ることが可能です
よって、yを上から抑えるg(x)が存在することになり、結果IsTerm(x)も再帰的になるのです
