- 665 名前：632 mailto:sage [2005/10/19(水) 00:44:31 ]
- >>663
＞でも述語論理の時ってsubformula propertyって成り立ちましたっけ？
まいったなぁ。成り立つに決まってるでしょ。っていうより、Cutが除去できるなら
あたりまえでしょ。もしかしてCut除去定理って何のことだかよく知らないんじゃないの？
っていうか、Cut以外の推論規則がどうなってるか知らないのかなぁ。
ちなみに証明図の最後のSequent（つまりその証明図によって証明されたSequent）
に使われていない、個体定数、関数記号、述語記号のすべてを証明図から
取り去ることもできます。
前原昭二「数理論理学」（培風館）
のp.100以降参照のこと。
