% Part: first-order-logic
% Chapter: syntax-and-semantics
% Section: substitution

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

\begin{document}

\olfileid{fol}{syn}{sub}

\olsection{Substitution}

\begin{defn}[Substitution in a term]
We define $\Subst{s}{t}{x}$, the result of \emph{substituting} $t$
for every occurrence of~$x$ in $s$, recursively:
\begin{enumerate}
\item \indcase{s}{c}{$\Subst{\indfrm}{t}{x}$ is just $s$.}

\item \indcase{s}{y}{$\Subst{\indfrm}{t}{x}$ is also just~$s$,
  provided $y$ is a variable and $y \not\ident x$.}

\item \indcase{s}{x}{$\Subst{\indfrm}{t}{x}$ is~$t$.}

\item\indcase{s}{\Atom{f}{t_1, \dots, t_n}}{$\Subst{\indfrmp}{t}{x}$ is
  $\Atom{f}{\Subst{t_1}{t}{x}, \dots, \Subst{t_n}{t}{x}}$.}
\end{enumerate}
\end{defn}

\begin{defn}
A term~$t$ is \emph{!!{free for}} $x$ in $!A$ if none of the free
occurrences of~$x$ in $!A$ occur in the scope of a quantifier that
binds a variable in~$t$.
\end{defn}

\begin{ex} ~
\begin{enumerate}
\item $\Obj v_8$ is free for $\Obj v_1$ in $\lexists[\Obj
  v_3]\Atom{\Obj A^2_4}{\Obj v_3,\Obj v_1}$

\item $\Obj f^2_1(\Obj v_1, \Obj v_2)$ is \emph{not} free for $\Obj
  v_0$ in $\lforall[\Obj v_2]\Atom{\Obj A^2_4}{\Obj v_0,\Obj v_2}$
\end{enumerate}
\end{ex}

\begin{defn}[Substitution in !!a{formula}]
If $!A$ is !!a{formula}, $x$~is !!a{variable}, and $t$~is a term
!!{free for}~$x$ in~$!A$, then $\Subst{!A}{t}{x}$ is the result of
substituting $t$ for all free occurrences of~$x$ in~$!A$.
\begin{enumerate}
\tagitem{prvFalse}{\indcase{!A}{\lfalse}{$\Subst{\indfrm}{t}{x}$ is
    $\lfalse$.}}{}

\tagitem{prvTrue}{\indcase{!A}{\ltrue}{$\Subst{\indfrm}{t}{x}$ is
    $\ltrue$.}}{}

\item \indcase{!A}{\Atom{P}{t_1,\dots,
    t_n}}{$\Subst{\indfrm}{t}{x}$ is $\Atom{P}{\Subst{t_1}{t}{x},
    \dots, \Subst{t_n}{t}{x}}$.}

\item \indcase{!A}{\eq[t_1][t_2]}{$\Subst{\indfrmp}{t}{x}$ is
  $\Subst{t_1}{t}{x} = \Subst{t_2}{t}{x}$.}

\tagitem{prvNot}{\indcase{!A}{\lnot !B}{$\Subst{\indfrmp}{t}{x}$ is
    $\lnot \Subst{!B}{t}{x}$.}}{}

\tagitem{prvAnd}{\indcase{!A}{(!B \land
    !C)}{$\Subst{\indfrmp}{t}{x}$ is $(\Subst{!B}{t}{x} \land
    \Subst{!C}{t}{x})$.}}{}

\tagitem{prvOr}{\indcase{!A}{(!B \lor
    !C)}{$\Subst{\indfrmp}{t}{x}$ is $(\Subst{!B}{t}{x} \lor
    \Subst{!C}{t}{x})$.}}{}

\tagitem{prvIf}{\indcase{!A}{(!B \lif
    !C)}{$\Subst{\indfrmp}{t}{x}$ is $(\Subst{!B}{t}{x} \lif
    \Subst{!C}{t}{x})$.}}{}

\tagitem{prvIff}{\indcase{!A}{(!B \liff
    !C)}{$\Subst{\indfrmp}{t}{x}$ is $(\Subst{!B}{t}{x} \liff
    \Subst{!C}{t}{x})$.}}{}

\tagitem{prvAll}{
\indcase{!A}{\lforall[y][!B]}{$\Subst{\indfrmp}{t}{x}$
    is $\lforall[y][\Subst{!B}{t}{x}]$, provided $y$ is a variable
    other than $x$; otherwise $\Subst{\indfrmp}{t}{x}$
    is just $\indfrm$.}}{}

\tagitem{prvEx}{
\indcase{!A}{\lexists[y][!B]}{$\Subst{\indfrmp}{t}{x}$
    is $\lexists[y][\Subst{!B}{t}{x}]$, provided $y$ is a variable
    other than $x$; otherwise $\Subst{\indfrmp}{t}{x}$
    is just $\indfrm$.}}{}
\end{enumerate}
\end{defn}

\begin{explain}
Note that substitution may be vacuous: If $x$ does not occur in $!A$
at all, then $\Subst{!A}{t}{x}$ is just~$!A$.

The restriction that $t$ must be !!{free for}~$x$ in~$!A$ is necessary to
exclude cases like the following. If $!A \ident \lexists[y][x < y]$
and $t \ident y$, then $\Subst{!A}{t}{x}$ would be $\lexists[y][y <
  y]$. In this case the free variable $y$ is ``captured'' by the
quantifier $\lexists[y]$ upon substitution, and that is undesirable.
For instance, we would like it to be the case that whenever
$\lforall[x][!B]$ holds, so does $\Subst{!B}{t}{x}$. But consider
$\lforall[x][\lexists[y][x < y]]$ (here $!B$ is $\lexists[y][x <
  y]$). It is a sentence that is true about, e.g., the natural numbers:
for every number~$x$ there is a number~$y$ greater than it. If we
allowed $y$ as a possible substitution for~$x$, we would end up with
$\Subst{!B}{y}{x} \ident \lexists[y][y < y]$, which is false. We
prevent this by requiring that none of the free variables in~$t$ would
end up being bound by a quantifier in~$!A$.
\end{explain}

We often use the following convention to avoid cumbersome notation: If
$!A$ is !!a{formula} which may contain the !!{variable}~$x$ free, we
also write~$!A(x)$ to indicate this. When it is clear which $!A$
and~$x$ we have in mind, and $t$ is a term (assumed to be free for $x$
in $!A(x)$), then we write $!A(t)$ as short for $\Subst{!A}{t}{x}$. So
for instance, we might say, ``we call $!A(t)$ an instance
of~$\lforall[x][!A(x)]$.'' By this we mean that if $!A$~is any
!!{formula}, $x$~!!a{variable}, and $t$~a term that's free for~$x$
in~$!A$, then $\Subst{!A}{t}{x}$ is an instance of~$\lforall[x][!A]$.

\end{document}