論理演算を導入する規則の次は、それを除去する規則を学びます。
推論規則 除去
定義
導入規則と対になる除去規則（elimination rules）がある（削除規則とも）。すなわち、複合型の命題を解体するものである。例えば、”A ∧ B true” から “A true” と “B true” を結論とすることができる。
$\frac{A \wedge B\hbox{ true}}{A\hbox{ true}}\ \wedge_{E1}
\qquad
\frac{A \wedge B\hbox{ true}}{B\hbox{ true}}\ \wedge_{E2}$
推論規則の適用例として、論理積の交換法則の例を示す。A ∧ B が真なら、B ∧ A も真である。その導出過程は、下にある推論の前提が前の推論の結論となるような記法で表される。
$\cfrac{\cfrac{A \wedge B\hbox{ true}}{B\hbox{ true}}\ \wedge_{E2}
\qquad
\cfrac{A \wedge B\hbox{ true}}{A\hbox{ true}}\ \wedge_{E1}}
{B \wedge A\hbox{ true}}\ \wedge_I$
ここまで述べてきた推論の手法では、含意の導入や論理和の除去といった規則を述べるのに十分ではない。そのためには、仮説的導出（hypothetical derivation）の一般的記法を必要とする。
「複合型の命題を解体するものである。」とあるように、除去は前提から論理演算記号を取り除き、新たに前提を作ってよいとする規則です。
A∧B
「AかつBである」
は
「Aである」と「Bである」
の二つに分解できます。
日常的な感覚なら「当たり前だろ」と感じますが、あくまでも新たな世界の規則を創る為です。いちいち決めます。
また、これ単体で見ると何がしたいのか理解できませんが、論理演算を積み重ね複雑化して演繹しようとした時にその威力を体感するのだと思います。
規則を決めておけば、人間の直観的な認識では理解できない規模や領域でも、それに従うことで意味は分からなくともとりあえず演繹できます。
∧（論理積）除去
上の引用の通り、A∧Bを分解し二つの前提を作ります。
$\frac{A \wedge B\hbox{ true}}{A\hbox{ true}}\ \wedge_{E1}
\qquad
\frac{A \wedge B\hbox{ true}}{B\hbox{ true}}\ \wedge_{E2}$
「AかつB」という一つの真の命題を「Aである」「Aである」にという二つの命題に分解できると取り決めています。
上記の引用にある通り、この推論規則はA∧Bのいずれかを命題として抜き出し、順番を入れ替えた後で再び論理積結合の定義を適用してB∧Aに演繹できます。交換法則です。
→（含意）除去
含意除去も含意導入と同様です。
前提の命題からA→Bを演繹できたなら、AとBを除去して、新たにBという前提命題に変換して演繹して良いよってことですね。
$\begin{gather} A \\ \vdots \\B \\ \vdots \\ \frac{A \to B}{B}\wedge_E \end{gather}$
「『AならばB』ならばB」を「Bである」に変形できることを定義しているので、日本語にすると意味不明ですが、演繹図を用いて推論するとその威力が理解できます。
$\frac{A \to A}{A}\ \wedge_{E}$
除去推論規則を用いればA→Aという同語反復を、含意と前件を排除した命題Aだけに変形できます。
つまり、「AならばAである」は「Aである」と論理的に変換でき、同値であると言えるわけです。
コメント