直観主義論理での対偶

つまり、もう片方しか成立しない。

部分的にしか成立してない。

対偶の同値性は不成立である。

つまり、否定（¬）の導入のカタチなら可能。除去はできない。

proof.

code:bussproofs

\begin{prooftree}

\def\fCenter{\mbox{\ $\vdash$\ }}

\AxiomC{}

\RightLabel{(ID)}

\UnaryInfC{$P \fCenter P$}

\AxiomC{}

\RightLabel{(ID)}

\UnaryInfC{$Q \fCenter Q$}

\RightLabel{$({\rightarrow\vdash})$}

\BinaryInf$P, P \rightarrow Q \fCenter Q$

\RightLabel{$({\neg\vdash})$}

\UnaryInfC{$P, P \rightarrow Q, \neg Q \fCenter$}

\RightLabel{$({\vdash\neg})$}

\UnaryInfC{$P \rightarrow Q, \neg Q \fCenter \neg P$}

\RightLabel{$({\vdash\rightarrow})$}

\UnaryInfC{$P \rightarrow Q \fCenter \neg Q \rightarrow \neg P$}

\end{prooftree}

facts.

直観主義論理上で次は同値:

ref.

直観主義論理のための自然演繹 NJでは対偶法則が部分的にしか成立しない。