再履修の諸君への連絡事項 このページの内容は　

Presentation on theme: "再履修の諸君への連絡事項 このページの内容は　"— Presentation transcript:

1 再履修の諸君への連絡事項 このページの内容は　 情報数学を再履修している諸君は、上田先生のＷＥＢページ (このURL) を参照してください。 そのページの冒頭の説明を引用します。 「本科目の受講者は，情報理工学科の「情報数学」 （２単位）への出席・レポート提出・定期試験受験の ほかに，本ページに指示する課題（１単位分）を提出する必要があります．」 具体的な課題の内容はWEBページを読んでください。

2 再履修の諸君への連絡事項（２） Waseda netのメールでエラーが発生している諸君は次の事項に注意をしてください。
このページの内容は　 Waseda netのメールでエラーが発生している諸君は次の事項に注意をしてください。 Waseda netからhotmailに転送するとエラーになります。この詳しい説明は次を参照してください。(説明) Quota (学生一人当り5MB)をオーバーしているとメールを受信できません。

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

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

5 公理と推論規則 公理 axiom 前提となる論理式 推論規則 inference rule 幾つかの正しい論理式から、別の正しい論理式を導く
証明　proof　推論の過程の記述 定理　theorem　証明可能な論理式

6 ヒルベルト流 Hilbert の体系 公理、公理型 axiom scheme 1.～11.（命題論理） A⇒（B⇒A）
（A⇒（B⇒C））⇒（（A⇒B）⇒（A⇒C）） A⇒（A∨B） B⇒（A∨B） （A⇒C）⇒（（B⇒C）⇒（（A∨B）⇒C）） （A∧B）⇒A （A∧B）⇒B （C⇒A）⇒（（C⇒B）⇒（C⇒（A∧B）））

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

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

9 定理と証明の例 A⇒A の証明： （A⇒（（A⇒A）⇒A）⇒（（A⇒（A⇒A））⇒（A⇒A）） ２ （A⇒（（A⇒A）⇒A） １
小野先生の本の他に次の教科書に上の証明がある 細井勉「論理数学」筑摩書房　 ISBN: さらに、B⇒（A⇒A） の証明：上に続けて （A⇒A）⇒（B⇒（A⇒A））　　　　　　　　　　　　　　　　１ B⇒（A⇒A）　　　　　　　　　　　　　　　　　　　　　　ＭＰ

10 ヒルベルト流 述語論理 公理に２つの論理式を追加 ∀xA ⇒ A[t/x] A[t/x] ⇒∃xA 推論規則を２つ追加する
ヒルベルト流　述語論理 公理に２つの論理式を追加 ∀xA ⇒ A[t/x] A[t/x] ⇒∃xA 推論規則を２つ追加する a は自由変数、導かれる論理式には出現しない 横棒の下の論理式 C⇒A(a) A(a)⇒C C⇒∀xA ∃xA⇒C

11 ゲンツェン 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 が証明可能（定理）である m＝０

12 シーケント計算の推論規則（構造） Γ→Δ A, Γ→Δ Γ→Δ, A A, A, Γ→Δ Γ→Δ, A, A Γ, A, B, Π→Δ
　ギリシャ大文字は　 A, Γ→Δ 有限個の論理式 Γ→Δ, A A, A, Γ→Δ Γ→Δ, A, A Γ, A, B, Π→Δ Γ→Δ, A, B, Σ Γ, B, A, Π→Δ Γ→Δ, B, A, Σ w左 w右 c左 c右 e左 e右 Γ→Δ, A　　　　A, Π→Σ　　　　 Γ, Π→Δ, Σ cut w: weakening, c: contraction, e: exchange, cut = Schnitt （独）

13 シーケント計算（論理記号） A, Γ→Δ B, Γ→Δ A∧B, Γ→Δ Γ→Δ, A Γ→Δ, B A, Γ→Δ B, Γ→Δ
∧左 ∧左 ∧右 ∨左 ∨右 ∨右 ⇒左 ⇒右 ￢左 ￢右

14 シーケントによる証明の例 A → A → （A⇒A） A→A B→B 短い証明の例： （A⇒B）, A → B 少し長い証明の例：
⇒右 少し長い証明の例： A→A 　　 B→B （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右 ⇒右

15 シーケント計算（述語論理） A[t/x], Γ→Δ Γ→Δ, A[z/x] ∀xA, Γ→Δ Γ→Δ, ∀xA A[z/x], Γ→Δ
∀左 ∀右 ∃右 ∃左 変数 z は横棒の下の式に自由変数として出現しない z を固有変数 eigen variable という　　　　変数条件

16 ゲンツェンの自然演繹法 natural deduction
公理　なし　（０個） 推論規則　１４（数え方によっては１６） 特有の記法　「仮定が落ちる discharge」 A を仮定して 点線は有限回の推論規則の適用を示す [ A ] B A⇒B B が導かれる もはや仮定 A とは無関係に A⇒Bが成り立つ 仮定 A が推論規則によって「落ちる」 この明快な説明は、松本和夫「数理論理学」共立出版　（復刊） 　　　　　ISBN-10: ，ISBN-13:

17 自然演繹法（ＮＪ，ＮＫ） [ A ] B A A⇒B A⇒B A B A∧B A [A] [B] A∨B C ⇒Ｉ ⇒Ｅ ∧Ｉ ∧Ｅ ∧Ｅ
∨Ｉ ∨Ｅ ∨Ｉ

18 自然演繹法（続） [A] f A ￢Ａ ｆ ￢A Ａ ￢￢Ａ A[z/x] ∀xA A[t/x] [A[z/x]] ∃xA B α ￢ Ｉ
￢ Ｅ β ＮＪでは β を除く t は任意の項 z に変数条件あり ∀Ｉ ∀Ｅ ∃Ｉ ∃Ｅ

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

20 自然演繹法による証明の例 述語論理の恒真論理式（１５） ∀x（B⇒C）⇒（∃xB⇒∃xC） [∀x（B⇒C）] [B(a)]
　　B(a) ⇒ C(a) [∃xB] C(a) 　C(a) ∃xC ∃xB⇒∃xC ∀x（B⇒C）⇒（∃xB⇒∃xC） ∀Ｅ ⇒Ｅ ∃Ｅ ∃Ｉ ⇒Ｉ ⇒Ｉ 演習問題：　恒真論理式（１４）を証明せよ ∀x（B ⇒ C） ⇒ （∀x B ⇒ ∀x C）

21 自然演繹法による証明の例 述語論理の恒真論理式（１５） ∀x（B⇒C）⇒（∃xB⇒∃xC） [∀x（B⇒C）] [B(a)]
　　B(a) ⇒ C(a) [∃xB] C(a) 　C(a) ∃xC ∃xB⇒∃xC ∀x（B⇒C）⇒（∃xB⇒∃xC） ∀Ｅ ⇒Ｅ ∃Ｅ ∃Ｉ ⇒Ｉ ⇒Ｉ 演習問題：　恒真論理式（１４）を証明せよ ∀x（B ⇒ C） ⇒ （∀x B ⇒ ∀x C）

22 自然演繹法による証明の例 述語論理の恒真論理式（１５） ∀x（B⇒C）⇒（∃xB⇒∃xC） [∀x（B⇒C）] [B(a)]
　　B(a) ⇒ C(a) [∃xB] C(a) 　C(a) ∃xC ∃xB⇒∃xC ∀x（B⇒C）⇒（∃xB⇒∃xC） ∀Ｅ ⇒Ｅ ∃Ｅ ∃Ｉ ⇒Ｉ ⇒Ｉ 演習問題：　恒真論理式（１４）を証明せよ ∀x（B ⇒ C） ⇒ （∀x B ⇒ ∀x C）

23 自然演繹法による証明の例 述語論理の恒真論理式（１５） ∀x（B⇒C）⇒（∃xB⇒∃xC） [∀x（B⇒C）] [B(a)]
　　B(a) ⇒ C(a) [∃xB] C(a) 　C(a) ∃xC ∃xB⇒∃xC ∀x（B⇒C）⇒（∃xB⇒∃xC） ∀Ｅ ⇒Ｅ ∃Ｅ ∃Ｉ ⇒Ｉ ⇒Ｉ 演習問題：　恒真論理式（１４）を証明せよ ∀x（B ⇒ C） ⇒ （∀x B ⇒ ∀x C）

24 自然演繹法による証明の例 述語論理の恒真論理式（１５） ∀x（B⇒C）⇒（∃xB⇒∃xC） [∀x（B⇒C）] [B(a)]
　　B(a) ⇒ C(a) [∃xB] C(a) 　C(a) ∃xC ∃xB⇒∃xC ∀x（B⇒C）⇒（∃xB⇒∃xC） ∀Ｅ ⇒Ｅ ∃Ｅ ∃Ｉ ⇒Ｉ ⇒Ｉ 演習問題：　恒真論理式（１４）を証明せよ ∀x（B ⇒ C） ⇒ （∀x B ⇒ ∀x C）

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

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

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

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

29 レポートの課題 （提出は CourseN@vi)
次の論理式の真理値表を作成せよ （A⇒（A∧￢B））∧（B⇒（B∧￢A）） 上の論理式の論理和標準形を求めよ ヒント：２つの方法のいずれを用いても良い 命題論理における恒真な論理式と、述語論理 における恒真な論理式の定義を各々述べよ ３の解答には、各自が参照した教科書、文献、ＷＥＢページなどを付記しておくこと 次の論理式を証明せよ。公理と推論規則の選択は３つの流儀のいずれでもよい ∀x（B ⇒ C） ⇒ （∀x B ⇒ ∀x C） 論理式 （∃x B∧∃x C）⇒∃x（B ∧ C）の反例を 具体的に挙げよ（授業中に説明した例を避ける）

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