寄せられた質問 : 演習問題について この講義の範囲に含まれる適切な演習問題が載っている参考書がありますか? できれば解答や解説が付いているものがあると良いのですが 第 回の授業の中で 演習問題に取り組む方法を説明しますこの授業は 回だけ行うもので 書籍の1 冊分に比べると少ない分量しかカバーしていません 回の講義の概観 : 1 完全性と不完全性 命題論理 命題論理 ( 真理値 ) ( 公理と推論規則 ) 2 述語論理 ( モデルと解釈 ) 述語論理 ( 公理と推論規則 ) 2 意味論 semantics syntax 構文論 公理と推論規則 公理 axiom 前提となる論理式 推論規則 inference rule 幾つかの正しい論理式から 別の正しい論理式を導く証明 proof 推論の過程の記述 定理 theorem 証明可能な論理式 使用する論理記号 論理式の定義は これまでと同じです ヒルベルト流 Hilbert の体系 公理 公理型 axiom scheme 1.~11.( 命題論理 ) 1. A ( A) 2. (A ( C)) ((A ) (A C)). A (A ) 4. (A ) 5. (A C) (( C) ((A ) C)) 6. (A ) A 7. (A ) 8. (C A) ((C ) (C (A ))) 4 5 ヒルベルト流の体系 ( 続 ) 9. (A ) ((A ) A) 10. A ( A ) 11. A A 推論規則 1 つ 注 ) 公理として選ばれている論理式は実は恒真であることが 後に示される ここでは 前提として 選ばれた論理式 なのであるから 形式的には公理が恒真であるか否かは問わない A A 三段論法, modus ponens, 分離規則 横棒の上 A と A が証明されるならば 横棒の下 も証明される 他の体系においても横棒の意味は同じ 6 公理の選び方 ヒルベルト流の公理の選び方は一通りではない廣瀬先生は A A を公理として採用している小野先生は A A を定理として証明している ( この証明は意外に長いステップである 後述 ) 重要な注意 : 証明の途中で公理とトートロジーを混同しないようにする例 : A A は A A と同値 既出 : 基本的なトートロジー 8 ただし公理として選ばれているかどうかは別 後出 : 実はトートロジーは定理になる しかし自明ではない 7 1
定理と証明の例 A A の証明 : 1. (A ((A A) A) ((A (A A)) (A A)) 2 2. (A ((A A) A) 1. (A (A A)) (A A) MP 4. A (A A) 1 5. (A A) MP 小野先生の本の他に次の教科書に上の証明がある 細井勉 論理数学 筑摩書房 ISN:9784480502018 さらに (A A) の証明 : 上に続けて 6. (A A) ( (A A)) 1 7. (A A) MP 8 ヒルベルト流述語論理 公理に2つの論理式を追加 12. A[t/x] 1. A[t/x] xa 横棒の下の論理式 推論規則を 2 つ追加する a は自由変数 導かれる論理式には出現しない C A(a) C A(a) C xa C 9 ゲンツェン Gentzen のシーケント計算 LK 論理式の列 論理式の列シーケント ( 式 ) A1, A2,, Am 1, 2,, n A1, A2,, Amを仮定すれば1 2 nが導かれる 左辺 m=0 のとき 仮定なし で導かれる右辺 n=0 のとき 矛盾が導かれる ( 導かれるもの無し ) 公理に相当する始式 ( シーケント ) 1つ A A 始式 initial sequent, beginning sequent m=0 論理式 が証明可能 ( 定理 ) である 10 シーケント計算の推論規則 ( 構造 ) Γ Δ ギリシャ大文字は Γ Δ w 左 A, Γ Δ 有限個の論理式 Γ Δ, A w 右 A, A, Γ Δ Γ Δ, A, A c 左 A, Γ Δ Γ Δ, A c 右 Γ, A,, Π Δ Γ Δ, A,, Σ e 左 Γ,, A, Π Δ Γ Δ,, A, Σ e 右 Γ Δ, A A, Π Σ Γ, Π Δ, Σ cut w: weakening, c: contraction, e: exchange, cut = Schnitt ( 独 ) 11 シーケント計算 ( 論理記号 ) A, Γ Δ, Γ Δ 左 左 A, Γ Δ A, Γ Δ Γ Δ, A Γ Δ, 右 A, Γ Δ, Γ Δ 左 Γ Δ, A A, Γ Δ Γ Δ, A Γ Δ, Γ Δ, A Γ Δ, A Γ Δ, A, Π Σ A, Γ Δ, 左 A, Γ,Π Δ,Σ Γ Δ, A Γ Δ, A A, Γ Δ 左 右 A, Γ Δ Γ Δ, A 11 シーケントによる証明の例 A A 短い証明の例 : (A A) 少し長い証明の例 : 注 ) 証明された論理式は命題論理の基本的なトートロジー (8) の を に置き換えた論理式 A A (A ), A A, (A ) (A ), A (A ), A (A ) A, (A ) A, A (A ) A ((A ) ( A )) 左 e 左 右 e 右 c 右 1 2
シーケント計算 ( 述語論理 ) A[t/x], Γ Δ Γ Δ, A[z/x] 左, Γ Δ Γ Δ, 右 ゲンツェンの自然演繹法 natural deduction 公理なし (0 個 ) 推論規則 14( 数え方によっては 16) 特有の記法 仮定が落ちる discharge A[z/x], Γ Δ Γ Δ, A[t/x] 左 xa, Γ Δ Γ Δ, xa 変数 z は横棒の下の式に自由変数として出現しない z を固有変数 eigen variable という変数条件 右 14 A を仮定して が導かれる [ A ] A 点線は有限回の推論規則の適用を示す もはや仮定 A とは無関係に A が成り立つ仮定 A が推論規則によって 落ちる 証明図において すべての仮定が落ちているとき一番下の論理式は証明可能である この明快な説明は 松本和夫 数理論理学 共立出版 ( 復刊 ) ISN-10: 42001682,ISN-1: 978-420016828 15 自然演繹法 (NJ,NK) [ A ] A A A A A A A A I E E [A] [] A A C C A A C I I E 16 自然演繹法 ( 続 ) [A] f A A f A f A A[z/x] I E α I A A A[t/x] [A[z/x]] A[t/x] xa xa β NJでは β を除くただし NJ は本講義の範囲外です t は任意の項 z に変数条件あり 17 変数条件 ( どちらが分かりやすい ) A[z/x] I 比較 : シーケントの 右 [A[z/x]] xa 変数 z は および が従属しているどの仮定にも現れない 比較 : シーケントの 左 Γ Δ, A[z/x] Γ Δ, z は下式に現れない 変数 z は xa, および [A[z/x]] の下の が従属しているどの仮定にも (A[z/x] を除いて ) 現れない A[z/x], Γ Δ xa, Γ Δ z は下式に現れない 述語論理の恒真論理式 (15) x( C) ( x ) [ x( C) ] [ (a) ] (a) [ x ] x x( C) ( x ) 18 19
述語論理の恒真論理式 (15) x( C) ( x ) 述語論理の恒真論理式 (15) x( C) ( x ) x( C) [ (a) ] (a) [ x ] x x( C) ( x ) [ (a) ] x x x( C) ( x ) x( C) (a) 20 21 述語論理の恒真論理式 (15) x( C) ( x ) 述語論理の恒真論理式 (15) x( C) ( x ) x( C) [ (a) ] (a) [ x ] x x( C) ( x ) [ x( C) ] [ (a) ] (a) [ x ] x x( C) ( x ) 22 演習問題 :(14) を証明せよ x( C) ( x x C) 2 公理と推論規則 ( いろいろな形式 ) ヒルベルト流 : 公理 11+2, 推論規則 1+2 シーケント計算 : 公理 ( 相当 ) 1, 推論規則多数自然演繹法 : 公理なし, 推論規則多数 いずれの形式でも証明可能な論理式は同じ 演習のヒント : ヒルベルト流の公理を他の流儀で証明してみる 24 恒真論理式と定理 恒真論理式 valid トートロジー 証明可能な論理式 theorem 定理 命題論理の健全性 soundness 定理 : 証明可能な論理式は必ずトートロジーになる 命題論理の完全性 completeness 定理 : 任意のトートロジーは証明可能な論理式である 述語論理の健全性 述語論理の完全性 25 4
演習の戦略 : チェックリスト 1. 命題論理の論理式の真理値表を作成できる論理記号に対応する真理関数, と に注意 2. 論理式が恒真論理式であるか否か判定できる恒真論理式の意味, 恒真でない場合も重要 ( ). 命題論理式を標準形に変形できる標準形への同値変形, または真理値表から作成 ( ) 4. 述語論理式を解釈できる特に全称記号, 存在記号 を含む論理式恒真でない場合には, 真にならない具体例がある 5. 公理と推論規則により論理式を証明できる 6. 健全性と完全性の意味を説明できる 26 反例 述語論理の恒真な論理式 (8) の逆向きの反例 y x x y 対象領域として自然数 恒真な論理式 (6) の逆向きの を考えてみよう ( x x C) x ( C) x ( C) ( x x C) 対象領域を自然数の集合 を Even(x) つまり x は偶数である Cを Odd(x) つまり x は奇数であるとする 左辺は真であるが 右辺は真でない 演習問題 : ( x x C) x( C) の反例を探せ 27 反例を探す時の注意事項 対象領域として集合が使われる ただし論理式と集合を混同しないように注意 x ( C) ( x x C) 上の は集合 ではない 例えば を Even(x) () と解釈する 同様に Cも集合ではない 例えば C を Odd(x) と解釈する ( x x C) x( C) の反例を探す場合も同様の注意がある 解釈の一例 対象領域をクラスの全員 を数学のテストが満点 Math(x), C を英語のテストが満点 English(x) と解釈する 28 レポートの課題 1. 次の論理式の真理値表を作成せよ (A (A )) ( ( A)) 2. 上の論理式の論理和標準形を求めよヒント :2つの方法のいずれを用いても良い. 命題論理における恒真な論理式と 述語論理における恒真な論理式の定義を各々述べよ の解答には 各自が参照した教科書 文献 WE ページなどを付記する 4. 次のスライドに示す証明図において 落ちている (discharged) 仮定が つある 各々の仮定は どの推論規則によって落ちたのか 仮定ごとに推論規則の番号 (1)~(7) で答えよ 5. 論理式 ( x x C) x( C) の反例を具体的に挙げよ ( 授業中に説明した例を避ける ) 29 問題 4 の証明図 [ x] [ xc] (1) () (a) I (2) I (4) [ x xc] (a) (a) E (5) (a) I (6) x( C) (7) ( x xc) x( C) 0 レポート提出上の注意 CourseN@viのレポート名 情報数学 ( 論理学入門 ) もし表示されない時は 教学支援課に相談 各自のプロフィールのメールアドレス2 を登録 提出期間 : 本日 ~7 月 20 日 ( 火 ) までもし期限を過ぎていても CourseN@vi で提出できれる時は提出 レポートの本文に氏名 学籍番号 解答を明記 ヒント : この講義で使用した論理記号はJIS 第一水準の漢字に含まれている 証明図は工夫が必要 特別の事情がある場合 : 担当教員にメールで連絡をする ( アドレスを学科事務室で聞く ) 1 5