一階述語論理のメモ2
〇エルフの村-エーリルの家
エーリル
「じゃあ、⊥からやっつける」
ディアナ
「やっつける？」
エーリル
「そう、やっつける」
■一階述語論理での⊥の定義
c:定数記号
⊥:⇔(￢(c = c))
エーリル
「OK、定義した」
ディアナ
「次は矛盾ですかね」
エーリル
「任せて」
■meta thm1.4
T:公理系
φ,ψ:論理式
とする。次の(1),(2),(3)は同値。
(1) すべての論理式ψでT |- ψ
(2) T |- φ かつ T |- (￢φ)
(3) T |- ⊥
proof
・(1)ならば(2),(2)ならば(1)の証明
命題論理と同様
・(1)ならば(3)の証明
すべての論理式ψでT |- ψだから、ψに⊥を代入すればT |- ⊥。
・(3)ならば(1)の証明
c:定数記号
とする。
1 ⊥ [Tの定理]
2 (￢(c = c)) [def⊥ el 1]
3 (∀x (x = x)) [Ax6]
4 (c = c) [∀el 3]
5 ψ [explosion 4,2]
よって、すべての論理式ψでT |- ψ。
■
エーリル
「一階述語論理がわかったら凄い理解ができた。
メタな論理でも同じようなことしてるのわかりすぎる。
しかも爆発して素晴らしい」
ディアナ
「explosionは⊥なしで定義できるのですか？」
エーリル
「できる」
ディアナ
「では問題ないと思います」
エーリル
「よし次！」
■meta thm1.6(代入の性質)
φ,ψ:論理式
x:変数記号
t:項
とする。
(11) ((φ∧ψ)[t/x]) = ((φ[t/x])∧(ψ[t/x]))
(12) ((φ∨ψ)[t/x]) = ((φ[t/x])∨(ψ[t/x]))
(13) ((φ⇔ψ)[t/x]) = ((φ[t/x])⇔(ψ[t/x]))
(14) (⊥[t/x]) = ⊥
(15) 変数記号yがx = yでない かつ tv(t)に含まれない ならば
((∃y φ)[t/x]) = (∃y (φ[t/x]))
(16) 変数記号yがx = yならば
((∃y φ)[t/x]) = (∃y φ)
(17) 変数記号yがx = yでない かつ tv(t)に含まれ、変数記号wがx = wでない かつ tv(t)に含まれない ならば
((∃y φ)[t/x]) = ((∃w (φ[w/y]))[t/x])
ただし、wは使用する変数の列の中で、x = yでない かつ tv(t)に含まれない最初の変数記号とする。
もし使用する変数の列の中で、x = yでない かつ tv(t)に含まれない変数記号がない場合は、新しい変数記号wを追加する。
proof
・(11)の証明
((φ∧ψ)[t/x])
= ((￢(φ⇒(￢ψ)))[t/x]) [∧の定義]
= (￢((φ⇒(￢ψ))[t/x])) [代入の定義(7)]
= (￢((φ[t/x])⇒((￢ψ)[t/x]))) [代入の定義(6)]
= (￢((φ[t/x])⇒(￢(ψ[t/x])))) [代入の定義(7)]
= ((φ[t/x])∧(ψ[t/x])) [∧の定義]
・(12)の証明
((φ∨ψ)[t/x])
= (((￢φ)⇒ψ)[t/x]) [∨の定義]
= (((￢φ)[t/x])⇒(ψ[t/x])) [代入の定義(6)]
= ((￢(φ[t/x]))⇒(ψ[t/x])) [代入の定義(7)]
= ((φ[t/x])∨(ψ[t/x])) [∨の定義]
・(13)の証明
((φ⇔ψ)[t/x])
= (((φ⇒ψ)∧(ψ⇒φ))[t/x]) [⇔の定義]
= (((φ⇒ψ)[t/x])∧((ψ⇒φ)[t/x])) [代入の性質(11)]
= (((φ[t/x])⇒(ψ[t/x]))∧((ψ[t/x])⇒(φ[t/x]))) [代入の定義(6)]
= ((φ[t/x])⇔(ψ[t/x])) [⇔の定義]
・(14)の証明
(⊥[t/x])
= ((￢(c = c))[t/x]) [⊥の定義]
= (￢((c = c)[t/x])) [代入の定義(7)]
= (￢((c[t/x]) = (c[t/x]))) [代入の定義(5)]
= (￢(c = c)) [代入の定義]
= ⊥ [⊥の定義]
・(15),(16),(17)
前回証明した。
■
エーリル
「代入をやっつけた」
ディアナ
「番号の(11)とかはどういう意図ですか？」
エーリル
「代入の定義の続き」
ディアナ
「なるほど」
■meta thm1.7(自由変数の性質)
φ,ψ:論理式
x:変数記号
とする。
(5) fv((φ∧ψ)) = fv(φ)∪fv(ψ)
(6) fv((φ∨ψ)) = fv(φ)∪fv(ψ)
(7) fv((φ⇔ψ)) = fv(φ)∪fv(ψ)
(8) fv(⊥) ={}
(9) fv((∃x φ)) = fv(φ)＼{x}
proof
・(5)の証明
fv((φ∧ψ))
= fv((￢(φ⇒(￢ψ)))) [∧の定義]
= fv((φ⇒(￢ψ))) [fvの定義(3)]
= fv(φ)∪fv((￢ψ))) [fvの定義(2)]
= fv(φ)∪fv(ψ) [fvの定義(3)]
・(6)の証明
fv((φ∨ψ))
= fv(((￢φ)⇒ψ)) [∨の定義]
= fv((￢φ))∪fv(ψ) [fvの定義(2)]
= fv(φ)∪fv(ψ) [fvの定義(3)]
・(7)の証明
fv((φ⇔ψ))
= fv(((φ⇒ψ)∧(ψ⇒φ))) [⇔の定義]
= fv((φ⇒ψ))∪fv((ψ⇒φ)) [fv∧]
= (fv(φ)∪fv(ψ))∪(fv(ψ)∪fv(φ)) [fvの定義(2),(2)]
-------------------
エーリル
「んー、fv(φ)∪fv(ψ)までいけると思ったんだけど詰まった」
ディアナ
「……(fv(φ)∪fv(ψ))と(fv(ψ)∪fv(φ))って違うんですか？」
エーリル
「あ、一緒か。どんな集まりを合わせる順番は関係ないはず。
しかも、同じ集まりを合わせても変わらないからこうか」
-------------------
= (fv(φ)∪fv(ψ))∪(fv(φ)∪fv(ψ)) [∪の順番を変えた]
= fv(φ)∪fv(ψ) [∪で同じ集まりを合わせた]
・(8)の証明
c:変数記号
とする。
fv(⊥)
= fv((￢(c = c))) [⊥の定義]
= fv((c = c)) [fvの定義(3)]
= tv(c)∪tv(c) [fvの定義(3)]
= tv(c) [∪の計算]
= {} [tvの定義(1)]
・(9)の証明
前回証明した。
■
エーリル
「よし、完璧」
ディアナ
「エーリルも証明ができるようになったんですね」
エーリル
「さトぅーさんから伝授してもらったから完璧」
ディアナ
「天々城さんからも教えてもらったのではないですか？」
エーリル
「今回はどこかに出かけて戻ってこなかった」
ディアナ
「……なにかあったんですかね」
■ここまでの参考文献と読書案内
[1]菊池誠, 不完全性定理, 共立出版, 2014.
作者が主に参考にしている本です。
Hibert流の命題論理から議論をしています。
タイトルは不完全性定理ですが、論理学の入門書としてもオススメです。
[2]鹿島亮, 数理論理学, 朝倉書店, 2010.
こちらは自然演繹で議論を進めています。
数学の証明をキチンと書けるようになりたいならオススメです。
[3]前原昭二,記号論理入門[新装版],日本評論社,2014
命題論理や一階述語論理について参考にさせていただきました。
