- 266 名前：253 [05/03/17 18:12:22 ]
- あ、私も勘違いしてた。Cut除去の証明においては、自由変数と束縛変数を区別する
というよりも、もし区別しない流儀を選んだ場合、
>>253の
＞例えば（∀右）
＞ の推論規則は
＞ Γ⇒Θ、A
＞−−−−−−−
＞ Γ⇒Θ、∀xA
＞ のように∀xを付け加えるだけなのでしょうか。それとも
＞ Γ⇒Θ、A(x)
＞−−−−−−−−−
＞ Γ⇒Θ、∀yA(y)
＞ のように変数を換えてしまう（上記ではxをyに換えている）のも推論規則の
＞ なかに含めてしまうのでしょうか。
のところが良く分からないのです。
