論理積の消去(ろんりせきのしょうきょ、英: Conjunction elimination)(論理積の除去、連言除去則、 ∧ {\displaystyle \land } -除去則[1][2][3][4]は、命題論理における妥当性のある推論規則のひとつである。もし、「PかつQ」とい命題が真であれば、「P」という命題が真であり、同時に「Q」という命題も真であることを指す。この規則を用いることによって、論理積(「かつ」、「 ∧ {\displaystyle \land } 」)で結び付けられた命題の片方を抽出することができる。例えば、「雨が降っており、土砂降りである」という命題が真であれば、「雨が降っている」という命題は真である。この規則は、下記のように、 P ∧ Q ∴ P {\displaystyle {\frac {P\land Q}{\therefore P}}}

および、 P ∧ Q ∴ Q {\displaystyle {\frac {P\land Q}{\therefore Q}}}

の２つの記述をすることができる。ここで、命題「 P ∧ Q {\displaystyle P\land Q} 」が証明のなかのどの行に出てきても、その後の行において、命題「 P {\displaystyle P} 」もしくは命題「 Q {\displaystyle Q} 」を示すことができるものとされている。
形式的な記法

論理積の消去の推論規則は、シークエント記法では、 ( P ∧ Q ) ⊢ P {\displaystyle (P\land Q)\vdash P}

および、 ( P ∧ Q ) ⊢ Q {\displaystyle (P\land Q)\vdash Q}

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

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

および、 ( P ∧ Q ) → Q {\displaystyle (P\land Q)\to Q}

と表される。
脚注^ David A. Duffy (1991). Principles of Automated Theorem Proving. New York: Wiley  Sect.3.1.2.1, p.46
^ Copi and Cohen
^ Moore and Parker
^ Hurley