- 461 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 14:15:57 ]
- レベルの高いお話の途中すいません。最近次のような述語論理に出会いました。
公理系
F,G,Hは任意の論理式。xは任意の変数。tは任意の項として、
公理
(1) F→(G→F)
(2) (F→(G→H))→((F→G)→(F→H))
(3) ((¬F)→(¬G))→(G→F)
(4) (∀x(F→G))→((∀xF)→(∀xG))
(5) F→∀xF ただし、変数xはFの中に現れない
(6) ¬∀x¬(x=t) ただし、変数xはtの中に現れない
(7) x=t→(P[x]→P[t/x]) P[x]は原子論理式
（P[t/x]は、P[x]にあるどれか1つのxに項tを代入したもの）
推論規則
(8) FとF→GからGを導く
(9) Fから∀xFを導く
以上です。これは「変数の自由出現に項を代入する」という表記法がないので
技術的に有利なのだそうです。しかし、以上の公理と推論規則から
(10) ∀x(x=x)
や
(11) Fの中に自由なxがないとき、(∀x(F→G))→(F→∀xG)
を導くにはどうすればいいのでしょう？ぐぐってもそれらしいのが
見つからず、また、自分の頭ではわからず困っています。
どなたか教えていただけないでしょうか。あるいはweb上で証明してある
ところがあるなら教えていただけないでしょうか。
|
 |
