一階述語論理の演繹定理、∀el
2017/1/30
演繹定理の証明を修正しました
〇健全な研究室
エーリル
「演繹定理を修正するってどういうこと？」
さトぅー
「証明や定理の定義は命題論理と一緒。
一階述語論理の証明に出てくる論理式は、Ax1,...,Ax7,公理系Tの公理,⇒elの結論,∀inの結論の10パターンしかない。
このうち命題論理の演繹定理のメタな証明に出てこないのは、Ax4,Ax5,Ax6,Ax7,∀inの結論の5パターン。
Ax4,Ax5,Ax6,Ax7は命題論理のときと同じ方法でできるけど、∀inの結論だけが違う。
今からメタな証明をするけど、命題論理のときと同じ方法で証明できるときは『同様』って言葉を使うから注意してね」
エーリル
「OK」
■meta thm1.2(一階述語論理の演繹定理)
T:公理系
φ,ψ:論理式
とする。次の(1),(2)は同値。
(1) T∪{φ} |- ψ
(2) T |- (φ⇒ψ)
proof
・(1)ならば(2)の証明。
T∪{φ} |- ψの証明の長さに関する帰納法で証明する。
T∪{φ} |- ψの証明の長さが1の証明があるとする。
このときψはAx1,...,Ax7,Tの公理,φのどれかになり、命題論理のときと同様にしてT |- (φ⇒ψ)。
----------------
さトぅー
「確認だけど、命題論理のときはどんな証明だった？」
エーリル
「えーっと。Ax1と⇒elを使うか、⇒の反射性(φ⇒φ)を使ったような気がする」
さトぅー
「大丈夫そうね。証明の長さに関する帰納法はわかる？」
エーリル
「最初の敵が倒せて、どんな敵の次の敵も倒せるなら、全部の敵が倒せる」
さトぅー
「うーん……まあ、いいんじゃない？」
-----------------
T∪{φ} |- ψ'の証明の長さが自然数n以下の証明があるすべての論理式ψ'について、T |- (φ⇒ψ')とする。
T∪{φ} |- ψの証明の長さがn+1の証明があるとする。
このときψはAx1,...,Ax7,Tの公理,φ,⇒elの結論,∀inの結論のどれかになる。
ψがAx1,...,Ax7,Tの公理,φ,⇒elの結論のどれかのときは命題論理と同様。
-----------------
さトぅー
「⇒elのときどんな証明だった？」
エーリル
「Ax2で敵を薙ぎ払った」
さトぅー
「Ax2は武器じゃないんだけど」
-----------------
ψが∀inの結論のときを証明する。
このとき、ψはある論理式ρについて(∀x ρ)の形をしている。
:
:
n ρ
n+1 (∀x ρ) [∀in]
ρを結論とする仮定かつ公理の集まりをT'と定義する。
このときT'|-ρとなる。
∀inが使えるから、T'のすべての論理式ψ'について、fv(ψ')はxを含まない。
・fv(φ)にxが含まれないとき
T'|-ρとT∪{φ}|-ρの証明の長さはnだからT'＼{φ} |- (φ⇒ρ)とT|-(φ⇒ρ)になる。
T'＼{φ}のすべての論理式ψ'について、fv(ψ')はxを含まないから(φ⇒ρ)に∀inが使えて、ある自然数kについて
:
:
k (φ⇒ρ) [Tの定理]
k+1 (∀x (φ⇒ρ)) [∀in k]
k+2 ((∀x (φ⇒ρ))⇒(φ⇒(∀x ρ))) [Ax5]
k+3 (φ⇒(∀x ρ)) [⇒el k+1,k+2]
ψは(∀x ρ)の形だからT |- (φ⇒ψ)。
・fv(φ)にxが含まれるとき
T'のすべての論理式ψ'について、fv(ψ')はxを含まないから、T'にφは含まれない。
よってT'＼{φ} = T'。
T' |- ρからρに∀inが使え、T |- ρとなり、
n ρ [Tの定理]
n+1 (∀x ρ) [∀in n]
n+2 ((∀x ρ)⇒(φ⇒(∀x ρ))) [Ax1]
n+3 (φ⇒(∀x ρ)) [⇒el n+1,n+2]
ψは(∀x ρ)の形だからT |- (φ⇒ψ)。
・(2)ならば(1)の証明。
命題論理と同様。
■
さトぅー
「これで一階述語論理の演繹定理が証明できたから、命題論理で使った推論規則や定理が使えるようになったわね」
エーリル
「助かった」
さトぅー
「ちなみに、演繹定理のメタな証明を具体例でするとこんな感じになる」
■例
x,y:変数記号
R,Q:項数1の関係記号
{R(y),Q(x)} |- (∀x R(y))
proof
1 R(y) [ax]
2 (∀x R(y)) [∀in 1]
-----------------------
さトぅー
「この証明を翻訳すると」
-----------------------
{Q(x)} |- (R(y)⇒(∀x R(y)))
proof
1 (R(y)⇒R(y)) [⇒の反射性]
2 (∀x (R(y)⇒R(y))) [∀in 1]
3 ((∀x (R(y)⇒R(y)))⇒((R(y)⇒(∀x R(y))))) [Ax5]
4 (R(y)⇒(∀x R(y))) [⇒el 2,3]
■
さトぅー
「やっぱり演繹定理がないとしんどいわね」
エーリル
「演繹定理は壊れ定理」
さトぅー
「あとは∀elかしらね」
■thm1.0
φ:論理式
x:変数記号
t:項
{(∀x φ)} |- (φ[t/x])
proof
1 (∀x φ) [ax]
2 ((∀x φ)⇒(φ[t/x])) [Ax4]
3 (φ[t/x]) [⇒el 1,2]
■
さトぅー
「推論規則を追加しよう」
■∀el
φ:論理式
x:変数記号
t:項
(∀x φ)
---------[∀el]
(φ[t/x])
エーリル
「演繹定理の後で見ると易しく感じる」
さトぅー
「これで∀in,と∀elが揃ったわね。
実際の証明で使うときは、どっちも神経を使う局面になりやすい」
エーリル
「どういうこと？」
さトぅー
「∀inは公理系の自由変数をチェックしないと使えない。
だから、公理をキャンセルしたときに公理系にどの自由変数がいるのかをわからないとミスをする」
エーリル
「∀elは自由変数を気にしなくてもいいのに」
さトぅー
「数えきれない量の項の中から、証明に必要な項を一つ代入できるかしら」
エーリル
「……それは難しい」
さトぅー
「そういう局面は今までずっとあった。
それでも証明ができてるのは、少し先の展開を予測して、選択肢を絞り込んでいるから」
エーリル
「さトぅーさん、予知能力あったの？」
さトぅー
「そんなのじゃないわよ。
示したい定理を決めて、そこから推論規則を遡れば、かなり選択肢を絞り込めるってだけ。
どの定理が示したいかを決めるのは、もっと難しいと思うけどね」
エーリル
「深淵を垣間見てしまった……」
