generated at
¬¬P∧¬¬Q⇒¬¬(P∧Q)
\lnot\lnot P\land\lnot\lnot Q\implies\lnot\lnot(P\land 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

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



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}

#2024-03-14 15:49:54
#2024-01-28 14:19:01