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*}

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)}$!