∧
さトぅー
「新しい記号を作る」
エーリル
「記号を作る。言語感があっていい」
さトぅー
「今までも何回かあったけど、こういうときは既にある記号の組み合わせで記号を追加する。
これを定義と呼ぶんだったわね」
■∧の定義
(φ∧ψ) :⇔ (￢(φ⇒(￢ψ)))
さトぅー
「∧を定義したけど、これが自然言語の"かつ"のような機能をしてくれる」
エーリル
「ホントに？ 信じられないんだけど」
さトぅー
「まあ見てて」
■thm0.2
{φ,ψ} |- (φ∧ψ)
proof
1 φ [ax]
2 (φ⇒(￢ψ)) [ax]
3 (￢ψ) [⇒el 1,2]
4 ψ [ax]
5 (￢(φ⇒(￢ψ))) [￢in 4,3 el 2]
6 (φ∧ψ) [def∧ in 5]
■
さトぅー
「推論規則を追加しよう」
■∧in
φ ψ
--------[∧in]
(φ∧ψ)
エーリル
「あ、これはわかりやすい」
天々城
「『エーリルはエルフ』と『エーリルは賢者』ってわかったら『エーリルはエルフで、エーリルは賢者』っていえるからナ」
さトぅー
「道具はそろってるからどんどんいくよ」
■thm0.3
{(φ∧ψ)} |- ψ
proof
1 (φ∧ψ) [ax]
2 (￢(φ⇒(￢ψ))) [def∧ el 1]
3 (￢ψ) [ax]
4 (φ⇒(￢ψ)) [⇒in 3]
5 ψ [￢el 4,3 el 3]
■
さトぅー
「推論規則を追加しよう」
■∧elL
(φ∧ψ)
---------[∧elL]
ψ
さトぅー
「これで∧の左側の論理式を消せる。
右側の論理式も一緒」
■thm0.4
{(φ∧ψ)} |- φ
proof
1 (φ∧ψ) [ax]
2 (￢(φ⇒(￢ψ))) [def∧ el 1]
3 (￢φ) [ax]
4 ((￢(￢ψ))⇒(￢φ)) [⇒in 3]
5 (((￢(￢ψ))⇒(￢φ))⇒(φ⇒(￢ψ))) [Ax3]
6 (φ⇒(￢ψ)) [⇒el 4,5]
7 φ [￢el 6,2 el 3]
■
さトぅー
「推論規則を追加しよう」
■∧elR
(φ∧ψ)
--------[∧elR]
φ
天々城
「『エーリルはエルフで、エーリルは賢者』ってわかったら『エーリルはエルフ』も『エーリルは賢者』もいえるからナ」
エーリル
「ホントに∧は『かつ』だった……」
