論理和の消去(ろんりわのしょうきょ、英: Disjunction elimination)(論理積の除去、選言削除則、 ∨ {\displaystyle \lor } -除去則[1][2]は、命題論理における妥当性のある推論規則のひとつである。この規則を用いることによって、論理式の証明から論理和を削除することができる。もし命題「 P {\displaystyle P} 」から命題「 Q {\displaystyle Q} 」が導き出され、かつ命題「 R {\displaystyle R} 」からも命題「 Q {\displaystyle Q} 」が導き出されるとき、「 P {\displaystyle P} もしくは R {\displaystyle R} 」のいずれかが真である場合に、「 Q {\displaystyle Q} 」が真となるという推論規則である。PもしくはRのうち少なくとも一方が正しく、QであるためにはPとRのうちどちらかが正しければよいから、Qは正しい、ということである。例えば、下記の例が挙げられる。もし私が屋内にいれば、私は財布を持っている。もし私が屋外にいれば、私は財布を持っている。私は屋内にいるか、屋外にいるかのどちらかである。したがって、私は財布を持っている。

この規則は、下記のように記述することができる。 P → Q , R → Q , P ∨ R ∴ Q {\displaystyle {\frac {P\to Q,R\to Q,P\lor R}{\therefore Q}}}

ここで、命題「 P → Q {\displaystyle P\to Q} 」、命題「 R → Q {\displaystyle R\to Q} 」、命題「 P ∨ R {\displaystyle P\lor R} 」が証明のなかのどの行に出てきても、その後の行において、 命題「 Q {\displaystyle Q} 」を示すことができるものとされている。
形式的な記法

論理和の削除の推論規則は、シークエントの記法では、 ( P → Q ) , ( R → Q ) , ( P ∨ R ) ⊢ Q {\displaystyle (P\to Q),(R\to Q),(P\lor R)\vdash Q}

と表すことができる。ここで、「 ⊢ {\displaystyle \vdash } 」は、ある論理の形式体系において、命題「 Q {\displaystyle Q} 」が、「 P → Q {\displaystyle P\to Q} 」・「 R → Q {\displaystyle R\to Q} 」・「 P ∨ R {\displaystyle P\lor R} 」の論理的帰結であることを表す、メタ言語の記号である。

この推論規則はまた、命題論理における真理関数のトートロジーもしくは定理として、 ( ( ( P → Q ) ∧ ( R → Q ) ) ∧ ( P ∨ R ) ) → Q {\displaystyle (((P\to Q)\land (R\to Q))\land (P\lor R))\to Q}

と表される。
関連項目

論理和

選言標準形

参考文献^ https://proofwiki.org/wiki/Rule_of_Or-Elimination
^ ⇒http://www.cs.gsu.edu/~cscskp/Automata/proofs/node6.html