a.k.a. 二重否定 (double negative)

二重否定の導入A\to\neg\neg Aは古典論理では無矛盾律\neg(A\land\neg A)に等しい

二重否定の除去\neg\neg A\to Aは古典論理では排中律A\lor\neg Aに等しい

de Morgan 雙對も否定の否定に關はる

否定を二種類考へる

否定 (負の樣相) :\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)

關聯論理の否定 : N + DNI + 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

精神分析で知的な exercise が行なはれる時。抑壓 (否定) を知る (否定) が、抑壓 (無意識 (Ubw)) は操作 (橫斷 (work through)) されない