satisfaction.tex

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

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

\begin{document}

\olfileid{sol}{syn}{sat}

\olsection{Satisfaction}

\begin{explain}
To define the satisfaction relation $\Sat{M}{!A}[s]$ for second-order
!!{formula}s, we have to extend the definitions to cover second-order
!!{variable}s.  The notion of !!a{structure} is the same for second-order
logic as it is for first-order logic. There is only a difference for
variable assignments~$s$: these now must not just provide values for
the first-order !!{variable}s, but also for the second-order !!{variable}s.
\end{explain}

\begin{defn}[Variable Assignment]
A \emph{variable assignment}~$s$ for !!a{structure}~$\Struct{M}$ is a
function which maps each
\begin{enumerate}
\item object !!{variable}~$\Obj{v_i}$ to an element of~$\Domain M$,
  i.e., $s(\Obj{v_i}) \in \Domain{M}$
\item $n$-place relation variable~$\Obj{V_i^n}$ to an $n$-place
  relation on~$\Domain{M}$, i.e., $s(\Obj{V_i^n}) \subseteq \Domain{M}^n$;
\item $n$-place function variable~$\Obj{u_i^n}$ to an $n$-place
  function from $\Domain{M}$ to $\Domain{M}$, i.e.,
  $s(\Obj{u_i^n})\colon \Domain{M}^n \to \Domain{M}$;
\end{enumerate}
\end{defn}

\begin{explain}
!!^a{structure} assigns !!a{value} to each !!{constant} and
!!{function}, and a second-order variable assignment assigns objects and
functions to each object and function variable. Together, they let us
assign a value to every term.
\end{explain}

\begin{defn}[\usetoken{S}{value} of a Term]
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
for first-order terms, plus the following clause:
\begin{quote}
\indcase{t}{\Atom{u}{t_1, \ldots, t_n}}{
\[
\Value{\indfrm}{M}[s] = s(u)(\Value{t_1}{M}[s], \ldots,
\Value{t_n}{M}[s]).
\]}
\end{quote}
\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}$. (Similarly for second-order variables $X$ or $u$.)
\end{defn}

\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}{y} = \begin{cases}
    m & \text{if } y \ident x\\
    s(y) & \text{otherwise},
  \end{cases}\]
  If $X$ is an $n$-place relation !!{variable} and $M \subseteq
  \Domain{M}^n$, then $\Subst{s}{M}{X}$ is the !!{variable} assignment
  defined by
  \[\Subst{s}{M}{y} = \begin{cases}
    M & \text{if } y \ident X\\
    s(y) & \text{otherwise}. 
  \end{cases}\]
  If $u$ is an $n$-place function !!{variable} and $f\colon \Domain{M}^n
  \to \Domain{M}$, then $\Subst{s}{f}{u}$ is the !!{variable} assignment
  defined by
  \[\Subst{s}{f}{y} = \begin{cases}
    f & \text{if } y \ident u\\
    s(y) & \text{otherwise}.
  \end{cases}\]
  In each case, $y$ may be any first- or second-order !!{variable}.
\end{defn}

\begin{defn}[Satisfaction]
For second-order !!{formula}s~$!A$, the definition of satisfaction is
like \olref[fol][syn][sat]{defn:satisfaction} with the addition of:
\begin{enumerate}
\item \indcase{!A}{\Atom{X^n}{t_1, \dots, t_n}}{$\Sat{M}{\indfrm}[s]$
  iff $\langle \Value{t_1}{M}[s], \dots, \Value{t_n}{M}[s] \rangle \in
  s(X^n)$.}
\tagitem{prvAll}{%
  \indcase{!A}{\lforall[X][!B]}{$\Sat{M}{\indfrm}[s]$ iff for every $M
  \subseteq \Domain{M}^n$, $\Sat{M}{!B}[\Subst{s}{M}{X}]$.}}{}

\tagitem{prvEx}{%
  \indcase{!A}{\lexists[X][!B]}{$\Sat{M}{\indfrm}[s]$ iff for at least
  one $M \subseteq \Domain{M}^n$ so that
  $\Sat{M}{!B}[\Subst{s}{M}{X}]$.}}{}

\tagitem{prvAll}{%
  \indcase{!A}{\lforall[u][!B]}{$\Sat{M}{\indfrm}[s]$ iff for every
  $f\colon \Domain{M}^n \to \Domain{M}$,
  $\Sat{M}{!B}[\Subst{s}{f}{u}]$.}}{}

\tagitem{prvEx}{%
  \indcase{!A}{\lexists[u][!B]}{$\Sat{M}{\indfrm}[s]$ iff for at least
  one $f\colon \Domain{M}^n \to \Domain{M}$ so that
  $\Sat{M}{!B}[\Subst{s}{f}{u}]$.}}{}
\end{enumerate}
\end{defn}

\begin{ex}
  Consider the !!{formula} $\lforall[z][(\Atom{X}{z} \liff \lnot
    \Atom{Y}{z})]$. It contains no second-order quantifiers, but does
  contain the second-order !!{variable}s $X$ and~$Y$ (here understood to
  be one-place). The corresponding first-order !!{sentence}
  $\lforall[z][(\Atom{P}{z} \liff \lnot \Atom{R}{z})]$ says that
  whatever falls under the interpretation of~$P$ does not fall under
  the interpretation of~$R$ and vice versa. In !!a{structure}, the
  interpretation of !!a{predicate}~$P$ is given by the
  interpretation~$\Assign{P}{M}$. But for second-order !!{variable}s
  like $X$ and~$Y$, the interpretation is provided, not by the
  !!{structure} itself, but by !!a{variable} assignment. Since the
  second-order !!{formula} is not !!a{sentence} (it includes free
  !!{variable}s $X$ and~$Y$), it is only satisfied relative to
  !!a{structure}~$\Struct{M}$ together with !!a{variable}
  assignment~$s$.

  $\Sat{M}{\lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})]}[s]$
  whenever the !!{element}s of~$s(X)$ are not !!{element}s of~$s(Y)$,
  and vice versa, i.e., iff $s(Y) = \Domain{M} \setminus s(X)$. For
  instance, take $\Domain{M} = \{1, 2, 3\}$. Since no !!{predicate}s,
  !!{function}s, or !!{constant}s are involved, the domain
  of~$\Struct{M}$ is all that is relevant. Now for $s_1(X) = \{1, 2\}$
  and $s_1(Y) = \{3\}$, we have $\Sat{M}{\lforall[z][(\Atom{X}{z}
      \liff \lnot \Atom{Y}{z})]}[s_1]$.

  By contrast, if we have $s_2(X) = \{1, 2\}$ and $s_2(Y) = \{2, 3\}$,
  $\Sat/{M}{\lforall[z][(\Atom{X}{z} \liff \lnot
      \Atom{Y}{z})]}[s_2]$. That's because 
  $\Sat{M}{\Atom{X}{z}}[\Subst{s_2}{2}{z}]$ (since $2 \in \Subst{s_2}{2}{z}(X)$) but
  $\Sat/{M}{\lnot \Atom{Y}{z}}[\Subst{s_2}{2}{z}]$ (since also $2 \in
  \Subst{s_2}{2}{z}(Y)$).
\end{ex}

\begin{ex}
  $\Sat{M}{\lexists[Y][(\lexists[y][\Atom{Y}{y}] \land
  \lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})])]}[s]$ if there
  is an $N \subseteq \Domain{M}$ such that
  $\Sat{M}{(\lexists[y][\Atom{Y}{y}] \land \lforall[z][(\Atom{X}{z}
  \liff \lnot \Atom{Y}{z})])}[\Subst{s}{N}{Y}]$. And that is the case
  for any $N \neq \emptyset$ (so that
  $\Sat{M}{\lexists[y][\Atom{Y}{y}]}[\Subst{s}{N}{Y}]$) and, as in the
  previous example, $N = \Domain{M} \setminus s(X)$. In other words,
  $\Sat{M}{\lexists[Y][(\lexists[y][\Atom{Y}{y}] \land
  \lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})])]}[s]$ iff
  $\Domain{M} \setminus s(X)$ is non-empty, i.e., $s(X) \neq
  \Domain{M}$. So, the !!{formula} is satisfied, e.g., if $\Domain{M}
  = \{1, 2, 3\}$ and $s(X) = \{1, 2\}$, but not if $s(X) = \{1, 2, 3\}
  = \Domain{M}$.

  Since the !!{formula} is not satisfied whenever $s(X) = \Domain{M}$,
  the !!{sentence}
  \[
  \lforall[X][\lexists[Y][(\lexists[y][\Atom{Y}{y}] \land
      \lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})])]]
  \]
  is never satisfied: For any !!{structure}~$\Struct{M}$, the
  assignment~$s(X) = \Domain{M}$ will make the !!{sentence} false. On
  the other hand, the sentence
  \[
  \lexists[X][\lexists[Y][(\lexists[y][\Atom{Y}{y}] \land
      \lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})])]]
  \]
  is satisfied relative to any assignment~$s$, since we can always
  find $M \subseteq \Domain{M}$ but $M \neq \Domain{M}$ (e.g., $M = \emptyset$).
\end{ex}

\begin{ex}
  The second-order !!{sentence}~$\lforall[X][\lforall[y][X(y)]]$ says
  that every $1$-place relation, i.e., every property, holds of every
  object. That is clearly never true, since in every~$\Struct{M}$, for
  a variable assignment~$s$ with $s(X) = \emptyset$, and $s(y) = a \in
  \Domain{M}$ we have $\Sat/{M}{X(y)}[s]$. This means that $!A \lif
  \lforall[X][\lforall[y][X(y)]]$ is equivalent in second-order logic
  to $\lnot !A$, that is: $\Sat{M}{!A \lif
  \lforall[X][\lforall[y][X(y)]]}$ iff $\Sat{M}{\lnot !A}$. In other
  words, in second-order logic we can define $\lnot$ using $\lforall$
  and~$\lif$.
\end{ex}

\begin{prob}
  Show that in second-order logic $\lforall$ and~$\lif$ can define the other
  connectives:
  \begin{enumerate}
    \item Prove that in second-order logic $!A \land !B$ is equivalent
    to $\lforall[X][(!A \lif (!B \lif \lforall[x][X(x)])\lif
    \lforall[x][X(x)])]$.
    \item Find a second-order formula using only $\lforall$ and $\lif$
    equivalent to $!A \lor !B$.
  \end{enumerate}
\end{prob}

\end{document}