講義資料 (PDF)

論理学
第 3 回証明
萩野達也
慶應義塾大学
環境情報学部
LOGIC03 (1/17)
これまで
命題
論理結合子
真理値表
トートロジー
標準形
論理和標準形
論理積標準形
論理結合子の制限
LOGIC03 (2/17)
推論
真理値表を用いた命題の正しさの定義
基本的な命題 (命題変数) の真偽値から，命題の真偽を計算する
推論
すでに正しいと分かっている命題から，別の正しい命題を導く
推論規則を繰り返し用いて，前提となる命題から，命題導く
「前提 B1 , . . . , Bn から A が推論される」
推論規則 (inference rule)
正しい命題から正しい命題を導く規則
例
A と A ⊃ B から B を導く
モーダスポネンス (modus ponens)
三段論法 (syllogium) とも呼ばれる
「人間は死すべきもの」であり「ソクラテスは人間である」，ゆえに「ソクラテ
スは死すべきもの」である．
LOGIC03 (3/17)
公理と定理
公理 (axiom)
正しいと考える前提
「異なった 2 点を通る直線はただ一つ存在する」
「平行線は交わらない」
定理 (theorem)
公理から推論規則を使って得られた命題
定理を導く推論の過程を証明 (proof) という
「3 角形の内角の和は 180 度である」
LOGIC03 (4/17)
形式論理体系
扱っている論理学を形式的に扱う体系
論理式の構文や操作に関する体系
公理と推論規則からなる
古典命題論理 (classical propositional logic) の形式体系
ヒルベルト (Hilbert) の体系
公理中心で推論規則はモーダスポネンスだけ
ゲンツェン (Gentzen) の自然演繹 (natural deduction) の体系
日常の推論に近いもの
NK 体系
ゲンツェンの sequent 計算の体系
形式的な表現にすぐれている
LK 体系
LOGIC03 (5/17)
LK の式
LK 体系では次の式 (sequent) を用いる
A1 , . . . , Am → B1 , . . . , Bn
直観的意味「A1 から Am を仮定すると B1 から Bn のどれかが導かれる」
m や n は 0 でもかまわない
→ B1 , . . . , Bn
仮定は必要ない
直観的意味「B1 から Bn のどれかが導かれる」
A1 , . . . , Am →
導くものがない
直観的意味「A1 から Am を仮定すると矛盾する」
→
仮定は必要がないのに，導くものがない
直観的意味「矛盾している」
LOGIC03 (6/17)
LK の公理と推論規則
LK 体系の公理: 始式 (initial sequent)
A→A
構造に関する推論規則
(weakening 左)
Γ→∆
A, Γ → ∆
(weakening 右)
Γ→∆
Γ → ∆, A
(contraction 左)
A, A, Γ → ∆
A, Γ → ∆
(contraction 右)
Γ → ∆, A, A
Γ → ∆, A
(exchange 左)
(cut)
Γ, A, B, Π → ∆
Γ, B, A, Π → ∆
(exchange 右)
Γ → ∆, A, B, Σ
Γ → ∆, B, A, Σ
Γ → ∆, A A, Π → Σ
Γ, Π → ∆, Σ
(Γ, ∆, Π, Σ は論理式の列)
LOGIC03 (7/17)
推論規則 (2)
論理結合子に関する推論規則
(∧ 左 1)
(∧ 右)
(∨ 右 1)
A, Γ → ∆
A ∧ B, Γ → ∆
Γ → ∆, A Γ → ∆, B
Γ → ∆, A ∧ B
Γ → ∆, A
Γ → ∆, A ∨ B
(∧ 左 2)
(∨ 左)
B, Γ → ∆
A ∧ B, Γ → ∆
A, Γ → ∆ B, Γ → ∆
A ∨ B, Γ → ∆
(∨ 右 2)
Γ → ∆, B
Γ → ∆, A ∨ B
(⊃ 左)
Γ → ∆, A B, Π → Σ
A ⊃ B, Γ, Π → ∆, Σ
(⊃ 右)
A, Γ → ∆, B
Γ → ∆, A ⊃ B
(¬ 左)
Γ → ∆, A
¬A, Γ → ∆
(¬ 右)
A, Γ → ∆
Γ → ∆, ¬A
命題定数に対する始式
→⊤
⊥→
LOGIC03 (8/17)
LK の証明図
LK の証明図 (proof figure)
始式から出発し，推論規則を次々に適用していく過程を記述したもの
証明図の一番下にある式を，その証明図の終式 (end sequent) という．
例: 証明図
A→A
→ A, ¬A
→ A, A ∨ ¬A
→ A ∨ ¬A, A
→ A ∨ ¬A, A ∨ ¬A
→ A ∨ ¬A
終式: → A ∨ ¬A
S を終式とする証明図が存在する時，S は LK で証明可能である (provable) という．
LOGIC03 (9/17)
推論の拡張
式の左端右端以外への推論規則の適用
exchange 規則を使うことで，適用させたい式を左端あるいは右
端に移動させることができる
どの位置の論理式に対しても，contraction, weakning, 論理結合
に関する推論規則を適用することができる
S1 , S2 , . . . , Sn から LK の推論規則を使って S を推論することができ
るとき，
S1
S2
···
Sn
S
上記推論は LK で導かれるという．
LOGIC03 (10/17)
式の構文的な意味
定理: 次の 3 つは同値である．
1. 式 A1 , . . . , Am → B1 , . . . , Bn が LK で証明可能である．
2. 式 A1 ∧ · · · ∧ Am → B1 ∨ · · · ∨ Bn が LK で証明可能である．
3. 論理式 A1 ∧ · · · ∧ Am ⊃ B1 ∨ · · · ∨ Bn が LK で証明可能である．
LOGIC03 (11/17)
練習問題 (1)
¬(A ∧ ¬B) → A ⊃ B の証明図を書きなさい．
LOGIC03 (12/17)
練習問題 (2)
A ⊃ B, A ⊃ ¬B → ¬A の証明図を書きなさい．
LOGIC03 (13/17)
練習問題 (3)
A ⊃ B → ¬(A ∧ ¬B) の証明図を書きなさい．
LOGIC03 (14/17)
練習問題 (4)
A → ¬¬A の証明図を書きなさい．
LOGIC03 (15/17)
練習問題 (5)
¬¬A → A の証明図を書きなさい．
LOGIC03 (16/17)
まとめ
推論
公理
定理
LK 体系
始式
LK 推論規則
証明
証明図
LOGIC03 (17/17)

Download Report