論理和の導入

論理和の導入(ろんりわのどうにゅう、英: Disjunction introduction)(選言導入則、$\lor$-導入則)は、命題論理の妥当性のある推論規則のひとつである。この規則を用いることによって、論理式の証明の中に新たに論理和(「$\lor$」)を加えることができる。もし「P」という命題が真であれば、「PまたはQ」という命題もまた真である、という推論規則である。例えば、「ソクラテスは人間である」という命題が真であれば、「ソクラテスが人間であるか、または豚が英仏海峡上空を編隊飛行している」という命題は真である。

この規則は、下記のように記述することができる。

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

ここで、命題「$P$」が証明のなかのどの行に出てきても、その後の行に「$P\lor Q$」を示すことができるものとされている。

論理和の導入の規則は、「矛盾からはあらゆることが導かれる」という爆発律を認めない矛盾許容論理の立場においては、他の論理的規則との組み合わせによっては認められないとする議論もある（矛盾許容論理におけるトレードオフを参照）。

形式的な記法

論理和の導入の推論規則は、シークエントの記法では、次のように表すことができる。

$P\vdash (P\lor Q)$

ここでは、「$\vdash$」は、ある論理の形式体系において、命題「$P\lor Q$」は命題「$P$」の論理的帰結であることを示す、メタ言語の記号である。

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

$P\to (P\lor Q)$

と表される。