11/02/17 20:36:27
>>323
ご回答ありがとうございます。図書館で調べてみます。
＞ωを 3 に置き換えればよい
というのは、無矛盾性証明において証明図に順序数を対応させたのと同様に、
LKのカット除去でも証明図に、例えば自然数3＾（3＾（1+1））を対応させる、ということでしょうか。
この方針で試みてみようと思います。
11/02/17 20:36:27
>>323
ご回答ありがとうございます。図書館で調べてみます。
＞ωを 3 に置き換えればよい
というのは、無矛盾性証明において証明図に順序数を対応させたのと同様に、
LKのカット除去でも証明図に、例えば自然数3＾（3＾（1+1））を対応させる、ということでしょうか。
この方針で試みてみようと思います。