- 257 名前：253 [05/03/16 17:59:48 ]
- >>256
私が今読んでる証明は、数学的帰納法を2重に使用する方法でCutを除去する
のですが、その場合、今着目している証明図の固有変数(eigen variable)
が各々の（∀右）と（∃左）で”固有”なものとなるように書き換えを行う
んです。とすれば、
Γ⇒Θ、A(x)
−−−−−−−−−
Γ⇒Θ、∀yA(y)
のように変数を換えてしまうのも推論規則の中に含めていないと考えづらい
ですよね。そこで上記のような話になるんです。
「下式に固有変数がないこと」という条件を無視して推論すると言うこと
を言っているのではありません。
