¬(P∧Q)⇒¬¬(¬P∨¬Q)
証明
proof.tikz(tex)\usepackage{fitch}
\usepackage{amsmath}
\begin{document}
$\Large\begin{nd}
\hypo {h1} {\lnot(P\land Q)}
\open
\hypo {h2} {\lnot(\lnot P\lor\lnot Q)}
\open
\hypo {h3} {P}
\open
\hypo {h4} {Q}
\have {pq} {P\land Q} \ai{h3,h4}
\have {h4-1} {\bot} \ie{h1,pq}
\close
\have {h3-1} {\lnot Q} \ii{h4-{h4-1}}
\have {h3-2} {\lnot P\lor\lnot Q} \oi{{h3-1}}
\have {h3-3} {\bot} \ie{h2,{h3-2}}
\close
\have {h2-1} {\lnot P} \ii{h3-{h3-3}}
\have {h2-2} {\lnot P\lor\lnot Q} \oi{{h2-1}}
\have {h2-3} {\bot} \ie{h2,{h2-2}}
\close
\have {h1-1} {\lnot\lnot(\lnot P\lor\lnot Q)} \ii{h2-{h2-3}}
\end{nd}$
\end{document}
ログ
全然思いつかん

また今度考えるか
そもそもこれは二重否定除去なしで証明できるのか?
この式、二重否定除去より弱いけど二重否定除去なしには導けない式になっていそう?
Thanks,

!