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

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

code:proof.tikz(tex)

\usepackage{fitch}

\usepackage{amsmath}

\begin{document}

$\Large\begin{nd}

\hypo {h} {\lnot P\lor P}

\open

\hypo {np} {\lnot P}

\open

\hypo {np-p} {P}

\have {np-b} {\bot} \ne{np,{np-p}}

\have {np-q} {Q} \be{{np-b}}

\close

\have {pq} {P\implies Q} \ii{{np-p}-{np-q}}

\have {d1} {(P\implies Q)\lor(Q\implies P)} \oi{pq}

\close

\open

\hypo {p} {P}

\open

\hypo {p-q} {Q}

\have {p-p} {P} \r{p}

\close

\have {qp} {Q\implies P} \ii{{p-q}-{p-p}}

\have {d2} {(P\implies Q)\lor(Q\implies P)} \oi{qp}

\close

\have {d} {(P\implies Q)\lor(Q\implies P)} \oe{h,np-d1,p-d2}

\end{nd}$

\end{document}