\begin{frame} \frametitle{Block Structure} \begin{alertgoal}{} When applying a rule \begin{align*} \infer {\beta} {\alpha_1 && \ldots && \alpha_n} \;\;, \end{align*} the $\alpha_1,\ldots,\alpha_n$ must be \emph{in the scope}, that is, must have been derived in the current block or a surrounding block. \end{alertgoal} (Compare with scopes of variables in programming languages.) \medskip\pause \begin{tikzpicture} \naturaldeduction{ \proofstep{$p \to q$}{premise}; \proofbox{ \proofstep{$p$}{assumption}; \proofstep{$q$}{$\to_e$ 1,2}; } \proofstep{$q \vee q$}{$\vee_i$ 3 \aemph{This is not allowed!!!}}; } \end{tikzpicture} \end{frame}