背理法、否定導入
前回分と分割しました
ここでは公理の除去に関する推論規則を定義していきます。
〇健全な研究室
さトぅー
「次は背理法をしよう」
天々城
「脱背理法なんていう人もいるが、背理法だって脱ぐと凄いんだぞ」
さトぅー
「ちょっと関心したけどそうじゃない」
エーリル
「そうじゃないんだ……」
■meta thm0.6
T∪{(￢φ)} |- ⊥
ならば
T |- φ
----------------------
さトぅー
「φと(￢φ)が一組でも公理Tに入ってたらなんでも言えるから、(￢φ)を取っちゃえばいいって感じかな」
エーリル
「マジで？」
----------------------
proof
1 (￢φ) [ax]
2 ⊥ [T∪{￢(φ)}の定理]
3 (￢(ψ⇒ψ)) [⊥el 2]
4 ((￢φ)⇒(￢(ψ⇒ψ))) [⇒in 3 el 1]
5 (((￢φ)⇒(￢(ψ⇒ψ)))⇒((ψ⇒ψ)⇒φ)) [Ax3]
6 ((ψ⇒ψ)⇒φ) [⇒el 4,5]
7 (ψ⇒ψ) [thm0.0]
8 φ [⇒el 7,6]
■
さトぅー
「T |- φ になったでしょ」
エーリル
「G0つよい」
さトぅー
「これも推論規則に追加する」
■RAA
(￢φ)
:
----
⊥
-----[RAA el (￢φ)]
φ
さトぅー
「これが背理法って呼ばれてるテクニック。
ただ実際は次のバージョンを使う方が便利」
■meta thm0.7
T∪{(￢φ)} |- ψ かつ T∪{(￢φ)} |- (￢ψ)
ならば
T |- φ
proof
1 (￢φ) [ax]
2 ψ [T∪{￢(φ)}の定理]
3 (￢ψ) [T∪{￢(φ)}の定理]
4 ⊥ [⊥in 2,3]
5 φ [RAA 4 el 1]
■
さトぅー
「推論規則を追加」
■￢el
(￢φ)
:
----
ψ (￢ψ)
---------[￢el el (￢φ)]
φ
天々城
「背理法使わないけどAx3使いますマンは矛盾の末に頭が爆発する」
さトぅー
「そういうのはいいから」
エーリル
「背理法の逆パターンみたいなのはないの？」
さトぅー
「あるよ」
■meta thm0.8
T∪{φ} |- ⊥
なら
T |- (￢φ)
proof
1 φ [ax]
2 ⊥ [T∪{φ}の定理]
3 (￢φ) [⊥el 2]
4 (φ⇒(￢φ)) [⇒in 3 el 1]
--------------
さトぅー
「今はT|- (φ⇒(￢φ))になった。
ここでTに(￢(￢φ))と(￢φ)を追加すると、矛盾して、さらに矛盾する」
--------------
5 (￢φ) [ax]
6 (￢(￢φ)) [ax]
7 φ [￢el 5,6 el 5]
8 (￢φ) [⇒el 7,4]
9 (￢φ) [￢el 7,8 el 6]
■
エーリル
「背理法の二連撃……だと！？」
さトぅー
「推論規則を追加しよう」
■raa
φ [ax]
---
:
:
---
⊥
------[raa el φ]
(￢φ)
さトぅー
「さっき￢elを何回か使ったでしょ。
これがRAAだったらどうなると思う？」
エーリル
「あーしてこうしてφと(￢φ)から⊥だから……。
そうか、⊥inからRAAの2回推論規則を使う流れになるのか。
￢elなら推論規則1回で進める」
天々城
「もう暗算できるのかよ。もしかして賢者なのでは？」
さトぅー
「RAAの方が都合がいい局面はあるけど、￢elはその1行分早い。
これはraaでも同じようなことが起こる」
■meta thm0.9
T∪{φ} |- ψ かつ T∪{φ} |- (￢ψ)
なら
T |- (￢φ)
proof
1 φ [ax]
2 ψ [T∪{φ}の定理]
3 (￢ψ) [T∪{φ}の定理]
4 ⊥ [⊥in 2,3]
5 (￢φ) [raa 4 el 1]
■
さトぅー
「推論規則を追加しよう」
■￢in
φ [ax]
---
:
:
---
ψ (￢ψ)
----------[￢in el φ]
(￢φ)
天々城
「￢inはあんまり話題にならないよなあ。背理法と混乱してませんかねえ」
さトぅー
「なんで私を見るのよ」
