含意
含意(がんい、implication、IMP)、論理包含
「→」は「真→偽」のときのみ「偽」になる演算。含意という。
if P then Q
「→」は命題論理から使えるようになる
真理値表は下記のようになる。
$ \begin{array}{c|c|c} P & Q & P→Q \\ \hline \colorbox{#fcc}{T} & \colorbox{#fcc}{T} & \colorbox{#fcc}{T} \\ \colorbox{#fcc}{T} & F & F \\ F & \colorbox{#fcc}{T} & \colorbox{#fcc}{T} \\ F & F & \colorbox{#fcc}{T} \end{array}
$ P → Q は命題
$ P の位置に来るものは前件、$ Q の位置にくるものは後件と呼ばれる
$ T は真、$ F は偽
どうも含意≠伴意らしい
含意の導入則は
code:tex
\dfrac{
\begin{array}{c}
A \\
\vdots \\
B
\end{array}
}{A \to B} {\to}\text{Intro}
この形式は自然演繹の記法
Intro: introduction(導入)
$ [A] : $ [\quad] は仮定
含意の「→の除去規則」はモーダスポネンス
$ \frac{P \quad P \to Q}{Q}\to \text{Elim}
Elim: Elimination(除去)
$ (P \to Q) \iff ( \lnot P \lor Q)
$ (P \to Q) \iff ( P \land \lnot Q)
対応するもの
(論理) 含意
(集合) 関数集合(余域Bがサブシングルトンのとき)
(圏論) 内部Hom/冪対象?(余域Bが部分終対象のとき)
(型理論) 関数型(余域Bが命題/h-propositionのとき)
(ホモトピー論) 関数空間(余域Bがmere propositionのとき?)
確認用
Q. 含意
関連
論理的帰結、エンテイルメント
⊨
恒真式(トートロジー)
intro
参考
論理包含 - Wikipedia
峯島 宏次. 『一歩ずつマスターする論理学入門』. 2025. P50, P72