% Part: first-order-logic
% Chapter: completeness
% Section: identity

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

\begin{document}

\olfileid{fol}{com}{ide}
\olsection{Identity}

\begin{explain}
The construction of the term model given in the preceding section is
enough to establish completeness for first-order logic for
sets~$\Gamma$ that do not contain~$\eq$.  The term model satisfies
every $!A \in \Gamma^*$ which does not contain~$\eq$ (and hence all
$!A \in \Gamma$).  It does not work, however, if $\eq$ is present.
The reason is that $\Gamma^*$ then may contain
!!a{sentence}~$\eq[t][t']$, but in the term model the value of any
term is that term itself.  Hence, if $t$ and $t'$ are different terms,
their values in the term model---i.e., $t$ and $t'$,
respectively---are different, and so $\eq[t][t']$ is false.  We can
fix this, however, using a construction known as ``factoring.''
\end{explain}

\begin{defn}
  Let $\Gamma^*$ be a consistent and !!{complete} set of sentences
  in~$\Lang L$.  We define the relation $\approx$ on the set of closed
  terms of~$\Lang L$ by
  \[
  t \approx t' \text{\quad iff \quad} \eq[t][t'] \in \Gamma^*
  \]
\end{defn}

\begin{prop}
\ollabel{prop:approx-equiv}
The relation $\approx$ has the following properties:
\begin{enumerate}
\item $\approx$ is reflexive.
\item $\approx$ is symmetric.
\item  $\approx$ is transitive.
\item If $t \approx t'$, $f$ is !!a{function}, and $t_1$, \dots,
  $t_{i-1}$, $t_{i+1}$, \dots, $t_n$ are closed terms, then
\[
\Atom{f}{t_1,\dots, t_{i-1}, t, t_{i+1}, \dots, t_n} \approx
\Atom{f}{t_1,\dots, t_{i-1}, t', t_{i+1}, \dots, t_n}.
\]
\item If $t \approx t'$, $R$ is !!a{predicate}, and $t_1$, \dots,
  $t_{i-1}$, $t_{i+1}$, \dots, $t_n$ are closed terms, then
\begin{multline*}
\Atom{R}{t_1,\dots, t_{i-1}, t, t_{i+1}, \dots, t_n} \in \Gamma^* \text{ iff } \\
\Atom{R}{t_1,\dots, t_{i-1}, t', t_{i+1}, \dots, t_n} \in \Gamma^*.
\end{multline*}
\end{enumerate}
\end{prop}

\begin{proof}
Since $\Gamma^*$ is consistent and !!{complete}, $\eq[t][t'] \in
\Gamma^*$ iff $\Gamma^* \Proves \eq[t][t']$.  Thus it is enough to
show the following:
\begin{enumerate}
\item $\Gamma^* \Proves \eq[t][t]$ for all closed terms~$t$.
\item If $\Gamma^* \Proves \eq[t][t']$ then $\Gamma^* \Proves \eq[t'][t]$.
\item If $\Gamma^* \Proves \eq[t][t']$ and $\Gamma^* \Proves
  \eq[t'][t'']$, then $\Gamma^* \Proves \eq[t][t'']$.
\item If $\Gamma^* \Proves \eq[t][t']$, then
\[
\Gamma^* \Proves
\eq[\Atom{f}{t_1,\dots,t_{i-1},t,t_{i+1},,\dots,t_n}][\Atom{f}{t_1,\dots,t_{i-1},t',t_{i+1},\dots,t_n}]
\]
for every $n$-place !!{function}~$f$ and closed terms $t_1$, \dots,
$t_{i-1}$, $t_{i+1}$, \dots,~$t_n$.
\item If $\Gamma^* \Proves \eq[t][t']$ and
$\Gamma^* \Proves
\Atom{R}{t_1,\dots,t_{i-1},t,t_{i+1},\dots,t_n}$, then
$\Gamma^* \Proves \Atom{R}{t_1,\dots,t_{i-1},t',t_{i+1},\dots,t_n}$
for every $n$-place !!{predicate}~$R$ and closed terms $t_1$, \dots,
$t_{i-1}$, $t_{i+1}$, \dots,~$t_n$.
\end{enumerate}
\end{proof}

\begin{prob}
Complete the proof of~\olref[fol][com][ide]{prop:approx-equiv}.
\end{prob}

\begin{defn}
Suppose $\Gamma^*$ is a consistent and !!{complete} set in a
language~$\Lang L$, $t$ is a closed term, and $\approx$ as in the
previous definition. Then:
\[
\equivrep{t}{\approx} = \Setabs{t'}{t'\in \Trm[L], t \approx t'}
\]
and $\equivclass{\Trm[L]}{\approx} = \Setabs{\equivrep{t}{\approx}}{t \in \Trm[L]}$.
\end{defn}

\begin{defn}
\ollabel{defn:term-model-factor}
Let $\Struct M = \Struct M(\Gamma^*)$ be the term model
for~$\Gamma^*$ from \olref[mod]{defn:termmodel}.  Then $\Struct{\equivclass{M}{\approx}}$ is the following
!!{structure}:
\begin{enumerate}
\item $\Domain{\equivclass{M}{\approx}} = \equivclass{\Trm[L]}{\approx}$.
\item $\Assign{c}{\equivclass{M}{\approx}} = \equivrep{c}{\approx}$
\item $\Assign{f}{\equivclass{M}{\approx}}(\equivrep{t_1}{\approx}, \dots,
  \equivrep{t_n}{\approx}) = \equivrep{\Atom{f}{t_1,\dots, t_n}}{\approx}$
\item $\tuple{\equivrep{t_1}{\approx}, \dots, \equivrep{t_n}{\approx}} \in
  \Assign{R}{\equivclass{M}{\approx}}$ iff
  $\Sat{M}{\Atom{R}{t_1,\dots, t_n}}$, i.e., iff $\Atom{R}{t_1,\dots,
  t_n} \in \Gamma^*$.
\end{enumerate}
\end{defn}

\begin{explain}
Note that we have defined $\Assign{f}{\equivclass{M}{\approx}}$ and
$\Assign{R}{\equivclass{M}{\approx}}$ for elements of
$\equivclass{\Trm[L]}{\approx}$ by referring to them as
$\equivrep{t}{\approx}$, i.e., via \emph{representatives}~$t \in
\equivrep{t}{\approx}$.  We have to make sure that these definitions
do not depend on the choice of these representatives, i.e., that for
some other choices~$t'$ which determine the same equivalence classes
($\equivrep{t}{\approx} = \equivrep{t'}{\approx}$), the definitions
yield the same result. For instance, if $R$ is a one-place
!!{predicate}, the last clause of the definition says that
$\equivrep{t}{\approx} \in \Assign{R}{\equivclass{M}{\approx}}$ iff
$\Sat{M}{\Atom{R}{t}}$. If for some other term~$t'$ with $t \approx
t'$, $\Sat/{M}{\Atom{R}{t}}$, then the definition would require
$\equivrep{t'}{\approx} \notin \Assign{R}{\equivclass{M}{\approx}}$.
If $t \approx t'$, then $\equivrep{t}{\approx} =
\equivrep{t'}{\approx}$, but we can't have both $\equivrep{t}{\approx}
\in \Assign{R}{\equivclass{M}{\approx}}$ and $\equivrep{t}{\approx}
\notin \Assign{R}{\equivclass{M}{\approx}}$.  However,
\olref{prop:approx-equiv} guarantees that this cannot happen.
\end{explain}

\begin{prop}
$\Struct{\equivclass{M}{\approx}}$ is well defined, i.e., if $t_1$,
  \dots, $t_n$, $t_1'$, \dots, $t_n'$ are closed terms,
  and $t_i \approx t_i'$ then
\begin{enumerate}
\item $\equivrep{\Atom{f}{t_1,\dots, t_n}}{\approx} =
    \equivrep{\Atom{f}{t_1',\dots, t_n'}}{\approx}$, i.e.,
  \[
  \Atom{f}{t_1,\dots, t_n} \approx \Atom{f}{t_1',\dots, t_n'}
  \]
  and
\item $\Sat{M}{\Atom{R}{t_1,\dots, t_n}}$ iff
  $\Sat{M}{\Atom{R}{t_1',\dots, t_n'}}$, i.e.,
  \[
    \Atom{R}{t_1,\dots, t_n} \in \Gamma^* \text{ iff }
    \Atom{R}{t_1',\dots, t_n'} \in \Gamma^*.
  \]
\end{enumerate}
\end{prop}

\begin{proof}
Follows from \olref{prop:approx-equiv} by induction on~$n$.
\end{proof}

As in the case of the term model, before proving the truth lemma we need the
following lemma.

\begin{lem} 
\ollabel{lem:val-in-termmodel-factored} Let $\Struct M = \Struct M
 (\Gamma^*)$, then $\Value{t}{\equivclass{M}{\approx}} = \equivrep{t}
 {\approx}$.
\end{lem}
\begin{proof} 
The proof is similar to that of \olref[mod]{lem:val-in-termmodel}.
\end{proof}

\begin{prob}
Complete the proof of~\olref[fol][com][ide]{lem:val-in-termmodel-factored}.
\end{prob}

\begin{lem}
\ollabel{lem:truth}
$\Sat{\equivclass{M}{\approx}}{!A}$ iff $!A \in \Gamma^*$ for all
  sentences~$!A$.
\end{lem}

\begin{proof}
By induction on~$!A$, just as in the proof of \olref[mod]{lem:truth}.
The only case that needs additional attention is when $!A \ident
\eq[t][t']$.
\begin{align*}
\Sat{\equivclass{M}{\approx}}{\eq[t][t']} & \text{ iff } \equivrep{t}{\approx} = \equivrep{t'}{\approx}
\text{ (by definition of $\Struct{\equivclass{M}{\approx}}$)}\\
& \text{ iff } t \approx t' \text{ (by definition of $\equivrep{t}{\approx}$)}\\
& \text{ iff } \eq[t][t'] \in \Gamma^* \text{ (by definition of $\approx$).}
\end{align*}
\end{proof}

\begin{digress}
Note that while $\Struct{M(\Gamma^*)}$ is always !!{enumerable} and
infinite, $\Struct{\equivclass{M}{\approx}}$ may be finite, since it
may turn out that there are only finitely many classes
$\equivrep{t}{\approx}$.  This is to be expected, since $\Gamma$ may
contain !!{sentence}s which require any !!{structure} in which they
are true to be finite.  For instance, $\lforall[x][\lforall[y][x =
y]]$ is a consistent !!{sentence}, but is satisfied only in
!!{structure}s with !!a{domain} that contains exactly one
!!{element}.
\end{digress}

\end{document}