否定の否定
a.k.a. 二重否定 (double negative)
二重否定の導入$ A\to\neg\neg Aは古典論理では無矛盾律$ \neg(A\land\neg A)に等しい 二重否定の除去$ \neg\neg A\to Aは古典論理では排中律$ A\lor\neg Aに等しい 否定を二種類考へる
否定 (負の樣相) :$ \frac{p\Vdash q}{\neg q\Vdash \neg p}
不可能 (impossible) :$ \frac{p\Vdash\blacksquare q}{\blacksquare q\Vdash p}
眞理否保存。否立證
$ A\to\blacksquare_>B\iff B\to\blacksquare_< A.
Kripke frame$ (W,\le)に對して兩立性 (compatibility)$ C\subseteq W\times Wを、$ xCy且つ$ x'\le x且つ$ y'\le yならば$ x'Cy'で定める 否兩立 (non-compatible)
$ x\vDash\blacksquare_> p:=\forall y(xCy\implies y\cancel\Vdash p).
$ x\vDash\blacksquare_< p:=\forall y(yCx\implies y\cancel\Vdash p).
maximum compatible
否定
直觀主義論理の否定 : N + DNI + Con + LNC 古典論理の否定 : N + DNI + Con + LNC + (LEM or DNE) 否必然 (unnecessity) :$ \frac{\blacklozenge p\Vdash q}{q\Vdash\blacklozenge p}
反例。反證
$ \blacklozenge_>A\to B\iff\blacklozenge_<B\to A.
Kripke frame$ (W,\le)に對して網羅性 (exhaustiveness)$ E\subseteq W\times Wを、$ xEy且つ$ x\le x'且つ$ y\le y'ならば$ x'Ey'で定める 否網羅 (non-exhaustive)
$ x\vDash\blacklozenge_>p\iff\exist y(xEy\&y\cancel\Vdash p).
$ x\vDash\blacklozenge_<p\iff\exist y(yEx\&y\cancel\Vdash p).
minimum exhaustive
$ \blacksquare A\to\blacklozenge A\iff\forall x,y,z(xCy\&(xEz\implies x\le z)).
$ \blacklozenge A\to\blacksquare A\iff\forall x\exist y(xCy\&xEy).
正の樣相 :$ \frac{p\Vdash q}{*p\Vdash*q}
必然 :$ \square p\iff\blacksquare\blacklozenge p
可能 :$ \Diamond p\iff\blacklozenge\blacksquare p
現實 :$ p