接続詞の除去

Inference rule in logic

接続詞の除去

タイプ	推論の規則
分野	命題計算
声明	接続詞とが真であれば、は真であり、は真です。 ${\displaystyle A}$ ${\displaystyle B}$ ${\displaystyle A}$ ${\displaystyle B}$
象徴的な声明	${\displaystyle {\frac {P\land Q}{\therefore P}},{\frac {P\land Q}{\therefore Q}}}$ ${\displaystyle (P\land Q)\vdash P,(P\land Q)\vdash Q}$ ${\displaystyle (P\land Q)\to P,(P\land Q)\to Q}$

命題論理において、連言消去（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}$

参考文献

1. David A. Duffy (1991). 『自動定理証明の原理』ニューヨーク: Wiley.セクション3.1.2.1、p.46
2. CopiとCohen ^[要出典]
3. ムーアとパーカー^[要出典]
4. ハーレー^[要出典]

Retrieved from "https://en.wikipedia.org/w/index.php?title=Conjunction_elimination&oldid=1314850935"