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

Size: px

Start display at page:

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

うのすけさくいし
5 years ago
Views:

1 寄せられた質問 : 演習問題についてこの講義の範囲に含まれる適切な演習問題が載っている参考書がありますか? できれば解答や解説が付いているものがあると良いのですが第回の授業の中で演習問題に取り組む方法を説明しますこの授業は回だけ行うもので書籍の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

2 定理と証明の例 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: さらに (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

3 シーケント計算 ( 述語論理 ) 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: ,ISN-1: 自然演繹法 (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

4 述語論理の恒真論理式 (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) 述語論理の恒真論理式 (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

5 演習の戦略 : チェックリスト 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

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

Microsoft PowerPoint - logic ppt [互換モード] 述語論理と ( 全称 ) ( 存在 ) 回の講義の概観 : 命題論理 ( 真理値 ) 2 述語論理 ( モデルと解釈 ) 意味論 semantics 命題論理 ( 公理と推論規則 ) 述語論理 ( 公理と推論規則 ) syntax 構文論 preview 述語論理は命題論理よりも複雑例題 : 次の文は真か偽か? ( 曖昧な文です ) すべての自然数 x に対して x < y を満たすような自然数