対偶
\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)