読者です 読者をやめる 読者になる 読者になる

選言から連言へ

ちょっとした経緯があり,NK,LKにおけるド・モルガン則の証明の作成手順を述べます.

ド・モルガン則は,¬(〇*□)⇔(●・■)の形の定理(〇は●の否定,■は■の否定,*,・の一方は,∨他方は∧)であり,証明は¬(〇*□)⊢(●・■)と(●・■)⊢¬(〇*□)とから成ります.

¬(〇∨□)⊢(●∧■)は,そのまま(●∧■)を展開.
¬(〇∧□)⊢(●∨■)は,背理法で¬(〇∧□),¬(●∨■)⊢⊥,¬の消去で¬(●∨■)⊢(〇∧□)に,
(●∧■)⊢¬(〇∨□)は,¬の導入で(●∧■),(〇∨□)⊢⊥として,(〇∨□)を展開,
(●∨■)⊢¬(〇∧□)は,¬の導入で(●∨■),(〇∧□)⊢⊥として,(●∨■)を展開

述語論理でも

¬∃○⊢∀●は,そのまま∀●の束縛変数をスコーレム定数に,
¬∀○⊢∃●は,背理法で¬∀○,¬∃●⊢⊥,¬の消去で¬∃●⊢∀○に,
∃○⊢¬∀●は,¬の導入で∃○,∀●⊢⊥として,∃○の束縛変数をスコーレム定数に,
∀○⊢¬∃●は,¬の導入で∀○,∃●⊢⊥として,∃●の束縛変数をスコーレム定数に

のように,選言は仮定にチャージ,連言は結論にディスチャージして,展開/束縛を高階化すればよく,LKでは更に簡潔で,対辺に移し¬を消去,仮定に集まるなら選言,特称から,結論に集まるなら連言,全称から展開すればよい.