解説資料集 2

数理論理学解説資料集 2
述語論理の構文
自然演繹の推論規則
述語論理の意味
論理式の標準形への変換
導出原理
山田俊行
http://www.cs.info.mie-u.ac.jp/~toshi/lectures/mathlogic/
2014 年 11 月
1
数理論理学解説資料 (山田)
述語論理の構文
●項
対象変数
不特定の対象を表す
x, y, z, a, b などで表す
対象定数
特定の対象を表す
c, d などで表す
関数記号
対象を対象に写す関数を表す
f , g などで表す
項
対象を表す記号表現
s, t などで表す
項の帰納的定義
• 対象変数や対象定数は項
• f が m 変数の関数記号で t1 , · · · , tm が項ならば，f (t1 , · · · , tm ) は項
※ 2 変数関数の中置 (t1 f t2 ) を許すこともある
●論理式
述語記号
対象の間の関係を表す
P , Q, R などで表す
論理式
複合命題や複合述語を表す記号表現
A, B, C などで表す
論理式の帰納的定義
• P が n 変数の述語記号で t1 , · · · , tn が項ならば，P (t1 , · · · , tn ) は論理式（原子論理式）
※ 2 変数述語の中置 (t1 P t2 ) を許すこともある
• A, B が共に論理式ならば，(¬A), (A ∧ B), (A ∨ B), (A ⊃ B), (A ≡ B) は全て論理式
※ ⊥ や ⊤ を論理式として使うこともある
• A が論理式で x が対象変数ならば，(∀xA), (∃xA) は共に論理式
記法の注意
混乱を生じない限り，括弧は省ける
¬, ∀, ∃
結合力：強
∧, ∨
⊃
≡
結合力：弱
同じ記号が並ぶ場合，左に結合すると約束して括弧を省く
2
●変数への項の代入
変数の出現
現れる場所によって区別された変数
自由出現と束縛出現の帰納的定義
• 原子論理式の中の変数の出現は全て自由
• 論理式 ¬A, A ∧ B, A ∨ B, A ⊃ B, A ≡ B 中の変数の出現が自由か束縛されているか
は，A か B の中での出現の状態（自由/束縛）と同じ
• ∀xA, ∃xA の A 中の変数 x の出現は全て束縛され，それ以外の変数の出現が自由か束
縛されているかは，A 中での出現の状態と同じ
変数への項の代入
変数の項への置き換え
A[t/x] … 論理式 A 中の変数 x の自由な出現を全て項 t で置き換えたもの
ただし，変数を新たに束縛しないよう，束縛変数の出現を組織的に付け替える
3
数理論理学解説資料 (山田)
自然演繹の推論規則
自然演繹の形式体系 NJ, NK の推論規則一覧を示す．
以下の規則中で，A, B, C は論理式，i, j は除去する仮定の印，x, a は対象変数，t は項を表す．
規則名の I と E は，下段への記号の導入 (introduction) と上段の記号の除去 (elimination) を表す．
●基本規則
含意 ⊃
論理積 ∧
i
hAi
..
.
B
⊃I, i
A⊃B
A
(注 ※ 1)
A B
∧I
A∧B
A∧B
∧E1
A
A
∨I1
A∨B
i
hAi
..
.
A∨B C
C
論理和 ∨
B
∨I2
A∨B
矛盾 ⊥
全称 ∀
A[a/x]
∀I
∀x A
i A[a/x]
..
.
B ∃E, i
∃x A
B
i
h¬Ai
..
.
⊥ RAA, i
A
背理法
(注 ※ 1)
(注 ※ 1, ※ 3)
(注 ※ 1)
.
0 回以上の規則適用で前提を導出 ( .. で表示) し，仮定 ( h i で表示) を 0 個以上除去
変数条件：次の場所に a を自由変数として使わない
• 結論 ∀x A で有効な (除去されていない) 各仮定
• 結論 ∀x A
(※ 3)
j
hBi
..
.
C ∨E, i, j
∀x A
∀E
A[t/x]
(注 ※ 2)
A[t/x]
∃I
∃x A
(※ 2)
A∧B
∧E2
B
⊥
⊥
A
存在 ∃
(※ 1)
A⊃B
⊃E
B
変数条件：次の場所に a を自由変数として使わない
• 結論 B で有効な (除去されていない) 各仮定
• 前提 ∃x A と結論 B
4
●規則の分類
直観主義論理
(NJ)
古典論理
(NK)
命題論理
⊃I
⊃E
∧I
∧E1 ∧E2
∨I1 ∨I2 ∨E
⊥
上の規則と
RAA
述語論理
左の規則と
∀I ∀E
∃I ∃E
全規則
●派生規則
否定 ¬
同値 ≡
i
hAi
..
.
⊥
¬I, i
¬A
A
j
i
hAi hBi
..
..
.
.
A
B
≡I, i, j
A≡B
¬A
¬E
⊥
A≡B
≡E1
A⊃B
A≡B
≡E2
B⊃A
排中律
A ∨ ¬A
EM
●派生規則の正式な導出
否定 ¬
同値 ≡
排中律
(¬A を A ⊃⊥ の略記と考える)
i
hAi
..
.
⊥
⊃I, i
A ⊃⊥
A
A ⊃⊥
⊃E
⊥
(A ≡ B を (A ⊃ B) ∧ (B ⊃ A) の略記と考える)
j
i
hBi
hAi
..
..
.
.
A
B
⊃I, i
⊃I, j
(A ⊃ B) ∧ (B ⊃ A)
A⊃B
B⊃A
∧I
∧E1
(A ⊃ B) ∧ (B ⊃ A)
A⊃B
2
A
1
∨I1
A ∨ (A ⊃⊥)
A ∨ (A ⊃⊥) ⊃⊥
⊃E
⊥
⊃I, 2
A ⊃⊥
1
∨I2
A ∨ (A ⊃⊥)
A ∨ (A ⊃⊥) ⊃⊥
⊃E
⊥
RAA, 1
A ∨ (A ⊃⊥)
5
(A ⊃ B) ∧ (B ⊃ A)
∧E2
B⊃A
数理論理学解説資料 (山田)
述語論理の意味
述語論理の意味論で使う基本的な定義を以下にまとめる．論理式の意味解釈の具体例を考えるとよい．
●言語に対する構造
言語
言語は形式体系の記述に使う記号の集合
述語論理の場合：論理結合子，量化記号，対象変数，対象定数，関数記号，述語記号，等
構造
構造は記号列に意味を与える
言語 L に対する構造 A = hU, Ii は，対象領域と解釈とで定める
U
…
対象領域
対象の集まりを定める非空集合
I
…
解釈
L の記号とその意味との対応
記号
対象定数
c
n 変数関数記号
n 変数述語記号
f
P
7→
7→
7
→
7→
意味
cI
I
f
PI
U の要素
cI ∈ U
U 上の n 変数関数
U 上の n 変数述語
fI : Un → U
PI ⊆ Un
言語の拡張
対象領域 U の各要素 u ごとに名前 u を対象定数として言語に追加
L[A] := L ∪ { u | u ∈ U }
解釈の固定
対象の名前と等号の解釈は常に固定
名前 u は常に U の要素 u と解釈
uI := u
=I
:=
{ (u, u) | u ∈ U }
等号 = は常に「U の同一の要素である」と解釈
●項と論理式の意味付け
項の意味
項は対象領域の要素として意味付け
cA
:= cI
A
f (t1 , · · · , tn )
:= f I (t1 A , …, tn A )
閉論理式の意味
自由変数のない論理式は真理値として意味付け
(
0
(t1 A , · · · , tn A ) 6∈ P I のとき
A
P (t1 , · · · , tn )
:=
1
(t1 A , · · · , tn A ) ∈ P I のとき
(¬A)A
:=
1 − AA
(A ∧ B)A
(A ∨ B)A
:=
:=
min{ AA , B A }
max{ AA , B A }
(A ⊃ B)A
(∀xA)A
:=
:=
max{ 1 − AA , B A }
min{ A[u/x]A | u ∈ U }
(∃xA)A
:=
max{ A[u/x]A | u ∈ U }
6
論理式の意味
自由変数のある論理式は全称化して意味付け
AA := (∀x1 ∀x2 · · · ∀xm A)A
A の自由変数が x1 , x2 , · · · , xm のとき
●恒真性と充足可能性
構造に対する式の正しさ
論理式の正しさは，構造が決める真理値で判断
論理式 A が構造 A に対して正しい (A |= A)
:⇐⇒ AA = 1
論理式 A が構造 A に対して正しくない (A 6|= A) :⇐⇒ AA = 0
恒真式
恒真式は，どんな対象についてどんな解釈をしても正しい式
論理式 A が恒真 ( |= A) :⇐⇒ 任意の構造に対して A が正しい
充足可能式
充足可能式は，対象や解釈をうまく選ぶと正しくなる式
論理式 A が充足可能
:⇐⇒ ある構造 A = hU, Ii のある要素 u1 , · · · , um ∈ U に対して，
論理式 A[u1 /x1 ] · · · [um /xm ] が正しい
(A の自由変数が x1 , · · · , xm のとき)
論理式 A が充足不可能 :⇐⇒ A が充足可能でない
7
数理論理学解説資料 (山田)
論理式の標準形への変換
導出原理を使って論理式の恒真性を判定するには，論理式をあらかじめ標準形に変換する必要がある．
各種の標準形を得るための変換規則を示す．
●論理和標準形への変換
論理和標準形
論理積の論理和の形
(A1,1 ∧ · · · ∧ A1,m1 ) ∨ · · · ∨ (An,1 ∧ · · · ∧ An,mn )
(ただし，n, m1 , . . . , mn ≥ 1 であり，各 Ai,j は原始論理式かその否定)
論理式 A の論理和標準形 … A と論理同値な論理和標準形
式変形による変換
次の同値変形の規則を繰り返し使う
⊃ の ¬, ∨ での表現
A ⊃ B → ¬A ∨ B
ド・モルガン
¬ (A ∧ B) → ¬A ∨ ¬B
¬ (A ∨ B) → ¬A ∧ ¬B
〃
二重否定の除去
∧ の ∨ への分配
¬¬A → A
A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C)
〃
(A ∨ B) ∧ C → (A ∧ C) ∨ (B ∧ C)
※論理式の論理和標準形は複数存在することもある
真理値表を使う変換 (命題論理の場合)
真理値表で真となる割り当てに着目して，論理積の論理和の形を作ることも可能
●冠頭標準形への変換
冠頭標準形
量化が先頭に並ぶ形
Φ1 x1 · · · Φk xk A
(ただし，k ≥ 0 であり，各 Φi は量化記号 ∀ か ∃ で，A は量化記号を含まない)
論理式 A の冠頭標準形 … A と論理同値な冠頭標準形
式変形による変換
次の同値変形の規則を繰り返し使う (ただし，y は A に現れない変数，⋆ は ∧ か ∨ )
A ⊃ B → ¬A ∨ B
∀x A → ∀y A[y/x]
∃x A → ∃y A[y/x]
¬ ∀x A → ∃x ¬A
∀x A ∧ ∀x B → ∀x (A ∧ B)
¬ ∃x A → ∀x ¬A
∃x A ∨ ∃x B → ∃x (A ∨ B)
A ⋆ ∀y B → ∀y (A ⋆ B)
∀y B ⋆ A → ∀y (B ⋆ A)
A ⋆ ∃y B → ∃y (A ⋆ B)
∃y B ⋆ A → ∃y (B ⋆ A)
※論理式の冠頭標準形は複数存在することもある
8
⊃ の ¬, ∨ での表現
変数の改名
ド・モルガン
∀, ∃ のくくり出し
〃
〃
●スコーレム標準形への変換
スコーレム標準形
存在記号による量化が先頭に並び，論理和標準形が続く形
∃x1 · · · ∃xk A
(ただし，k ≥ 0，A は量化記号を含まない論理和標準形)
論理式 A のスコーレム標準形 … A と恒真性が一致するスコーレム標準形
式変形による変換
論理和標準形を内部に含む冠頭標準形を求めてから，
次の変形規則を繰り返し使う (ただし，c は新しい対象定数，f は新しい関数記号)
対象定数の導入
∀y A → A[c/y]
∃x1 · · · ∃xk ∀y A → ∃x1 · · · ∃xk A[f (x1 , · · · , xk )/y]
関数記号の導入
※冠頭標準形を求めるとき ∀ をなるべく左に寄せると，スコーレム標準形が簡単
※変形前後で恒真性が不変 (同値変形ではない)
※論理式のスコーレム標準形は複数存在することもある
変換例
∀x ∃y R(x, y) ∧ ∀x ∀y (R(x, y) ⊃ R(y, x)) ⊃ ∀y ∃x R(x, f (y))
→ ¬ ∀x ∃y R(x, y) ∧ ∀x ∀y (¬R(x, y) ∨ R(y, x)) ∨ ∀y ∃x R(x, f (y))
⊃ を ¬, ∨ に
→ ∃x ∀y ¬R(x, y) ∨ ∃x ∃y (R(x, y) ∧ ¬R(y, x)) ∨ ∀y ∃x R(x, f (y))
¬ を最内へ
→ ∃w ∀w′ ¬R(w, w′ ) ∨ ∃x ∃y (R(x, y) ∧ ¬R(y, x)) ∨ ∀z ′ ∃z R(z, f (z ′))
→ ∀z ′ ∃w ∀w′ ∃x ∃y ∃z ¬R(w, w′ ) ∨ (R(x, y) ∧ ¬R(y, x)) ∨ R(z, f (z ′))
→ ∃w ∃x ∃y ∃z ¬R(w, g(w)) ∨ (R(x, y) ∧ ¬R(y, x)) ∨ R(z, f (c))
変数を改名
9
∀, ∃ を先頭へ
c と g を導入
数理論理学解説資料 (山田)
導出原理
●命題論理の導出原理
基本用語
リテラル
…
原子論理式 P かその否定 ¬P
節
…
リテラルの有限集合 {A1 , · · · , Ak }
空節
…
リテラルの空集合 ( で表す)
導出原理
…
2 つの節 C ∪ {P } と D ∪ {¬P } から節 C ∪ D を得る操作
C ∪ {P }
D ∪ {¬P }
P
PP
PP
C∪D
導出図
…
導出原理を反復適用し，節集合から 1 つの節を導く図
導出原理の健全性と完全性
論理和標準形の論理式 (A1,1 ∧ · · · ∧ A1,m1 ) ∨ · · · ∨ (An,1 ∧ · · · ∧ An,mn ) (ただし，n ≥ 1，
m1 , · · · mn ≥ 0，各 Ai,j はリテラル) が恒真であるための必要十分条件は，節集合
{A1,1 , · · · , A1,m1 }, · · · , {An,1 , · · · , An,mn } から空節が導出できることである．
導出の例
4 つの節からなる集合 {P, Q, ¬R}, {¬P, Q}, {P, R}, {¬Q} から空節を導出
{P, Q, ¬R}
{P, R}
P
PP
PP
{P, Q}
{¬P, Q}
P
PP
PP
{Q}
{¬Q}
P
PP
PP
論理式 (P ∧ Q ∧ ¬R) ∨ (¬P ∧ Q) ∨ (P ∧ R) ∨ ¬Q は恒真
●述語論理の導出原理
基本用語
代入
…
節 {A1 , · · · , Ak } から節 {A1 [t/x], · · · , Ak [t/x]} を得る操作
{A1 , · · · , Ak }
[t/x]
{A1 [t/x], · · · , Ak [t/x]}
導出図
…
導出原理と代入を反復適用し，節集合から 1 つの節を導く図
10
導出原理の健全性と完全性
A を論理和標準形の論理式 (A1,1 ∧ · · · ∧ A1,m1 ) ∨ · · · ∨ (An,1 ∧ · · · ∧ An,mn ) (ただし，
n ≥ 1，m1 , · · · mn ≥ 0，各 Ai,j はリテラル) とし，x1, · · · , xk を A 中に現れる全ての変
数とする．スコーレム標準形 ∃x1 · · · ∃xk A が恒真であるための必要十分条件は，節集合
{A1,1 , · · · , A1,m1 }, · · · , {An,1 , · · · , An,mn } から空節が導けることである．
導出の例
節集合 {P (x), ¬R(c, x)}, {R(y, f (z))}, {¬P (f (g(c)))} から空節を導出
{P (x), ¬R(c, x)}
{R(y, f (z))}
[f (z)/x]
[c/y]
{P (f (z)), ¬R(c, f (z))} {R(c, f (z))}
P
PP
PP
{P (f (z))}
[g(c)/z]
{P (f (g(c)))}
{¬P (f (g(c)))}
P
PP
PP
論理式 P (x) ∧ ¬R(c, x) ∨ R(y, f (z)) ∨ ¬P (f (g(c))) は恒真
11

Download Report