Semantics of First-Order Logic — Source and provenance

Source and provenance

All 8 authority files and all 1,322 lines are shown exactly and copied byte-for-byte. Seven reader corrections, four bounded normalization decisions, and fifty-three exact normalization applications are disclosures only; the accepted projected text and authority source below are not altered. Open the exact accepted projected chapter transcript (SHA-256 1c6e2b5bc74625edc7496b795b1950956ee28f3d03a148e65624e592340a5299).

Seven disclosed reader corrections

The frozen source remains unchanged. These reviewed interventions are visible wherever affected material is presented.

occurrence-correction-projected-formula-0007228: The source writes only equals three after already naming the interpreted function value in the same sentence. The reader repeats f superscript M of x comma y so the isolated occurrence has its actual left-hand side.
occurrence-correction-projected-formula-0007240: The source appends the assignment marker s to the interpreted relation rather than to a satisfaction statement. The reader omits that stray assignment marker.
occurrence-correction-projected-formula-0007293: The source omits m from the second case in the phrase 'm equals one and m equals two.' The reader supplies m before equals two.
occurrence-correction-projected-formula-0007401: The source starts the argument-value tuple with t sub i although the displayed sequence runs from the first through the k-th term. The reader uses t sub one.
TR017-SOURCE-PROSE-001: a structure for the set-theory language requires a set and a single two-place relation.
TR017-SOURCE-PROSE-002: for every m in the domain of M, either the antecedent fails or the existential consequent holds.
TR017-SOURCE-PROSE-003: If Gamma is a set of sentences, we say that.

content/first-order-logic/syntax-and-semantics/semantics.tex

26 lines; SHA-256 d863c375746602be962b1b45545d8a51e72f9d0d9dca516f434152131b4107ec. Open the byte-exact preserved source file.

% Part: first-order-logic
% Chapter: semantics
\documentclass[../../../include/open-logic-chapter]{subfiles}
\begin{document}
\olchapter{fol}{sem}{Semantics of First-Order Logic}
\olimport{intro-semantics}
\olimport{structures}
\olimport{covered-structures}
\olimport{satisfaction}
\olimport{assignments}
\olimport{extensionality}
\olimport{semantic-notions}
\OLEndChapterHook
\end{document}

content/first-order-logic/syntax-and-semantics/intro-semantics.tex

47 lines; SHA-256 0bcf5a399c46716183aba26ed6d331abae45bdb63ed5bb26b3a7085b840e86e4. Open the byte-exact preserved source file.

% Part: first-order-logic
% Chapter: semantics
% Section: intro-semantics
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\olfileid{fol}{syn}{its}
\olsection{Introduction}
Giving the meaning of expressions is the domain of semantics. The
central concept in semantics is that of satisfaction in
!!a{structure}. !!^a{structure} gives meaning to the building blocks
of the language: !!a{domain} is a non-empty set of objects. The
quantifiers are interpreted as ranging over this domain, !!{constant}s
are assigned elements in the domain, !!{function}s are assigned
functions from the !!{domain} to itself, and !!{predicate}s are
assigned relations on the !!{domain}. The !!{domain} together with
assignments to the basic vocabulary constitutes !!a{structure}.
!!^{variable}s may appear in !!{formula}s, and in order to give a
semantics, we also have to assign !!{element}s of the !!{domain} to
them---this is a variable assignment. The satisfaction relation,
finally, brings these together. !!^a{formula} may be satisfied in
!!a{structure}~$\Struct{M}$ relative to !!a{variable} assignment~$s$,
written as $\Sat{M}{!A}[s]$. This relation is also defined by
induction on the structure of~$!A$, using the truth tables for the
logical connectives to define, say, satisfaction of $(!A \land !B)$ in
terms of satisfaction (or not) of $!A$ and ~$!B$. It then turns out
that the !!{variable} assignment is irrelevant if the !!{formula}~$!A$
is !!a{sentence}, i.e., has no free variables, and so we can talk of
!!{sentence}s being simply satisfied (or not) in !!{structure}s.
On the basis of the satisfaction relation $\Sat{M}{!A}$ for !!{sentence}s
we can then define the basic semantic notions of validity, entailment,
and satisfiability. !!^a{sentence} is valid, $\Entails !A$, if every
!!{structure} satisfies it. It is entailed by a set of !!{sentence}s,
$\Gamma \Entails !A$, if every !!{structure} that satisfies all the
!!{sentence}s in~$\Gamma$ also satisfies~$!A$. And a set of !!{sentence}s
is satisfiable if some !!{structure} satisfies all !!{sentence}s in it
at the same time. Because !!{formula}s are inductively defined, and
satisfaction is in turn defined by induction on the structure of
!!{formula}s, we can use induction to prove properties of our
semantics and to relate the semantic notions defined.
\end{document}

content/first-order-logic/syntax-and-semantics/structures.tex

109 lines; SHA-256 653be0fbc8ef1d61d9f39e7515bd1b1b1911f42147e0131a3235670e677cc241. Open the byte-exact preserved source file.

% Part: first-order-logic
% Chapter: syntax-and-semantics
% Section: Structures
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\olfileid{fol}{syn}{str}
\olsection{\printtoken{P}{structure} for First-order Languages}
\begin{explain}
First-order languages are, by themselves, \emph{uninterpreted:} the
!!{constant}s, !!{function}s, and !!{predicate}s have no specific
meaning attached to them. Meanings are given by specifying
\article{structure} \emph{!!{structure}}. It specifies the
\emph{domain}, i.e., the objects which the !!{constant}s pick out, the
!!{function}s operate on, and the quantifiers range over. In addition,
it specifies which !!{constant}s pick out which objects, how
!!a{function} maps objects to objects, and which objects the
!!{predicate}s apply to. !!^{structure}s are the basis for
\emph{semantic} notions in logic, e.g., the notion of consequence,
validity, satisfiability. They are variously called ``structures,''
``interpretations,'' or ``models'' in the literature.
\end{explain}
\begin{defn}[!!^{structure}s]
\Article{structure} \emph{!!{structure}}~$\Struct M$, for a language
$\Lang{L}$ of first-order logic consists of the following elements:
\begin{enumerate}
\item \emph{Domain:} a non-empty set, $\Domain M$
\item \emph{Interpretation of !!{constant}s:} for each !!{constant}~$c$ of
$\Lang{L}$, !!a{element} $\Assign{c}{M} \in \Domain M$
\item \emph{Interpretation of !!{predicate}s:} for each $n$-place
!!{predicate}~$R$ of $\Lang{L}$ (other than $\eq$), an $n$-place
relation $\Assign{R}{M} \subseteq \Domain{M}^n$
\item \emph{Interpretation of !!{function}s:} for each $n$-place
!!{function}~$f$ of $\Lang{L}$, an $n$-place function $\Assign{f}{M}
\colon \Domain{M}^n \to \Domain{M}$
\end{enumerate}
\end{defn}
\begin{ex}
!!^a{structure}~$\Struct M$ for the language of arithmetic consists of a
set, an element of $\Domain M$, $\Assign{\Obj 0}{M}$, as
interpretation of the !!{constant}~$\Obj 0$, a one-place function
$\Assign{\Obj \prime}{M} \colon \Domain{M} \to \Domain M$, two
two-place functions $\Assign{\Obj +}{M}$ and $\Assign{\Obj
\times}{M}$, both $\Domain M^2 \to \Domain M$, and a two-place
relation $\Assign{\Obj <}{M} \subseteq \Domain{M}^2$.
An obvious example of such a structure is the following:
\begin{enumerate}
\item $\Domain N = \Nat$
\item $\Assign{\Obj 0}{N} = 0$
\item $\Assign{\Obj \prime}{N}(n) = n + 1$ for all $n \in \Nat$
\item $\Assign{\Obj +}{N}(n, m) = n + m$ for all $n, m \in \Nat$
\item $\Assign{\Obj \times}{N}(n, m) = n\cdot m$ for all $n, m \in \Nat$
\item $\Assign{\Obj <}{N} = \Setabs{\tuple{n, m}}{n \in \Nat, m \in
\Nat, n < m}$
\end{enumerate}
The structure~$\Struct N$ for $\Lang L_A$ so defined is called the
\emph{standard model of arithmetic}, because it interprets the
non-logical constants of~$\Lang L_A$ exactly how you would expect.
However, there are many other possible !!{structure}s for~$\Lang
L_A$. For instance, we might take as the domain the set~$\Int$ of
integers instead of~$\Nat$, and define the interpretations of $\Obj
0$, $\Obj \prime$, $\Obj +$, $\Obj \times$, $\Obj <$ accordingly. But
we can also define structures for~$\Lang L_A$ which have nothing even
remotely to do with numbers.
\end{ex}
\begin{ex}
A structure~$\Struct M$ for the language~$\Lang L_Z$ of set theory requires
just a set and a single-two place relation. So technically, e.g., the
TR017-SOURCE-PROSE-001: a structure for the set-theory language requires a set and a single two-place relation.
set of people plus the relation ``$x$ is older than $y$'' could be
used as !!a{structure} for $\Lang L_Z$, as well as $\Nat$ together
with $n \ge m$ for $n, m \in \Nat$.
A particularly interesting !!{structure} for $\Lang L_Z$ in which the
!!{element}s of the domain are actually sets, and the interpretation
of $\Obj \in$ actually is the relation ``$x$ is !!a{element} of~$y$''
is the !!{structure}~$\Struct{{HF}}$ of \emph{hereditarily finite sets}:
\begin{enumerate}
\item $\Domain{{{HF}}} = \emptyset \cup \Pow{\emptyset} \cup
\Pow{\Pow{\emptyset}} \cup \Pow{\Pow{\Pow{\emptyset}}} \cup \dots$;
\item $\Assign{\Obj \in}{{{HF}}} = \Setabs{\tuple{x, y}}{x, y \in
\Domain{{{HF}}}, x \in y}$.
\end{enumerate}
\end{ex}
\begin{digress}
The stipulations we make as to what counts as !!a{structure} impact
our logic. For example, the choice to prevent empty domains ensures,
given the usual account of satisfaction (or truth) for quantified
sentences, that $\lexists[x][(!A(x) \lor \lnot !A(x))]$ is
valid---that is, a logical truth. And the stipulation that all
!!{constant}s must refer to an object in the domain ensures that the
existential generalization is a sound pattern of inference: $!A(a)$,
therefore $\lexists[x][!A(x)]$. If we allowed names to refer outside
the domain, or to not refer, then we would be on our way to a
\emph{free logic}, in which existential generalization requires an
additional premise: $!A(a)$ and $\lexists[x][\eq[x][a]]$, therefore
$\lexists[x][!A(x)]$.
\end{digress}
\end{document}

content/first-order-logic/syntax-and-semantics/covered-structures.tex

72 lines; SHA-256 47b8c3e2f2455d6fdefbf11157cae904e95c858545997fd9b22e7a2a8a1948d7. Open the byte-exact preserved source file.

% Part: first-order-logic
% Chapter: syntax-and-semantics
% Section: covered-structures
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\olfileid{fol}{syn}{cov}
\olsection{Covered \printtoken{P}{structure} for First-order Languages}
\begin{explain}
Recall that a term is \emph{closed} if it contains no !!{variable}s.
\end{explain}
\begin{defn}[!!^{value} of closed terms]
If $t$ is a closed term of the language~$\Lang L$ and $\Struct M$ is a
!!{structure} for~$\Lang L$, the \emph{!!{value}}~$\Value{t}{M}$ is
defined as follows:
\begin{enumerate}
\item If $t$ is just the !!{constant}~$c$, then $\Value{c}{M} = \Assign{c}{M}$.
\item If $t$ is of the form $\Atom{f}{t_1, \ldots, t_n}$, then
\[
\Value{t}{M} = \Assign{f}{M}(\Value{t_1}{M}, \ldots,
\Value{t_n}{M}).
\]
\end{enumerate}
\end{defn}
\begin{defn}[Covered !!{structure}]
A !!{structure} is \emph{covered} if every element of the domain is the
!!{value} of some closed term.
\end{defn}
\begin{ex}
Let ~$\Lang L$ be the language with !!{constant}s $\Obj{zero}$,
$\Obj{one}$, $\Obj{two}$, \dots, the binary !!{predicate}~$<$, and the
binary !!{function}s $+$ and $\times$. Then !!a{structure}~$\Struct
M$ for~$\Lang L$ is the one with domain $\Domain M = \{0, 1, 2, \ldots
\}$ and assignments $\Assign{\Obj{zero}}{M} = 0$,
$\Assign{\Obj{one}}{M} = 1$, $\Assign{\Obj{two}}{M} = 2$, and so
forth. For the binary relation symbol $<$, the set $\Assign{<}{M}$ is
the set of all pairs $\tuple{c_1, c_2} \in \Domain{M}^2$ such that
$c_1$ is less than~$c_2$: for example, $\tuple{1, 3} \in
\Assign{<}{M}$ but $\tuple{2, 2} \notin \Assign{<}{M}$. For the binary
!!{function} $+$, define $\Assign{+}{M}$ in the usual way---for
example, $\Assign{+}{M}(2,3)$ maps to~$5$, and similarly for the
binary !!{function}~$\times$. Hence, the !!{value} of $\Obj{four}$ is
just~$4$, and the !!{value} of $\times(\Obj{two},
+(\Obj{three},\Obj{zero}))$ (or in infix notation, $\Obj{two} \times
(\Obj{three} + \Obj{zero})$) is
\begin{multline*}
\Value{\times(\Obj{two}, +(\Obj{three},\Obj{zero}))}{M} =\\
\begin{aligned}
& =\Assign{\times}{M}(\Value{\Obj{two}}{M}, \Value{+(\Obj{three}, \Obj{zero})}{M})\\
& = \Assign{\times}{M}(\Value{\Obj{two}}{M}, \Assign{+}{M}(\Value{\Obj{three}}{M},
\Value{\Obj{zero}}{M})) \\
& = \Assign{\times}{M}(\Assign{\Obj{two}}{M}, \Assign{+}{M}(\Assign{\Obj{three}}{M},
\Assign{\Obj{zero}}{M})) \\
& = \Assign{\times}{M}(2, \Assign{+}{M}(3, 0)) \\
& = \Assign{\times}{M}(2, 3) \\
& = 6
\end{aligned}
\end{multline*}
\end{ex}
\begin{prob}
Is $\Struct N$, the standard model of arithmetic, covered? Explain.
\end{prob}
\end{document}

content/first-order-logic/syntax-and-semantics/satisfaction.tex

421 lines; SHA-256 e44b0bea8c5d130077516bc8d757f46d4b337517aab77049841581313820fd32. Open the byte-exact preserved source file.

% 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.
occurrence-correction-projected-formula-0007228: The source writes only equals three after already naming the interpreted function value in the same sentence. The reader repeats f superscript M of x comma y so the isolated occurrence has its actual left-hand side.
\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]$.
occurrence-correction-projected-formula-0007240: The source appends the assignment marker s to the interpreted relation rather than to a satisfaction statement. The reader omits that stray assignment marker.
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}]$
occurrence-correction-projected-formula-0007293: The source omits m from the second case in the phrase 'm equals one and m equals two.' The reader supplies m before equals two.
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
TR017-SOURCE-PROSE-002: for every m in the domain of M, either the antecedent fails or the existential consequent holds.
$\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}

content/first-order-logic/syntax-and-semantics/assignments.tex

353 lines; SHA-256 158d852e2ead50b060a48332cac8c72c475cfc206d3dab7aac24a01be3ff1771. Open the byte-exact preserved source file.

% Part: first-order-logic
% Chapter: syntax-and-semantics
% Section: assignments
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\olfileid{fol}{syn}{ass}
\olsection{Variable Assignments}
\begin{explain}
A !!{variable} assignment~$s$ provides a value for \emph{every}
variable---and there are infinitely many of them. This is of course
not necessary. We require !!{variable} assignments to assign values to
all !!{variable}s simply because it makes things a lot easier. The
value of a term~$t$, and whether or not !!a{formula}~$!A$ is
satisfied in !!a{structure} with respect to~$s$, only depend on the
assignments~$s$ makes to the !!{variable}s in~$t$ and the free
!!{variable}s of~$!A$. This is the content of the next two
propositions. To make the idea of ``depends on'' precise, we show
that any two variable assignments that agree on all the variables
in~$t$ give the same value, and that $!A$ is satisfied relative to one
iff it is satisfied relative to the other if two variable assignments
agree on all free variables of~$!A$.
\end{explain}
\begin{prop}\ollabel{prop:valindep}
If the !!{variable}s in a term~$t$ are among $x_1$, \dots,~$x_n$, and
$s_1(x_i) = s_2(x_i)$ for $i = 1$, \dots,~$n$, then $\Value{t}{M}[s_1]
= \Value{t}{M}[s_2]$.
\end{prop}
\begin{proof}
By induction on the complexity of~$t$. For the base case, $t$ can be
!!a{constant} or one of the variables~$x_1$, \dots,~$x_n$. If $t
= c$, then $\Value{t}{M}[s_1] = \Assign{c}{M} = \Value{t}{M}[s_2]$. If
$t = x_i$, $s_1(x_i) = s_2(x_i)$ by the hypothesis of the proposition,
and so $\Value{t}{M}[s_1] = s_1(x_i) = s_2(x_i) = \Value{t}{M}[s_2]$.
For the inductive step, assume that $t = \Atom{f}{t_1, \dots, t_k}$
and that the claim holds for $t_1$, \dots, $t_k$. Then
\begin{align*}
\Value{t}{M}[s_1] & = \Value{\Atom{f}{t_1, \dots, t_k}}{M}[s_1] \\
& = \Assign{f}{M}(\Value{t_1}{M}[s_1], \dots, \Value{t_k}{M}[s_1]).
\intertext{For $j = 1$, \dots,~$k$, the !!{variable}s of~$t_j$ are
among $x_1$, \dots,~$x_n$. By the induction hypothesis,
$\Value{t_j}{M}[s_1] = \Value{t_j}{M}[s_2]$. So,}
\Value{t}{M}[s_1] & = \Value{\Atom{f}{t_1, \dots, t_k}}{M}[s_1] \\
& = \Assign{f}{M}(\Value{t_1}{M}[s_1], \dots, \Value{t_k}{M}[s_1]) \\
& = \Assign{f}{M}(\Value{t_1}{M}[s_2], \dots, \Value{t_k}{M}[s_2]) \\
& = \Value{\Atom{f}{t_1, \dots, t_k}}{M}[s_2] = \Value{t}{M}[s_2].
\end{align*}
\end{proof}
\begin{prop}\ollabel{prop:satindep}
If the free !!{variable}s in $!A$ are among $x_1$, \dots,~$x_n$, and
$s_1(x_i) = s_2(x_i)$ for $i = 1$, \dots,~$n$, then $\Sat{M}{!A}[s_1]$
iff $\Sat{M}{!A}[s_2]$.
\end{prop}
\begin{proof}
We use induction on the complexity of $!A$. For the base case, where
$!A$ is atomic, $!A$ can be:
\iftag{prvTrue}{$\ltrue$,}{}
\iftag{prvFalse}{$\lfalse$,}{}
$\Atom{R}{t_1, \dots, t_k}$ for a $k$-place predicate $R$ and terms
$t_1$, \dots,~$t_k$, or $\eq[t_1][t_2]$ for terms $t_1$ and~$t_2$.
In the latter two cases, we only demonstrate the forward direction of
the !!{biconditional}, since the proof of the reverse is symmetrical.
\begin{enumerate}
\tagitem{prvTrue}{%
\indcase{!A}{\ltrue}{both $\Sat{M}{\indfrm}[s_1]$ and
$\Sat{M}{\indfrm}[s_2]$.}}{}
\tagitem{prvFalse}{%
\indcase{!A}{\lfalse}{both $\Sat/{M}{!A}[s_1]$ and
$\Sat/{M}{!A}[s_2]$.}}{}
\item
\indcase{!A}{\Atom{R}{t_1, \ldots, t_k}}{let
$\Sat{M}{\indfrm}[s_1]$. Then
\[
\langle \Value{t_1}{M}[s_1], \ldots, \Value{t_k}{M}[s_1] \rangle
\in \Assign{R}{M}.
\]
For $i = 1$, \dots,~$k$, $\Value{t_i}{M}[s_1] =
\Value{t_i}{M}[s_2]$ by \olref{prop:valindep}. So we also have
$\langle \Value{t_i}{M}[s_2], \ldots, \Value{t_k}{M}[s_2] \rangle
occurrence-correction-projected-formula-0007401: The source starts the argument-value tuple with t sub i although the displayed sequence runs from the first through the k-th term. The reader uses t sub one.
\in \Assign{R}{M}$, and hence $\Sat{M}{\indfrm}[s_2]$.}
\item
\indcase{!A}{\eq[t_1][t_2]}{suppose $\Sat{M}{\indfrm}[s_1]$.
Then $\Value{t_1}{M}[s_1] = \Value{t_2}{M}[s_1]$. So,
\begin{align*}
\Value{t_1}{M}[s_2] & = \Value{t_1}{M}[s_1]
& \text{(by \olref{prop:valindep})} \\
& = \Value{t_2}{M}[s_1]
& \text{(since $\Sat{M}{\eq[t_1][t_2]}[s_1]$)}\\
&= \Value{t_2}{M}[s_2]
& \text{(by \olref{prop:valindep}),}
\end{align*}
so $\Sat{M}{\eq[t_1][t_2]}[s_2]$.}
\end{enumerate}
Now assume $\Sat{M}{!B}[s_1]$ iff $\Sat{M}{!B}[s_2]$ for all
!!{formula}s $!B$ less complex than~$!A$. The induction step proceeds
by cases determined by the main operator of~$!A$. In each case, we
only demonstrate the forward direction of the !!{biconditional}; the
proof of the reverse direction is symmetrical. In all cases except
those for the quantifiers, we apply the induction hypothesis to
sub-!!{formula}s~$!B$ of~$!A$. The free variables of~$!B$ are among
those of~$!A$. Thus, if $s_1$ and $s_2$ agree on the free variables
of~$!A$, they also agree on those of~$!B$, and the induction
hypothesis applies to~$!B$.
\begin{enumerate}
\tagitem{defNot}{}{%
\iftag{probNot}{%
\indcase!{!A}{\lnot !B}{}}{%
\indcase{!A}{\lnot !B}{if $\Sat{M}{\indfrm}[s_1]$, then
$\Sat/{M}{!B}[s_1]$, so by the induction hypothesis,
$\Sat/{M}{!B}[s_2]$, hence $\Sat{M}{\indfrm}[s_2]$.}}}
\tagitem{defAnd}{}{%
\iftag{probAnd}{%
\indcase!{!A}{!B \land !C}{}}{%
\indcase{!A}{!B \land !C}{if $\Sat{M}{\indfrm}[s_1]$, then
$\Sat{M}{!B}[s_1]$ and $\Sat{M}{!C}[s_1]$, so by induction
hypothesis, $\Sat{M}{!B}[s_2]$ and $\Sat{M}{!C}[s_2]$. Hence,
$\Sat{M}{\indfrm}[s_2]$.}}}
\tagitem{defOr}{}{%
\iftag{probOr}{%
\indcase!{!A}{!B \lor !C}{}}{%
\indcase{!A}{!B \lor !C}{if $\Sat{M}{\indfrm}[s_1]$, then
$\Sat{M}{!B}[s_1]$ or $\Sat{M}{!C}[s_1]$. By induction hypothesis,
$\Sat{M}{!B}[s_2]$ or $\Sat{M}{!C}[s_2]$, so $\Sat{M}{\indfrm}[s_2]$.}}}
\tagitem{defIf}{}{%
\iftag{probIf}{%
\indcase!{!A}{!B \lif !C}{}}{%
\indcase{!A}{!B \lif !C}{if $\Sat{M}{\indfrm}[s_1]$, then
$\Sat/{M}{!B}[s_1]$ or $\Sat{M}{!C}[s_1]$. By the induction hypothesis,
$\Sat/{M}{!B}[s_2]$ or $\Sat{M}{!C}[s_2]$, so $\Sat{M}{\indfrm}[s_2]$.}}}
\tagitem{defIff}{}{%
\iftag{probIff}{%
\indcase!{!A}{!B \liff !C}{}}{%
\indcase{!A}{!B \liff !C}{if $\Sat{M}{\indfrm}[s_1]$, then either
$\Sat{M}{!B}[s_1]$ and $\Sat{M}{!C}[s_1]$, or $\Sat/{M}{!B}[s_1]$ and
$\Sat/{M}{!C}[s_1]$. By the induction hypothesis, either
$\Sat{M}{!B}[s_2]$ and $\Sat{M}{!C}[s_2]$ or $\Sat/{M}{!B}[s_2]$
and $\Sat/{M}{!C}[s_2]$. In either case, $\Sat{M}{\indfrm}[s_2]$.}}}
\tagitem{defEx}{}{%
\iftag{probEx}{%
\indcase!{!A}{\lexists[x][!B]}{}}{%
\indcase{!A}{\lexists[x][!B]}{if $\Sat{M}{\indfrm}[s_1]$, there is
an $m \in \Domain{M}$ so that $\Sat{M}{!B}[\Subst{s_1}{m}{x}]$.
Let $s_1' = \Subst{s_1}{m}{x}$ and $s_2' =
\Subst{s_2}{m}{x}$. The free variables of~$!B$ are among $x_1$,
\dots, $x_n$, and $x$. $s_1'(x_i) = s_2'(x_i)$, since $s_1'$ and
$s_2'$ are $x$-variants of $s_1$ and~$s_2$, respectively, and by
hypothesis $s_1(x_i) = s_2(x_i)$. $s_1'(x) = s_2'(x) = m$ by the
way we have defined $s_1'$ and~$s_2'$. Then the induction
hypothesis applies to $!B$ and $s_1'$, $s_2'$, so
$\Sat{M}{!B}[s_2']$. Hence, since $s_2' = \Subst{s_2}{m}{x}$,
there is an $m \in \Domain{M}$ such that
$\Sat{M}{!B}[\Subst{s_2}{m}{x}]$, and so
$\Sat{M}{\indfrm}[s_2]$.}}}
\tagitem{defAll}{}{%
\iftag{probAll}{%
\indcase!{!A}{\lforall[x][!B]}{}}{%
\indcase{!A}{\lforall[x][!B]}{if $\Sat{M}{\indfrm}[s_1]$, then for
every $m \in \Domain{M}$, $\Sat{M}{!B}[\Subst{s_1}{m}{x}]$. We
want to show that also, for every $m \in \Domain{M}$,
$\Sat{M}{!B}[\Subst{s_2}{m}{x}]$. So let $m \in \Domain{M}$ be
arbitrary, and consider $s_1' = \Subst{s}{m}{x}$ and $s_2' =
\Subst{s}{m}{x}$. We have that $\Sat{M}{!B}[s_1']$. The free
variables of~$!B$ are among $x_1$, \dots, $x_n$, and $x$.
$s_1'(x_i) = s_2'(x_i)$, since $s_1'$ and $s_2'$ are
$x$-variants of $s_1$ and~$s_2$, respectively, and by hypothesis
$s_1(x_i) = s_2(x_i)$. $s_1'(x) = s_2'(x) = m$ by the way we
have defined $s_1'$ and~$s_2'$. Then the induction hypothesis
applies to~$!B$ and~$s_1'$, $s_2'$, and we have
$\Sat{M}{!B}[s_2']$. This applies to every $m \in \Domain{M}$,
i.e., $\Sat{M}{!B}[\Subst{s_2}{m}{x}]$ for all~$m \in
\Domain{M}$, so $\Sat{M}{\indfrm}[s_2]$.}}}
\end{enumerate}
By induction, we get that $\Sat{M}{!A}[s_1]$ iff $\Sat{M}{!A}[s_2]$
whenever the free !!{variable}s in $!A$ are among $x_1$, \dots, $x_n$
and $s_1(x_i)=s_2(x_i)$ for $i = 1$, \dots,~$n$.
\end{proof}
\begin{probtag}{probNot,probOr,probAnd,probIf,probIff,probEx,probAll}
Complete the proof of \olref[fol][syn][ass]{prop:satindep}.
\end{probtag}
\begin{explain}
!!^{sentence}s have no free variables, so any two variable assignments
assign the same things to all the (zero) free variables of any
sentence. The proposition just proved then means that whether or not
!!a{sentence} is satisfied in a structure relative to a variable
assignment is completely independent of the assignment. We'll record
this fact. It justifies the definition of satisfaction of
!!a{sentence} in !!a{structure} (without mentioning a variable
assignment) that follows.
\end{explain}
\begin{cor}
\ollabel{cor:sat-sentence}
If $!A$ is !!a{sentence} and $s$ a variable assignment, then
$\Sat{M}{!A}[s]$ iff $\Sat{M}{!A}[s']$ for every variable
assignment~$s'$.
\end{cor}
\begin{proof}
Let $s'$ be any variable assignment. Since $!A$ is !!a{sentence}, it
has no free variables, and so every variable assignment~$s'$
trivially assigns the same things to all free variables of~$!A$ as
does~$s$. So the condition of \olref{prop:satindep} is satisfied,
and we have $\Sat{M}{!A}[s]$ iff $\Sat{M}{!A}[s']$.
\end{proof}
\begin{defn}
\ollabel{defn:satisfaction}
If $!A$ is !!a{sentence}, we say that !!a{structure}~$\Struct M$
\emph{satisfies}~$!A$, $\Sat{M}{!A}$, iff $\Sat{M}{!A}[s]$ for all
variable assignments~$s$.
\end{defn}
If $\Sat{M}{!A}$, we also simply say that \emph{$!A$ is true
in~$\Struct{M}$.} The notion of satisfaction naturally extends
from individual !!{sentence}s to sets of !!{sentence}s.
\begin{defn}
\ollabel{defn:sat}
If $\Gamma$ is a set of !!{sentence}s~$\Gamma$, we say that
TR017-SOURCE-PROSE-003: If Gamma is a set of sentences, we say that.
!!a{structure}~$\Struct M$ \emph{satisfies}~$\Gamma$,
$\Sat{M}{\Gamma}$, iff $\Sat{M}{!A}$ for all $!A \in \Gamma$.
\end{defn}
\begin{prop}\ollabel{prop:sentence-sat-true}
Let $\Struct{M}$ be !!a{structure}, $!A$ be !!a{sentence}, and $s$ a
variable assignment. $\Sat{M}{!A}$ iff $\Sat{M}{!A}[s]$.
\end{prop}
\begin{proof}
Exercise.
\end{proof}
\begin{prob}
Prove \olref[fol][syn][ass]{prop:sentence-sat-true}
\end{prob}
\begin{prop}\ollabel{prop:sat-quant}
Suppose $!A(x)$ only contains $x$ free, and $\Struct M$ is
!!a{structure}. Then:
\begin{tagenumerate}{prvEx,prvAll}
\tagitem{prvEx}{$\Sat{M}{\lexists[x][!A(x)]}$ iff $\Sat{M}{!A(x)}[s]$
for at least one variable assignment~$s$.}{}
\tagitem{prvAll}{$\Sat{M}{\lforall[x][!A(x)]}$ iff $\Sat{M}{!A(x)}[s]$
for all variable assignments~$s$.}{}
\end{tagenumerate}
\end{prop}
\begin{proof}
Exercise.
\end{proof}
\begin{prob}
Prove \olref[fol][syn][ass]{prop:sat-quant}.
\end{prob}
\begin{prob}
\DeclareRobustCommand{\VDash}{\mathrel{||}\joinrel\Relbar}
Suppose $\Lang L$ is a language without !!{function}s. Given a
!!{structure}~$\Struct M$, $c$ !!a{constant} and $a \in \Domain M$,
define $\Struct M[a/c]$ to be the !!{structure} that is just
like~$\Struct M$, except that $\Assign{c}{M[a/c]} = a$. Define
$\Struct M \VDash !A$ for !!{sentence}s~$!A$ by:
\begin{enumerate}
\tagitem{prvFalse}{%
\indcase{!A}{\lfalse}{not $\Struct{M} \VDash \indfrm$.}}{}
\tagitem{prvTrue}{%
\indcase{!A}{\ltrue}{$\Struct{M} \VDash \indfrm$.}}{}
\item \indcase{!A}{\Atom{R}{d_1, \dots, d_n}}{$\Struct M \VDash \indfrm$
iff $\langle \Assign{d_1}{M}, \dots, \Assign{d_n}{M} \rangle \in
\Assign{R}{M}$.}
\item \indcase{!A}{\eq[d_1][d_2]}{$\Struct M \VDash \indfrm$ iff
$\Assign{d_1}{M} = \Assign{d_2}{M}$.}
\tagitem{prvNot}{%
\indcase{!A}{\lnot !B}{$\Struct{M} \VDash \indfrm$ iff
not $\Struct{M} \VDash {!B}$.}}{}
\tagitem{prvAnd}{%
\indcase{!A}{(!B \land !C)}{$\Struct{M} \VDash
\indfrm$ iff $\Struct{M} \VDash!B$ and $\Struct{M} \VDash !C$.}}{}
\tagitem{prvOr}{%
\indcase{!A}{(!B \lor !C)}{$\Struct{M} \VDash \indfrm$ iff
$\Struct{M} \VDash !B$ or $\Struct{M} \VDash !C$ (or both).}}{}
\tagitem{prvIf}{%
\indcase{!A}{(!B \lif !C)}{$\Struct{M} \VDash \indfrm$ iff
not $\Struct {M} \VDash !B$ or $\Struct M \VDash !C$ (or both).}}{}
\tagitem{prvIff}{%
\indcase{!A}{(!B \liff !C)}{$\Struct{M} \VDash {\indfrm}$ iff either
both $\Struct{M} \VDash {!B}$ and $\Struct{M} \VDash {!C}$, or
neither $\Struct{M} \VDash {!B}$ nor $\Struct{M} \VDash {!C}$.}}{}
\tagitem{prvAll}{%
\indcase{!A}{\lforall[x][!B]}{$\Struct{M} \VDash {\indfrm}$ iff for
all $a \in \Domain{M}$, $\Struct{M[a/c]} \VDash \Subst{!B}{c}{x}$,
if $c$ does not occur in~$!B$.}}{}
\tagitem{prvEx}{%
\indcase{!A}{\lexists[x][!B]}{$\Struct{M} \VDash
{\indfrm}$ iff there is an $a \in \Domain M$ such that
$\Struct{M[a/c]} \VDash \Subst{!B}{c}{x}$, if $c$ does not occur
in~$!B$.}}{}
\end{enumerate}
Let $x_1$, \dots, $x_n$ be all free !!{variable}s in~$!A$,
$c_1$, \dots, $c_n$ constant symbols not in~$!A$,
$a_1$, \dots, $a_n \in \Domain M$, and $s(x_i) = a_i$.
Show that $\Sat{M}{!A}[s]$ iff $\Struct M[a_1/c_1,\dots,a_n/c_n]
\VDash \Subst{\Subst{!A}{c_1}{x_1}\dots}{c_n}{x_n}$.
(This problem shows that it is possible to give a semantics for
first-order logic that makes do without variable assignments.)
\end{prob}
\begin{prob}
Suppose that $f$ is a function symbol not in~$!A(x,y)$. Show that
there is !!a{structure}~$\Struct{M}$ such that
$\Sat{M}{\lforall[x][\lexists[y][!A(x,y)]]}$ iff there is an~$\Struct
M'$ such that $\Sat{M'}{\lforall[x][!A(x,f(x))]}$.
(This problem is a special case of what's known as Skolem's Theorem;
$\lforall[x][!A(x,f(x))]$ is called a \emph{Skolem normal form} of
$\lforall[x][\lexists[y][!A(x,y)]]$.)
\end{prob}
\end{document}

content/first-order-logic/syntax-and-semantics/extensionality.tex

137 lines; SHA-256 b96be00c844c1a06be3dc8c18e237fdb595ed60b18462b01bca43e6886d1da4d. Open the byte-exact preserved source file.

% 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}

content/first-order-logic/syntax-and-semantics/semantic-notions.tex

157 lines; SHA-256 8b8740c064a3a876ff0cdf5dacd51bb8d3bbba87256fe49180de5f7c80fe08dd. Open the byte-exact preserved source file.

% Part: first-order-logic
% Chapter: syntax-and-semantics
% Section: Semantic Notions
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\olfileid{fol}{syn}{sem}
\olsection{Semantic Notions}
\begin{explain}
Given the definition of !!{structure}s for first-order languages, we can
define some basic semantic properties of and relationships between
sentences. The simplest of these is the notion of \emph{validity} of
a sentence. A sentence is valid if it is satisfied in every
!!{structure}. Valid sentences are those that are satisfied regardless of
how the non-logical symbols in it are interpreted. Valid sentences
are therefore also called \emph{logical truths}---they are true, i.e.,
satisfied, in any !!{structure} and hence their truth depends only on the
logical symbols occurring in them and their syntactic !!{structure}, but not
on the non-logical symbols or their interpretation.
\end{explain}
\begin{defn}[Validity]
A sentence $!A$ is \emph{valid}, $\Entails !A$, iff $\Sat{M}{!A}$ for every
!!{structure}~$\Struct M$.
\end{defn}
\begin{defn}[Entailment]
A set of sentences~$\Gamma$ \emph{entails} a sentence~$!A$, $\Gamma
\Entails !A$, iff for every !!{structure}~$\Struct M$ with
$\Sat{M}{\Gamma}$, $\Sat{M}{!A}$.
\end{defn}
\begin{defn}[Satisfiability]
A set of sentences~$\Gamma$ is \emph{satisfiable} if $\Sat{M}{\Gamma}$
for some !!{structure}~$\Struct M$. If $\Gamma$ is not satisfiable it is
called \emph{unsatisfiable}.
\end{defn}
\begin{prop}
A sentence $!A$ is valid iff $\Gamma \Entails !A$ for every set of
sentences~$\Gamma$.
\end{prop}
\begin{proof}
For the forward direction, let $!A$ be valid, and let $\Gamma$ be a
set of sentences. Let $\Struct M$ be !!a{structure} so that
$\Sat{M}{\Gamma}$. Since $!A$ is valid, $\Sat{M}{!A}$, hence $\Gamma
\Entails !A$.
For the contrapositive of the reverse direction, let $!A$ be invalid,
so there is !!a{structure}~$\Struct M$ with $\Sat/{M}{!A}$. When $\Gamma
= \{ \ltrue \}$, since $\ltrue$ is valid, $\Sat{M}{\Gamma}$. Hence,
there is !!a{structure}~$\Struct M$ so that $\Sat{M}{\Gamma}$ but
$\Sat/{M}{!A}$, hence $\Gamma$ does not entail $!A$.
\end{proof}
\begin{prop}
\ollabel{prop:entails-unsat}
$\Gamma \Entails !A$ iff $\Gamma \cup \{\lnot !A\}$ is unsatisfiable.
\end{prop}
\begin{proof}
For the forward direction, suppose $\Gamma \Entails !A$ and suppose to the
contrary that there is !!a{structure}~$\Struct M$ so that $\Sat{M}{\Gamma
\cup \{ \lnot !A \}}$. Since $\Sat{M}{\Gamma}$ and $\Gamma \Entails
!A$, $\Sat{M}{!A}$. Also, since $\Sat{M}{\Gamma\cup \{ \lnot !A \}}$,
$\Sat{M}{\lnot !A}$, so we have both $\Sat{M}{!A}$ and $\Sat/{M}{!A}$,
a contradiction. Hence, there can be no such !!{structure}~$\Struct M$, so
$\Gamma \cup \{ \lnot !A \}$ is unsatisfiable.
For the reverse direction, suppose $\Gamma \cup \{ \lnot !A \}$ is
unsatisfiable. So for every !!{structure}~$\Struct M$, either
$\Sat/{M}{\Gamma}$ or $\Sat{M}{!A}$. Hence, for every !!{structure}
$\Struct M$ with $\Sat{M}{\Gamma}$, $\Sat{M}{!A}$, so $\Gamma \Entails
!A$.
\end{proof}
\begin{prob}
\begin{enumerate}
\item Show that $\Gamma \Entails \bot$ iff $\Gamma$ is unsatisfiable.
\item Show that $\Gamma \cup \{!A\} \Entails \bot$ iff $\Gamma \Entails \lnot !A$.
\item Suppose $c$ does not occur in $!A$ or $\Gamma$. Show that
$\Gamma \Entails \lforall[x][!A]$ iff $\Gamma \Entails
\Subst{!A}{c}{x}$.
\end{enumerate}
\end{prob}
\begin{prop}
If $\Gamma \subseteq \Gamma'$ and $\Gamma \Entails !A$, then $\Gamma'
\Entails !A$.
\end{prop}
\begin{proof}
Suppose that $\Gamma \subseteq \Gamma'$ and $\Gamma \Entails !A$. Let
$\Struct M$ be a structure such that $\Sat{M}{\Gamma'}$; then $\Sat{M}{\Gamma}$,
and since $\Gamma \Entails !A$, we get that $\Sat{M}{!A}$. Hence,
whenever $\Sat{M}{\Gamma'}$, $\Sat{M}{!A}$, so $\Gamma' \Entails !A$.
\end{proof}
\begin{thm}[Semantic Deduction Theorem]
\ollabel{thm:sem-deduction}
$\Gamma \cup \{!A\} \Entails !B$ iff $\Gamma \Entails !A \lif !B$.
\end{thm}
\begin{proof}
For the forward direction, let $\Gamma \cup \{ !A \} \Entails !B$ and
let $\Struct M$ be !!a{structure} so that $\Sat{M}{\Gamma}$. If
$\Sat{M}{!A}$, then $\Sat{M}{\Gamma \cup \{ !A \} }$, so since $\Gamma
\cup \{ !A \}$ entails $!B$, we get $\Sat{M}{!B}$. Therefore,
$\Sat{M}{!A \lif !B}$, so $\Gamma \Entails !A \lif !B$.
For the reverse direction, let $\Gamma \Entails !A \lif !B$ and
$\Struct M$ be !!a{structure} so that $\Sat{M}{\Gamma \cup \{ !A
\}}$. Then $\Sat{M}{\Gamma}$, so $\Sat{M}{!A \lif !B}$, and since
$\Sat{M}{!A}$, $\Sat{M}{!B}$. Hence, whenever $\Sat{M}{\Gamma \cup \{
!A \} }$, $\Sat{M}{!B}$, so $\Gamma \cup \{ !A \} \Entails !B$.
\end{proof}
\begin{prop}\ollabel{prop:quant-terms}
Let $\Struct{M}$ be !!a{structure}, and $!A(x)$ !!a{formula} with
one free variable~$x$, and $t$~a closed term. Then:
\begin{tagenumerate}{prvEx,prvAll}
\tagitem{prvEx}{$!A(t) \Entails \lexists[x][!A(x)]$}{}
\tagitem{prvAll}{$\lforall[x][!A(x)] \Entails !A(t)$}{}
\end{tagenumerate}
\end{prop}
\begin{proof}
\begin{tagenumerate}{prvEx,prvAll}
\tagitem{prvEx}{%
\iftag{probEx}{Exercise.}{Suppose $\Sat{M}{!A(t)}$. Let $s$ be a
variable assignment with $s(x) = \Value{t}{M}$. Then
$\Sat{M}{!A(t)}[s]$ since $!A(t)$ is !!a{sentence}. By
\olref[ext]{prop:ext-formulas}, $\Sat{M}{!A(x)}[s]$. By
\olref[ass]{prop:sat-quant},
$\Sat{M}{\lexists[x][!A(x)]}$.}}{}
\tagitem{prvAll}{%
\iftag{probAll}{Exercise.}{Suppose
$\Sat{M}{\lforall[x][!A(x)]}$. Let $s$ be a variable
assignment with $s(x) = \Value{t}{M}$. By
\olref[ass]{prop:sat-quant}, $\Sat{M}{!A(x)}[s]$. By
\olref[ext]{prop:ext-formulas}, $\Sat{M}{!A(t)}[s]$. By
\olref[ass]{prop:sentence-sat-true}, $\Sat{M}{!A(t)}$ since
$!A(t)$ is !!a{sentence}.}}{}
\end{tagenumerate}
\end{proof}
\begin{probtag}{probEx,probAll}
Complete the proof of \olref[fol][syn][sem]{prop:quant-terms}.
\end{probtag}
\end{document}