仮説的導出と論理和の除去

A∨B⇔B∨A
に繋がりそうな考え方を学んでいきます。

仮説的導出と論理和の除去

【仮説的導出】
数理論理学での一般的操作として、「仮定からの推論; reasoning from assumptions」がある。例として、次のような演繹過程を見てみよう。
$\cfrac{A \wedge \left ( B \wedge C \right ) \ true}{\cfrac{B \wedge C \ true}{B \ true} \wedge E_1} \wedge E_2$

このような導出によって B が真であることが確定するわけではないが、次のような事実は確定する。

もし A ∧ (B ∧ C) が真なら B は真である。

Wikipedia

A ∧ (B ∧ C)
この論理式は8通りの命題変数の組み合わせが考えられますが、論理式全体が真となると仮定した場合、推論規則∧除去規則により、Bが真であることが導出できます。Aが真、Cが真も当然導出法されます。

論理和除去

仮説的導出を使うと、論理和の除去規則を書くことができる。

$\cfrac{
A \vee B \hbox{ true}
\quad
\begin{matrix}
\cfrac{}{A \ true} u \
\vdots \
C \ true
\end{matrix}
\quad
\begin{matrix}
\cfrac{}{B \ true} w \
\vdots \
C \ true
\end{matrix}
}{C \ true} \vee E^{u,w}$

これを説明すると、A ∨ B が真で、A true と B true それぞれから C true が導かれるなら、C は必ず真となる。ここで、A true や B true を保証しているわけではないことに注意されたい。

Wikipedia

A→C,B→Cが真ならA∨Bが真の時、Cが導出できます。

1.A∨B,A→C,B→C(仮定)
2.C(→除去,∨除去)

論理和除去の演繹はこんな感じかなと。