38/179
\begin{frame}
  \frametitle{Block Structure}

  \begin{alertgoal}{}
    When applying a rule
      \begin{align*}
        \infer
        {\psi}
        {\phi_1 && \ldots && \phi_n} \;\;,
      \end{align*}
    the $\phi_1,\ldots,\phi_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}