25/77
\begin{frame}
  \frametitle{The Condition}
  
  \vspace{-2ex}
  \begin{align*}
    \infer[\rulename{\exists_i}]
    {\myex{x}{\phi}}
    {\phi\;[t/x]}
  &&
    \infer[\rulename{\forall_e}]
    {\phi\;[t/x]}
    {\myall{x}{\phi}}
  \end{align*}

  \begin{alertgoal}{}
  Is the following derivation correct?
  \smallskip
  
  \begin{tikzpicture}
  \naturaldeduction{
    \proofbox{
      \proofstep{$\myall{x}{\myex{y}{R(x,y)}}$}{premise};
      \proofstep{$\myex{y}{R(y,y)}$}{$\forall_e$ 1 \only<3->{\alert{(wrong!)}}};
    }
    \proofstep{$\myall{x}{\myex{y}{R(x,y)}} \to \myex{y}{R(y,y)}$}{$\to_i$ 1--2};
  }
  \end{tikzpicture}
  \medskip\pause
  
  This is clearly a wrong derivation. 
  \begin{center}
    \begin{tikzpicture}[node distance=15mm,
      dot/.style={minimum size=4mm, circle, draw=none, fill=black, inner sep=0, outer sep=1mm, text=white}]
      \node [dot] (1) {1};
      \node [dot,below right of=1] (2) {2};
      \node [dot,above right of=2] (3) {3};
      \begin{scope}[->,thick]
      \draw (1) -- (2);
      \draw (2) -- (3);
      \draw (3) -- (1);
      \end{scope}
    \end{tikzpicture}
  \end{center}\vspace{-1ex}
  This model fulfils $\myall{x}{\myex{y}{R(x,y)}}$ but not $\myex{y}{R(y,y)}$.
  \smallskip\pause
  
  \aemph{The problem:} $y$ is not free for $x$ in $\myex{y}{R(x,y)}$!  
  \end{alertgoal}
\end{frame}