述語論理と∀（全称）∃（存在） ３回の講義の概観： 命題論理 （真理値） （公理と推論規則） 述語論理 （モデルと解釈）

Presentation on theme: "述語論理と∀（全称）∃（存在） ３回の講義の概観： 命題論理 （真理値） （公理と推論規則） 述語論理 （モデルと解釈）"— Presentation transcript:

1 述語論理と∀（全称）∃（存在） ３回の講義の概観： 命題論理 （真理値） （公理と推論規則） 述語論理 （モデルと解釈）
１ ２ ３ 意味論　semantics syntax　構文論

2 preview 述語論理は命題論理よりも複雑 例題：　次の文は真か偽か？ 「すべての自然数 x に対して x ＜ y を満たすような自然数 y が存在する」 　　（小野先生の例題） 解釈（その一） すべての x に対して「 x ＜ y を満たすような y が存在する」 ：∀x ∃y （x ＜ y） 解釈（その二） 「すべての x に対して x ＜ y を満たす」ような y が存在する ：∃y ∀x （x ＜ y） 曖昧

3 述語と対象変数 P : D×D  T, 2変数（引数）の述語
復習 命題とは真理値（真偽）が確定している文のこと 真偽のいずれかの値 { t, f } をとる：命題変数 対象変数を含む文の真理値は確定しない 例： ｘ ≦ y は素数である このような文を扱うために 命題関数 P を考える P : D  T, ここに T = { t, f } 例：　対象領域 D として自然数の集合を考える P : D×D  T, 2変数（引数）の述語 対象変数　individual variable, object variable 命題関数　propositional function

4 述語 predicate ↑ 正確な記法を次に述べる。∀と∃が多重になるときに注意
述語: 命題関数の具体的な表現　例: Le, Prime Le (x, 200) : （x ≦ 200 ）, ２変数（引数） Prime (y) ： 「 y は素数である」 対象領域 D の要素を対象 object, individual という 対象領域 D の上を動く変数を対象変数、D の定数を対象定数 object (individual) constant という 全称記号∀, と存在記号∃ ∀x P(x): すべての x∈D に対して P(x) が真になる ∃y Q(y): ある y ∈D が存在して Q(y) が真になる 述語記号 ↑　正確な記法を次に述べる。∀と∃が多重になるときに注意

5 述語論理の項 term 今までに登場したもの： 対象変数、対象定数
今までに登場したもの：　対象変数、対象定数 さらに必要なもの：　対象領域の上の関数記号 関数記号の例：　自然数の上の ＋, × 項 term の定義： 個々の対象定数、対象変数は項である f が n 変数（引数）の関数記号で, t1, t2, …, tn が項であるならば f (t1, t2,…, tn) は項である 項の例： 200, x, y, (3＋x), 6×(x＋y) ＋(3,x), ×(6, ＋(x, y)) とも書く

6 論理式 formula, wff 述語記号： 述語を表す記号
述語記号：　述語を表す記号 P が n 変数（引数）の述語記号で t1, t2, …, tn が項ならば 、P(t1, t2, …, tn) は論理式である A, B が論理式ならば、 A∧B, A∨B, A⇒B, ￢Aは、いずれも論理式である A が論理式で x が対象変数ならば 、 (∀x A), (∃x A) は論理式である 注：「1」の形の論理式を原子(atomic)論理式 という 復習：⇔は省略してよい 例：　∀x（∀y（∃q（∃r（x=q×y+r））））, = は述語記号

7 ∀, ∃ quantifier 限定記号, 量化記号, 限量子
「すべての x に対して R（x, y） を満たす y が存在する」 という文は曖昧である ∀x ∃y （x ＜ y） すべての自然数 x に対して，x よりも大きな 自然数 y （例えば x＋1 ）が存在する　（真） ∃y ∀x （x ＜ y） ある自然数 y が存在して，y は如何なる （すべての）自然数 x よりも大きい　（偽） 前出

8 自由変数と束縛変数 free and bound variables
∀x ∃y （x ＜ y） の変数 x, y は、変数と呼ばれているが、代入の対象にならない ∀z ∃y （z ＜ y） と書いても意味が変わらない 変数には２種類ある。自由変数と束縛変数 ここで注意するべき事は、同じ変数が自由であり、同時に束縛されることがある 例： ∃y （x ＝ y＋y ）∧ ∃z （ y ＝ z＋z＋1 ） x は偶数である y は奇数である 自由変数と束縛変数を出現 occurrenceという単位で区別しなければならない　

9 出現 occurrence A が原子論理式であるとき、A に含まれる変数 x の出現は、すべて自由な出現である
A が B∧C, B∨C, B⇒C, ￢B のいずれかであるとする。もし x が B または C における自由な出現であるならば、その x は A において自由である。もし x が B または C における束縛された出現であるならば、その x は A において束縛されている A が (∀z B) または (∃z B) であるとする。もし z が x であるときは、Aにおける x の出現は束縛されている。 z が x と異なる場合には、もし x が B における自由な出現であるならば、その x の出現は A において自由である。もし x が B における束縛された出現であるならば、その x の出現は A において束縛されている

10 自由変数と束縛変数（例） 例： ∃y （x ＝ y＋y ）∧ ∃z （ y ＝ z＋z＋1 ）
論理式が自由変数を一つも含まない時 閉論理式 closed formula という 論理式 A に含まれる自由変数 x に項 t を代入して得られる論理式を A[t/x] と表す 代入をめぐる珍現象： （小野先生の例題） ∃z（x＝y×z）　　: x は y の倍数である ∃z（x＝100×z） : x は 100 の倍数である ∃z（x＝z×z）　　: x は平方数である これを避けるために自由変数と束縛変数の記号の種類を分ける流儀の教科書もある

11 代入の方法 A は ∀zB または ∃zB の形の論理式とする
A[t/x]は z が x のとき A[t/x] は A 自身（束縛変数に代入不可） z が x とは異なる変数のとき、 t に z が出現しなければ、 A[t/x] は ∀zA[t/x] または ∃zA[t/x] t に z が出現する場合は、 A[t/x] は ∀w（（A[w/z]）[t/x]） または ∃w（（A[w/z]）[t/x] ） ただし w は A にも t にも現れない新しい対象変数 i.e. 項 t に変数 w が現れることがない

12 論理式の意味 述語論理の論理式の意味を考えるには、対象領域domain を定める必要がある
（解釈 interpretation, モデル model, 構造 structure） 空でない集合 D を定める 対象定数に D の要素（元）を対応づける 対象変数は D の上を動く 関数記号に D の上の関数を対応づける 述語記号に D の上の述語を対応づける　※ 単なる記号 に 具体的な要素、関数、述語 を対応 ※　ただし述語記号 ＝ （等号）の解釈は通常の等号とする

13 解釈 ⊨ 閉論理式 M ⊨ A 解釈 M において論理式 A が真 M ⊭ A 解釈 M において論理式 A が偽
⊭⊨ M ⊨ A 解釈 M において論理式 A が真 M ⊭ A 解釈 M において論理式 A が偽 A が原子論理式のとき M ⊨ P(t1, t2, …, tn) となるのは、Pの解釈が項 t1, t2, …, tn の解釈において真になる場合である. M ⊨ A∧B となるのは （M ⊨ A かつ M ⊨ B ）, M ⊨ A∨B となるのは（M ⊨ A または M ⊨ B）, M ⊨ A⇒B となるのは （M ⊨ A ならば M ⊨ B）, M ⊨ ￢A となるのは M ⊭ A の時である . ⊭⊨ : MSゴシック(UTF) M: Lucida Calligraph

14 （続） 解釈 ⊨ 閉論理式 M ⊨ ∀x A となるのは、すべての D の要素 u に対して M ⊨ A[u/x] となるとき,
（続）　解釈 ⊨ 閉論理式 ⊭⊨ M ⊨ ∀x A となるのは、すべての D の要素 u に対して M ⊨ A[u/x] となるとき, M ⊨ ∃x A となるのは、D のある要素 u が存在して M ⊨ A[u/x] となるときである. 論理式 B に対して、B に含まれる自由変数 が x1, x2, …, xm であるとき、 ∀x1∀x2…∀xm Bを B の閉包 universal closureという. BC と書く M ⊨ B となるのは M ⊨ BC となるときである. ⊭⊨ : MSゴシック(UTF) M: Lucida Calligraph

15 恒真な（valid）論理式 いかなる解釈（モデル）に対しても真になる論理式を恒真な valid 論理式という 「述語論理におけるトートロジー」ということもある どのような解釈をしても真になるということは、個別の対象要素、関数記号、述語記号の解釈に依存しないという意味である すなわち論理式の形（構造）により、恒真であるか否かが定まる

16 恒真な論理式の例（その一） A は x を自由変数として含まない
∀x A ⇔ A, ∃x A ⇔ A ∀x B ⇔ ∀y（B[y/x]）, ∃x B ⇔ ∃y （B[y/x]） ここに y は B に含まれていない新しい変数 A ∧ ∀x B ⇔ ∀x （A∧B）, A ∨ ∃x B ⇔ ∃x （A∨B） A ∨ ∀x B ⇔ ∀x （A∨B）, A ∧ ∃x B ⇔ ∃x （A∧B） ∀x B ∧ ∀x C ⇔ ∀x （B∧C）, ∃x B ∨ ∃x C ⇔ ∃x （B∨C） （∀x B ∨ ∀x C） ⇒ ∀x （B∨C）, ∃x（B ∧ C） ⇒ （∃x B∧∃x C）

17 恒真な論理式の例（その二） ∀x∀y B ⇔ ∀y∀x B , ∃x∃y B ⇔ ∃y∃x B ∃x∀y B ⇒ ∀y∃x B
∀x B ⇒ ∃x B ￢∀x B ⇔ ∃x￢B, ￢∃x B ⇔ ∀x￢B （A ⇒∀x B） ⇔ ∀x（A ⇒ B）, （A ⇒∃x B） ⇔ ∃x（A ⇒ B） （∀x B ⇒ A） ⇔ ∃x（B ⇒ A）, （∃x B ⇒ A） ⇔ ∀x（B ⇒ A） ∃x（B ⇒ C） ⇔ （∀x B ⇒ ∃x C） ∀x（B ⇒ C） ⇒ （∀x B ⇒ ∀x C） ∀x（B ⇒ C） ⇒ （∃x B ⇒ ∃x C） （関連の話題が前出） ド・モルガンの法則

18 恒真な論理式の説明 （∃x B ⇒ A） ⇔ ∀x（B ⇒ A）
この論理式に含まれる自由変数が y1, …, ym のとき、任意の解釈 M について次をいえばよい M ⊨∀y1…∀ym｛（∃x B ⇒ A） ⇔ ∀x（B ⇒ A）｝ 上は閉論理式であるから次をいう（解釈 4, 6） すべての u1, …,um ∈ D に対して M ⊨（∃x B ⇒ A）[u1/y1,…,um/ym] ⇔ M ⊨ ∀x（B ⇒ A） [u1/y1,…,um/ym] 以下では、既に項の代入が済んでいると仮定

19 恒真な論理式の説明（２） M ⊨ （∃x B ⇒ A） ⇔ M ⊨ ∀x（B ⇒ A）
M ⊨（∃x B ⇒ A） であると仮定する. これは解釈４と７から「（ある v∈D が存在して M ⊨ B[v/x]） ならば（M ⊨ A）である 」 ということになる 上は「（M ⊨ B[v/x] を満たすような v∈D は存在しない）または（M ⊨ A）である 」となる さらに「（すべての v∈D に対して M ⊭ B[v/x] ）または（M ⊨ A）である 」となる 論理式 A は x を自由変数として含まない 「（すべての v∈D に対して （M ⊭ B[v/x] またはM ⊨ A[v/x]）である 」 半分終り

20 恒真な論理式の説明（３） M ⊨ （∃x B ⇒ A） ⇔ M ⊨ ∀x（B ⇒ A）
M ⊨∀x（B ⇒ A） であると仮定する. 解釈６と４から「すべての v∈D に対して（M ⊨ B[v/x] ならば M ⊨ A[v/x]）である 」 になる 論理式 A は x を自由変数として含まない「すべての v∈D に対して（M ⊭ B[v/x] または M ⊨ A ）」 「（すべての v∈D に対してM ⊭ B[v/x]）または （M ⊨ A）である ）」，さらに「（M ⊨ B[v/x] を満たすv∈D は存在しない） または（M ⊨ A）である 」 「（M ⊨ B[v/x] を満たすv∈D が存在する） ならば （M ⊨ A）である 」 終

21 充足可能な論理式 ある解釈（モデル）に対して真になる論理式を充足可能な satisfiable 論理式という
充足可能でない論理式を充足不可能 unsatisfiable という 論理式 A が充足不可能であることは、￢A が恒真であることの必要十分条件である

22 冠頭標準形 prenex normal form
全称記号∀と存在記号∃が、他の論理記号の外側にあるとき、冠頭論理式という QxQyQz…A, Qは∀あるいは∃記号 A は全称記号も存在記号も含まない論理式 論理式 A と同値な冠頭論理式が存在する これを冠頭標準形という （小野先生の説明） 恒真な論理式の 3, 4, 10, 11, 12 を使って同値変形する。ただし A が自由変数 x を含むときは、まず 2. により x を新しい変数で置き換えておく

23 冠頭標準形への同値変形 ￢∃yP(x,y)∧∀y｛∃zQ(x,y,z)⇒R(x,y)}
￢∃yP(x,y)∧∀w｛∃zQ(x,w,z)⇒R(x,w)} ∀y￢P(x,y)∧∀w｛∃zQ(x,w,z)⇒R(x,w)} ∀y∀w{￢P(x,y)∧（∃zQ(x,w,z)⇒R(x,w)）} ∀y∀w{￢P(x,y)∧∀z（Q(x,w,z)⇒R(x,w)）} ∀y∀w∀z{￢P(x,y)∧（Q(x,w,z)⇒R(x,w)）} さらに ∀y∀w∀z{￢P(x,y)∧（￢Q(x,w,z)∨R(x,w)）} ∀y∀w∀z{（￢P(x,y)∧￢Q(x,w,z)） 　　　　　 ∨（ ￢P(x,y)∧R(x,w)）} 訂正： 廣瀬先生のp.24, ∃zは∀zです 分配法則

24 冠頭標準形 （廣瀬先生の説明） 与えられた述語の中の別の変数が同じ変数の記号で表されているとき、すべて異なる変数に書き換える
（廣瀬先生の説明） 与えられた述語の中の別の変数が同じ変数の記号で表されているとき、すべて異なる変数に書き換える 例: ∀x P（x,y）∨∃y Q（y,z）は∀x P（x,y）∨∃w Q（w,z） ∃x P（x）∧∀x Q（x, y）は∃x P（x）∧∀z Q（z, y） ド・モルガンの法則を用いて否定記号￢を内側に移動する（10） 全称記号∀と存在記号∃を外側に移動する （3, 4, 11, 12） さらに、冠頭標準形と論理和標準形、冠頭標準形と論理積標準形を組合せることができる