(¬P∨Q)⇒(P⇒Q)
証明
方針
矛盾からは何でも導ける(⊥除去)ことと、正しい命題に仮定を追加しても正しいことを使う https://scrapbox.io/files/65f29c0c9045b5002522c8bb.svg
code:proof.tikz(tex)
\usepackage{fitch}
\usepackage{amsmath}
\begin{document}
$\Large\begin{nd}
\hypo {1} {\lnot P\lor Q}
\open
\hypo {2l} {\lnot P}
\open
\hypo {3l} { P}
\have {4l}{\bot} \ne{2l,3l}
\have {5l}{Q} \be{4l}
\close
\have {6l} {P\implies Q} \ii{3l-5l}
\close
\open
\hypo {2r} {Q}
\open
\hypo {3r} {P}
\have {4r} {Q} \r{2r}
\close
\have {5r} {P\implies Q} \ii{3r-4r}
\close
\have {7} {P\implies Q} \oe{1,2l-6l,2r-5r}
\end{nd}$
\end{document}