数理論理学第2回

数理論理学第11回
茨城大学工学部情報工学科
佐々木稔
前回までのあらすじ
 述語論理の解釈
 述語論理式の形成規則
 述語論理式の解釈
 述語論理の恒真式
 配布資料は以下のURLからダウンロードできます
http://sas.cis.ibaraki.ac.jp/logic/
今週のお題
 述語論理の解釈
 量記号を含む述語論理式の性質
 スコーレム標準形




束縛変数の付け替え
冠頭標準形
スコーレム関数
スコーレム標準形
量記号を含む述語論理式の性質
 命題論理の性質は述語論理でも使える
 論理式に任意の述語論理式を代入しても成立
 量記号を使った場合にできる性質が存在
 すべての第1階述語論理で成り立つ
 論理式の記述は単項述語とする
 n 項述語でも成り立つ
述語論理式の性質1
1.
2.
3.
4.
5.
6.
7.
~∀xP(x) = ∃x~P(x)
~∃xP(x) = ∀x~P(x)
∀xP(x) ⇒ ∃xP(x)
∀xP(x)∧Q(y) = ∀x (P(x)∧Q(y))
∃xP(x)∧Q(y) = ∃x (P(x)∧Q(y))
∀xP(x)∨Q(y) = ∀x (P(x)∨Q(y))
∃xP(x)∨Q(y) = ∃x (P(x)∨Q(y))
述語論理式の性質2
8. ∀xP(x)∧∀xQ(x) = ∀x (P(x)∧Q(x))
9. ∀xP(x)∨∀xQ(x) ⇒ ∀x (P(x)∨Q(x))
10.∃xP(x)∨∃xQ(x) = ∃x (P(x)∨Q(x))
11.∃x(P(x)∧Q(x)) ⇒ ∃xP(x)∧∃xQ(x)
12.P(x) が恒真 ⇔ ∀xP(x)が恒真
補足（述語論理式の性質）
 ∀xP(x)∨∀xQ(x) ⇒ ∀x (P(x)∨Q(x))
P(x)
Q(x)
∀x (P(x)∨Q(x)) が真ならば、∀xP(x)は?
補足の続き（述語論理式の性質）
 ∀xP(x)∨∀xQ(x) ⇒ ∀x (P(x)∨Q(x))
P(x)
Q(x)
重なった部分があるので等しくない
補足（述語論理式の性質）
 ∃x(P(x)∧Q(x)) ⇒ ∃xP(x)∧∃xQ(x)
P(x)
Q(x)
スコープの違いで真偽値も異なる
スコーレム標準形
 述語論理による推論の難しさ
 量記号の存在
 量記号の混在した論理式の推論
 量記号を全称記号に統一
 スコーレム標準形
 存在記号を除去して全称記号と連言で記述
束縛変数の付け替え
 論理式 P
 自由変数 x1, x2, ・・・, xn
 全称閉形
 ∀x1∀x2・・・∀xn P
 存在閉形
 ∃x1∃x2・・・∃xn P
束縛変数の付け替え
 P(x)⇒∃xQ(x) を全称閉形に変形する





x を全称記号で束縛する
∀x(P(x)⇒∃xQ(x))
P(x) の x と ∃xQ(x) の x が区別できない
∃xQ(x) の x を y に付け替える
∀x(P(x)⇒∃yQ(y))
 ∀xP の形となので全称閉形
冠頭標準形
 変数の付け替えをした論理式
 命題論理式、述語論理式の性質を使って変形
 冠頭連言標準形
 Qx1Qx2・・・Qxn P1∧P2∧・・・∧Pm
 Q は ∀、∃のどちらかの記号
 Pk は論理式
 冠頭選言標準形
 Qx1Qx2・・・Qxn P1∨P2∨・・・∨Pm
冠頭標準形への変換方法
1. 量記号 Qx のスコープ内に x がなければ、
量記号を削除
2. ⇒、⇔記号を~、∨、∧記号で書き換える
3. ~記号を基本論理式の直前に移動
4. 量記号を左に移す
 スコープ、束縛変数の名前に注意
 変数の数が少なくならないよう注意
 ∀xP(x)∧∀xQ(x) = ∀x (P(x)∧Q(x))
5. 分配律などで、選言または連言に統一
冠頭標準形への変換例
 ∀x(∀y∀z(P(x, y)⇒Q(y, z))
⇒∃y∀zR(y, z))
1. ⇒記号の除去

∀x(~∀y∀z(~P(x, y)∨Q(y, z))∨∃y∀zR(y, z))
2. ~の移動

∀x(∃y∃z(~~P(x, y)∧~Q(y, z))∨∃y∀zR(y, z))
3. 変数の標準化

∀x(∃y∃z(P(x, y)∧~Q(y, z))∨∃y∀wR(y, w))
冠頭標準形への変換例
4. ∃y でくくる（量記号をまとめる）

∀x(∃y(∃z(P(x, y)∧~Q(y, z))∨∀wR(y, w)))
5. 量記号の移動

∀x∃y∃z∀w((P(x, y)∧~Q(y, z))∨R(y, w))
6. 分配律を使い、連言標準形にする
 ∀x∃y∃z∀w((P(x, y)∨R(y, w))
∧(~Q(y, z)∨R(y, w)))
スコーレム関数
 存在記号を取り除く
 論理式は同値ではなくなる
 真偽は等しい
 なぜ書き換えるのか
 論理式の恒真性を証明するため
スコーレム関数
 ∀x∃y(P(x)⇒Q(x,f(y)))
 任意のxで P(x)⇒Q(x,f(y)) を満たすyが存在
x
x の定義域
y
どんな x を与えても、
y の値が存在する
関数として記述可能
y  g x 
スコーレム関数
 存在記号で束縛された変数 y
 それより左の全称記号で束縛された変数の関数
 ∀x1∀x2・・・∀xn∃yP(x1, x2,・・・, xn, y)
 y = f(x1, x2,・・・, xn) と置いて
∀x1∀x2・・・∀xnP(x1, x2,・・・, xn, f(x1, x2,・・・, xn))
 存在記号の左に全称記号がなければ定数
 ∃wP(w)
 P(a)
スコーレム関数の例
 ∃y∀zP(y, z)∧∀x∃wQ(x, w)
 y = a とおいて
 ∀zP(a, z)
 w = f(x) とおいて
 ∀xQ(x, f(x))
 したがって、
 ∀zP(a, z)∧∀xQ(x, f(x))
 ∀x∀z(P(a, z)∧Q(x, f(x)))
スコーレム標準形
 スコーレム標準形
 存在記号を除去した冠頭連言標準形
 節の連言から成る
 節集合
 スコーレム標準形に含まれるすべての節の集合
 ∀x1∀x2・・・∀xn P1∧P2∧・・・∧Pm
 節集合 {P1, P2, ・・・, Pm}
スコーレム標準形への変換方法
1. 量記号のスコープ内に束縛変数がなければ、
量記号を削除
2. ⇒、⇔記号を~、∨、∧記号で書き換える
3. ~記号を基本論理式の直前に移動
4. 束縛変数の付け替え
5. スコーレム関数を導入し、存在記号を除去
6. 全称記号を左に移す
7. 分配律などで、連言に統一
スコーレム標準形への変換例
 ∀x(∃y(P(x, y)⇒∀zQ(y, z))⇒∀y∃zR(y, z))
1. ⇒記号の除去

∀x(~∃y(~P(x, y)∨∀zQ(y, z))∨∀y∃zR(y, z))
2. ~を内側に移動

∀x(∀y(~~P(x, y)∧~∀zQ(y, z))∨∀y∃zR(y, z))
3. ~を内側に移動

∀x(∀y(P(x, y)∧∃z~Q(y, z))∨∀y∃zR(y, z))
4. 変数の標準化

∀x(∀y(P(x, y)∧∃z~Q(y, z))∨∀u∃vR(u, v))
スコーレム標準形への変換例
5. スコーレム関数

∀x(∀y(P(x,y)∧~Q(y,f(x,y)))∨∀uR(u,g(x,u)))
6. 冠頭形に変換

∀x∀y∀u(P(x,y)∧~Q(y,f(x,y))∨R(u,g(x,u)))
7. 連言冠頭形に変換

∀x∀y∀u((P(x, y)∨R(u, g(x, u)))
∧(~Q(y,f(x,y))∨R(u,g(x,u))))
8. 節集合を取り出す

{P(x, y)∨R(u, g(x, u)),
~Q(y,f(x, y))∨R(u, g(x, u))}
導出とは
 肯定式
P⇒Q
P
Q
 もしくは、
~P ∨ Q
P
Q
導出
 否定式１
P⇒Q
~Q
~P
 もしくは、
~P ∨ Q
~Q
~P
導出
 否定式２
P∨Q
~P
Q
導出
 否定式３
P
Q
P
~Q
 もしくは、
（P ∨ Q）∧（~P ∨ ~Q）
P
~Q
導出
 三段論法
P⇒Q
Q⇒R
P⇒R
 もしくは、
~P ∨ Q
~Q ∨ R
~P ∨ R
導出
 三段論法
P⇒Q
R ⇒ ~Q
P ⇒ ~R
 もしくは、
~P ∨ Q
~R ∨ ~Q
~P ∨ ~R
導出
 推論規則の法則
 ある述語の正のリテラルを含む選言式
 その述語の負のリテラルを含む選言式
 以上の2つの選言式から
 その述語を削除した選言式を導くことができる
p∨Q
~p ∨ R
Q∨R
導出節
反駁導出
 論理式 P
 P = P1∧P2∧・・・∧Pm
 論理式 P から、ある論理式 Q が導ける
 P1∧P2∧・・・∧Pm ⇒ Q
 背理法より、下の論理式が恒偽なのと同値
 P1∧P2∧・・・∧Pm∧~Q
 次の節形式が矛盾することでQの証明が可能
 {P1, P2, ・・・, Pm , ~Q}
反駁導出による証明方法
 節形式から以下の２つの節を取り出す
 { ･･･, p ∨ Q, ~p ∨ R, ･･･}
 導出した新しい節を節形式に加える
 { ･･･, Q ∨ R, ･･･}
 2つの節が同一述語で正負のリテラルの場合、
 { ･･･, p, ~p, ･･･}
 導出により、何も残らない（空節）
 { ･･･, □, ･･･}
反駁導出による証明方法
 反駁木
 導出過程を木構造で表現
 節集合 {A(a), ~A(y)∨B(a), ~B(x)∨C(x)}
 ∃xC(x) を証明
 便宜上、x, y はすべて a と置き換える
 以下の節集合を反駁導出により証明
 {A(a), ~A(a)∨B(a), ~B(a)∨C(a), ~C(a)}
反駁導出による証明方法
A(a)
~A(a)∨B(a)
B(a)
~B(a)∨C(a)
C(a)
~C(a)
□
矛盾するため、 ∃xC(x) は成り立つ（証明終わり）

Download Report