Microsoft PowerPoint - logic ppt [互換モード]

寄せられた質問： 演習問題について

• この講義の範囲に含まれる適切な演習問題が 載っている参考書がありますか？ できれば解答や解説が付いているものがあると 良いのですが 良いのですが… • 第３回の授業の中で、演習問題に取り組む方法 を説明します この授業は３回だけ行うもので、書籍の１冊分に 比べると少ない分量しかカバーしていません 2

完全性と不完全性

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

公理と推論規則

公理 axiom 前提となる論理式 推論規則 inference rule 幾つかの正しい論理式から、別の正しい論理 式を導く 4 式を導く 証明 proof 推論の過程の記述 定理 theorem 証明可能な論理式 使用する論理記号、論理式の定義は、 これまでと同じです。

ヒルベルト流 Hilbert の体系

公理、公理型 axiom scheme  1.～11.（命題論理） 1. A⇒（B⇒A） 2. （A⇒（B⇒C））⇒（（A⇒B）⇒（A⇒C）） 3. A⇒（A∨B） 4. B⇒（A∨B） 5. （A⇒C）⇒（（B⇒C）⇒（（A∨B）⇒C）） 6. （A∧B）⇒A 7. （A∧B）⇒B 8. （C⇒A）⇒（（C⇒B）⇒（C⇒（A∧B））） 5

ヒルベルト流の体系（続）

9. （A⇒B）⇒（（A⇒￢B）⇒￢A） 10. A⇒（￢A⇒B） 11. A∨￢A 注） 公理として選ばれている論理式は実は恒真であることが、後に示される。 ここでは「前提として」選ばれた論理式 なのであるから、形式的には公理が 推論規則 1つ 6 A A⇒B B 三段論法, modus ponens, 分離規則 横棒の上、A と A⇒B が証明されるならば、 横棒の下、B も証明される なのであるから、形式的には公理が 恒真であるか否かは問わない。 他の体系においても横棒の意味は同じ

公理の選び方

• ヒルベルト流の公理の選び方は一通りではない 廣瀬先生は A⇒A を公理として採用している 小野先生は A⇒A を定理として証明している （この証明は意外に長いステップである—後述） • 重要な注意： 証明の途中で公理とトートロジーを 混同しないようにする 例：A⇒A は ￢A∨A と同値 ←既出：基本的なトートロジー８ ただし公理として選ばれているかどうかは別 7 後出： 実はトートロジーは定理になる。しかし自明ではない

定理と証明の例

A⇒A の証明：

1. （A⇒（（A⇒A）⇒A）⇒（（A⇒（A⇒A））⇒（A⇒A）） ２

2. （A⇒（（A⇒A）⇒A） １

3. （A⇒（A⇒A））⇒（A⇒A） ＭＰ

4. A⇒（A⇒A） １ 5. （A⇒A） ＭＰ 小野先生の本の他に次の教科書に上の証明がある 細井勉「論理数学」筑摩書房 ISBN:9784480502018 さらに、B⇒（A⇒A） の証明：上に続けて 6. （A⇒A）⇒（B⇒（A⇒A）） １ 7. B⇒（A⇒A） ＭＰ 8

ヒルベルト流 述語論理

公理に２つの論理式を追加 12. ∀xA ⇒ A[t/x] 13. A[t/x] ⇒∃xA 横棒の下の論理式 推論規則を２つ追加する a は自由変数、導かれる論理式には出現しない 9 C⇒A(a) A(a)⇒C C⇒∀xA ∃xA⇒C

ゲンツェン Gentzen のシーケント計算ＬＫ

論理式の列→論理式の列 シーケント（式） A1, A2,…, Am →B1, B2, …, Bn A1, A2,…, Amを仮定すればB1∨B2∨…∨Bnが導かれる 左辺 m=0 のとき「仮定なし」で導かれる 右辺 n=0 のとき「矛盾が導かれる」（導かれるもの無し） 公理に相当する始式（シーケント） １つ

A → A         始式initial sequent, beginning sequent

→ B        論理式 B が証明可能（定理）である 10 m＝０

シーケント計算の推論規則（構造）

Γ→Δ ギリシャ大文字は Γ→Δ A, Γ→Δ 有限個の論理式 Γ→Δ, A A, A, Γ→Δ Γ→Δ, A, A A, Γ→Δ Γ→Δ, A w左 w右 c左 c右 11 , , Γ, A, B, Π→Δ Γ→Δ, A, B, Σ Γ, B, A, Π→Δ Γ→Δ, B, A, Σ Γ→Δ, A A,Π→Σ Γ, Π→Δ, Σ cut e左 e右

w: weakening, c: contraction, e: exchange, cut = Schnitt （独）

シーケント計算（論理記号）

A, Γ→Δ B, Γ→Δ A∧B, Γ→Δ A∧B, Γ→Δ Γ→Δ, A Γ→Δ, B A, Γ→Δ B, Γ→Δ Γ→Δ, A∧B A∨B, Γ→Δ ∧左 ∧左 ∧右 ∨左 Γ→Δ, A Γ→Δ, B Γ→Δ, A∨B Γ→Δ, A∨B Γ→Δ, A B, Π→Σ A, Γ→Δ, B A⇒B, Γ,Π→Δ,Σ Γ→Δ, A⇒B Γ→Δ, A A, Γ→Δ ￢A, Γ→Δ Γ→Δ, ￢A ∨右 ∨右 ⇒左 ⇒右 ￢左 ￢右

シーケントによる証明の例

A→A B→B （A⇒B） A → B A → A → （A⇒A） 短い証明の例： 少し長い証明の例： ⇒右 ⇒左 （A⇒B）, A → B A, （A⇒B） → B （A⇒B） → B, ￢A （A⇒B） → B, ￢A∨B （A⇒B） → ￢A∨B, B （A⇒B） → ￢A∨B, ￢A∨B

（A⇒B） → ￢A∨B →（（A⇒B）⇒（￢A∨B）） e左 ￢右 ∨右 e右 ∨右 c右 ⇒右 注） 証明された論理式は命題 論理の基本的なトートロジー（８） の⇔を⇒に置き換えた論理式

シーケント計算（述語論理）

A[t/x], Γ→Δ Γ→Δ, A[z/x] ∀xA, Γ→Δ Γ→Δ, ∀xA A[z/x], Γ→Δ Γ→Δ, A[t/x] Γ Δ Γ Δ ∀左 ∀右 ∃左 ∃右 ∃xA, Γ→Δ Γ→Δ, ∃xA 14 変数zは横棒の下の式に自由変数として出現しない z を固有変数eigen variable という 変数条件 ∃左 右

ゲンツェンの自然演繹法 natural deduction

• 公理 なし （０個） • 推論規則 １４（数え方によっては１６） • 特有の記法 「仮定が落ちる discharge」 [ A] B Aを仮定して Bが導かれる 点線は有限回の推論 規則の適用を示す 15 B A⇒B Bが導かれる 規則の適用を示す もはや仮定A とは無関係にA⇒Bが成り立つ 仮定A が推論規則によって「落ちる」 証明図において、すべての仮定が落ちているとき 一番下の論理式は証明可能である。 この明快な説明は、松本和夫「数理論理学」共立出版 （復刊） ISBN-10: 4320016823，ISBN-13: 978-4320016828

自然演繹法（ＮＪ，ＮＫ）

[ A ] B A A⇒B A⇒B B A B A∧B A∧B ⇒Ｉ ⇒Ｅ ∧Ｉ ∧Ｅ ∧Ｅ A∧B A B [A] [B] A B A∨B C C A∨B A∨B C 16 ∧Ｉ ∧Ｅ ∧Ｅ ∨Ｉ _∨Ｉ ∨Ｅ

自然演繹法（続）

[A] f A ￢Ａ ｆ ￢A ｆ Ａ ￢￢Ａ Ａ ￢ Ｉ ￢ Ｅ α β ＮＪではβ を除く ただしNJは本講義 Ａ A[z/x] ∀xA ∀xA A[t/x] [A[z/x]] A[t/x] ∃xA B ∃xA B 17 ただしNJは本講義 の範囲外です ∀Ｉ ∀Ｅ ∃Ｉ _∃Ｅ t は任意の項 zに変数条件あり

変数条件

（どちらが分かりやすい） A[z/x] ∀xA ∀Ｉ 変数z は∀xA および ∀xA が従属して いるどの仮定にも現れない 比較： シーケントの∀右 Γ→Δ, A[z/x] Γ→Δ, ∀xA zは下式に現れない 18 [A[z/x]] ∃xA B B ∃Ｅ 変数z は∃xA, B および[A[z/x]]の 下のB が従属しているどの仮定にも （A[z/x]を除いて）現れない A[z/x], Γ→Δ ∃xA, Γ→Δ 比較： シーケントの∃左 _zは下式に現れない

自然演繹法による証明の例

述語論理の恒真論理式（１５） ∀x（B⇒C）⇒（∃xB⇒∃xC） ∀E [ B(a) ] ⇒E C(a) 　[ ∀x（B⇒C） ] 　　B(a) ⇒ C(a) 19 C(a) ∃I [ ∃xB ] ∃xC ∃E ∃xC ⇒I ∃xB⇒∃xC ⇒I ∀x（B⇒C）⇒（∃xB⇒∃xC）

自然演繹法による証明の例

述語論理の恒真論理式（１５） ∀x（B⇒C）⇒（∃xB⇒∃xC） ∀E [ B(a) ] ⇒E C(a) 　 ∀x（B⇒C） 　　B(a) ⇒ C(a) 20 C(a) ∃I [ ∃xB ] ∃xC ∃E ∃xC ⇒I ∃xB⇒∃xC ⇒I ∀x（B⇒C）⇒（∃xB⇒∃xC）

自然演繹法による証明の例

述語論理の恒真論理式（１５） ∀x（B⇒C）⇒（∃xB⇒∃xC） ∀E [ B(a) ] ⇒E C(a) 　 ∀x（B⇒C） 　　B(a) ⇒ C(a) 21 C(a) ∃I ∃xB ∃xC ∃E ∃xC ⇒I ∃xB⇒∃xC ⇒I ∀x（B⇒C）⇒（∃xB⇒∃xC）

自然演繹法による証明の例

述語論理の恒真論理式（１５） ∀x（B⇒C）⇒（∃xB⇒∃xC） ∀E [ B(a) ] ⇒E C(a) 　∀x（B⇒C） 　　B(a) ⇒ C(a) 22 C(a) ∃I [ ∃xB ] ∃xC ∃E ∃xC ⇒I ∃xB⇒∃xC ⇒I ∀x（B⇒C）⇒（∃xB⇒∃xC）

自然演繹法による証明の例

述語論理の恒真論理式（１５） ∀x（B⇒C）⇒（∃xB⇒∃xC） ∀E [ B(a) ] ⇒E C(a) 　[ ∀x（B⇒C） ] 　　B(a) ⇒ C(a) 23 C(a) ∃I [ ∃xB ] ∃xC ∃E ∃xC ⇒I ∃xB⇒∃xC ⇒I ∀x（B⇒C）⇒（∃xB⇒∃xC） 演習問題：（１４）を証明せよ ∀x（B ⇒ C）⇒（∀x B ⇒ ∀x C）

公理と推論規則（いろいろな形式）

• ヒルベルト流： 公理 11+2, 推論規則 1+2 シーケント計算： 公理（相当） 1, 推論規則 多数 自然演繹法： 公理 なし, 推論規則 多数 • いずれの形式でも証明可能な論理式は同じ 演習のヒント： ヒルベルト流の公理を他の流儀 で証明してみる

恒真論理式と定理

• 命題論理の健全性soundness 定理： 恒真論理式 valid トートロジー 証明可能な論理式 theorem 定理 命題論理の健全性soundness 定理： 証明可能な論理式は必ずトートロジーになる • 命題論理の完全性completeness 定理： 任意のトートロジーは証明可能な論理式である • 述語論理の健全性 • 述語論理の完全性

演習の戦略： チェックリスト

1. 命題論理の論理式の真理値表を作成できる 論理記号に対応する真理関数, ∨と⇒に注意 2. 論理式が恒真論理式であるか否か判定できる 恒真論理式の意味, 恒真でない場合も重要（※） 3 命題論理式を標準形に変形できる 3. 命題論理式を標準形に変形できる 標準形への同値変形, または真理値表から作成（※） 4. 述語論理式を解釈できる 特に全称記号∀, 存在記号∃を含む論理式 恒真でない場合には, 真にならない具体例がある 5. 公理と推論規則により論理式を証明できる 6. 健全性と完全性の意味を説明できる。 26

反例

• 述語論理の恒真な論理式（８）の逆向きの反例 ∀y∃x B⇒∃x∀y B  対象領域として自然数 • 恒真な論理式（６）の逆向きの⇒を考えてみよう （∀x B ∨ ∀x C）⇒∀x （B∨C） ∀x （B∨C）⇒（∀x B ∨ ∀x C） ∀x （B∨C）⇒（∀x B ∨ ∀x C） 対象領域を自然数の集合、Bを Even(x) つまり x は 偶数である。Cを Odd(x) つまり x は奇数であると する。左辺は真であるが、右辺は真でない。 • 演習問題： （∃x B∧∃x C）⇒∃x（B ∧ C）の反例 を探せ。 27

反例を探す時の注意事項

• 対象領域として集合が使われる。ただし論理 式と集合を混同しないように注意。 ∀x （B∨C）⇒（∀x B ∨ ∀x C） • 上の Bは集合 Bではない。例えば Bを Even(x)と解釈する。同様に Cも集合ではを ( ) 解釈する。同様 も集合 は ない。例えば C を Odd(x)と解釈する。 • （∃x B∧∃x C）⇒∃x（B ∧ C）の反例を探す 場合も同様の注意がある。 • 解釈の一例、対象領域をクラスの全員。 Bを数学のテストが満点 Math(ｘ), C を英語の テストが満点 English(x)と解釈する。 28

レポートの課題

1. 次の論理式の真理値表を作成せよ （A⇒（A∧￢B））∧（B⇒（B∧￢A）） 2. 上の論理式の論理和標準形を求めよ ヒント：２つの方法のいずれを用いても良い 3. 命題論理における恒真な論理式と、述語論理 における恒真な論理式の定義を各々述べよ における恒真な論理式の定義を各々述べよ ３の解答には、各自が参照した教科書、文献、ＷＥＢページなどを付記する 4. 次のスライドに示す証明図において、落ちている (discharged)仮定が３つある。各々の仮定は、どの 推論規則によって落ちたのか。仮定ごとに推論規 則の番号(1)～(7)で答えよ。 5. 論理式 （∃x B∧∃x C）⇒∃x（B ∧ C）の反例を 具体的に挙げよ（授業中に説明した例を避ける）。29

問題４の証明図

[∀xB] [∀xC] ∀E (1) ∀E (3) B(a) C(a) ∨I (2) ∨I (4) [∀xB∨∀xC] B(a)∨C(a) B(a)∨C(a) ∨E (5) B(a)∨C(a) 30 　B(a)∨C(a) ∀I (6) ∀x(B∨C) ⇒I (7) (∀xB∨∀xC)⇒∀x(B∨C)

レポート提出上の注意

• CourseN@viのレポート名「情報数学（論理学入門）」 もし表示されない時は、教学支援課に相談 • 各自のプロフィールのメールアドレス２を登録 • 提出期間： 本日～７月２０日（火）まで もし期限を過ぎていても CourseN@vi で提出できれる時は提出 もし期限を過ぎていても CourseN@vi で提出できれる時は提出 • レポートの本文に氏名、学籍番号、解答を明記 • ヒント： この講義で使用した論理記号はＪＩＳ第一 水準の漢字に含まれている 。証明図は工夫が必要 • 特別の事情がある場合： 担当教員にメールで連 絡をする（アドレスを学科事務室で聞く） 31