- 265 名前：253 [05/03/17 18:02:42 ]
- >>264
レスありがとうございます。
＞区別無しの
＞システムを作って、区別ありのシステムとの間で証明図の相互書き換えが
＞可能であること示せば？
とのことですが、証明図の終式（証明図最後のSequent）で、同じ変数が
自由変数としても束縛変数としても使用されている場合を考えると、あまり
うまくいかない気がします。やはり「終式（証明図の最後のSequent）を変えず」
にCut除去するのではなくて、「束縛変数の違いを無視して、終式を変えずに」
Cut除去すると言う風になるような気がしてきました。
