論理和の消去のソースを表示

'''論理和の消去'''(ろんりわのしょうきょ、{{lang-en-short|Disjunction elimination}})('''論理積の除去'''、'''選言削除則'''、'''<math>\lor</math>-除去則'''<ref>https://proofwiki.org/wiki/Rule_of_Or-Elimination</ref><ref>http://www.cs.gsu.edu/~cscskp/Automata/proofs/node6.html</ref>は、[[命題論理]]における[[妥当性]]のある[[推論規則]]のひとつである。この規則を用いることによって、[[論理式 (数学)|論理式]]の証明から[[論理和]]を削除することができる。もし命題「<math>P</math>」から命題「<math>Q</math>」が導き出され、かつ命題「<math>R</math>」からも命題「<math>Q</math>」が導き出されるとき、「<math>P</math>もしくは<math>R</math>」のいずれかが真である場合に、「<math>Q</math>」が真となるという[[推論規則]]である。PもしくはRのうち少なくとも一方が正しく、QであるためにはPとRのうちどちらかが正しければよいから、Qは正しい、ということである。例えば、下記の例が挙げられる。

:もし私が屋内にいれば、私は財布を持っている。
:もし私が屋外にいれば、私は財布を持っている。
:私は屋内にいるか、屋外にいるかのどちらかである。
:したがって、私は財布を持っている。

この規則は、下記のように記述することができる。

:<math>\frac{P \to Q, R \to Q, P \lor R}{\therefore Q}</math>

ここで、命題「<math>P \to Q</math>」、命題「<math>R \to Q</math>」、命題「<math>P \lor R</math>」が証明のなかのどの行に出てきても、その後の行において、 命題「<math>Q</math>」を示すことができるものとされている。

== 形式的な記法 ==
論理和の削除の推論規則は、[[シークエント]]の記法では、

: <math>(P \to Q), (R \to Q), (P \lor R) \vdash Q</math>

と表すことができる。ここで、「<math>\vdash</math>」は、ある論理の[[形式体系]]において、命題「<math>Q</math>」が、「<math>P \to Q</math>」・「<math>R \to Q</math>」・「<math>P \lor R</math>」の[[論理的帰結]]であることを表す、[[メタ言語]]の記号である。

この推論規則はまた、[[命題論理]]における[[真理関数]]の[[トートロジー]]もしくは[[定理]]として、

:<math>(((P \to Q) \land (R \to Q)) \land (P \lor R)) \to Q</math>

と表される。

==関連項目==
* [[論理和]]
* [[選言標準形]]

==参考文献==
{{Reflist}}

{{DEFAULTSORT:すいろんきそく}}
[[Category:推論規則|*]]
[[Category:命題論理の定理]]
[[Category:数学に関する記事]]