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

'''論理積の消去'''(ろんりせきのしょうきょ、{{lang-en-short|Conjunction elimination}})('''論理積の除去'''、'''連言除去則'''、'''<math>\land</math>-除去則'''<ref>{{cite book | author=David A. Duffy | title=Principles of Automated Theorem Proving | location=New York | publisher=Wiley | year=1991 }} Sect.3.1.2.1, p.46</ref><ref>Copi and Cohen</ref><ref>Moore and Parker</ref><ref>Hurley</ref>は、[[命題論理]]における[[妥当性]]のある[[推論規則]]のひとつである。もし、「PかつQ」とい[[命題]]が真であれば、「P」という命題が真であり、同時に「Q」という命題も真であることを指す。この規則を用いることによって、[[論理積]](「かつ」、「<math>\land</math>」)で結び付けられた命題の片方を抽出することができる。例えば、「雨が降っており、土砂降りである」という命題が真であれば、「雨が降っている」という命題は真である。この規則は、下記のように、

:<math>\frac{P \land Q}{\therefore P}</math>

および、

:<math>\frac{P \land Q}{\therefore Q}</math>

の２つの記述をすることができる。ここで、命題「<math>P \land Q</math>」が証明のなかのどの行に出てきても、その後の行において、命題「<math>P</math>」もしくは命題「<math>Q</math>」を示すことができるものとされている。

== 形式的な記法 ==

論理積の消去の推論規則は、[[シークエント]]記法では、

: <math>(P \land Q) \vdash P</math>

および、

: <math>(P \land Q) \vdash Q</math>

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

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

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

および、

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

と表される。

== 脚注 ==
{{reflist}}

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

[[sv:Matematiskt uttryck#Förenkling]]