We have defined satisfaction in a model with a variable assignment. We have expressed formula
φ
{\displaystyle \varphi \,\!}
M
{\displaystyle {\mathfrak {M}}\,\!}
s
{\displaystyle \mathrm {s} \,\!}
<
M
,
s
>
⊨
φ
{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \varphi \,\!}
Now we can also say that a formula
φ
{\displaystyle \varphi \,\!}
M
{\displaystyle {\mathfrak {M}}\,\!}
φ
{\displaystyle \varphi \,\!}
M
{\displaystyle {\mathfrak {M}}\,\!}
M
⊨
φ
{\displaystyle {\mathfrak {M}}\ \vDash \varphi \,\!}
if and only if
<
M
,
s
>
⊨
φ
for every
s
.
{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \varphi \ {\mbox{for every}}\ \mathrm {s} \ .\,\!}
If no free variables occur in
φ
,
{\displaystyle \varphi ,\,\!}
φ
{\displaystyle \varphi \,\!}
φ
{\displaystyle \varphi \,\!}
M
{\displaystyle {\mathfrak {M}}\,\!}
Variable assignments allow us to deal with free variables when doing the semantic analysis of a formula. For two variable assignments,
s
1
{\displaystyle \mathrm {s_{1}} \,\!}
s
2
{\displaystyle \mathrm {s_{2}} \,\!}
<
M
,
s
1
>
{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s_{1}} \!>\,\!}
<
M
,
s
2
>
{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s_{2}} \!>\,\!}
φ
{\displaystyle \varphi \,\!}
M
{\displaystyle {\mathfrak {M}}\,\!}
s
{\displaystyle \mathrm {s} \,\!}
<
M
,
s
>
⊨
φ
.
{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \varphi \ .\,\!}
φ
{\displaystyle \varphi \,\!}
M
{\displaystyle {\mathfrak {M}}\,\!}
s
,
{\displaystyle \mathrm {s} ,\,\!}
<
M
,
s
>
⊨
φ
.
{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \varphi \ .\,\!}
The latter is just a notational variant of:
φ
{\displaystyle \varphi \,\!}
M
{\displaystyle {\mathfrak {M}}\,\!}
M
⊨
φ
.
{\displaystyle {\mathfrak {M}}\ \vDash \varphi \ .\,\!}
On the previous page , we looked at the following model and variable assignment.
For the model
I
M
:
{\displaystyle I_{\mathfrak {M}}\ :\,\!}
|
M
|
=
{
1
,
2
,
3
}
.
{\displaystyle |{\mathfrak {M}}|\ =\ \{1,\,2,\,3\}\ .\,\!}
I
M
(
a
0
0
)
=
0
.
{\displaystyle I_{\mathfrak {M}}(a_{0}^{0})\ =\ 0\ .\,\!}
I
M
(
b
0
0
)
=
1
.
{\displaystyle I_{\mathfrak {M}}(b_{0}^{0})\ =\ 1\ .\,\!}
I
M
(
c
0
0
)
=
2
.
{\displaystyle I_{\mathfrak {M}}(c_{0}^{0})\ =\ 2\ .\,\!}
I
M
(
f
0
2
)
=
f
0
2
such that:
f
0
2
(
0
,
0
)
=
2
,
f
0
2
(
0
,
1
)
=
1
,
f
0
2
(
0
,
2
)
=
0
,
{\displaystyle I_{\mathfrak {M}}(f_{0}^{2})\ =\ {\mathfrak {f}}_{0}^{2}\ {\mbox{such that:}}\quad {\mathfrak {f}}_{0}^{2}(0,\,0)=2,\ {\mathfrak {f}}_{0}^{2}(0,\,1)\ =\ 1,\ {\mathfrak {f}}_{0}^{2}(0,\,2)=0,\,\!}
f
0
2
(
1
,
0
)
=
1
,
f
0
2
(
1
,
1
)
=
0
,
f
0
2
(
1
,
2
)
=
2
,
f
0
2
(
2
,
0
)
=
0
,
{\displaystyle {\mathfrak {f}}_{0}^{2}(1,\,0)=1,\ {\mathfrak {f}}_{0}^{2}(1,\,1)\ =\ 0,\ {\mathfrak {f}}_{0}^{2}(1,\,2)=2,\ {\mathfrak {f}}_{0}^{2}(2,\,0)=0,\,\!}
f
0
2
(
2
,
1
)
=
2
,
and
f
0
2
(
2
,
2
)
=
1
.
{\displaystyle {\mathfrak {f}}_{0}^{2}(2,\,1)=2,\ {\mbox{and}}\ {\mathfrak {f}}_{0}^{2}(2,\,2)=1\ .\,\!}
I
M
(
F
0
2
)
=
{
<
0
,
1
>
,
<
1
,
2
>
,
<
2
,
1
>
}
.
{\displaystyle I_{\mathfrak {M}}(\mathrm {F_{0}^{2}} )\ =\ \{<\!0,\ 1\!>,\ <\!1,\ 2\!>,\ <\!2,\ 1\!>\}\ .\,\!}
For the variable assignment
s
:
{\displaystyle \mathrm {s} \ :\,\!}
s
(
x
0
)
=
0
.
{\displaystyle \mathrm {s} (x_{0})\ =\ 0\ .\,\!}
s
(
y
0
)
=
1
.
{\displaystyle \mathrm {s} (y_{0})\ =\ 1\ .\,\!}
s
(
z
0
)
=
2
.
{\displaystyle \mathrm {s} (z_{0})\ =\ 2\ .\,\!}
We noted the following results:
<
M
,
s
>
⊨
F
(
a
,
b
)
,
F
(
b
,
c
)
,
and
F
(
c
,
b
)
.
{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \mathrm {F} (a,b),\ \mathrm {F} (b,c),\ {\mbox{and}}\ \mathrm {F} (c,b)\ .\,\!}
<
M
,
s
>
⊭
F
(
a
,
a
)
)
.
{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \not \vDash \mathrm {F} (a,a))\ .\,\!}
<
M
,
s
>
⊨
F
(
a
,
f
(
a
,
b
)
)
.
{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \mathrm {F} (a,f(a,b))\ .\,\!}
<
M
,
s
>
⊭
F
(
f
(
a
,
b
)
,
a
)
.
{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \not \vDash \mathrm {F} (f(a,b),a)\ .\,\!}
<
M
,
s
>
⊨
F
(
c
,
b
)
→
F
(
a
,
b
)
.
{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \mathrm {F} (c,b)\rightarrow \mathrm {F} (a,b)\ .\,\!}
<
M
,
s
>
⊭
F
(
c
,
b
)
→
F
(
b
,
a
)
.
{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \not \vDash \mathrm {F} (c,b)\rightarrow \mathrm {F} (b,a)\ .\,\!}
<
M
,
s
>
⊭
∀
x
∀
y
(
F
(
x
,
y
)
→
F
(
y
,
x
)
)
{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \not \vDash \forall x\,\forall y\,(\mathrm {F} (x,y)\rightarrow \mathrm {F} (y,x))\,\!}
<
M
,
s
>
⊨
∃
x
∃
y
(
F
(
x
,
y
)
∧
F
(
y
,
x
)
)
{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \exists x\,\exists y\,(\mathrm {F} (x,y)\land \mathrm {F} (y,x))\,\!}
We also noted above that for sentences (though not for formulae in general), a model satisfies the sentence with at least one variable assignment if and only if it satisfies the sentence with every variable assignment. Thus the results just listed hold for every variable assignment, not just
s
{\displaystyle \mathrm {s} \,\!}
Applying our definition of truth, we get:
(
1
)
F
(
a
,
b
)
,
F
(
b
,
c
)
,
and
F
(
c
,
b
)
are True in
M
.
{\displaystyle (1)\quad \mathrm {F} (a,b),\ \mathrm {F} (b,c),\ {\mbox{and}}\ \mathrm {F} (c,b)\ {\mbox{are True in}}\ {\mathfrak {M}}\ .\,\!}
(
2
)
F
(
a
,
a
)
is False in
M
.
{\displaystyle (2)\quad \mathrm {F} (a,a)\ {\mbox{is False in}}\ {\mathfrak {M}}\ .\,\!}
(
3
)
F
(
a
,
f
(
a
,
b
)
)
is True in
M
.
{\displaystyle (3)\quad \mathrm {F} (a,f(a,b))\ {\mbox{is True in}}\ {\mathfrak {M}}\ .\,\!}
(
4
)
F
(
f
(
a
,
b
)
,
a
)
is False in
M
.
{\displaystyle (4)\quad \mathrm {F} (f(a,b),a)\ {\mbox{is False in}}\ {\mathfrak {M}}\ .\,\!}
(
5
)
F
(
c
,
b
)
→
F
(
a
,
b
)
is True in
M
.
{\displaystyle (5)\quad \mathrm {F} (c,b)\rightarrow \mathrm {F} (a,b)\ {\mbox{is True in}}\ {\mathfrak {M}}\ .\,\!}
(
6
)
F
(
c
,
b
)
→
F
(
b
,
a
)
is False in
M
.
{\displaystyle (6)\quad \mathrm {F} (c,b)\rightarrow \mathrm {F} (b,a)\ {\mbox{is False in}}\ {\mathfrak {M}}\ .\,\!}
(
7
)
∀
x
∀
y
(
F
(
x
,
y
)
→
F
(
y
,
x
)
)
is false in
M
.
{\displaystyle (7)\quad \forall x\,\forall y\,(\mathrm {F} (x,y)\rightarrow \mathrm {F} (y,x))\ {\mbox{is false in }}\ {\mathfrak {M}}\ .\,\!}
(
8
)
∃
x
∃
y
(
F
(
x
,
y
)
∧
F
(
y
,
x
)
)
is true in
M
.
{\displaystyle (8)\quad \exists x\,\exists y\,(\mathrm {F} (x,y)\land \mathrm {F} (y,x))\ {\mbox{is true in}}\ {\mathfrak {M}}\ .\,\!}
This corresponds to the goals (1)–(8) of the previous page . We have now achieved those goals.
On Models page , we also considered an infinite model
I
M
2
:
{\displaystyle I_{\mathfrak {M_{2}}}\ :\,\!}
|
M
2
|
=
{
0
,
1
,
2
,
.
.
.
}
{\displaystyle |{\mathfrak {M}}_{2}|=\{0,1,2,...\}\,\!}
I
M
2
(
a
0
0
)
=
0
.
{\displaystyle I_{{\mathfrak {M}}_{2}}(a_{0}^{0})\ =\ 0\ .\,\!}
I
M
2
(
b
0
0
)
=
1
.
{\displaystyle I_{{\mathfrak {M}}_{2}}(b_{0}^{0})\ =\ 1\ .\,\!}
I
M
2
(
c
0
0
)
=
2
.
{\displaystyle I_{{\mathfrak {M}}_{2}}(c_{0}^{0})\ =\ 2\ .\,\!}
I
M
2
(
f
0
2
)
=
f
0
2
such that
f
0
2
(
u
,
v
)
=
u
+
v
.
{\displaystyle I_{{\mathfrak {M}}_{2}}(f_{0}^{2})\ =\ {\mathfrak {f}}_{0}^{2}\ {\mbox{such that}}\ {\mathfrak {f}}_{0}^{2}(u,v)=u+v\ .\,\!}
I
M
2
(
F
0
2
)
=
{
<
x
,
y
>:
x
<
y
}
.
{\displaystyle I_{{\mathfrak {M}}_{2}}(\mathrm {F_{0}^{2}} )\ =\ \{<\!x,\ y\!>:\ x<y\}\ .\,\!}
We can reuse the same variable assignment from above, namely
s
:
{\displaystyle \mathrm {s} \ :\,\!}
s
(
x
0
)
=
0
.
{\displaystyle \mathrm {s} (x_{0})\ =\ 0\ .\,\!}
s
(
y
0
)
=
1
.
{\displaystyle \mathrm {s} (y_{0})\ =\ 1\ .\,\!}
s
(
z
0
)
=
2
.
{\displaystyle \mathrm {s} (z_{0})\ =\ 2\ .\,\!}
Example of extended varable assignment
edit
On the Models page , we listed the following goals for our defintions.
f
(
a
,
b
)
resolves to
1
i
n
M
2
.
{\displaystyle f(a,b)\ {\mbox{resolves to}}\ 1\ \mathrm {in} \ {\mathfrak {M}}_{2}\ .\,\!}
This does not require our definition of truth or the definition of satisfaction; it is simply requires evaluating the exended variable assignment. We have for any
s
{\displaystyle \mathrm {s} \,\!}
I
M
{\displaystyle I_{\mathfrak {M}}\,\!}
s
¯
(
f
(
a
,
b
)
)
=
I
M
(
f
)
(
s
¯
(
a
)
,
s
¯
(
b
)
)
=
f
0
2
(
s
¯
(
a
)
,
s
¯
(
b
)
)
{\displaystyle {\overline {\mathrm {s} }}(f(a,b))\ =\ I_{\mathfrak {M}}(f)\,(\ {\overline {\mathrm {s} }}(a),\,{\overline {\mathrm {s} }}(b)\ )\ =\ {\mathfrak {f}}_{0}^{2}(\ {\overline {\mathrm {s} }}(a),\,{\overline {\mathrm {s} }}(b)\ )\,\!}
=
f
0
2
(
I
M
(
a
)
,
I
M
(
b
)
)
=
f
0
2
(
0
,
1
)
{\displaystyle =\ {\mathfrak {f}}_{0}^{2}(\ I_{\mathfrak {M}}(a),\,I_{\mathfrak {M}}(b)\ )\ =\ {\mathfrak {f}}_{0}^{2}(0,\,1)\,\!}
=
0
+
1
=
1
.
{\displaystyle =\ 0+1\ =\ 1\ .\,\!}
Example results without quantifiers
edit
We also listed the following goal on the Models page .
(
9
)
F
(
a
,
b
)
and
F
(
b
,
c
)
are True in
M
2
.
{\displaystyle (9)\quad \mathrm {F} (a,b)\ {\mbox{and}}\ \mathrm {F} (b,c)\ {\mbox{are True in}}\ {\mathfrak {M}}_{2}\ .\,\!}
(
10
)
F
(
c
,
b
)
and
F
(
a
,
a
)
are False in
M
2
.
{\displaystyle (10)\quad \mathrm {F} (c,b)\ {\mbox{and}}\ \mathrm {F} (a,a)\ {\mbox{are False in}}\ {\mathfrak {M}}_{2}\ .\,\!}
First we note that:
<
M
,
s
>
⊨
F
(
a
,
b
)
because
<
s
¯
(
a
)
,
s
¯
(
b
)
>
=
<
0
,
1
>
∈
I
M
(
F
)
{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \mathrm {F} (a,b)\ \ {\mbox{because}}\ <\!{\overline {\mathrm {s} }}(a),\,{\overline {\mathrm {s} }}(b)\!>\ =\ <\!0,\,1\!>\ \in \ I_{\mathfrak {M}}(\mathrm {F} )\ \,\!}
<
M
,
s
>
⊨
F
(
b
,
c
)
because
<
s
¯
(
b
)
,
s
¯
(
c
)
>
=
<
1
,
2
>
∈
I
M
(
F
)
{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \mathrm {F} (b,c)\ \ {\mbox{because}}\ <\!{\overline {\mathrm {s} }}(b),\,{\overline {\mathrm {s} }}(c)\!>\ =\ <\!1,\,2\!>\ \in \ I_{\mathfrak {M}}(\mathrm {F} )\,\!}
<
M
,
s
>
⊭
F
(
c
,
b
)
because
<
s
¯
(
c
)
,
s
¯
(
b
)
>
=
<
2
,
1
>
∉
I
M
(
F
)
{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \not \vDash \mathrm {F} (c,b)\ \ {\mbox{because}}\ <\!{\overline {\mathrm {s} }}(c),\,{\overline {\mathrm {s} }}(b)\!>\ =\ <\!2,\,1\!>\ \notin \ I_{\mathfrak {M}}(\mathrm {F} )\,\!}
<
M
,
s
>
⊭
F
(
a
,
a
)
because
<
s
¯
(
a
)
,
s
¯
(
a
)
>
=
<
0
,
0
>
∉
I
M
(
F
)
.
{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \not \vDash \mathrm {F} (a,a)\ \ {\mbox{because}}\ <\!{\overline {\mathrm {s} }}(a),\,{\overline {\mathrm {s} }}(a)\!>\ =\ <\!0,\,0\!>\ \notin \ I_{\mathfrak {M}}(\mathrm {F} )\ .\,\!}
Indeed:
<
0
,
1
>
∈
I
M
(
F
)
because
0
<
1
{\displaystyle <\!0,\,1\!>\ \in \ I_{\mathfrak {M}}(\mathrm {F} )\ \ {\mbox{because}}\ \ 0<1\,\!}
<
1
,
2
>
∈
I
M
(
F
)
because
1
<
2
{\displaystyle <\!1,\,2\!>\ \in \ I_{\mathfrak {M}}(\mathrm {F} )\ \ {\mbox{because}}\ \ 1<2\,\!}
<
2
,
1
>
∉
I
M
(
F
)
because
2
≮
1
{\displaystyle <\!2,\,1\!>\ \notin \ I_{\mathfrak {M}}(\mathrm {F} )\ \ {\mbox{because}}\ \ 2\not <1\,\!}
<
0
,
0
>
∉
I
M
(
F
)
because
0
≮
0
.
{\displaystyle <\!0,\,0\!>\ \notin \ I_{\mathfrak {M}}(\mathrm {F} )\ \ {\mbox{because}}\ \ 0\not <0\ .\,\!}
Because the formulae of (9) and (10) are sentences,
<
M
>
⊨
F
(
a
,
b
)
.
{\displaystyle <\!{\mathfrak {M}}\!>\ \vDash \mathrm {F} (a,b)\ .\,\!}
<
M
>
⊨
F
(
b
,
c
)
.
{\displaystyle <\!{\mathfrak {M}}\!>\ \vDash \mathrm {F} (b,c)\ .\,\!}
<
M
>
⊭
F
(
c
,
b
)
.
{\displaystyle <\!{\mathfrak {M}}\!>\ \not \vDash \mathrm {F} (c,b)\ .\,\!}
<
M
>
⊭
F
(
a
,
a
)
.
{\displaystyle <\!{\mathfrak {M}}\!>\ \not \vDash \mathrm {F} (a,a)\ .\,\!}
Applying the definition of truth, we find the goals of (9) and (10) achieved. The sentences of (9) are true and those of (10) are false.
Example results with quantifiers
edit
In addition, we listed the following goal on the Models page .
(
11
)
∀
x
∃
y
F
(
x
,
y
)
is true in
M
2
.
{\displaystyle (11)\quad \forall x\,\exists y\,\mathrm {F} (x,y)\ {\mbox{is true in}}\ {\mathfrak {M}}_{2}\ .\,\!}
(
12
)
∀
x
∃
y
F
(
y
,
x
)
is false in
M
2
.
{\displaystyle (12)\quad \forall x\,\exists y\,\mathrm {F} (y,x)\ {\mbox{is false in}}\ {\mathfrak {M}}_{2}\ .\,\!}
Corresponding to (11):
(
13
)
<
M
2
,
s
>
⊨
∀
x
∃
y
F
(
x
,
y
)
{\displaystyle (13)\quad <\!{\mathfrak {M_{2}}},\ \mathrm {s} \!>\ \vDash \forall x\,\exists y\,\mathrm {F} (x,y)\,\!}
is true if and only if, for each i a member of the domain, the following is true of at least one j a member of the domain:
<
M
2
,
s
[
x
:
i
,
x
:
j
]
>
⊨
F
(
x
,
y
)
.
{\displaystyle <\!{\mathfrak {M_{2}}},\ \mathrm {s} [x\!:\,i,x\!:\,j]\!>\ \vDash \mathrm {F} (x,y)\ .\,\!}
But
F
0
2
{\displaystyle \mathrm {F_{0}^{2}} \,\!}
less then relation. Thus the preceeding holds if and only if, for every member of the domain, there is a larger member of the domain. Given that the domain is
{
0
,
1
,
2
,
.
.
.
}
,
{\displaystyle \{0,1,2,...\},\,\!}
Corresponding to (12):
(
14
)
<
M
2
,
s
>
⊨
∀
x
∃
y
F
(
y
,
x
)
{\displaystyle (14)\quad <\!{\mathfrak {M_{2}}},\ \mathrm {s} \!>\ \vDash \forall x\,\exists y\,\mathrm {F} (y,x)\,\!}
is true if and only if, for each i a member of the domain, the following is true of at least one j a member of the domain:
<
M
2
,
s
[
x
:
i
,
x
:
j
]
>
⊨
F
(
y
,
x
)
.
{\displaystyle <\!{\mathfrak {M_{2}}},\ \mathrm {s} [x\!:\,i,x\!:\,j]\!>\ \vDash \mathrm {F} (y,x)\ .\,\!}
This holds if and only if, for every member of the domain, there is a smaller member of the domain. But there is no member of the domain smaller than 0. Thus (14) is false. The formula of (12) and (14) fails to be satisfied by
M
2
{\displaystyle {\mathfrak {M_{2}}}\,\!}
s
{\displaystyle \mathrm {s} \,\!}
M
2
{\displaystyle {\mathfrak {M_{2}}}\,\!}
any variable assignment. The formula (a sentence) of (12) and (14) is false, and so the goal of (12) is met.
![{\displaystyle <\!{\mathfrak {M_{2}}},\ \mathrm {s} [x\!:\,i,x\!:\,j]\!>\ \vDash \mathrm {F} (x,y)\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a430a5fb616c5367c810a5cba055aed20f5fd308)
![{\displaystyle <\!{\mathfrak {M_{2}}},\ \mathrm {s} [x\!:\,i,x\!:\,j]\!>\ \vDash \mathrm {F} (y,x)\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/56db4c668f9ccae6b639d459446b24da2afe694c)
