論理否定 - pogi-log

論理否定

論理否定(Logical not)、否定(negation)

論理演算のひとつ

$ \lnot P , $ P \to \bot

$ \to は含意

⊥には0割り当てるときもある

$ \lnot P \equiv P \to 0

真理値表

$ \begin{array}{c|c} P & \lnot P \\ \hline \colorbox{#fcc}{T} & F \\ F & \colorbox{#fcc}{T} \end{array}

$ \lnot P は$ P \to \bot と見ることができる

$ \to は含意

BHK解釈あたりの見方？

→の導入規則、→導入

code:tex

\dfrac{

\begin{array}{c}

A \\

\vdots \\

\bot

\end{array}

}{\lnot A} {\to}\text{Intro}

$ [A] : $ [\quad] は仮定

→の除去規則、→除去

$ \frac{A \quad \lnot A }{\bot}\to \text{Elim}