\begin{frame} \frametitle{Derivation with Natural Deduction} \begin{exampleblock}{} Can we derive \quad$q$\quad from \quad$\neg\neg p \to (\neg q \to r),\;p,\;\neg r$\quad? \pause\medskip \begin{tikzpicture} \naturaldeduction{ \proofstep{$\neg\neg p \to (\neg q \to r)$}{premise}; \mpause[1]{ \proofstep{$p$}{premise}; } \mpause{ \proofstep{$\neg r$}{premise}; } \mpause{ \proofstep{$\neg\neg p$}{$\neg\neg_i$ 2}; } \mpause{ \proofstep{$\neg q \to r$}{$\to_e$ 4,1}; } \mpause{ \proofstep{$\neg\neg q$}{MT 5,3}; } \mpause{ \proofstep{$q$}{$\neg\neg_e$ 6}; } } \end{tikzpicture} \pause\pause\pause\pause\pause\pause\pause \medskip Hence we have derived \begin{talign} \neg\neg p \to (\neg q \to r),\;p,\;\neg r \quad\vdash\quad q \end{talign} \end{exampleblock} \end{frame}