論理積の消去

論理積の消去(ろんりせきのしょうきょ、テンプレート:Lang-en-short)(論理積の除去、連言除去則、$\wedge$-除去則は、命題論理における妥当性のある推論規則のひとつである。もし、「PかつQ」とい命題が真であれば、「P」という命題が真であり、同時に「Q」という命題も真であることを指す。この規則を用いることによって、論理積(「かつ」、「$\wedge$」)で結び付けられた命題の片方を抽出することができる。例えば、「雨が降っており、土砂降りである」という命題が真であれば、「雨が降っている」という命題は真である。この規則は、下記のように、

$\frac{P\wedge Q}{\therefore P}$

および、

$\frac{P\wedge Q}{\therefore Q}$

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

形式的な記法

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

$(P\wedge Q)⊢P$

および、

$(P\wedge Q)⊢Q$

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

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

$(P\wedge Q)\to P$

および、

$(P\wedge Q)\to Q$

と表される。