∨
○健全な研究室
さトぅー
「もう一つ記号を追加」
■∨の定義
(φ∨ψ) :⇔ ((￢φ)⇒ψ)
さトぅー
「これは自然言語だと『または』のような機能をしてくれる」
エーリル
「∧のときもそうだったけど、元の論理式からは全然そんな雰囲気しないのよね」
■thm0.5
{φ} |- (φ∨ψ)
proof
1 φ [ax]
2 (￢φ) [ax]
3 ψ [explosion 1,2]
4 ((￢φ)⇒ψ) [⇒in 3 el 2]
5 (φ∨ψ) [def∨ in 4]
■
さトぅー
「推論規則を追加しよう」
■∨inR
φ
--------[∨inR]
(φ∨ψ)
エーリル
「あれ、∧と似てない？」
さトぅー
「そうね。それに左側でも似たようなことが起きる」
■thm0.6
{ψ} |- (φ∨ψ)
proof
1 ψ [ax]
2 ((￢φ)⇒ψ) [⇒in 1]
3 (φ∨ψ) [def∨ in 2]
■
さトぅー
「推論規則を追加しよう」
■∨inL
ψ
--------[∨inL]
(φ∨ψ)
天々城
「さトぅーさんが推論規則追加マシーンになっている……」
さトぅー
「これ以外にどうしろっていうのよ」
エーリル
「∨も自然言語の『または』に似てますね」
天々城
「『エーリルはエルフ』だったら『エーリルはエルフか、エーリルは人間』っていえるからナ」
エーリル
「一瞬戸惑ったけど、確かに合ってる。
この流れだと∨elもあるの？」
さトぅー
「ある。ちょっと難しいけど」
■thm0.7
{(φ∨ψ),(φ⇒ρ),(ψ⇒ρ)} |- ρ
proof
1 ￢ρ [ax]
2 (φ∨ψ) [ax]
3 ((￢φ)⇒ψ) [def∨ el 2]
4 (￢φ) [ax]
5 ψ [⇒el 4,3]
6 (ψ⇒ρ) [ax]
7 ρ [⇒el 5,6]
8 φ [￢el 7,1 el 4]
9 (φ⇒ρ) [ax]
10 ρ [⇒el 8,9]
11 ρ [￢el 10,1 el 1]
■
さトぅー
「推論規則を追加しよう」
■∨el
(φ∨ψ) (φ⇒ρ) (ψ⇒ρ)
---------------------------[∨el]
ρ
エーリル
「証明がテクニカルで変な笑い出た」
さトぅー
「私も初めて証明できたときは嬉しさで変なポーズをした覚えがある。
背理法2回使ってるし、実際テクニカルよね」
エーリル
「でもこれ、自然言語の『または』っぽく感じない……」
天々城
「場合分けだナ。
『エーリルが賢者エルフならエーリルはエルフで、エーリルの耳が長くてもエーリルはエルフといえた。
そしたら、エーリルが賢者エルフまたはエーリルの耳が長いなら、エーリルはエルフといえる」
エーリル
「今のでわかった」
さトぅー
「これで一仕事終えた感じがする」
天々城
「いや、まだアレをやってない」
