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

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

\begin{document}

\olfileid{fol}{syn}{ext}

\olsection{Extensionality}

\begin{explain}
Extensionality, sometimes called relevance, can be expressed
informally as follows: the only factors that bear upon the
satisfaction of !!{formula}~$!A$ in !!a{structure}~$\Struct M$
relative to !!a{variable} assignment~$s$, are the size of the
!!{domain} and the assignments made by~$\Struct M$ and~$s$ to the
elements of the language that actually appear in~$!A$.

One immediate consequence of extensionality is that where two
!!{structure}s~$\Struct M$ and~$\Struct M'$ agree on all the elements
of the language appearing in a sentence~$!A$ and have the same
domain,~$\Struct M$ and~$\Struct M'$ must also agree on whether or not
$!A$ itself is true.
\end{explain}

\begin{prop}[Extensionality]
  \ollabel{prop:extensionality}
  Let $!A$ be !!a{formula}, and $\Struct M_1$ and $\Struct M_2$ be
  !!{structure}s with $\Domain{M_1} = \Domain{M_2}$, and $s$ a
  variable assignment on $\Domain{M_1} = \Domain{M_2}$.  If
  $\Assign{c}{M_1} = \Assign{c}{M_2}$, $\Assign{R}{M_1}=\Assign{R}{M_2}$,
  and $\Assign{f}{M_1} = \Assign{f}{M_2}$ for every !!{constant}~$c$,
  relation symbol~$R$, and !!{function} $f$ occurring in~$!A$, then
  $\Sat{M_1}{!A}[s]$ iff $\Sat{M_2}{!A}[s]$.
\end{prop}

\begin{proof}
  First prove (by induction on~$t$) that for every term,
  $\Value{t}{M_1}[s] = \Value{t}{M_2}[s]$.  Then prove the proposition
  by induction on~$!A$, making use of the claim just proved for the
  induction basis (where $!A$ is atomic).
\end{proof}

\begin{prob}
Carry out the proof of \olref[fol][syn][ext]{prop:extensionality} in
detail.
\end{prob}

\begin{cor}[Extensionality for !!^{sentence}s]
  \ollabel{cor:extensionality-sent}
  Let $!A$ be !!a{sentence} and $\Struct{M_1}$, $\Struct{M_2}$ as in
  \olref{prop:extensionality}. Then $\Sat{M_1}{!A}$ iff $\Sat{M_2}{!A}$.
\end{cor}

\begin{proof}
Follows from \olref{prop:extensionality} by \olref[ass]{cor:sat-sentence}.
\end{proof}

Moreover, the value of a term, and whether or not !!a{structure}
satisfies !!a{formula}, only depend on the values of its subterms.

\begin{prop}\ollabel{prop:ext-terms}
Let $\Struct M$ be !!a{structure}, $t$ and $t'$ terms, and $s$ a
variable assignment. Then $\Value{\Subst{t}{t'}{x}}{M}[s] =
\Value{t}{M}[\Subst{s}{\Value{t'}{M}[s]}{x}]$.
\end{prop}

\begin{proof}
By induction on~$t$.
\begin{enumerate}
\item If $t$ is a constant, say, $t\ident c$, then $\Subst{t}{t'}{x} =
  c$, and $\Value{c}{M}[s] = \Assign{c}{M} =
  \Value{c}{M}[\Subst{s}{\Value{t'}{M}[s]}{x}]$.

\item If $t$ is a variable other than~$x$, say, $t \ident y$, then
  $\Subst{t}{t'}{x} = y$, and $\Value{y}{M}[s] =
  \Value{y}{M}[\Subst{s}{\Value{t'}{M}[s]}{x}]$ since
  $\varAssign{s}{\Subst{s}{\Value{t'}{M}[s]}{x}}{x}$.

\item If $t \ident x$, then $\Subst{t}{t'}{x} = t'$. But
  $\Value{x}{M}[\Subst{s}{\Value{t'}{M}[s]}{x}] = \Value{t'}{M}[s]$ by
  definition of~$\Subst{s}{\Value{t'}{M}[s]}{x}$.

\item If $t \ident \Atom{f}{t_1,\dots,t_n}$ then we have:
\begin{multline*}
  \Value{\Subst{t}{t'}{x}}{M}[s]  = \\
  \begin{aligned}[b]
& = \Value{\Atom{f}{\Subst{t_1}{t'}{x}, \dots, \Subst{t_n}{t'}{x}}}{M}[s]\\
& \qquad    \text{ by definition of $\Subst{t}{t'}{x}$}\\
& = \Assign{f}{M}(\Value{\Subst{t_1}{t'}{x}}{M}[s], \dots,
    \Value{\Subst{t_n}{t'}{x}}{M}[s])\\
    & \qquad  \text{ by definition of $\Value{\Atom{f}{\dots}}{M}[s]$}\\
& = \Assign{f}{M}(\Value{t_1}{M}[\Subst{s}{\Value{t'}{M}[s]}{x}], \dots,
   \Value{t_n}{M}[\Subst{s}{\Value{t'}{M}[s]}{x}])\\
& \qquad    \text{ by induction hypothesis}\\
& = \Value{t}{M}[\Subst{s}{\Value{t'}{M}[s]}{x}]
    \text{ by definition of $\Value{\Atom{f}{\dots}}{M}[\Subst{s}{\Value{t'}{M}[s]}{x}]$}
  \end{aligned}
\end{multline*}
\end{enumerate}
\end{proof}

\begin{prop}\ollabel{prop:ext-formulas} Let $\Struct M$ be
!!a{structure}, $!A$ !!a{formula}, $t'$~a term, and $s$~a variable
assignment. Then $\Sat{M}{\Subst{!A}{t'}{x}}[s]$ iff
$\Sat{M}{!A}[\Subst{s}{\Value{t'}{M}[s]}{x}]$.
\end{prop}

\begin{proof}
Exercise.
\end{proof}

\begin{prob}
Prove \olref[fol][syn][ext]{prop:ext-formulas}
\end{prob}

\begin{explain}
  The point of
  \cref{fol:syn:ext:prop:ext-terms,fol:syn:ext:prop:ext-formulas} is
  the following. Suppose we have a term $t$ or !!a{formula}~$!A$ and
  some term~$t'$, and we want to know the value of $\Subst{t}{t'}{x}$
  or whether or not $\Subst{!A}{t'}{x}$ is satisfied in
  !!a{structure}~$\Struct M$ relative to !!a{variable} assignment~$s$.
  Then we can either perform the substitution first and then consider
  the value or satisfaction relative to $\Struct{M}$ and~$s$, or we
  can first determine the value~$m = \Value{t'}{M}[s]$ of $t'$ in
  $\Struct{M}$ relative to~$s$, change the !!{variable} assignment
  to~$\Subst{s}{m}{x}$ and then consider the value of~$t$ in
  $\Struct{M}$ and~$\Subst{s}{m}{x}$, or whether
  $\Sat{M}{!A}[\Subst{s}{m}{x}]$.
  \Cref{fol:syn:ext:prop:ext-terms,fol:syn:ext:prop:ext-formulas}
  guarantee that the answer will be the same, whichever way we do it.
\end{explain}

\end{document}