スライド 1

「情報数学０６前再」の注意事項
このページの内容は http://www.goto.info.waseda.ac.jp/~goto/infomath.html の下半分
「情報数学０６前再」（３単位）を履修している諸君には
上田先生からの連絡が届きます。
「０６前再」の受講者は，情報理工学科の「情報数学」
（２単位）への出席・レポート提出・定期試験受験の
ほかに，上田先生の指示する課題（１単位分）を提出
する必要があります．
２０１０年度の課題の内容は上田先生からの指示によ
ります。Waseda Netのメールボックスが over quotaに
ならないように注意してください。なおセカンドメールを
活用してください。
1
寄せられた質問：演習問題について
• この講義の範囲に含まれる適切な演習問題が
載っている参考書がありますか？
できれば解答や解説が付いているものがあると
良いのですが…
• 第３回の授業の中で、演習問題に取り組む方法
を説明します
この授業は３回だけ行うもので、書籍の１冊分に
比べると少ない分量しかカバーしていません
2
完全性と不完全性
３回の講義の概観：
１
命題論理
（真理値）
命題論理
（公理と推論規則）
３
２
述語論理
（モデルと解釈）
意味論 semantics
述語論理
（公理と推論規則）
syntax 構文論
3
公理と推論規則
公理 axiom 前提となる論理式
推論規則 inference rule
幾つかの正しい論理式から、別の正しい論理
式を導く
証明 proof 推論の過程の記述
定理 theorem 証明可能な論理式
使用する論理記号、論理式の定義は、
これまでと同じです。
4
ヒルベルト流 Hilbert の体系
公理、公理型 axiom scheme 1.～11.（命題論理）
1. A⇒（B⇒A）
2. （A⇒（B⇒C））⇒（（A⇒B）⇒（A⇒C））
3. A⇒（A∨B）
4. B⇒（A∨B）
5. （A⇒C）⇒（（B⇒C）⇒（（A∨B）⇒C））
6. （A∧B）⇒A
7. （A∧B）⇒B
8. （C⇒A）⇒（（C⇒B）⇒（C⇒（A∧B）））
5
ヒルベルト流の体系（続）
9. （A⇒B）⇒（（A⇒￢B）⇒￢A）
10. A⇒（￢A⇒B）
11. A∨￢A
推論規則 1つ
A
A⇒B
B
注）公理として選ばれている論理式は
実は恒真であることが、後に示される。
ここでは「前提として」選ばれた論理式
なのであるから、形式的には公理が
恒真であるか否かは問わない。
三段論法, modus ponens, 分離規則
横棒の上、A と A⇒B が証明されるならば、
横棒の下、 B も証明される
他の体系においても横棒の意味は同じ
6
公理の選び方
• ヒルベルト流の公理の選び方は一通りではない
廣瀬先生は A⇒A を公理として採用している
小野先生は A⇒A を定理として証明している
（この証明は意外に長いステップである—後述）
• 重要な注意：証明の途中で公理とトートロジーを
混同しないようにする
例： A⇒A は￢A∨A と同値 ←既出：基本的なトートロジー８
ただし公理として選ばれているかどうかは別
後出：実はトートロジーは定理になる。しかし自明ではない
7
定理と証明の例
A⇒A の証明：
1. （A⇒（（A⇒A）⇒A）⇒（（A⇒（A⇒A））⇒（A⇒A））２
2. （A⇒（（A⇒A）⇒A）
１
3. （A⇒（A⇒A））⇒（A⇒A）
ＭＰ
4. A⇒（A⇒A）
１
5. （A⇒A）
ＭＰ
小野先生の本の他に次の教科書に上の証明がある
細井勉「論理数学」筑摩書房 ISBN:9784480502018
さらに、B⇒（A⇒A）の証明：上に続けて
6. （A⇒A）⇒（B⇒（A⇒A））
１
7. B⇒（A⇒A）
ＭＰ
8
ヒルベルト流述語論理
公理に２つの論理式を追加
12. ∀xA ⇒ A[t/x]
13. A[t/x] ⇒∃xA
横棒の下の論理式
推論規則を２つ追加する
a は自由変数、導かれる論理式には出現しない
C⇒A(a)
C⇒∀xA
A(a)⇒C
∃xA⇒C
9
ゲンツェン Gentzen のシーケント計算ＬＫ
論理式の列 → 論理式の列シーケント（式）
A1, A2,…, Am → B1, B2, …, Bn
A1, A2,…, Amを仮定すればB1∨B2∨…∨Bnが導かれる
左辺 m=0 のとき「仮定なし」で導かれる
右辺 n=0 のとき「矛盾が導かれる」（導かれるもの無し）
公理に相当する始式（シーケント）１つ
A→A
始式 initial sequent, beginning sequent
→B
m＝０
論理式 B が証明可能（定理）である
10
シーケント計算の推論規則（構造）
Γ→Δ
A, Γ→Δ
w左
A, A, Γ→Δ
A, Γ→Δ
c左
Γ, A, B, Π→Δ
e左
Γ, B, A, Π→Δ
ギリシャ大文字は
有限個の論理式
Γ→Δ
Γ→Δ, A
w右
Γ→Δ, A, A
Γ→Δ, A
c右
Γ→Δ, A, B, Σ
e右
Γ→Δ, B, A, Σ
Γ→Δ, A
A, Π→Σ
Γ, Π→Δ, Σ
cut
w: weakening, c: contraction, e: exchange, cut = Schnitt （独）
11
シーケント計算（論理記号）
A, Γ→Δ
A∧B, Γ→Δ
∧左
Γ→Δ, A Γ→Δ, B ∧右
Γ→Δ, A∧B
Γ→Δ, A
Γ→Δ, A∨B
∨右
Γ→Δ, A B, Π→Σ ⇒左
A⇒B, Γ,Π→Δ,Σ
Γ→Δ, A
￢A, Γ→Δ
￢左
B, Γ→Δ
A∧B, Γ→Δ
∧左
A, Γ→Δ B, Γ→Δ
∨左
A∨B, Γ→Δ
Γ→Δ, B
Γ→Δ, A∨B
∨右
A, Γ→Δ, B
Γ→Δ, A⇒B
⇒右
A, Γ→Δ
Γ→Δ, ￢A
￢右
11
シーケントによる証明の例
短い証明の例：
A→A
⇒右
→ （A⇒A）
少し長い証明の例：
A→A
B→B
⇒左
（A⇒B）, A → B
注）証明された論理式は命題
e左
A, （A⇒B） → B
論理の基本的なトートロジー（８）
￢右
の⇔を⇒に置き換えた論理式
（A⇒B） → B, ￢A
∨右
（A⇒B） → B, ￢A∨B
e右
（A⇒B） → ￢A∨B, B
∨右
（A⇒B） → ￢A∨B, ￢A∨B c右
（A⇒B） → ￢A∨B
⇒右
→（（A⇒B）⇒（￢A∨B））
13
シーケント計算（述語論理）
A[t/x], Γ→Δ
∀左
∀xA, Γ→Δ
Γ→Δ, A[z/x]
Γ→Δ, ∀xA
∀右
A[z/x], Γ→Δ
∃左
∃xA, Γ→Δ
Γ→Δ, A[t/x]
Γ→Δ, ∃xA
∃右
変数 z は横棒の下の式に自由変数として出現しない
z を固有変数 eigen variable という
変数条件
14
ゲンツェンの自然演繹法 natural deduction
• 公理なし（０個）
• 推論規則１４（数え方によっては１６）
• 特有の記法「仮定が落ちる discharge」
A を仮定して
B が導かれる
[A]
B
A⇒B
点線は有限回の推論
規則の適用を示す
もはや仮定 A とは無関係に A⇒Bが成り立つ
仮定 A が推論規則によって「落ちる」
証明図において、すべての仮定が落ちているとき
一番下の論理式は証明可能である。
この明快な説明は、松本和夫「数理論理学」共立出版（復刊）
ISBN-10: 4320016823，ISBN-13: 978-4320016828
15
自然演繹法（ＮＪ，ＮＫ）
[A]
B
A⇒B
A
B
A∧B
A
A∨B
⇒Ｉ
∧Ｉ
∨Ｉ
A
A⇒B
B
A∧B
A
B
A∨B
⇒Ｅ
∧Ｅ
∨Ｉ
A∧B
B
A∨B
∧Ｅ
[A] [B]
C
C
C
∨Ｅ
16
自然演繹法（続）
[A]
f
￢A
A[z/x]
∀xA
A[t/x]
∃xA
￢Ｉ
∀Ｉ
∃Ｉ
A
￢Ａ
ｆ
￢Ｅ
￢￢Ａ
Ａ
β
∀xA
A[t/x]
∀Ｅ
∃xA
ｆ
Ａ
α
ＮＪでは β を除く
ただしNJは本講義
の範囲外です
t は任意の項
z に変数条件あり
[A[z/x]]
B
B
∃Ｅ
17
変数条件（どちらが分かりやすい）
A[z/x]
∀xA
∀Ｉ
変数 z は∀xA および ∀xA が従属して
いるどの仮定にも現れない
比較：シーケントの∀右
[A[z/x]]
∃xA
B
B
∃Ｅ
比較：シーケントの∃左
Γ→Δ, A[z/x]
Γ→Δ, ∀xA
z は下式に現れない
変数 z は∃xA, B および [A[z/x]]の
下の B が従属しているどの仮定にも
（A[z/x]を除いて）現れない
A[z/x], Γ→Δ
∃xA, Γ→Δ
z は下式に現れない
18
自然演繹法による証明の例
述語論理の恒真論理式（１５） ∀x（B⇒C）⇒（∃xB⇒∃xC）
[ ∀x（B⇒C） ]
∀E
B(a) ⇒ C(a)
[ B(a) ]
⇒E
C(a)
∃I
[ ∃xB ]
∃xC
∃E
∃xC
⇒I
∃xB⇒∃xC
⇒I
∀x（B⇒C）⇒（∃xB⇒∃xC）
19
自然演繹法による証明の例
述語論理の恒真論理式（１５） ∀x（B⇒C）⇒（∃xB⇒∃xC）
∀x（B⇒C）
∀E
B(a) ⇒ C(a)
[ B(a) ]
⇒E
C(a)
∃I
[ ∃xB ]
∃xC
∃E
∃xC
⇒I
∃xB⇒∃xC
⇒I
∀x（B⇒C）⇒（∃xB⇒∃xC）
20
自然演繹法による証明の例
述語論理の恒真論理式（１５） ∀x（B⇒C）⇒（∃xB⇒∃xC）
∀x（B⇒C）
∀E
B(a) ⇒ C(a)
[ B(a) ]
⇒E
C(a)
∃I
∃xB
∃xC
∃E
∃xC
⇒I
∃xB⇒∃xC
⇒I
∀x（B⇒C）⇒（∃xB⇒∃xC）
21
自然演繹法による証明の例
述語論理の恒真論理式（１５） ∀x（B⇒C）⇒（∃xB⇒∃xC）
∀x（B⇒C）
∀E
B(a) ⇒ C(a)
[ B(a) ]
⇒E
C(a)
∃I
[ ∃xB ]
∃xC
∃E
∃xC
⇒I
∃xB⇒∃xC
⇒I
∀x（B⇒C）⇒（∃xB⇒∃xC）
22
自然演繹法による証明の例
述語論理の恒真論理式（１５） ∀x（B⇒C）⇒（∃xB⇒∃xC）
[ ∀x（B⇒C） ]
∀E
B(a) ⇒ C(a)
[ B(a) ]
⇒E
C(a)
∃I
[ ∃xB ]
∃xC
∃E
∃xC
⇒I
∃xB⇒∃xC
⇒I
∀x（B⇒C）⇒（∃xB⇒∃xC）
演習問題：（１４）を証明せよ ∀x（B ⇒ C） ⇒ （∀x B ⇒ ∀x C）
23
公理と推論規則（いろいろな形式）
• ヒルベルト流：公理 11+2, 推論規則 1+2
シーケント計算：公理（相当） 1, 推論規則多数
自然演繹法：公理なし, 推論規則多数
• いずれの形式でも証明可能な論理式は同じ
演習のヒント：ヒルベルト流の公理を他の流儀
で証明してみる
24
恒真論理式と定理
恒真論理式
valid
トートロジー
証明可能な論理式
theorem
定理
• 命題論理の健全性 soundness 定理：
証明可能な論理式は必ずトートロジーになる
• 命題論理の完全性 completeness 定理：
任意のトートロジーは証明可能な論理式である
• 述語論理の健全性
• 述語論理の完全性
25
演習の戦略：チェックリスト
1. 命題論理の論理式の真理値表を作成できる
論理記号に対応する真理関数, ∨と⇒に注意
2. 論理式が恒真論理式であるか否か判定できる
恒真論理式の意味, 恒真でない場合も重要（※）
3. 命題論理式を標準形に変形できる
標準形への同値変形, または真理値表から作成（※）
4. 述語論理式を解釈できる
特に全称記号∀, 存在記号∃を含む論理式
恒真でない場合には, 真にならない具体例がある
5. 公理と推論規則により論理式を証明できる
6. 健全性と完全性の意味を説明できる。
26
反例
• 述語論理の恒真な論理式（８）の逆向きの反例
∀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）の反例を探せ
。
27
反例を探す時の注意事項
• 対象領域として集合が使われる。ただし論理
式と集合を混同しないように注意。
∀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)と解釈する。
28
レポートの課題
1. 次の論理式の真理値表を作成せよ
（A⇒（A∧￢B））∧（B⇒（B∧￢A））
2. 上の論理式の論理和標準形を求めよ
ヒント：２つの方法のいずれを用いても良い
3. 命題論理における恒真な論理式と、述語論理
における恒真な論理式の定義を各々述べよ
３の解答には、各自が参照した教科書、文献、ＷＥＢページなどを付記する
4. 次のスライドに示す証明図において、落ちている
(discharged)仮定が３つある。各々の仮定は、どの
推論規則によって落ちたのか。仮定ごとに推論規
則の番号(1)～(7)で答えよ。
5. 論理式（∃x B∧∃x C）⇒∃x（B ∧ C）の反例を
具体的に挙げよ（授業中に説明した例を避ける）。
29
問題４の証明図
[∀xB]
[∀xC]
∀E (1)
∀E (3)
B(a)
C(a)
∨I (2)
[∀xB∨∀xC]
∨I (4)
B(a)∨C(a)
B(a)∨C(a)
∨E (5)
B(a)∨C(a)
∀I (6)
∀x(B∨C)
⇒I (7)
(∀xB∨∀xC)⇒∀x(B∨C)
30
レポート提出上の注意
• CourseN@viのレポート名「情報数学（論理学入門）」
もし表示されない時は、教学支援課に相談
• 各自のプロフィールのメールアドレス２を登録
• 提出期間：本日～７月２０日（火）まで
もし期限を過ぎていても CourseN@vi で提出できれる時は提出
• レポートの本文に氏名、学籍番号、解答を明記
• ヒント：この講義で使用した論理記号はＪＩＳ第一
水準の漢字に含まれている。証明図は工夫が必要
• 特別の事情がある場合：担当教員にメールで連
絡をする（アドレスを学科事務室で聞く）
31

Download Report