選言から連言へ

ちょっとした経緯があり，ＮＫ，ＬＫにおけるド・モルガン則の証明の作成手順を述べます．

ド・モルガン則は，¬（〇＊□）⇔（●・■）の形の定理（〇は●の否定，■は■の否定，＊，・の一方は，∨他方は∧）であり，証明は¬（〇＊□）⊢（●・■）と（●・■）⊢¬（〇＊□）とから成ります．

¬（〇∨□）⊢（●∧■）は，そのまま（●∧■）を展開．
¬（〇∧□）⊢（●∨■）は，背理法で¬（〇∧□），¬（●∨■）⊢⊥，¬¬の消去で¬（●∨■）⊢（〇∧□）に，
（●∧■）⊢¬（〇∨□）は，¬の導入で（●∧■），（〇∨□）⊢⊥として，（〇∨□）を展開，
（●∨■）⊢¬（〇∧□）は，¬の導入で（●∨■），（〇∧□）⊢⊥として，（●∨■）を展開

述語論理でも

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

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