>>591
＞カットって何のこといってるの？
おお、先走った。
ロッサーの方法による無矛盾性と、
カット抜きの証明の定義による無矛盾性は
別物だったな。
とはいえ、ここでは無矛盾性のようなものにも
異なる形式化が考えられ、しかもそれは体系に
よっては異なる意味をもつ場合があると考えられる
わけであるから、単純に形式化以降の話をチェック
したって「真偽判定」については無意味だってこと。