¬¬P∧¬¬Q⇒¬¬(P∧Q)

二重否定除去がなくても成立することを以下に示す

$ \lnot\lnot P\land\lnot\lnot Q\implies\lnot(\lnot P\lor\lnot Q)

$ \implies \lnot\lnot\lnot(\lnot P\lor\lnot Q)

$ \implies\lnot\lnot(P\land Q)

$ \because\lnot\lnot\lnot(\lnot P\lor\lnot Q)\implies\lnot\lnot(P\land Q)

$ \underline{\therefore\lnot\lnot P\land\lnot\lnot Q\implies\lnot\lnot(P\land Q)\quad}_\blacksquare

他の定理を用いず、自然演繹だけで示す場合

https://scrapbox.io/files/65f29e206f631e00252e5ae0.svg

code:proof.tikz(tex)

\usepackage{fitch}

\usepackage{amsmath}

\begin{document}

$\Large\begin{nd}

\hypo {h1} {\lnot\lnot P\land\lnot\lnot Q}

\open

\hypo {h2} {\lnot(P\land Q)}

\open

\hypo {h3} {P}

\open

\hypo {h4} {Q}

\have {pq} {P\land Q} \ai{h3,h4}

\have {h4-1} {\bot} \ne{h2,pq}

\close

\have {h3-1} {\lnot Q} \ii{h4-{h4-1}}

\have {h3-2} {\lnot\lnot Q} \ae{h1}

\have {h3-3} {\bot} \ne{{h3-1},{h3-2}}

\close

\have {h2-1} {\lnot P} \ii{h3-{h3-3}}

\have {h2-2} {\lnot\lnot P} \ae{h1}

\have {h2-3} {\bot} \ne{{h2-1},{h2-2}}

\close

\have {h1-1} {\lnot\lnot(P\land Q)} \ii{h2-{h2-3}}

\end{nd}$

\end{document}