「情報数学０６前再」の注意事項 このページの内容は　http://www.goto.info.waseda.ac.jp/~goto/infomath.html　の下半分 「情報数学０６前再」（３単位）を履修している諸君には上田先生からの連絡が届きます。 「０６前再」の受講者は，情報理工学科の「情報数学」 （２単位）への出席・レポート提出・定期試験受験の ほかに，上田先生の指示する課題（１単位分）を提出する必要があります． ２００９年度の課題の内容は上田先生からの指示によります。Waseda Netのメールボックスが over quotaにならないように注意してください。

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

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

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

ヒルベルト流 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）））

ヒルベルト流の体系（続） 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 も証明される 他の体系においても横棒の意味は同じ

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

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

ヒルベルト流 述語論理 公理に２つの論理式を追加 ∀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

ゲンツェン 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＝０

シーケント計算の推論規則（構造） Γ→Δ 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 （独）

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

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

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

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

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

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

変数条件（どちらが分かりやすい） 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 は下式に現れない

自然演繹法による証明の例 述語論理の恒真論理式（１５） ∀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）

自然演繹法による証明の例 述語論理の恒真論理式（１５） ∀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）

自然演繹法による証明の例 述語論理の恒真論理式（１５） ∀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）

自然演繹法による証明の例 述語論理の恒真論理式（１５） ∀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）

自然演繹法による証明の例 述語論理の恒真論理式（１５） ∀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）

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

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

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

反例 述語論理の恒真な論理式（８）の逆向きの反例 ∀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）の反例を探せ。

反例を探す時の注意事項 対象領域として集合が使われる。ただし論理式と集合を混同しないように注意。 ∀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)と解釈する。

レポートの課題 次の論理式の真理値表を作成せよ (Ａ⇒Ｂ) ⇒ [(Ｃ⇒Ａ) ⇒ (Ｃ⇒Ｂ)] 次の論理式の真理値表を作成せよ (Ａ⇒Ｂ) ⇒ [(Ｃ⇒Ａ) ⇒ (Ｃ⇒Ｂ)] 上の論理式の論理和標準形を求めよ ヒント：２つの方法のいずれを用いても良い 命題論理における恒真な論理式と、述語論理 における恒真な論理式の定義を各々述べよ ３の解答には、各自が参照した教科書、文献、ＷＥＢページなどを付記しておくこと 次のスライドの証明図の 1～7 の推論規則の 名称を各々述べよ。 論理式 （∃x B∧∃x C）⇒∃x（B ∧ C）の反例を 具体的に挙げよ（授業中に説明した例を避ける）。

問題４の証明図

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

Extra roman version ∀x（B⇒C） [B(a)] B(a) ⇒ C(a) [∃xB] C(a) C(a) ∃xC ∃xB⇒∃xC ∀x（B⇒C）⇒（∃xB⇒∃xC） ∀Ｅ ⇒Ｅ ∃Ｅ ∃Ｉ ⇒Ｉ ⇒Ｉ