スライド 1

寄せられた質問：演習問題について
• この講義の範囲に含まれる適切な演習問題が
載っている参考書がありますか？
できれば解答や解説が付いているものがあると
良いのですが…
• 第３回の授業の中で、演習問題に取り組む方法
を説明します
1
完全性と不完全性
３回の講義の概観：
１
命題論理
（真理値）
命題論理
（公理と推論規則）
３
２
述語論理
（モデルと解釈）
意味論 semantics
述語論理
（公理と推論規則）
syntax 構文論
2
公理と推論規則
公理 axiom 前提となる論理式
推論規則 inference rule
幾つかの正しい論理式から、別の正しい論理
式を導く
証明 proof 推論の過程の記述
定理 theorem 証明可能な論理式
3
ヒルベルト流 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）））
4
ヒルベルト流の体系（続）
9. （A⇒B）⇒（（A⇒￢B）⇒￢A）
10. A⇒（￢A⇒B）
11. A∨￢A
推論規則 1つ
A
A⇒B
B
三段論法, modus ponens, 分離規則
A と A⇒B が証明されるならば B も証明される
5
公理の選び方
• ヒルベルト流の公理の選び方は一通りではない
廣瀬先生は A⇒A を公理として採用している
小野先生は A⇒A を定理として証明している
（この証明は意外に長いステップである—後述）
• 重要な注意：証明の途中で公理とトートロジーを
混同しないようにする
例： A⇒A は￢A∨A と同値 ←既出：基本的なトートロジー８
公理として選ばれているかどうか
後出：実はトートロジーは定理になる
6
定理と証明の例
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）
ＭＰ
7
ヒルベルト流述語論理
公理に２つの論理式を追加
12. ∀xA ⇒ A[t/x]
13. A[t/x] ⇒∃xA
横棒の下の論理式
推論規則を２つ追加する
a は自由変数、導かれる論理式には出現しない
C⇒A(a)
C⇒∀xA
A(a)⇒C
∃xA⇒C
8
ゲンツェン 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 が証明可能（定理）である
9
シーケント計算の推論規則（構造）
Γ→Δ
A, Γ→Δ
ギリシャ大文字は
有限個の論理式の列
Γ→Δ
Γ→Δ, A
A, A, Γ→Δ
A, Γ→Δ
Γ→Δ, A, A
Γ→Δ, A
Γ, A, B, Π→Δ
Γ, B, A, Π→Δ
Γ→Δ, A, B, Σ
Γ→Δ, B, A, Σ
Γ→Δ, A
A, Π→Σ
Γ, Π→Δ, Σ
cut
10
シーケント計算（論理記号）
A, Γ→Δ
A∧B, Γ→Δ
B, Γ→Δ
A∧B, Γ→Δ
Γ→Δ, A Γ→Δ, B
Γ→Δ, A∧B
A, Γ→Δ B, Γ→Δ
A∨B, Γ→Δ
Γ→Δ, A
Γ→Δ, A∨B
Γ→Δ, B
Γ→Δ, A∨B
Γ→Δ, A B, Π→Σ
A⇒B, Γ,Π→Δ,Σ
A, Γ→Δ, B
Γ→Δ, A⇒B
Γ→Δ, A
￢A, Γ→Δ
A, Γ→Δ
Γ→Δ, ￢A
シーケントによる証明の例
A→A
→（A⇒A）
短い証明の例：
少し長い証明の例：
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））
12
シーケント計算（述語論理）
A[t/x], Γ→Δ
∀xA, Γ→Δ
Γ→Δ, A[z/x]
Γ→Δ, ∀xA
A[z/x], Γ→Δ
∃xA, Γ→Δ
Γ→Δ, A[t/x]
Γ→Δ, ∃xA
変数 z は横棒の下の式に自由変数として出現しない
z を固有変数 eigen variable という
13
ゲンツェンの自然演繹法 natural deduction
• 公理なし（０個）
• 推論規則１４
• 特有の記法「仮定が落ちる discharge」
A を仮定して
B が導かれる
[A]
B
A⇒B
点線は有限回の推論
規則の適用を示す
もはや仮定 A とは無関係に A⇒Bが成り立つ
仮定 A が推論規則によって「落ちる」
この明快な説明は、松本和夫「数理論理学」共立出版（復刊）
ISBN-10: 4320016823，ISBN-13: 978-4320016828
14
自然演繹法（ＮＪ，ＮＫ）
[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
15
自然演繹法（続）
[A]
f
￢A
A
￢Ａ
ｆ
ｆ
Ａ
￢￢Ａ
Ａ
A[z/x]
∀xA
A[t/x]
∃xA
∀xA
A[t/x]
∃xA
[A[z/x]]
B
B
16
自然演繹法による証明の例
[B(a)]
∃xB
[∀x（B⇒C）]
B(a) ⇒ C(a)
C(a)
C(a)
∃xC
∃xB⇒∃xC
∀x（B⇒C）⇒（∃xB⇒∃xC）
17
公理と推論規則（いろいろな形式）
• ヒルベルト流：公理１つ
シーケント計算：公理１つ
自然演繹法：公理なし
• いずれの形式でも証明可能な論理式は不変
演習のヒント：ヒルベルト流の公理を他の流儀で
証明してみる
18
恒真論理式と定理
恒真論理式
valid
トートロジー
証明可能な論理式
theorem
定理
• 命題論理の健全性 soundness 定理：
証明可能な論理式は必ずトートロジーになる
• 命題論理の完全性 completeness 定理：
任意のトートロジーは証明可能な論理式である
• 述語論理の健全性
• 述語論理の完全性
19
演習の戦略：チェックリスト
1. 命題論理の論理式の真理値表を作成できる
論理記号に対応する真理関数, ∨と⇒に注意
2. 論理式が恒真論理式であるか否か判定できる
恒真論理式の意味, 恒真でない場合も重要（※）
3. 命題論理式を標準形に変形できる
標準形への同値変形, または真理値表から作成
4. 述語論理式を解釈できる
特に全称記号∀, 存在記号∃を含む論理式
恒真でない場合には, 真にならない具体例がある
5. 公理と推論規則により論理式を証明できる
6. 健全性と完全性の意味を説明できる。
20
演習の戦略
21
反例
22

Download Report