37/179
\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}