- 253 名前：１３２人目の素数さん [05/03/16 11:21:22 ]
- あのーみなさんは自由変数と束縛変数で文字の使い分けしてますか？
例えば自由変数にはa,b,cなどのアルファベットの最初の方を使い、
束縛変数にはx,y,zなどのアルファベットの後ろの方を使う、というような。
私はどうせ本質は変わらないのだからいちいち区別すんのやめよーー、
と思っていました。
最近GentzenのCut除去定理の証明をなぜかもう一度フォローしたくなって
読んでるんですが、この証明見ると自由変数と束縛変数を区別しなかったら
ちょっとやりにくいなあ、としきりに思えてくるわけです。そこでいろいろ
疑問がわいてきたのですが、私はもう社会人？？年生。いまさら近くにこんな
話題にのってくれる人もなし、文献もなし。どなたかご教示ください。
・そもそもGentzenのLKの形式って自由変数と束縛変数の区別をするのが普通な
のでしょうか？
・もし、GentzenのLKで自由変数と束縛変数を区別しない場合、例えば（∀右）
の推論規則は
Γ⇒Θ、A
−−−−−−−
Γ⇒Θ、∀xA
のように∀xを付け加えるだけなのでしょうか。それとも
Γ⇒Θ、A(x)
−−−−−−−−−
Γ⇒Θ、∀yA(y)
のように変数を換えてしまう（上記ではxをyに換えている）のも推論規則の
なかに含めてしまうのでしょうか。
＊そもそも自由変数と束縛変数を区別しないGentzenの流儀なんてなかったりして。
＊こんな細かいことってどこ探しても説明なんてないんだよなあ。
＊ほんと、誰かたすけてちょ。
|
 |
