数理論理学　第11回 茨城大学工学部情報工学科 佐々木　稔.

Presentation on theme: "数理論理学　第11回 茨城大学工学部情報工学科 佐々木　稔."— Presentation transcript:

1 数理論理学　第11回 茨城大学工学部情報工学科 佐々木　稔

2 前回までのあらすじ http://sas.cis.ibaraki.ac.jp/logic/ 述語論理の解釈 述語論理式の形成規則
述語論理式の解釈 述語論理の恒真式 量記号を含む述語論理式の性質 配布資料は以下のURLからダウンロードできます

3 前回の問題 以下の論理式について考える。 この論理式の解釈として、以下のものを設定する この論理式の真偽を判定せよ。
∀x(P(x)∨Q(f(x), a)) 　この論理式の解釈として、以下のものを設定する 定義域 D={0, 1, 2, 3, 4} a = 10 f : f(x) = x2 P(x) : 「x は偶数である」 Q(x、y) : 「x>y である」 　この論理式の真偽を判定せよ。

4 前回の問題2 x=0 のとき、 x=1 のとき、 x=2 のとき、 x=3 のとき、 x=4 のとき、
P(0)∨Q(f(0), 10) = T ∨ F = T x=1 のとき、 P(1)∨Q(f(1), 10) = F ∨ F = F x=2 のとき、 P(2)∨Q(f(2), 10) = T ∨ F = T x=3 のとき、 P(3)∨Q(f(3), 10) = F ∨ F = F x=4 のとき、 P(4)∨Q(f(4), 10) = T ∨ T = T 以上より、∀x(P(x)∨Q(f(x), a)) は偽である。

5 今週のお題 述語論理の解釈 スコーレム標準形 束縛変数の付け替え 冠頭標準形 スコーレム関数 導出と推論 導出とは

6 スコーレム標準形 述語論理による推論の難しさ 量記号の混在した論理式の推論 スコーレム標準形 量記号の存在 量記号を全称記号に統一
存在記号を除去して全称記号と連言で記述

7 束縛変数の付け替え 論理式 P 全称閉形 存在閉形 自由変数 x1, x2, ・・・, xn ∀x1∀x2・・・∀xn P

8 束縛変数の付け替え 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 の形となので全称閉形

9 冠頭標準形 変数の付け替えをした論理式 冠頭連言標準形 冠頭選言標準形 命題論理式、述語論理式の性質を使って変形
Qx1Qx2・・・Qxn P1∧P2∧・・・∧Pm Q は ∀、∃のどちらかの記号 Pk は論理式 冠頭選言標準形 Qx1Qx2・・・Qxn P1∨P2∨・・・∨Pm

10 冠頭標準形への変換方法 量記号 Qx のスコープ内に x がなければ、量記号を削除 ⇒、⇔記号を~、∨、∧記号で書き換える
~記号を基本論理式の直前に移動 量記号を左に移す スコープ、束縛変数の名前に注意 変数の数が少なくならないよう注意 ∀xP(x)∧∀xQ(x) = ∀x (P(x)∧Q(x)) 分配律などで、選言または連言に統一

11 ∀x(∀y∀z(P(x, y)⇒Q(y, z)) ⇒∃y∀zR(y, z))
冠頭標準形への変換例 ∀x(∀y∀z(P(x, y)⇒Q(y, z))　⇒∃y∀zR(y, z)) ⇒記号の除去 ∀x(~∀y∀z(~P(x, y)∨Q(y, z))∨∃y∀zR(y, z)) ~の移動 ∀x(∃y∃z(~~P(x, y)∧~Q(y, z))∨∃y∀zR(y, z)) 変数の標準化 ∀x(∃y∃z(P(x, y)∧~Q(y, z))∨∃y∀wR(y, w))

12 冠頭標準形への変換例 ∃y でくくる（量記号をまとめる） 量記号の移動 分配律を使い、連言標準形にする
∀x(∃y(∃z(P(x, y)∧~Q(y, z))∨∀wR(y, w))) 量記号の移動 ∀x∃y∃z∀w((P(x, y)∧~Q(y, z))∨R(y, w)) 分配律を使い、連言標準形にする ∀x∃y∃z∀w((P(x, y)∨R(y, w)) ∧(~Q(y, z)∨R(y, w)))

13 スコーレム関数 存在記号を取り除く 論理式は同値ではなくなる 真偽は等しい なぜ書き換えるのか 論理式の恒真性を証明するため

14 スコーレム関数 x y x の定義域 ∀x∃y(P(x)⇒Q(x,f(y))) どんな x を与えても、 y の値が存在する
任意のxで P(x)⇒Q(x,f(y)) を満たすyが存在 x y どんな x を与えても、 y の値が存在する 関数として記述可能 x の定義域

15 スコーレム関数 存在記号で束縛された変数 y ∀x1∀x2・・・∀xn∃yP(x1, x2,・・・, xn, 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)

16 スコーレム関数の例 ∃y∀zP(y, z)∧∀x∃wQ(x, w) y = a とおいて w = f(x) とおいて したがって、
∀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)))

17 スコーレム標準形 スコーレム標準形 節集合 存在記号を除去した冠頭連言標準形 節の連言から成る スコーレム標準形に含まれるすべての節の集合
∀x1∀x2・・・∀xn P1∧P2∧・・・∧Pm 節集合　{P1, P2, ・・・, Pm}

18 スコーレム標準形への変換方法 量記号のスコープ内に束縛変数がなければ、量記号を削除 ⇒、⇔記号を~、∨、∧記号で書き換える
~記号を基本論理式の直前に移動 束縛変数の付け替え スコーレム関数を導入し、存在記号を除去 全称記号を左に移す 分配律などで、連言に統一

19 スコーレム標準形への変換例 ∀x(∃y(P(x, y)⇒∀zQ(y, z))⇒∀y∃zR(y, z)) ⇒記号の除去 ~を内側に移動
変数の標準化 ∀x(∀y(P(x, y)∧∃z~Q(y, z))∨∀u∃vR(u, v))

20 スコーレム標準形への変換例 節集合を取り出す スコーレム関数 冠頭形に変換 連言冠頭形に変換
∀x(∀y(P(x,y)∧~Q(y,f(x,y)))∨∀uR(u,g(x,u))) 冠頭形に変換 ∀x∀y∀u(P(x,y)∧~Q(y,f(x,y))∨R(u,g(x,u))) 連言冠頭形に変換 ∀x∀y∀u((P(x, y)∨R(u, g(x, u))) ∧(~Q(y,f(x,y))∨R(u,g(x,u)))) 節集合を取り出す {P(x, y)∨R(u, g(x, u)), ~Q(y,f(x, y))∨R(u, g(x, u))}

21 導出とは 肯定式 もしくは、 P ⇒ Q P Q ~P ∨ Q P Q

22 導出 否定式１ もしくは、 P ⇒ Q ~Q ~P ~P ∨ Q ~Q ~P

23 導出 否定式２ P ∨ Q ~P Q

24 導出 否定式３ もしくは、 P 　 Q P ~Q （P ∨ Q）∧（~P ∨ ~Q） P ~Q

25 導出 三段論法 もしくは、 P ⇒ Q Q ⇒ R P ⇒ R ~P ∨ Q ~Q ∨ R ~P ∨ R

26 導出 三段論法 もしくは、 P ⇒ Q R ⇒ ~Q P ⇒ ~R ~P ∨ Q ~R ∨ ~Q ~P ∨ ~R

27 導出 導出節 p ∨ Q ~p ∨ R Q ∨ R 推論規則の法則 ある述語の正のリテラルを含む選言式 その述語の負のリテラルを含む選言式
以上の2つの選言式から その述語を削除した選言式を導くことができる 　p ∨ Q ~p ∨ R 　Q ∨ R 導出節

28 練習問題 次の述語論理式をスコーレム標準形に変換せよ。 ∀x∃y (P(x, y)⇒Q(x))
～(∀x∃y((P(x, y)⇒～R(y))∨∀z R(z)))