対偶 - くたくたじゅうよん

対偶

$ \lnot B\implies \lnot Aを「$ A\implies Bの対偶」と呼ぶ

古典論理の推論規則では両者が常に同値になる

$ (A\implies B)\iff(\lnot B\implies \lnot A)

このAとAの対偶とが同値になる性質は便利なので、証明でよく使われる

しかし以下に示すように、直観主義論理だと否定を被せる方向にしか成立しない

$ (R)\implies(L)

$ (\lnot P\implies\lnot Q)\implies(\lnot\lnot Q\implies\lnot\lnot P)に二重否定除去を使えば題意を得る

この証明には必ず二重否定除去を使わざるを得ない

集合論での表示

$ A\subseteq B\iff(U\setminus B)\subseteq(U\setminus A)