2.1.11: Satisfaction of a Formula in a Structure

\(\def\Assign#1#2{ { #1^{\Struct{#2}} } }\)
\(\def\Atom#1#2{ { \mathord{#1}(#2) } }\)
\(\def\Bin{ {\mathbb{B}} }\)
\(\def\cardeq#1#2{ { #1 \approx #2 } }\)
\(\def\cardle#1#2{ { #1 \preceq #2 } }\)
\(\def\cardless#1#2{ { #1 \prec #2 } }\)
\(\def\cardneq#1#2{ { #1 \not\approx #2 } }\)
\(\def\comp#1#2{ { #2 \circ #1 } }\)
\(\def\concat{ { \;\frown\; } }\)
\(\def\Cut{ { \text{Cut} } }\)
\(\def\Discharge#1#2{ { [#1]^#2 } }\)
\(\def\DischargeRule#1#2{ { \RightLabel{#1}\LeftLabel{\scriptsize{#2} } } }\)
\(\def\dom#1{ {\operatorname{dom}(#1)} }\)
\(\def\Domain#1{ {\left| \Struct{#1} \right|} }\)
\(\def\Elim#1{ { {#1}\mathrm{Elim} } }\)
\(\newcommand{\Entails}{\vDash}\)
\(\newcommand{\EntailsN}{\nvDash}\)
\(\def\eq[#1][#2]{ { #1 = #2 } }\)
\(\def\eqN[#1][#2]{ { #1 \neq #2 } }\)
\(\def\equivclass#1#2{ { #1/_{#2} } }\)
\(\def\equivrep#1#2{ { [#1]_{#2} } }\)
\(\def\Exchange{ { \text{X} } }\)
\(\def\False{ { \mathbb{F} } }\)
\(\def\FalseCl{ { \lfalse_C } }\)
\(\def\FalseInt{ { \lfalse_I } }\)
\(\def\fCenter{ { \,\Sequent\, } }\)
\(\def\fdefined{ { \;\downarrow } }\)
\(\def\fn#1{ { \operatorname{#1} } }\)
\(\def\Frm[#1]{ {\operatorname{Frm}(\Lang #1)} }\)
\(\def\fundefined{ { \;\uparrow } }\)
\(\def\funimage#1#2{ { #1[#2] } }\)
\(\def\funrestrictionto#1#2{ { #1 \restriction_{#2} } }\)
\(\newcommand{\ident}{\equiv}\)
\(\newcommand{\indcase}[2]{#1 \ident #2\text{:}}\)
\(\newcommand{\indcaseA}[2]{#1 \text{ is atomic:}}\)
\(\def\indfrm{ { A } }\)
\(\def\indfrmp{ { A } }\)
\(\def\joinrel{\mathrel{\mkern-3mu}}\)
\(\def\lambd[#1][#2]{\lambda #1 . #2}\)
\(\def\Lang#1{ { \mathcal{#1} } }\)
\(\def\LeftR#1{ { {#1}\mathrm{L} } }\)
\(\def\len#1{ {\operatorname{len}(#1)} }\)
\(\def\lexists#1#2{ { \exists #1\, #2 } }\)
\(\def\lfalse{ {\bot} }\)
\(\def\lforall#1#2{ { \forall#1\, #2 } }\)
\(\newcommand{\lif}{\rightarrow}\)
\(\newcommand{\liff}{\leftrightarrow}\)
\(\def\Log#1{ { \mathbf{#1} } }\)
\(\def\ltrue{ {\top} }\)
\(\def\Id#1{ {\operatorname{Id}_#1} }\)
\(\def\Int{ {\mathbb{Z}} }\)
\(\def\Intro#1{ { {#1}\mathrm{Intro} } }\)
\(\def\mModel#1{ { \mathfrak{#1} } }\)
\(\newcommand{\mSat}[3][{}]{\mModel{#2}{#1}\Vdash{#3}}\)
\(\newcommand{\mSatN}[3][{}]{\mModel{#2}{#1}\nVdash{#3}}\)
\(\def\Nat{ {\mathbb{N}} }\)
\(\def\nicefrac#1#2{ {{}^#1/_#2} }\)
\(\def\num#1{ { \overline{#1} } }\)

\(\def\ran#1{ {\operatorname{ran}(#1)} }\)
\(\newcommand{\Obj}[1]{\mathsf{#1}}\)
\(\def\Rat{ {\mathbb{Q}} }\)
\(\def\Real{ {\mathbb{R}} }\)
\(\def\RightR#1{ { {#1}\mathrm{R} } }\)
\(\def\Part#1#2{ { \Atom{\Obj P}{#1, #2} } }\)
\(\def\pto{ { \hspace{0.1 cm}\to\hspace{-0.44 cm}\vcenter{\tiny{\hbox{|}}}\hspace{0.35 cm} } }\)
\(\def\PosInt{ {\mathbb{Z}^+} }\)
\(\def\Pow#1{ {\wp(#1)} }\)
\(\newcommand{\Proves}{\vdash}\)
\(\newcommand{\ProvesN}{\nvdash}\)
\(\def\Relbar{\mathrel{=}}\)
\(\newcommand{\Sat}[3][{}]{\Struct{#2}{#1}\vDash{#3}}\)
\(\newcommand{\SatN}[3][{}]{\Struct{#2}{#1}\nvDash{#3}}\)
\(\newcommand{\Sequent}{\Rightarrow}\)
\(\def\Setabs#1#2{ { \{#1:#2\} } }\)
\(\newcommand{\sFmla}[2]{#1\,#2}\)
\(\def\Struct#1{ {#1} }\)
\(\def\subst#1#2{ { #1/#2 } }\)
\(\def\Subst#1#2#3{ { #1[\subst{#2}{#3}] } }\)
\(\def\TMblank{ { 0 } }\)
\(\newcommand{\TMendtape}{\triangleright}\)
\(\def\TMleft{ { L } }\)
\(\def\TMright{ { R } }\)
\(\def\TMstay{ { N } }\)
\(\def\TMstroke{ { 1 } }\)
\(\def\TMtrans#1#2#3{ { #1,#2,#3 } }\)
\(\def\Trm[#1]{ {\operatorname{Trm}(\Lang #1)} }\)
\(\def\True{ { \mathbb{T} } }\)
\(\newcommand{\TRule}[2]{#2#1}\)
\(\def\tuple#1{ {\langle #1 \rangle} }\)
\(\newcommand{\Value}[3][\,]{\mathrm{Val}_{#1}^{#3}(#2)}\)
\(\def\Var{ { \mathrm{Var} } }\)
\(\newcommand{\varAssign}[3]{#1 \sim_{#3} #2}\)
\(\def\Weakening{ { \text{W} } }\)

The basic notion that relates expressions such as terms and formulas, on the one hand, and structures on the other, are those of value of a term and 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 symbols, the value is computed from the values of constants and the functions assigned to the functions in the term. A formula is 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 formulas are satisfied, and we define when a complex formula is satisfied depending on the main connective or quantifier and whether or not the immediate subformulas 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 structures don’t specify the values of variables. In order to deal with this difficulty, we also introduce variable assignments and define satisfaction not with respect to a structure alone, but with respect to a structure plus a variable assignment.

Definition \(\PageIndex{1}\): Variable Assignment

A variable assignment \(s\) for a structure \(\Struct{M}\) is a function which maps each variable to an element of \(\Domain M\), i.e., \(s\colon \Var \to \Domain M\).

A structure assigns a value to each constant symbol, and a variable assignment to each variable. But we want to use terms built up from them to also name elements of the domain. For this we define the value of terms inductively. For constant symbols 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 symbols.

Definition \(\PageIndex{2}\): 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 value \(\Value[s]{t}{M}\) is defined as follows:

1. \(\indcase{t}{c}\) \(\Value[s]{t}{M} = \Assign{c}{M}\).
2. \(\indcase{t}{x}\) \(\Value[s]{t}{M} = s(x)\).
3. \(\indcase{t}{\Atom{f}{t_1, \ldots, t_n}}\) \[\Value[s]{t}{M} = \Assign{f}{M}(\Value[s]{t_1}{M}, \ldots, \Value[s]{t_n}{M}).\nonumber\]

Definition \(\PageIndex{3}\): \(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 \(x\)-variant of \(s\). If \(s'\) is an \(x\)-variant of \(s\) we write \(\varAssign{s'}{s}{x}\).

Note that an \(x\)-variant of an assignment \(s\) does not have to assign something different to \(x\). In fact, every assignment counts as an \(x\)-variant of itself.

Definition \(\PageIndex{4}\): Satisfaction

Satisfaction of a formula \(A\) in a structure \(\Struct M\) relative to a variable assignment \(s\), in symbols: \(\Sat[,s]{M}{A}\), is defined recursively as follows. (We write \(\SatN[,s]{M}{A}\) to mean “not \(\Sat[,s]{M}{A}\).”)

1. \(\indcase{A}{\lfalse}\) \(\SatN[,s]{M}{\indfrm}\).
2. \(\indcase{A}{\Atom{R}{t_1, \dots, t_n}}\) \(\Sat[,s]{M}{\indfrm}\) iff \(\langle \Value[s]{t_1}{M}, \dots, \Value[s]{t_n}{M} \rangle \in \Assign{R}{M}\).
3. \(\indcase{A}{\eq[t_1][t_2]}\) \(\Sat[,s]{M}{\indfrm}\) iff \(\Value[s]{t_1}{M} = \Value[s]{t_2}{M}\).
4. \(\indcase{A}{\lnot B}\) \(\Sat[,s]{M}{\indfrm}\) iff \(\SatN[,s]{M}{B}\).
5. \(\indcase{A}{(B \land C)}\) \(\Sat[,s]{M}{\indfrm}\) iff \(\Sat[,s]{M}{B}\) and \(\Sat[,s]{M}{C}\).
6. \(\indcase{A}{(B \lor C)}\) \(\Sat[,s]{M}{\indfrm}\) iff \(\Sat[,s]{M}{A}\) or \(\Sat[,s]{M}{B}\) (or both).
7. \(\indcase{A}{(B \lif C)}\) \(\Sat[,s]{M}{\indfrm}\) iff \(\SatN[,s]{M}{B}\) or \(\Sat[,s]{M}{C}\) (or both).
8. \(\indcase{A}{\lforall{x}{B}}\) \(\Sat[,s]{M}{\indfrm}\) iff for every \(x\)-variant \(s'\) of \(s\), \(\Sat[,s']{M}{B}\).
9. \(\indcase{A}{\lexists{x}{B}}\) \(\Sat[,s]{M}{\indfrm}\) iff there is an \(x\)-variant \(s'\) of \(s\) so that \(\Sat[,s']{M}{B}\).

The variable assignments are important in the last two clauses. We cannot define satisfaction of \(\lforall{x}{B(x)}\) by “for all \(a \in \Domain{M}\), \(\Sat{M}{B(a)}\).” We cannot define satisfaction of \(\lexists{x}{B(x)}\) by “for at least one \(a \in \Domain{M}\), \(\Sat{M}{B(a)}\).” The reason is that \(a\) is not symbol of the language, and so \(B(a)\) is not a formula (that is, \(\Subst{B}{a}{x}\) is undefined). We also cannot assume that we have constant symbols or terms available that name every element of \(\Struct{M}\), since there is nothing in the definition of structures that requires it. Even in the standard language the set of constant symbols is countably infinite, so if \(\Domain{M}\) is not enumerable there aren’t even enough constant symbols to name every object.

Example \(\PageIndex{1}\)

Let \(\Lang{L} = \{a, b, f, R\}\) where \(a\) and \(b\) are constant symbols, \(f\) is a two-place function symbol, and \(R\) is a two-place predicate symbol. Consider the structure \(\Struct{M}\) defined by:

1. \(\Domain M = \{1, 2, 3, 4\}\)
2. \(\Assign{a}{M} = 1\)
3. \(\Assign{b}{M} = 2\)
4. \(\Assign{f}{M}(x, y) = x+y\) if \(x+y \le 3\) and \(= 3\) otherwise.
5. \(\Assign{R}{M} = \{\tuple{1, 1}, \tuple{1, 2}, \tuple{2, 3}, \tuple{2, 4}\}\)

The function \(s(x) = 1\) that assigns \(1 \in \Domain{M}\) to every variable is a variable assignment for \(\Struct{M}\).

Then

\[\Value[s]{f(a,b)}{M} = \Assign{f}{M}(\Value[s]{a}{M}, \Value[s]{b}{M}).\nonumber\]

Since \(a\) and \(b\) are constant symbols, \(\Value[s]{a}{M} = \Assign{a}{M} = 1\) and \(\Value[s]{b}{M} = \Assign{b}{M} = 2\). So

\[\Value[s]{f(a,b)}{M} = \Assign{f}{M}(1, 2) = 1+2 = 3.\nonumber\]

To compute the value of \(f(f(a,b),a)\) we have to consider

\[\Value[s]{f(f(a,b),a)}{M} = \Assign{f}{M}(\Value[s]{f(a, b)}{M}, \Value[s]{a}{M}) = \Assign{f}{M}(3, 1) = 3,\nonumber\]

since \(3+1 > 3\). Since \(s(x) = 1\) and \(\Value[s]{x}{M} = s(x)\), we also have

\[\Value[s]{f(f(a,b),x)}{M} = \Assign{f}{M}(\Value[s]{f(a, b)}{M}, \Value[s]{x}{M}) = \Assign{f}{M}(3, 1) = 3.\nonumber\]

An atomic formula \(R(t_1, t_2)\) is satisfied if the tuple of values of its arguments, i.e., \(\tuple{\Value[s]{t_1}{M}, \Value[s]{t_2}{M}}\), is an element of \(\Assign{R}{M}\). So, e.g., we have \(\Sat[,s]{M}{R(b,f(a,b))}\) since \(\tuple{\Value{b}{M}, \Value{f(a,b)}{M}} = \tuple{2, 3} \in \Assign{R}{M}\), but \(\SatN[,s]{M}{R(x, f(a,b))}\) 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{aligned}
& \Sat[,s]{M}{R(a, a) \lif (R(b, x) \lor R(x, b))} \text{ iff }\\
& \qquad \SatN[,s]{M}{R(a,a)} \text{ or } \Sat[,s]{M}{R(b, x) \lor R(x, b)}
\end{aligned}\]

Since \(\Sat[,s]{M}{R(a,a)}\) (because \(\tuple{1,1} \in \Assign{R}{M}\)) we can't yet determine the answer and must first figure out if \(\Sat[,s]{M}{R(b, x) \lor R(x, b)}\):

\[\begin{aligned}
& \Sat[,s]{M}{R(b, x) \lor R(x, b)} \text{ iff }\\
& \qquad \Sat[,s]{M}{R(b,x)} \text{ or } \Sat[,s]{M}{R(x, b)}
\end{aligned}\]

And this is the case, since \(\Sat[,s]{M}{R(x, b)}\) (because \(\tuple{1,2} \in \Assign{R}{M}\)).

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\): \(s_1(x) = 1\), \(s_2(x) = 2\), \(s_3(x) = 3\), \(s_4(x) = 4\), and with \(s_i(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\) is also an \(x\)-variant of \(s\), i.e., \(s\) is always an \(x\)-variant of itself.

To determine if an existentially quantified formula \(\lexists{x}{A(x)}\) is satisfied, we have to determine if \(\Sat[,s']{M}{A(x)}\) for at least one \(x\)-variant \(s'\) of \(s\). So, \[\Sat[,s]{M}{\lexists{x}{(R(b,x) \lor R(x,b))}},\nonumber\] since \(\Sat[,s_1]{M}{R(b,x) \lor R(x, b)}\) (\(s_3\) would also fit the bill). But, \[\SatN[,s]{M}{\lexists{x}{(R(b,x) \land R(x,b))}}\nonumber\] since for none of the \(s_i\), \(\Sat[,s_i]{M}{R(b,x) \land R(x,b)}\).

To determine if a universally quantified formula \(\lforall{x}{A(x)}\) is satisfied, we have to determine if \(\Sat[,s']{M}{A(x)}\) for all \(x\)-variants \(s'\) of \(s\). So, \[\Sat[,s]{M}{\lforall{x}{(R(x,a) \lif R(a,x))}},\nonumber\] since \(\Sat[,s_i]{M}{R(x,a) \lif R(a,x)}\) for all \(s_i\) (\(\Sat[,s_1]{M}{R(a,x)}\) and \(\SatN[,s_j]{M}{R(x,a)}\) for \(j = 2\), \(3\), and \(4\)). But, \[\SatN[,s]{M}{\lforall{x}{(R(a,x) \lif R(x,a))}}\nonumber\] since \(\SatN[,s_2]{M}{R(a,x) \lif R(x,a)}\) (because \(\Sat[,s_2]{M}{R(a, x)}\) and \(\SatN[,s_2]{M}{R(x, a)}\)).

For a more complicated case, consider \[\lforall{x}{(R(a,x) \lif \lexists{y}{R(x,y)})}.\nonumber\] Since \(\SatN[,s_3]{M}{R(a,x)}\) and \(\SatN[,s_4]{M}{R(a,x)}\), the interesting cases where we have to worry about the consequent of the conditional are only \(s_1\) and \(s_2\). Does \(\Sat[,s_1]{M}{\lexists{y}{R(x,y)}}\) hold? It does if there is at least one \(y\)-variant \(s_1'\) of \(s_1\) so that \(\Sat[,s_1']{M}{R(x,y)}\). In fact, \(s_1\) is such a \(y\)-variant (\(s_1(x) = 1\), \(s_1(y) = 1\), and \(\tuple{1,1} \in \Assign{R}{M}\)), so the answer is yes. To determine if \(\Sat[,s_2]{M}{\lexists{y}{R(x,y)}}\) we have to look at the \(y\)-variants of \(s_2\). Here, \(s_2\) itself does not satisfy \(R(x,y)\) (\(s_2(x) = 2\), \(s_2(y) = 1\), and \(\tuple{2,1}\notin \Assign{R}{M}\)). However, consider \(\varAssign{s_2'}{s_2}{y}\) with \(s_2'(y) = 3\). \(\Sat[,s_2']{M}{R(x,y)}\) since \(\tuple{2,3} \in \Assign{R}{M}\), and so \(\Sat[,s_2]{M}{\lexists{y}{R(x,y)}}\). In sum, for every \(x\)-variant \(s_i\) of \(s\), either \(\SatN[,s_i]{M}{R(a,x)}\) (\(i = 3\), \(4\)) or \(\Sat[,s_i]{M}{\lexists{y}{R(x,y)}}\) (\(i = 1\), \(2\)), and so \[\Sat[,s]{M}{\lforall{x}{(R(a,x) \lif \lexists{y}{R(x,y)})}}.\nonumber\] On the other hand, \[\SatN[,s]{M}{\lexists{x}{(R(a,x) \land \lforall{y}{R(x,y)})}}.\nonumber\] The only \(x\)-variants \(s_i\) of \(s\) with \(\Sat[,s_i]{M}{R(a,x)}\) are \(s_1\) and \(s_2\). But for each, there is in turn a \(y\)-variant \(\varAssign{s_i'}{s_i}{y}\) with \(s_i'(y) = 4\) so that \(\SatN[,s_i']{M}{R(x,y)}\) and so \(\SatN[,s_i]{M}{\lforall{y}{R(x,y)}}\) for \(i = 1\), \(2\). In sum, none of the \(x\)-variants \(\varAssign{s_i}{s}{x}\) are such that \(\Sat[,s_i]{M}{R(a,x) \land \lforall{y}{R(x,y)}}\).

Problem \(\PageIndex{1}\)

Let \(\Lang L = \{c, f, A\}\) with one constant symbol, one one-place function symbol and one two-place predicate symbol, and let the structure \(\Struct{M}\) be given by

1. \(\Domain M = \{1, 2, 3\}\)
2. \(\Assign{c}{M} = 3\)
3. \(\Assign{f}{M}(1) = 2, \Assign{f}{M}(2) = 3, \Assign{f}{M}(3) = 2\)
4. \(\Assign{A}{M} = \{\tuple{1, 2}, \tuple{2, 3}, \tuple{3, 3}\}\)

(a) Let \(s(v) = 1\) for all variables \(v\). Find out whether \[\Sat[,s]{M}{\lexists{x}{(A(f(z), c) \lif \lforall{y}{(A(y, x) \lor A(f(y), x))})}}\nonumber\] Explain why or why not.

(b) Give a different structure and variable assignment in which the formula is not satisfied.