接続詞の除去

命題論理において、連言除去（and除去、∧除去^{[ 1 ]}または単純化とも呼ばれる）^{[ 2 ] [ 3 ] [ 4 ]}は、有効な即時推論、議論形式、および推論規則であり、連言AとBが真であれば、Aは真であり、Bも真であるという推論を行う。この規則により、連言の連言項の1つを単独で導出することで、より長い証明を短縮することが可能となる。

英語での例：

雨が降っている。しかも土砂降りだ。

だから雨が降っているのです。

この規則は2つの独立した副規則から構成されており、形式言語では次のように表現できます。

${\displaystyle {\frac {P\land Q}{\therefore P}}}$

そして

${\displaystyle {\frac {P\land Q}{\therefore Q}}}$

この2つのサブルールを合わせると、次のようになります。${\displaystyle P\land Q}$「」は証明の行に表示されます。${\displaystyle P}$" または "${\displaystyle Q}$「」は単独で次の行に置くことができます。上記の英語の例は、最初のサブルールを適用したものです。

連言消去の副規則は、シーケント記法で次のように記述できます。

${\displaystyle (P\land Q)\vdash P}$

そして

${\displaystyle (P\land Q)\vdash Q}$

どこ${\displaystyle \vdash }$はメタ論理的なシンボルであり、${\displaystyle P}$これは構文上の結果である${\displaystyle P\land Q}$そして${\displaystyle Q}$は、${\displaystyle P\land Q}$論理システムにおいて;

そして、真理関数的なトートロジーまたは命題論理の定理として表現される。

${\displaystyle (P\land Q)\to P}$

そして

${\displaystyle (P\land Q)\to Q}$

どこ${\displaystyle P}$そして${\displaystyle Q}$それらは何らかの形式体系で表現された命題である。