% Part: first-order-logic
% Chapter: sequent-calculus
% Section: quantifier-rules

\documentclass[../../../include/open-logic-section]{subfiles}

\begin{document}

\olfileid{fol}{seq}{qrl}

\olsection{Quantifier Rules}

\subsection{Rules for $\lforall$}

\begin{defish}
\Axiom$ !A(t), \Gamma \fCenter \Delta$
\RightLabel{\LeftR{\lforall}}
\UnaryInf$ \lforall[x][!A(x)],\Gamma \fCenter \Delta$
\DisplayProof
\hfill
\Axiom$ \Gamma \fCenter \Delta, !A(a) $
\RightLabel{\RightR{\lforall}}
\UnaryInf$ \Gamma \fCenter \Delta, \lforall[x][!A(x)]$
\DisplayProof
\end{defish}

In \LeftR{\lforall}, $t$ is a closed term (i.e., one without
variables). In \RightR{\lforall}, $a$~is !!a{constant} which must not
occur anywhere in the lower sequent of the \RightR{\lforall} rule. We
call $a$ the \emph{eigenvariable} of the \RightR{\forall}
inference.\footnote{We use the term ``eigenvariable'' even though $a$
in the above rule is !!a{constant}. This has historical reasons.}

\subsection{Rules for $\lexists$}

\begin{defish}
\Axiom$ !A(a), \Gamma \fCenter \Delta $
\RightLabel{\LeftR{\lexists}}
\UnaryInf$ \lexists[x][!A(x)], \Gamma \fCenter \Delta$
\DisplayProof
\hfill
\Axiom$ \Gamma \fCenter \Delta, !A(t) $
\RightLabel{\RightR{\lexists}}
\UnaryInf$ \Gamma \fCenter \Delta, \lexists[x][!A(x)]$
\DisplayProof
\end{defish}

Again, $t$~is a closed term, and $a$~is !!a{constant} which does not
occur in the lower sequent of the \LeftR{\lexists} rule. We call $a$
the \emph{eigenvariable} of the \LeftR{\lexists} inference.

The condition that an eigenvariable not occur in the lower sequent of
the \RightR{\lforall} or \LeftR{\lexists} inference is called the
\emph{eigenvariable condition}.

\begin{explain}
Recall the convention that when $!A$ is !!a{formula} with the
!!{variable}~$x$ free, we indicate this by writing~$!A(x)$. In the
same context, $!A(t)$ then is short for~$\Subst{!A}{t}{x}$. So we
could also write the \RightR{\lexists} rule as:
\begin{prooftree}
  \Axiom$\Gamma \fCenter \Delta, \Subst{!A}{t}{x}$
  \RightLabel{\RightR{\lexists}}
  \UnaryInf$\Gamma \fCenter \Delta, \lexists[x][!A]$
\end{prooftree}
Note that $t$ may already occur in~$!A$, e.g., $!A$~might
be~$\Atom{\Obj P}{t,x}$. Thus, inferring $\Gamma \Sequent \Delta,
\lexists[x][\Atom{\Obj P}{t,x}]$ from~$\Gamma \Sequent \Delta,
\Atom{\Obj P}{t,t}$ is a correct application
of~\RightR{\lexists}---you may ``replace'' one or more, and not
necessarily all, occurrences of~$t$ in the premise by the bound
!!{variable}~$x$. However, the eigenvariable conditions in
\RightR{\lforall} and~\LeftR{\lexists} require that the
!!{constant}~$a$ does not occur in~$!A$. So, you cannot correctly
infer $\Gamma \Sequent \Delta, \lforall[x][\Atom{\Obj P}{a,x}]$ from
$\Gamma \Sequent \Delta, \Atom{\Obj P}{a,a}$ using~$\RightR{\lforall}$.
\end{explain}

\begin{explain}
In \RightR{\lexists} and \LeftR{\lforall} there are no restrictions on
the term~$t$. On the other hand, in the \LeftR{\lexists} and
\RightR{\lforall} rules, the eigenvariable condition requires that the
!!{constant}~$a$ does not occur anywhere outside of~$!A(a)$ in the
upper sequent. It is necessary to ensure that the system is sound,
i.e., only !!{derive}s sequents that are valid. Without this
condition, the following would be allowed:
\begin{prooftree}
  \Axiom$!A(a) \fCenter !A(a)$
  \RightLabel{*\LeftR{\lexists}}
  \UnaryInf$\lexists[x][!A(x)] \fCenter !A(a)$
  \RightLabel{\RightR{\lforall}}
  \UnaryInf$\lexists[x][!A(x)] \fCenter \lforall[x][!A(x)]$
  \DisplayProof\bottomAlignProof
  \qquad
  \Axiom$!A(a) \fCenter !A(a)$
  \RightLabel{*\RightR{\lforall}}
  \UnaryInf$!A(a) \fCenter \lforall[x][!A(x)]$
  \RightLabel{\LeftR{\lexists}}
  \UnaryInf$\lexists[x][!A(x)] \fCenter \lforall[x][!A(x)]$
\end{prooftree}
However, $\lexists[x][!A(x)] \Sequent \lforall[x][!A(x)]$ is not valid.
\end{explain}

\end{document}