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