- 347 名前：１３２人目の素数さん [2009/07/30(木) 13:15:06 ]
- 述語論理のカット除去定理で、左前提(Γ⇒Δ,D)と右前提(D,Γ⇒Δ)で、カットによって消える論理式Dが、∀xφ(x)や∃xφ(x)であり、
さらに両方の前提でDが主式だった場合(ここではD＝∀xφ(x)とおきます)、両前提はL∀とR∀から出て来て、片方はφ(a)、もう片方はφ(t)
(a:固有変数,t:適当なターム)から出てきますが、これをカットで消すには、φ(a)を持ったシーケントを根とした枝全体の、固有変数aを全てtに置き換えれば良いのでしょうか？
