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

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

\begin{document}

\olfileid{fol}{syn}{sat}

\olsection{Satisfaction of \article{formula} \printtoken{S}{formula}
  in \article{structure} \printtoken{S}{structure}}

\begin{explain}
The basic notion that relates expressions such as terms and
!!{formula}s, on the one hand, and !!{structure}s on the other, are
those of \emph{!!{value}} of a term and \emph{satisfaction} of 
!!a{formula}.  Informally, the !!{value} of a term is an !!{element} of
!!a{structure}---if the term is just a constant, its !!{value} is the
object assigned to the constant by the !!{structure}, and if it is
built up using !!{function}s, the !!{value} is computed from the
!!{value}s of constants and the functions assigned to the functions in
the term.  !!^a{formula} is \emph{satisfied} in !!a{structure} if the
interpretation given to the predicates makes the !!{formula} true in
the domain of the !!{structure}. This notion of satisfaction is
specified inductively: the specification of the !!{structure} directly
states when atomic !!{formula}s are satisfied, and we define when a
complex !!{formula} is satisfied depending on the main connective or
quantifier and whether or not the immediate !!{subformula}s are
satisfied. 

The case of the quantifiers here is a bit tricky, as the
immediate !!{subformula} of a quantified !!{formula} has a free
!!{variable}, and !!{structure}s don't specify the !!{value}s of
!!{variable}s.  In order to deal with this difficulty, we also
introduce \emph{variable assignments} and define satisfaction not with
respect to !!a{structure} alone, but with respect to !!a{structure}
plus !!a{variable} assignment.
\end{explain}

\begin{defn}[Variable Assignment]
A \emph{variable assignment}~$s$ for !!a{structure}~$\Struct{M}$ is a
function which maps each !!{variable} to !!a{element} of~$\Domain M$,
i.e., $s\colon \Var \to \Domain M$.
\end{defn}

\begin{explain}
!!^a{structure} assigns !!a{value} to each !!{constant}, and a
variable assignment to each variable.  But we want to use terms built
up from them to also name !!{element}s of the !!{domain}.  For this we
define the !!{value} of terms inductively. For !!{constant}s and
variables the value is just as the !!{structure} or the variable
assignment specifies it; for more complex terms it is computed
recursively using the functions the !!{structure} assigns to the
!!{function}s.
\end{explain}

\begin{defn}[!!^{value} of Terms]
If $t$ is a term of the language~$\Lang L$, $\Struct M$ is a
!!{structure} for~$\Lang L$, and $s$ is !!a{variable} assignment
for~$\Struct M$, the \emph{!!{value}}~$\Value{t}{M}[s]$ is defined as
follows:
\begin{enumerate}
\item \indcase{t}{c}{$\Value{\indfrm}{M}[s] = \Assign{\indcomplex}{M}$.}
\item \indcase{t}{x}{$\Value{\indfrm}{M}[s] = s(\indcomplex)$.}
\item \indcase{t}{\Atom{f}{t_1, \ldots, t_n}}{
\[
\Value{\indfrm}{M}[s] = \Assign{f}{M}(\Value{t_1}{M}[s], \ldots,
\Value{t_n}{M}[s]).
\]}
\end{enumerate}
\end{defn}

\begin{defn}[$x$-Variant]
If $s$ is !!a{variable} assignment for !!a{structure}~$\Struct M$, then any
!!{variable} assignment~$s'$ for~$\Struct M$ which differs from~$s$ at most
in what it assigns to~$x$ is called an \emph{$x$-variant} of~$s$.  If
$s'$ is an $x$-variant of~$s$ we write $\varAssign{s'}{s}{x}$.
\end{defn}

\begin{explain}
Note that an $x$-variant of an assignment~$s$ does not \emph{have} to
assign something different to~$x$.  In fact, every assignment counts
as an $x$-variant of itself.
\end{explain}

\begin{defn}
  If $s$ is !!a{variable} assignment for !!a{structure}~$\Struct M$
  and $m \in \Domain{M}$, then the assignment~$\Subst{s}{m}{x}$ is the
  variable assignment defined by
  \[\Subst{s}{m}{x}(y) = \begin{cases}
    m & \text{if } y \ident x\\
    s(y) & \text{otherwise}.
  \end{cases}\]
\end{defn}

In other words, $\Subst{s}{m}{x}$ is the particular $x$-variant of~$s$
which assigns the domain !!{element}~$m$ to~$x$, and assigns the same
things to !!{variable}s other than~$x$ that $s$ does.

\begin{defn}[Satisfaction]
\ollabel{defn:satisfaction}
Satisfaction of !!a{formula}~$!A$ in !!a{structure}~$\Struct M$
relative to !!a{variable} assignment~$s$, in symbols:
$\Sat{M}{!A}[s]$, is defined recursively as follows. (We write
$\Sat/{M}{!A}[s]$ to mean ``not $\Sat{M}{!A}[s]$.'')
\begin{enumerate}
\tagitem{prvFalse}{%
  \indcase{!A}{\lfalse}{$\Sat/{M}{\indfrm}[s]$.}}{}

\tagitem{prvTrue}{%
  \indcase{!A}{\ltrue}{$\Sat{M}{\indfrm}[s]$.}}{}

\item \indcase{!A}{\Atom{R}{t_1, \dots, t_n}}{$\Sat{M}{\indfrm}[s]$
  iff $\langle \Value{t_1}{M}[s], \dots, \Value{t_n}{M}[s] \rangle \in
  \Assign{R}{M}$.}

\item \indcase{!A}{\eq[t_1][t_2]}{$\Sat{M}{\indfrm}[s]$ iff
  $\Value{t_1}{M}[s] = \Value{t_2}{M}[s]$.}

\tagitem{prvNot}{%
  \indcase{!A}{\lnot !B}{$\Sat{M}{\indfrm}[s]$ iff
    $\Sat/{M}{!B}[s]$.}}{}

\tagitem{prvAnd}{%
  \indcase{!A}{(!B \land !C)}{$\Sat{M}{\indfrm}[s]$ iff $\Sat{M}{!B}[s]$
    and $\Sat{M}{!C}[s]$.}}{}

\tagitem{prvOr}{%
  \indcase{!A}{(!B \lor !C)}{$\Sat{M}{\indfrm}[s]$ iff
    $\Sat{M}{!B}[s]$ or $\Sat{M}{!C}[s]$ (or both).}}{}

\tagitem{prvIf}{%
  \indcase{!A}{(!B \lif !C)}{$\Sat{M}{\indfrm}[s]$ iff $\Sat/{M}{!B}[s]$
    or $\Sat{M}{!C}[s]$ (or both).}}{}

\tagitem{prvIff}{%
  \indcase{!A}{(!B \liff !C)}{$\Sat{M}{\indfrm}[s]$ iff either both
    $\Sat{M}{!B}[s]$ and $\Sat{M}{!C}[s]$, or neither $\Sat{M}{!B}[s]$
    nor $\Sat{M}{!C}[s]$.}}{}

\tagitem{prvAll}{%
  \indcase{!A}{\lforall[x][!B]}{$\Sat{M}{\indfrm}[s]$ iff for every
    !!{element}~$m \in \Domain M$, $\Sat{M}{!B}[\Subst{s}{m}{x}]$.}}{}

\tagitem{prvEx}{%
  \indcase{!A}{\lexists[x][!B]}{$\Sat{M}{\indfrm}[s]$ iff for at least
  one !!{element}~$m \in \Domain M$, $\Sat{M}{!B}[\Subst{s}{m}{x}]$.}}{}
\end{enumerate}
\end{defn}

\begin{explain}
The variable assignments are important in the last
\iftag{notprvEx,notprvAll}{clause}{two clauses}.\iftag{prvAll}{ We
cannot define satisfaction of $\lforall[x][!B(x)]$ by ``for all $m \in
\Domain{M}$, $\Sat{M}{!B(m)}$.''}{}\iftag{prvEx}{ We cannot define
satisfaction of $\lexists[x][!B(x)]$ by ``for at least one $m \in
\Domain{M}$, $\Sat{M}{!B(m)}$.''}{} The reason is that if $m \in
\Domain M$, it is not a symbol of the language, and so $!B(m)$~is not
!!a{formula} (that is, $\Subst{!B}{m}{x}$ is undefined).  We also
cannot assume that we have !!{constant}s or terms available that name
every !!{element} of~$\Struct{M}$, since there is nothing in the
definition of !!{structure}s that requires it.  In the standard
language, the set of !!{constant}s is !!{denumerable}, so if
$\Domain{M}$ is not !!{enumerable} there aren't even enough
!!{constant}s to name every object. 

We solve this problem by introducing !!{variable} assignments, which
allow us to link variables directly with !!{element}s of the domain.
Then instead of saying that, e.g.,
\iftag{prvEx}{$\lexists[x][!B(x)]$}{$\lforall[x][!B(x)]$} is satisfied
in~$\Struct M$ iff \iftag{prvEx}{for at least one $m \in
\Domain{M}$}{for all $m \in \Domain{M}$, $\Sat{M}{!B(m)}$}, we say it
is satisfied in~$\Struct M$ \emph{relative to}~$s$ iff $!B(x)$ is
satisfied relative to~$\Subst{s}{m}{x}$ \iftag{prvEx}{for at least
one}{for every} $m \in \Domain M$.
\end{explain}

\begin{ex}
Let $\Lang{L} = \{a, b, f, R\}$ where $a$ and $b$ are !!{constant}s,
$f$~is a two-place !!{function}, and $R$~is a two-place !!{predicate}.
Consider the !!{structure}~$\Struct{M}$ defined by:
\begin{enumerate}
\item $\Domain M = \{1, 2, 3, 4\}$
\item $\Assign{a}{M} = 1$
\item $\Assign{b}{M} = 2$
\item $\Assign{f}{M}(x, y) = x+y$ if $x+y \le 3$ and $= 3$ otherwise.
\item $\Assign{R}{M} = \{\tuple{1, 1}, \tuple{1, 2}, \tuple{2, 3}, \tuple{2, 4}\}$
\end{enumerate}
The function $s(x) = 1$ that assigns $1 \in \Domain{M}$ to every
!!{variable} is a variable assignment for~$\Struct{M}$.

Then
\begin{align*}
\Value{f(a,b)}{M}[s] & = \Assign{f}{M}(\Value{a}{M}[s], \Value{b}{M}[s]).
\intertext{Since $a$ and $b$ are !!{constant}s, $\Value{a}{M}[s]
  = \Assign{a}{M} = 1$ and $\Value{b}{M}[s] = \Assign{b}{M} = 2$. So}
\Value{f(a,b)}{M}[s] & = \Assign{f}{M}(1, 2) = 1+2 = 3.
\intertext{To compute the value of $f(f(a,b),a)$ we have to consider}
\Value{f(f(a,b),a)}{M}[s] & = \Assign{f}{M}(\Value{f(a, b)}{M}[s],
\Value{a}{M}[s]) = \Assign{f}{M}(3, 1) = 3,
\intertext{since $3+1 > 3$. Since $s(x) = 1$ and $\Value{x}{M}[s] =
  s(x)$, we also have}
\Value{f(f(a,b),x)}{M}[s] & = \Assign{f}{M}(\Value{f(a, b)}{M}[s],
\Value{x}{M}[s]) = \Assign{f}{M}(3, 1) = 3,
\end{align*}

An atomic !!{formula}~$R(t_1, t_2)$ is satisfied if the tuple of
values of its arguments, i.e., $\tuple{\Value{t_1}{M}[s],
  \Value{t_2}{M}[s]}$, is !!a{element} of~$\Assign{R}{M}$. So, e.g., we
have $\Sat{M}{R(b,f(a,b))}[s]$ since $\tuple{\Value{b}{M},
  \Value{f(a,b)}{M}} = \tuple{2, 3} \in \Assign{R}{M}$, but
$\Sat/{M}{R(x, f(a,b))}[s]$ since $\tuple{1, 3} \notin \Assign{R}{M}[s]$.

To determine if a non-atomic formula~$!A$ is satisfied, you apply the
clauses in the inductive definition that applies to the main
connective. For instance, the main connective in $R(a, a) \lif (R(b,
x) \lor R(x, b))$ is the~$\lif$, and
\begin{align*}
  & \Sat{M}{R(a, a) \lif (R(b, x) \lor R(x, b))}[s] \text{ iff }\\
  & \qquad
  \Sat/{M}{R(a,a)}[s] \text{ or } \Sat{M}{R(b, x) \lor R(x, b)}[s]
  \intertext{Since $\Sat{M}{R(a,a)}[s]$ (because $\tuple{1,1} \in
    \Assign{R}{M}$) we can't yet determine the answer and must first
    figure out if $\Sat{M}{R(b, x) \lor R(x, b)}[s]$:}
  & \Sat{M}{R(b, x) \lor R(x, b)}[s] \text{ iff }\\
  & \qquad \Sat{M}{R(b,x)}[s] \text{ or } \Sat{M}{R(x, b)}[s]
  \intertext{And this is the case, since $\Sat{M}{R(x, b)}[s]$
    (because $\tuple{1,2} \in \Assign{R}{M}$).}
\end{align*}

Recall that an $x$-variant of~$s$ is a variable assignment that
differs from $s$ at most in what it assigns to~$x$. For every
!!{element} of~$\Domain{M}$, there is an $x$-variant of~$s$:
\begin{align*}
  s_1 & = \Subst{s}{1}{x}, &
  s_2 & = \Subst{s}{2}{x},\\
  s_3 & = \Subst{s}{3}{x}, &
  s_4 & = \Subst{s}{4}{x}.
\end{align*}
So, e.g., $s_2(x) = 2$ and $s_2(y) = s(y) = 1$ for all variables~$y$
other than~$x$. These are all the $x$-variants of~$s$ for the
structure~$\Struct{M}$, since $\Domain{M} = \{1, 2, 3, 4\}$. Note, in
particular, that $s_1 = s$ ($s$~is always an $x$-variant of itself).

\iftag{prvEx}{To determine if an existentially quantified
  !!{formula}~$\lexists[x][!A(x)]$ is satisfied, we have to determine
  if $\Sat{M}{!A(x)}[\Subst{s}{m}{x}]$ for at least one $m \in \Domain
  M$. So,
  \[
  \Sat{M}{\lexists[x][(R(b,x) \lor R(x,b))]}[s],
  \]
  since $\Sat{M}{R(b,x) \lor R(x, b)}[\Subst{s}{1}{x}]$
  ($\Subst{s}{3}{x}$ would also fit the bill).  But,
  \[
  \Sat/{M}{\lexists[x][(R(b,x) \land R(x,b))]}[s]
  \]
  since, whichever $m \in \Domain{M}$ we pick, $\Sat/{M}{R(b,x) \land R(x,b)}[\Subst{s}{m}{x}]$.}{}

\iftag{prvAll}{To determine if a universally quantified
  !!{formula}~$\lforall[x][!A(x)]$ is satisfied, we have to determine
  if $\Sat{M}{!A(x)}[\Subst{s}{m}{x}]$ for all $m \in \Domain M$. So,
  \[
  \Sat{M}{\lforall[x][(R(x,a) \lif R(a,x))]}[s],
  \]
  since $\Sat{M}{R(x,a) \lif R(a,x)}[\Subst{s}{m}{x}]$ for all $m \in
  \Domain M$. For $m = 1$, we have $\Sat{M}{R(a,x)}[\Subst{s}{1}{x}]$
  so the consequent is true; for $m = 2$, $3$, and~$4$, we have
  $\Sat/{M}{R(x,a)}[\Subst{s}{m}{x}]$, so the antecedent is false.
  But,
  \[
  \Sat/{M}{\lforall[x][(R(a,x) \lif R(x,a))]}[s]
  \]
  since $\Sat/{M}{R(a,x) \lif R(x,a)}[\Subst{s}{2}{x}]$ (because
  $\Sat{M}{R(a, x)}[\Subst{s}{2}{x}]$ and $\Sat/{M}{R(x,
  a)}[\Subst{s}{2}{x}]$).}{}

\iftag{defEx}{To determine if an existentially quantified
  !!{formula}~$\lexists[x][!A(x)]$ is satisfied, we have to determine
  if $\Sat{M}{\lnot \lforall[x][\lnot !A(x)]}[s]$. For instance, we
  have
  \[
  \Sat{M}{\lexists[x][(R(b,x) \lor R(x,b))]}[s].
  \]
  First, $\Sat{M}{R(b,x) \lor R(x, b)}[\Subst{s}{1}{x}]$
  ($\Subst{s}{3}{x}$ would also fit the bill).  So,
  $\Sat/{M}{\lnot(R(b,x) \lor R(x,b))}[\Subst{s}{1}{x}]$, thus
  $\Sat/{M}{\lforall[x][\lnot((R(b,x) \lor R(x,b))]}[s]$, and
  therefore $\Sat{M}{\lnot\lforall[x][\lnot((R(b,x) \lor
  R(x,b))]}[s]$. On the other hand,
  \[
  \Sat/{M}{\lexists[x][(R(b,x) \land R(x,b))],}[s].
  \]
  That's because $\Sat{M}{\lforall[x][\lnot(R(b,x) \land
  R(x,b))]}[s]$, since for no $m \in \Domain M$, $\Sat{M}{R(b,x) \land
  R(x,b)}[\Subst{s}{m}{x}]$. As you can probably guess from these
  examples, $\Sat{M}{\lexists[x][!A(x)]}[s]$ iff
  $\Sat{M}{!A(x)}[\Subst{s}{m}{x}]$ for at least one $m \in \Domain
  M$.}{}

\iftag{defAll}{To determine if a universally quantified
  !!{formula}~$\lforall[x][!A(x)]$ is satisfied, we have to determine
  if $\Sat{M}{\lnot\lexists[x][\lnot !A(x)]}[s]$. For instance,
  \[
  \Sat{M}{\lforall[x][(R(x,a) \lif R(a,x))]}[s],
  \]
  First, $\Sat{M}{R(x,a) \lif R(a,x)}[\Subst{s}{m}{x}]$ for all $m \in
  \Domain M$ ($\Sat{M}{R(a,x)}[\Subst{s}{1}{x}]$ and
  $\Sat/{M}{R(a,x)}[\Subst{s}{m}{x}]$ for $m = 2$, $3$, or~$4$).
  Thus, there is no $m \in \Domain M$ such that
  $\Sat{M}{\lnot(R(x,a) \lif R(a,x))}[\Subst{s}{m}{x}]$ and hence
  $\Sat/{M}{\lexists[x][\lnot(R(x,a) \lif R(a,x))]}[s]$. Therefore,
  $\Sat{M}{\lnot\lexists[x][\lnot(R(x,a) \lif R(a,x))]}[s]$. On the
  other hand,
  \[
  \Sat/{M}{\lforall[x][(R(a,x) \lif R(x,a))]}[s],
  \]
  since $\Sat/{M}{R(a,x) \lif R(x,a)}[\Subst{s}{2}{x}]$, and so
  $\Sat{M}{\lexists[x][\lnot(R(a,x) \lif R(x,a))]}[s]$. As you can
  probably guess from these examples, $\Sat{M}{\lforall[x][!A(x)]}[s]$
  iff $\Sat{M}{!A(x)}[\Subst{s}{m}{x}]$ for every $m \in \Domain
  M$.}{}

For a more complicated case, consider
\[
\lforall[x][(R(a,x) \lif \lexists[y][R(x,y)])].
\]
Since $\Sat/{M}{R(a,x)}[\Subst{s}{3}{x}]$ and
$\Sat/{M}{R(a,x)}[\Subst{s}{4}{x}]$, the interesting cases where we
have to worry about the consequent of the conditional are only $m = 1$
and $ = 2$. Does $\Sat{M}{\lexists[y][R(x,y)]}[\Subst{s}{1}{x}]$
hold? It does if there is at least one $n \in \Domain M$ so that
$\Sat{M}{R(x,y)}[\Subst{\Subst{s}{1}{x}}{n}{y}]$. In fact, if we take
$n = 1$, we have $\Subst{\Subst{s}{1}{x}}{n}{y} = \Subst{s}{1}{y} =
s$. Since $s(x) = 1$, $s(y) = 1$, and $\tuple{1,1} \in \Assign{R}{M}$,
the answer is yes. 

To determine if $\Sat{M}{\lexists[y][R(x,y)]}[\Subst{s}{2}{x}]$, we
have to look at the !!{variable} assignments
$\Subst{\Subst{s}{2}{x}}{n}{y}$. Here, for $n = 1$, this assignment
is~$s_2 = \Subst{s}{2}{x}$, which does not satisfy $R(x,y)$ ($s_2(x) =
2$, $s_2(y) = 1$, and $\tuple{2,1}\notin \Assign{R}{M}$). However,
consider $\Subst{\Subst{s}{2}{x}}{3}{y} = \Subst{s_2}{3}{y}$.
$\Sat{M}{R(x,y)}[\Subst{s_2}{3}{y}]$ since $\tuple{2,3} \in
\Assign{R}{M}$, and so $\Sat{M}{\lexists[y][R(x,y)]}[s_2]$.

So, for all $n \in \Domain M$, either
$\Sat/{M}{R(a,x)}[\Subst{s}{m}{x}]$ (if $m = 3$, $4$) or
$\Sat{M}{\lexists[y][R(x,y)]}[\Subst{s}{m}{x}]$ (if $m = 1$, $2$), and so
\[
\Sat{M}{\lforall[x][(R(a,x) \lif \lexists[y][R(x,y)])]}[s].
\]
On the other hand,
\[
\Sat/{M}{\lexists[x][(R(a,x) \land \lforall[y][R(x,y)])]}[s].
\]
We have $\Sat{M}{R(a,x)}[\Subst{s}{m}{x}]$ only for $m = 1$ and $m =
2$. But for both of these values of~$m$, there is in turn an $n \in
\Domain M$, namely $n = 4$, so that
$\Sat/{M}{R(x,y)}[\Subst{\Subst{s}{m}{x}}{n}{y}]$ and so
$\Sat/{M}{\lforall[y][R(x,y)]}[\Subst{s}{m}{x}]$ for $m = 1$ and $m =
2$. In sum, there is no $m \in \Domain M$ such that $\Sat{M}{R(a,x)
\land \lforall[y][R(x,y)]}[\Subst{s}{m}{x}]$.
\end{ex}

\iftag{defEx}{%
\begin{prop}\ollabel{prop:sat-ex}
$\Sat{M}{\lexists[x][!B(x)]}[s]$ iff there is an $x$-variant $s'$ of $s$
    so that $\Sat{M}{!B(x)}[s']$.
\end{prop}

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

\tagprob{defEx}
\begin{prob}
  Prove \olref[fol][syn][sat]{prop:sat-ex}
\end{prob}
\tagendprob

\iftag{defAll}{%
\begin{prop}\ollabel{prop:sat-all}
$\Sat{M}{\lforall[x][!B(x)]}[s]$ iff for every $x$-variant~$s'$ of $s$,
  $\Sat{M}{!B(x)}[s']$
\end{prop}

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

\tagprob{defAll}
\begin{prob}
  Prove \olref[fol][syn][sat]{prop:sat-all}
\end{prob}
\tagendprob

\begin{prob}
Let $\Lang L = \{c, f, A\}$ with one !!{constant}, one one-place
!!{function} and one two-place !!{predicate}, and let the
!!{structure}~$\Struct{M}$ be given by
\begin{enumerate}
\item $\Domain M = \{1, 2, 3\}$
\item $\Assign{c}{M} = 3$
\item $\Assign{f}{M}(1) = 2, \Assign{f}{M}(2) = 3, \Assign{f}{M}(3) = 2$
\item $\Assign{A}{M} = \{\tuple{1, 2}, \tuple{2, 3}, \tuple{3, 3}\}$
\end{enumerate}
(a) Let $s(v) = 1$ for all !!{variable}s~$v$.  Find out whether
\[
\Sat{M}{\lexists[x][(A(f(z), c) \lif \lforall[y][(A(y, x) \lor A(f(y),
      x))])]}[s]
\]
Explain why or why not.

(b) Give a different structure and !!{variable} assignment in which the
!!{formula} is not satisfied.
\end{prob}

\end{document}