\begin{frame} \frametitle{Example from a Previous Exam} \begin{exampleblock}{} Show that \quad$\vdash\; \neg q \vee (p \to q)$\quad with PBC instead of LEM: \smallskip \begin{tikzpicture} \naturaldeduction{ \mpause[1]{ \proofbox{ \mpause{ \proofstep{$\neg (\neg q \vee (p \to q))$}{assumption}; } \mpause{ \proofbox{ \mpause{ \proofstep{$\neg q$}{assumption}; } \mpause{ \proofstep{$\neg q \vee (p\to q)$}{$\vee_{i_1}$ 2}; } \mpause{ \proofstep{$\bot$}{$\neg_e$ 3,1}; } } } \mpause{ \proofstep{$q$}{PBC 2--4}; } \mpause{ \proofbox{ \mpause{ \proofstep{$p$}{assumption}; } \mpause{ \proofstep{$q$}{copy 5}; } } } \mpause{ \proofstep{$p \to q$}{$\to_i$ 6--7}; } \mpause{ \proofstep{$\neg q \vee (p \to q)$}{$\vee_{i_2}$ 8}; } \mpause{ \proofstep{$\bot$}{$\neg_e$ 9,1}; } } } \mpause{ \proofstep{$\neg q \vee (p \to q)$}{PBC 1--11}; } } \end{tikzpicture} \end{exampleblock} \end{frame}