Questionnaire-2024/natural_deduction_propositional_logic/0069_sol.tex

This sequent is provable.

\begin{logicproof}{3}
  \begin{subproof}
    \neg ((p \imp q) \lor \neg q) & \assum\\
    \begin{subproof}
      p \imp q & \assum \\
      (p \imp q) \lor \neg q & $\ori{1} 3$ \\
      \bot & $\nege 3, 1 $
    \end{subproof}
    \neg (p \imp q) & $\negi 2-4 $ \\
    \begin{subproof}
      q & \assum \\
      \begin{subproof}
        p & \assum \\
        q & $\copying 6$
      \end{subproof}
      p \imp q & $\impi 7-8$ \\
      \bot & $\nege 9, 5$
    \end{subproof}
    \neg q & $\negi 6-10$ \\
    (p \imp q) \lor \neg q & $\ori 11$ \\
    \bot & $\nege 12, 1$
  \end{subproof}
  (p \imp q) \lor \neg q & $\PBC 1-13$
\end{logicproof}