¬(P∧Q)⇒¬¬(¬P∨¬Q)
¬(P∧Q)⇒¬P∨¬Qを直観主義論理でも成り立つように弱めたもの
証明
https://scrapbox.io/files/6614ac71d8672d0025bae255.svg
code: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}
ログ
https://kakeru.app/18c467c0133750fc66df30781837031c https://i.kakeru.app/18c467c0133750fc66df30781837031c.svg
¬(P∧Q)⇒¬¬(¬P∨¬Q)を二重否定除去なしに証明するのが非常に難しい
全然思いつかんtakker.icon
また今度考えるか
そもそもこれは二重否定除去なしで証明できるのか？
証明不可能性は、¬(P∧Q)⇒¬¬(¬P∨¬Q)から二重否定除去を導ければ証明できるが……
https://kakeru.app/b0b876c3c741651f4582a8deac5a7bd4 https://i.kakeru.app/b0b876c3c741651f4582a8deac5a7bd4.svg
¬¬P∧¬¬Q⇒¬¬(P∧Q)を二重否定除去なしに示せるかどうかに帰着できた
この式、二重否定除去より弱いけど二重否定除去なしには導けない式になっていそう？
井戸端で問いかけてみた/villagepump/2021/11/18#619635bc1280f00000975811
2021-11-21 11:08:52 直観主義論理だけで導けた！！！/villagepump/連言と二重否定の関係について#61997d116668720000a7aea9
Thanks, /public-minaph/yuki_minoh.icon！
https://kakeru.app/18c467c0133750fc66df30781837031c https://i.kakeru.app/18c467c0133750fc66df30781837031c.svg
弱排中律を使う必要がある？
#2024-04-09 11:47:55 neをieに変更
#2024-01-28 14:26:12
#2021-11-29 17:03:39
#2021-11-18 20:16:54
#2021-11-21 11:19:17