(P⇒Q)⇒¬¬(¬P∨Q)

証明

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

https://kakeru.app/6b009bc74c35fb54be6ea38fb20f7dde https://i.kakeru.app/6b009bc74c35fb54be6ea38fb20f7dde.svg

3-6を一番下に持って行けば、もう少し短く書けるな

後で直すか

code:proof.tikz(tex)

\usepackage{fitch}

\usepackage{amsmath}

\begin{document}

$\Large\begin{nd}

\hypo {1} {P\implies Q}

\open

\hypo {h} {\lnot(\lnot P\lor Q)}

\open

\hypo {p} {P}

\have {p2} {Q} \ie{1,p}

\have {p3} {\lnot P\lor Q} \oi{p2}

\have {p4} {\bot} \ne{h,p3}

\close

\have {np} {\lnot P} \ii{p-p4}

\have {pq} {\lnot P\lor Q} \oi{np}

\have {b} {\bot} \ne{h,pq}

\close

\have {qed} {\lnot\lnot(\lnot P\lor Q)} \ii{h-b}

\end{nd}$

\end{document}