¬¬((¬P⇒Q)∧(Q⇒P)⇒P)
$ ¬¬((¬α \implies β) ∧ (β \implies α) \implies α)
これ難しすぎるtakker.icon
解けるのか……?
Pに$ (¬α \implies β) ∧ (β \implies α)を、Qに$ \alphaを代入すれば$ \lnot\lnot((\lnot\alpha\implies\beta)\land(\beta\implies\alpha))\land\lnot\alphaを導ける
さらに¬¬(P∧Q)⇒¬¬P∧¬¬Qも使えば、$ \lnot\lnot(\lnot\alpha\implies\beta)\land\lnot\lnot(\beta\implies\alpha)\land\lnot\alphaとなるが……これは袋小路だ。 https://scrapbox.io/files/65e7f4413bc95600258481fb.svg
code:proof.tikz(tex)
\usepackage{fitch}
\usepackage{amsmath}
\begin{document}
$\Large\begin{nd}
\open
\hypo {h} {\lnot((\lnot P\implies Q)\land(Q\implies P)\implies P)}
\open
\hypo {1} {P}
\open
\hypo {2} {(\lnot P\implies Q)\land(Q\implies P)}
\have {3} {P} \r{1}
\close
\have {4} {(\lnot P\implies Q)\land(Q\implies P)\implies P} \ii{2-3}
\have {5} {\bot} \ne{h,4}
\close
\have {6} {\lnot P} \ii{1-5}
\open
\hypo {7} {(\lnot P\implies Q)\land(Q\implies P)}
\have {8} {\lnot P\implies Q} \ae{7}
\have {9} {Q} \ie{6,8}
\have {10} {Q\implies P} \ae{7}
\have {11} {P} \ie{9,10}
\close
\have {12} {(\lnot P\implies Q)\land(Q\implies P)\implies P} \ii{7-11}
\have {13} {\bot} \ne{h,12}
\close
\have {ee} {\lnot\lnot((\lnot P\implies Q)\land(Q\implies P)\implies P)} \ii{1-13}
\end{nd}$
\end{document}