二重否定

二重否定導入規則は、シーケント記法で次のように記述できます。

${\displaystyle P\vdash \neg \neg P}$

二重否定除去規則は次のように記述できます。

${\displaystyle \neg \neg P\vdash P}$

ルール形式で：

${\displaystyle {\frac {P}{\neg \neg P}}}$

そして

${\displaystyle {\frac {\neg \neg P}{P}}}$

またはトートロジー（単純な命題論理の文）として：

${\displaystyle P\to \neg \neg P}$

そして

${\displaystyle \neg \neg P\to P}$

これらは単一の双条件式にまとめることができます。

${\displaystyle \neg \neg P\leftrightarrow P}$。

双条件性は同値関係であるため、整形式論理式中の¬¬ Aの任意のインスタンスをAに置き換えても、整形式論理式の真理値は変わりません。

二重否定の除去は古典論理の定理ですが、直観主義論理や最小論理のような弱い論理の定理ではありません。二重否定の導入は直観主義論理と最小論理の両方の定理です。${\displaystyle \neg \neg \neg A\vdash \neg A}$。

構成的な性質を持つため、「雨が降っていないというわけではない」という文は、 「雨が降っている」という文よりも弱い。後者は雨が降っていることの証明を必要とするのに対し、前者は雨が降っていることが矛盾しないという証明だけを必要とする。この区別は、自然言語においても緩叙法という形で現れる。

命題論理のヒルベルト型演繹体系では、二重否定は必ずしも公理として扱われるわけではなく（ヒルベルト体系の一覧を参照）、むしろ定理として扱われます。ここでは、ヤン・ルカシェヴィチが提案した3つの公理体系におけるこの定理の証明について説明します。

A1.${\displaystyle \phi \to \left(\psi \to \phi \right)}$

A2。${\displaystyle \left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)}$

A3。${\displaystyle \left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)}$

補題を使用する${\displaystyle p\to p}$ここで証明されている(L1)と呼び、ここで証明されている次の追加の補題を使用します。

(L2)${\displaystyle p\to ((p\to q)\to q)}$

まず証明します${\displaystyle \neg \neg p\to p}$簡潔にするため、${\displaystyle q\to (r\to q)}$φ ₀によって。また、いくつかの証明ステップの簡略化として、仮言三段論法メタ定理の方法を繰り返し使用します。

（１）$\displaystyle \varphi _{0}}$   （（A1）のインスタンス）

（２）${\displaystyle (\neg \neg \varphi _{0}\to \neg \neg p)\to (\neg p\to \neg \varphi _{0})}$   （（A3）のインスタンス）

（３）${\displaystyle (\neg p\to \neg \varphi _{0})\to (\varphi _{0}\to p)}$   （（A3）のインスタンス）

（４）${\displaystyle (\neg \neg \varphi _{0}\to \neg \neg p)\to (\varphi _{0}\to p)}$   （（２）と（３）より仮言三段論法メタ定理による）

（５）${\displaystyle \neg \neg p\to (\neg \neg \varphi _{0}\to \neg \neg p)}$   （（A1）のインスタンス）

（６）${\displaystyle \neg \neg p\to (\varphi _{0}\to p)}$   （（４）と（５）より仮言三段論法メタ定理による）

（７）${\displaystyle \varphi _{0}\to ((\varphi _{0}\to p)\to p)}$   (L2 のインスタンス)

（８）${\displaystyle (\varphi _{0}\to p)\to p}$   （（１）と（７）よりモーダス・ポネンスによる）

（9）${\displaystyle \neg \neg p\to p}$   （（６）と（８）より仮言三段論法メタ定理による）

ここで証明します${\displaystyle p\to \neg \neg p}$。

（１）${\displaystyle \neg \neg \neg p\to \neg p}$   （先ほど証明した定理の最初の部分の具体例）

（２）${\displaystyle (\neg \neg \neg p\to \neg p)\to (p\to \neg \neg p)}$   （（A3）のインスタンス）

（３）${\displaystyle p\to \neg \neg p}$   （（１）と（２）よりモーダス・ポネンスによる）

これで証明は完了です。