>>663
＞でも述語論理の時ってsubformula propertyって成り立ちましたっけ？
まいったなぁ。成り立つに決まってるでしょ。っていうより、Cutが除去できるなら
あたりまえでしょ。もしかしてCut除去定理って何のことだかよく知らないんじゃないの？
っていうか、Cut以外の推論規則がどうなってるか知らないのかなぁ。

ちなみに証明図の最後のSequent（つまりその証明図によって証明されたSequent）
に使われていない、個体定数、関数記号、述語記号のすべてを証明図から
取り去ることもできます。
　前原昭二「数理論理学」（培風館）
のp.100以降参照のこと。