寄せられた質問： 演習問題について この講義の範囲に含まれる適切な演習問題が載っている参考書がありますか？ できれば解答や解説が付いているものがあると良いのですが… 第３回の授業の中で、演習問題に取り組む方法を説明します

完全性と不完全性 ３回の講義の概観： 命題論理 （真理値） （公理と推論規則） 述語論理 （モデルと解釈） 意味論 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 が証明可能（定理）である

シーケント計算の推論規則（構造） Γ→Δ A, Γ→Δ Γ→Δ, A A, A, Γ→Δ Γ→Δ, A, A Γ, A, B, Π→Δ 　ギリシャ大文字は A, Γ→Δ 　有限個の論理式の列 Γ→Δ, A A, A, Γ→Δ Γ→Δ, A, A Γ, A, B, Π→Δ Γ→Δ, A, B, Σ Γ, B, A, Π→Δ Γ→Δ, B, A, Σ Γ→Δ, A　　　　A, Π→Σ　　　　 Γ, Π→Δ, Σ cut

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

シーケントによる証明の例 A→A →（A⇒A） A→A B→B 短い証明の例： （A⇒B）, A → B 少し長い証明の例： （A⇒B） → ￢A∨B, B （A⇒B） → ￢A∨B, ￢A∨B （A⇒B） → ￢A∨B →（（A⇒B）⇒（￢A∨B））

シーケント計算（述語論理） 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

自然演繹法による証明の例 [∀x（B⇒C）] [B(a)] B(a) ⇒ C(a) ∃xB C(a) C(a) ∃xC ∃xB⇒∃xC 　　　∀x（B⇒C）⇒（∃xB⇒∃xC）

公理と推論規則（いろいろな形式） ヒルベルト流： 公理１つ シーケント計算： 公理１つ 自然演繹法： 公理なし ヒルベルト流：　公理１つ シーケント計算：　公理１つ 自然演繹法：　公理なし いずれの形式でも証明可能な論理式は不変 演習のヒント：　ヒルベルト流の公理を他の流儀で証明してみる

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

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

演習の戦略

反例