Questionnaire-2024/natural_deduction_propositional_logic/0012_sol.tex

This sequent is provable.

\begin{logicproof}{3}
    \begin{subproof}
        (p \imp q) \imp p & \assum \\
        \begin{subproof}
            \lnot p & \assum \\
            \lnot (p \imp q) & $\MT 1,2$ \\
            \begin{subproof}
                p & \assum \\
                \bot & $\nege 2,4$ \\
                q & $\bote 5$
            \end{subproof}
            p \imp q & $\impi 4-6$ \\
            \bot & $\nege 3,7$
        \end{subproof}
        p & $\PBC 2-8$
    \end{subproof}
    ((p \imp q) \imp p) \imp p & $\impi 1-9$
\end{logicproof}