カリー・ハワード対応 (9)

遅れて集まったこともあり、ほとんど進んでいない。∀-introのvariable conditionについてちょっと議論。自然演繹で考えるときにも、sub-proofに現れるeigenvariableの条件にはいろいろなものがあって、このタームの振り方がいったいどういうものを考えているのだろうかと。自分はその証明図中にまったく現れていない新たなvariableを取れ、という条件を覚えていて、いろいろとメタでいじるときにはこれがすっきりするのだが、必ずしもここまで強い条件はいらないわけで。