Satisfaction
The rules for assigning truth to sentences of
should say, in effect, that
![{\displaystyle \forall \alpha \,\varphi \,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/13fb906bb0986fb26843aed9b41c52c7889e0838)
is true if and only if
is true of every object in the domain. There are two problems. First,
will normally have free variables. In particular, it will normally have free
. But formulae with free variables are not sentences and do not have a truth value. Second, we do not yet have a precise way of saying that
is true of every object in the domain. The solution to these problems comes in two parts.
- We will need an assignment of objects from the domain to the variables.
- We will need to say that a model satisfies (or does not satisfy) a formula with a variable assignment.
We can then define truth in a model in terms of satisfaction.
Variable assignment
Given model
, a variable assignment
is a function assigning each variable of
a member of
. The function
is defined for all variables of
, so each one is assigned a member of the domain.
Okay, we have assignments of domain members to variables. We also have an assignment of domain members to constant symbols—this achieved by the model's interpretation function. Now we need to use this information to generate assignments of domain members to arbitrary terms including, in addition to constant symbols and variables, complex terms formed by using n-place operation letters where n is greater than 0. This is accomplished by an extended variable assignment
defined below. Remember that
is the interpretation function of model
. It assigns semantic values to the operation letters and predicate letters of
.
An extended variable assignment
is a function making assignments as follows.
- If
is a variable, then:
![{\displaystyle {\overline {\mathrm {s} }}(\alpha )\ =\ \mathrm {s} (\alpha )\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9c0481edddd534b4668a16d4095854af9ece143f)
- If
is a constant symbol (i.e., a 0-place operation letter), then:
![{\displaystyle {\overline {\mathrm {s} }}(\alpha )\ =\ I_{\mathfrak {M}}(\alpha )\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2457da9071d68a1f2405d93c4e472aa080ea224b)
- If
is an n-place operation letter (n greater than 0) and
are terms, then:
![{\displaystyle {\overline {\mathrm {s} }}(\,\zeta (\alpha _{1},\,\alpha _{2},\,\ldots ,\,\alpha _{n})\,)\ =\ I_{\mathfrak {M}}(\zeta )\,(\ {\overline {\mathrm {s} }}(\,\alpha _{1}),\,{\overline {\mathrm {s} }}(\alpha _{2}),\,\ldots ,\,{\overline {\mathrm {s} }}(\alpha _{n})\ )\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/880560f472b42561bad5b06bc486089cca80c4e7)
Some examples may help. Suppose we have model
where:
![{\displaystyle |{\mathfrak {M}}|\ =\ \{1,\,2,\,3\}\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/095f4b9fb8401cee8c4fad69c50b22c01ab2ca6b)
![{\displaystyle I_{\mathfrak {M}}(a_{0}^{0})\ =\ 0\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7ec5bc1835e52531f6307e10c4331cddfb687de9)
![{\displaystyle I_{\mathfrak {M}}(b_{0}^{0})\ =\ 1\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/532ffbe2d56387a28ac9d1194277a9b71c127b85)
![{\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,\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0868ba6e0fc766e0d7e7d916587b47d927bb7d70)
![{\displaystyle {\mathfrak {f}}_{0}^{2}(2,\,1)=2,\ {\mbox{and}}\ {\mathfrak {f}}_{0}^{2}(2,\,2)=1\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ec0e0ff4bfcd1a112f276027b04e59df5556401f)
On the previous page, it was noted that we want the following result:
![{\displaystyle f(a,b)\ {\mbox{resolves to}}\ 1\ \mathrm {in} \ {\mathfrak {M}}\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/67e03ec885ab61e4547239e5fea6e7dd8314a3dc)
We now have achieved this because we have for any
defined on
:
![{\displaystyle =\ {\mathfrak {f}}_{0}^{2}(\ I_{\mathfrak {M}}(a),\,I_{\mathfrak {M}}(b)\ )\ =\ {\mathfrak {f}}_{0}^{2}(0,\,1)\ =\ 1\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/208978fdd0f4edcf597b37f7d3674f2c73129ede)
Suppose we also have a variable assignment
where:
![{\displaystyle \mathrm {s} (x_{0})\ =\ 0\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/311a7a1a68b5972a1376c17a367bb63e51786225)
![{\displaystyle \mathrm {s} (y_{0})\ =\ 1\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/39720d49fd4af1acc7af1a4bdf466dec81f0b415)
Then we get:
![{\displaystyle =\ {\mathfrak {f}}_{0}^{2}(f)\,(\ \mathrm {s} (x),\,\mathrm {s} (y)\ )\ =\ {\mathfrak {f}}_{0}^{2}(0,\,1)\ =\ 1\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f9d70dc7774d451629d77bfd670e2246c004b7cc)
Satisfaction
A model, together with a variable assignment, can satisfy (or fail to satisfy) a formula. Then we will use the notion of satisfaction with a variable assignment to define truth of a sentence in a model. We can use the following convenient notation to say that the interpretaion
satisfies (or does not satisfy)
with
.
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \varphi \,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4eb0658c805f67721ae7f76251736d62f9ae6916)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \not \vDash \,\varphi \,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/21b0f0befb60f90e19b504e33436fd674256ceb2)
We now define satisfaction of a formula by a model with a variable assignment. In the following, 'iff' is used to mean 'if and only if'.
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \sigma \quad {\mbox{iff}}\quad I_{\mathfrak {M}}(\sigma )\ =\ \mathrm {True} \ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7f5aac190d5b2bd96b1bfe6662d67979af1c2580)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \pi (\alpha _{0},\,\alpha _{1},\,\ldots ,\,\alpha _{n})\quad {\mbox{iff}}\ <\!{\overline {\mathrm {s} }}(\alpha _{0}),\,{\overline {\mathrm {s} }}(\alpha _{1}),\,\ldots ,\,{\overline {\mathrm {s} }}(\alpha _{n})\!>\ \in \ I_{\mathfrak {M}}(\pi )\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e1db15c9d0e0a9f1e0dcb26554cde34d76749b53)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \lnot \varphi \quad {\mbox{iff}}\ <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \not \vDash \varphi \ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/62ba26be2af23f3ec2e518a89332783b169e6229)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash (\varphi \land \psi )\quad {\mbox{iff}}\ <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \varphi \ \ {\mbox{and}}\ <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \psi \ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9f0187014b41e0183b457059d69da3903e986ec8)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash (\varphi \lor \psi )\quad {\mbox{iff}}\ <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \varphi \ \ {\mbox{or}}\ <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \psi \ {\mbox{(or both)}}\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4cf1d1cf02ba81354dd89f164afc0cab6fe0fd4a)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash (\varphi \rightarrow \psi )\quad {\mbox{iff}}\ <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \not \vDash \varphi \ \ {\mbox{or}}\ <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \psi \ {\mbox{(or both)}}\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0d7d10b7d6a7df99ef86ac808febcfb7f52bf36e)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash (\varphi \leftrightarrow \psi )\quad {\mbox{iff}}\ <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash (\varphi \land \psi )\ \ {\mbox{or}}\ <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash (\lnot \varphi \land \lnot \psi )\ {\mbox{(or both)}}\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/12a556d4a2ff881dcdf48f255e93e7575ba74850)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \forall \alpha \,\varphi \quad {\mbox{iff}}\ \ {\mbox{for every}}\ \mathrm {d} \ \in |{\mathfrak {M}}|,\ <\!{\mathfrak {M}},\ \mathrm {s[\alpha \!:\,d]} \!>\ \vDash \varphi \ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6f28a4da215c678f79f1298de5bb3fe150b06e89)
.
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \exists \alpha \,\varphi \quad {\mbox{iff}}\ \ {\mbox{for at least one}}\ \mathrm {d} \in |{\mathfrak {M}}|,\ <\!{\mathfrak {M}},\ \mathrm {s[\alpha \!:\,d]} \!>\ \vDash \varphi \ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/229f836ac6731e39bd3a84b05966c3601178900a)
.
Examples
The following continue the examples used when describing extended variable assignments above. They are based on the examples of the previous page.
A model and variable assignment for examples
Suppose we have model
where
![{\displaystyle |{\mathfrak {M}}|\ =\ \{0,\,1,\,2\}\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6a9c5f28dfab0b0d817b284fe9d6b298dec9950f)
![{\displaystyle I_{\mathfrak {M}}(a_{0}^{0})\ =\ 0\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7ec5bc1835e52531f6307e10c4331cddfb687de9)
![{\displaystyle I_{\mathfrak {M}}(b_{0}^{0})\ =\ 1\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/532ffbe2d56387a28ac9d1194277a9b71c127b85)
![{\displaystyle I_{\mathfrak {M}}(c_{0}^{0})\ =\ 2\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/066a3c59e15adcc6145c5680fdce5076b183da6d)
![{\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,\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0868ba6e0fc766e0d7e7d916587b47d927bb7d70)
![{\displaystyle {\mathfrak {f}}_{0}^{2}(2,\,1)=2,\ {\mbox{and}}\ {\mathfrak {f}}_{0}^{2}(2,\,2)=1\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ec0e0ff4bfcd1a112f276027b04e59df5556401f)
![{\displaystyle I_{\mathfrak {M}}(\mathrm {F_{0}^{2}} )\ =\ \{<\!0,\ 1\!>,\ <\!1,\ 2\!>,\ <\!2,\ 1\!>\}\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/38e8d0156c8acade8cf7678183f123868a5bbdf3)
Suppose further we have a variable assignment
where:
![{\displaystyle \mathrm {s} (x_{0})\ =\ 0\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/311a7a1a68b5972a1376c17a367bb63e51786225)
![{\displaystyle \mathrm {s} (y_{0})\ =\ 1\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/39720d49fd4af1acc7af1a4bdf466dec81f0b415)
![{\displaystyle \mathrm {s} (z_{0})\ =\ 2\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/73498f9da7dce16a10c9bfb5cb8d12a809174546)
We already saw that both of the following resove to 1:
![{\displaystyle f(a,b)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/77a9955109321538028d8b28a6878c1f4c7ada38)
![{\displaystyle f(x,y)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8837419af6cca6097deb17c7736ff2a588e0982a)
Examples without quantifiers
Given model
, the previous page noted the following further goals:
![{\displaystyle (1)\quad \mathrm {F} (a,b),\ \mathrm {F} (b,c),\ {\mbox{and}}\ \mathrm {F} (c,b)\ {\mbox{are True in}}\ {\mathfrak {M}}\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/14444f56b332357cbea176ed486e8d15bfe1e6d2)
![{\displaystyle (2)\quad \mathrm {F} (a,a)\ {\mbox{is False in}}\ {\mathfrak {M}}\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c842fdc36e869158ffbb6975574c511cb2f99488)
![{\displaystyle (3)\quad \mathrm {F} (a,f(a,b))\ {\mbox{is True in}}\ {\mathfrak {M}}\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/12086057cd1b3d8ac4e266fa94f2dea07870f254)
![{\displaystyle (4)\quad \mathrm {F} (f(a,b),a)\ {\mbox{is False in}}\ {\mathfrak {M}}\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9b42b1cd8b41ffa0806d28dc0cc812a3f16108e1)
![{\displaystyle (5)\quad \mathrm {F} (c,b)\rightarrow \mathrm {F} (a,b)\ {\mbox{is True in}}\ {\mathfrak {M}}\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fd34409967165b75e927889fdcde2eecb5a36970)
![{\displaystyle (6)\quad \mathrm {F} (c,b)\rightarrow \mathrm {F} (b,a)\ {\mbox{is False in}}\ {\mathfrak {M}}\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/26ede4841f4cff8731925d0eb0391c8c86f2a777)
We are not yet ready to evaluate for truth or falsity, but we can take a step in that direction by seeing that these sentences are satisfied by
with
Indeed, the details of
will not figure in determining which of these are satisfied. Thus
satisfies (or fails to satisfy) them with any variable assignment. As we will see on the next page, that is the criterion for truth (or falsity) in
.
Corresponding to (1),
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \mathrm {F} (a,b),\ \mathrm {F} (b,c),\ {\mbox{and}}\ \mathrm {F} (c,b)\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d00aa240e74599ceca7d8de093a2c26a75e8f3d0)
In particular:
![{\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} )\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dd1ac5f53831e3ad85147e269f386a8a5ff9bae1)
![{\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} )\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0ca1fbd70ee25ac78bc2c316818df7ce8d4d64f9)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \mathrm {F} (c,b)\ \ {\mbox{because}}\ <\!{\overline {\mathrm {s} }}(c),\,{\overline {\mathrm {s} }}(b)\!>\ =\ <\!2,\,1\!>\ \in \ I_{\mathfrak {M}}(\mathrm {F} )\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d8ae5cf4d378a25bf93ff7e893aab2b69fa91347)
Corresponding to (2) through (6) respectively:
![{\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} )\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/004f4fd7eb8157217185b6ea60dcd78a6a2e0d9e)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \mathrm {F} (a,f(a,b))\ \ {\mbox{because}}\ <\!{\overline {\mathrm {s} }}(a),\,{\overline {\mathrm {s} }}(f(a,b))\!>\ =\ <\!0,\,1\!>\ \in \ I_{\mathfrak {M}}(\mathrm {F} )\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c002790f3bb80917fe98ad765403141d0f8f0bd7)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \not \vDash \mathrm {F} (f(a,b),a)\ \ {\mbox{because}}\ <\!{\overline {\mathrm {s} }}(f(a,b),\,{\overline {\mathrm {s} }}(a)\!>\ =\ <\!1,\,0\!>\ \notin \ I_{\mathfrak {M}}(\mathrm {F} )\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2ebab2d887b26b779799bd99fc36a13b86f64ca7)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \mathrm {F} (c,b)\rightarrow \mathrm {F} (a,b)\ \ {\mbox{because}}\ <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \mathrm {F} (a,b)\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0cf657da1256aafbf550f3670ce055879bcd6465)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \not \vDash \mathrm {F} (c,b)\rightarrow \mathrm {F} (b,a)\ \ {\mbox{because}}\ <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \mathrm {F} (c,b)\ {\mbox{but}}\ <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \not \vDash \mathrm {F} (b,a)\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5afcd84f53e47e59ded27ac4bd75a08754bc048a)
As noted above, the details of
were not relevant to these evaluations. But for similar formulae using free variables instead of constant symbols, the details or
do become relevant. Examples based the above are:
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \mathrm {F} (x,y)\ \ {\mbox{because}}\ <\!{\overline {\mathrm {s} }}(x),\,{\overline {\mathrm {s} }}(y)\!>\ =\ <\!0,\,1\!>\ \in \ I_{\mathfrak {M}}(\mathrm {F} )\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e26e4ce47a154bb320b0d0a961307fe012a8b134)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \mathrm {F} (y,z)\ \ {\mbox{because}}\ <\!{\overline {\mathrm {s} }}(y),\,{\overline {\mathrm {s} }}(z)\!>\ =\ <\!1,\,2\!>\ \in \ I_{\mathfrak {M}}(\mathrm {F} )\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/564459ce3c59d5279581a0988b473bf2f54cf44f)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \mathrm {F} (z,y)\ \ {\mbox{because}}\ <\!{\overline {\mathrm {s} }}(z),\,{\overline {\mathrm {s} }}(y)\!>\ =\ <\!2,\,1\!>\ \in \ I_{\mathfrak {M}}(\mathrm {F} )\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/88bc7f9364aaf0d31ec91ec6d618bf7edf384aed)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \not \vDash \mathrm {F} (x,x))\ \ {\mbox{because}}\ <\!{\overline {\mathrm {s} }}(x),\,{\overline {\mathrm {s} }}(x)\!>\ =\ <\!0,\,0\!>\ \notin \ I_{\mathfrak {M}}(\mathrm {F} )\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8ae5bf84aea6ab4d3d98fb956c184111eaa5cd25)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \mathrm {F} (x,f(x,y))\ \ {\mbox{because}}\ <\!{\overline {\mathrm {s} }}(x),\,{\overline {\mathrm {s} }}(f(x,y))\!>\ =\ <\!0,\,1\!>\ \in \ I_{\mathfrak {M}}(\mathrm {F} )\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e7ee809e6ea6b68270dbb36be7976b5d12b9bed6)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \not \vDash \mathrm {F} (f(x,y),x)\ \ {\mbox{because}}\ <\!{\overline {\mathrm {s} }}(f(x,y),\,{\overline {\mathrm {s} }}(x)\!>\ =\ <\!1,\,0\!>\ \notin \ I_{\mathfrak {M}}(\mathrm {F} )\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8da075a85b5908773ea85fa4910fd9779f0497f0)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \mathrm {F} (z,y)\rightarrow \mathrm {F} (x,y)\ \ {\mbox{because}}\ <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \mathrm {F} (x,y)\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5e99aad97bf6b5789a4d0a00c95ab73af7ddbc8f)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \not \vDash \mathrm {F} (z,y)\rightarrow \mathrm {F} (y,x)\ \ {\mbox{because}}\ <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \mathrm {F} (z,y)\ {\mbox{but}}\ <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \not \vDash \mathrm {F} (y,x)\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/df6b3fbcc589895bdee5c6298de829a19e5ad65e)
Examples with quantifiers
Given model
, the previous page also noted the following further goals:
![{\displaystyle (7)\quad \forall x\,\forall y\,(\mathrm {F} (x,y)\rightarrow \mathrm {F} (y,x))\ {\mbox{is false in }}\ {\mathfrak {M}}\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/26bd1337116173d30230e06339aed81d2f0a854c)
![{\displaystyle (8)\quad \exists x\,\exists y\,(\mathrm {F} (x,y)\land \mathrm {F} (y,x))\ {\mbox{is true in}}\ {\mathfrak {M}}\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/41e6e838fa9c3bd6177da981384a9d407de597fc)
Again, we are not yet ready to evaluate for truth or falsity, but again we can take a step in that direction by seeing that the sentence in (7) is and the sentence in (8) is not satisfied by
with
Corresponding to (7):
![{\displaystyle (9)\quad <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \not \vDash \forall x\,\forall y\,(\mathrm {F} (x,y)\rightarrow \mathrm {F} (y,x))\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c2dfd845dcf587737a25704c009634dde97858e7)
is true if and only if at least one of the following is true:
![{\displaystyle (10)\quad <\!{\mathfrak {M}},\ \mathrm {s} [x\!:\,0]\!>\ \not \vDash \forall y\,(\mathrm {F} (x,y)\rightarrow \mathrm {F} (y,x))\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b2bb225aef4339ad168c7b6b93644e8b5b5abd67)
![{\displaystyle (11)\quad <\!{\mathfrak {M}},\ \mathrm {s} [x\!:\,1]\!>\ \not \vDash \forall y\,(\mathrm {F} (x,y)\rightarrow \mathrm {F} (y,x))\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/39a765e98043fcb9ec84516531ab3fcec676b30b)
![{\displaystyle (12)\quad <\!{\mathfrak {M}},\ \mathrm {s} [x\!:\,2]\!>\ \not \vDash \forall y\,(\mathrm {F} (x,y)\rightarrow \mathrm {F} (y,x))\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e19303a90e30de7cf733d3e0831a90c34b19a3d5)
The formula of (7) and (9) is satisfied by
if and only if it is satified by
with each of the modified variable assignments. Turn this around, and we get the formula failing to be satisfied by
if and only if it fails to be satisfied by the model with at least one of the three modified variable assignments as per (10) through (12). Similarly, (10) is true if and only if at least one of the following are true:
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} [x\!:\,0,\ y\!:\,0]\!>\ \not \vDash \mathrm {F} (x,y)\rightarrow \mathrm {F} (y,x)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/001df704ae2f359efe852100203a4571dcfeb8f2)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} [x\!:\,0,\ y\!:\,1]\!>\ \not \vDash \mathrm {F} (x,y)\rightarrow \mathrm {F} (y,x)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7be590a37a38d010c4232e966d2e97d74511d6d6)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} [x\!:\,0,\ y\!:\,2]\!>\ \not \vDash \mathrm {F} (x,y)\rightarrow \mathrm {F} (y,x)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c5fd10469c1b79afc3ff481f3e00ac36b70da134)
Indeed, the middle one of these is true. This is because
![{\displaystyle <\!0,\,1\!>\ \in \ I_{\mathfrak {M}}(\mathrm {F} )\ {\mbox{but}}\,<\!1,\,0\!>\ \not \in \ I_{\mathfrak {M}}(\mathrm {F} )\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/176bbea600d986139b915b38ac45f30d841faff5)
Thus (9) is true.
Corresponding to (8),
![{\displaystyle (13)\quad <\!{\mathfrak {M}},\ \mathrm {s} \!>\ \vDash \exists x\,\exists y\,(\mathrm {F} (x,y)\land \mathrm {F} (y,x))\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/70e76199b1b6462d6d5729f04f9804ecbc265e24)
is true if and only if at least one of the following is true:
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} [x\!:\,0]\!>\ \vDash \exists y\,(\mathrm {F} (x,y)\land \mathrm {F} (y,x))\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cb0a84fe775e44643e144b8bfcef8a6684f15511)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} [x\!:\,1]\!>\ \vDash \exists y\,(\mathrm {F} (x,y)\land \mathrm {F} (y,x))\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7fd94628ea2c1e543a7550e5ddcaf0acc41eafd0)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} [x\!:\,2]\!>\ \vDash \exists y\,(\mathrm {F} (x,y)\land \mathrm {F} (y,x))\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/17700ac3cc88a9b181f8a1d95360641dd29fb9ed)
The middle of these is true if and only if at least one of the following are true:
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} [x\!:\,1,\ y\!:\,0]\!>\ \vDash \mathrm {F} (x,y)\land \mathrm {F} (y,x)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ccf9b54bb71e87398691ac2750bbbbd74df9ffc3)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} [x\!:\,1,\ y\!:\,1]\!>\ \vDash \mathrm {F} (x,y)\land \mathrm {F} (y,x)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4de9f1db67cfb137e611234fedc0e73e395c7f50)
![{\displaystyle <\!{\mathfrak {M}},\ \mathrm {s} [x\!:\,1,\ y\!:\,2]\!>\ \vDash \mathrm {F} (x,y)\land \mathrm {F} (y,x)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/26a31ebe47044361285a65e8b68989f32dff3b72)
Indeed, the last of these is true. This is because:
![{\displaystyle <\!1,\,2\!>\ \in \ I_{\mathfrak {M}}(\mathrm {F} )\ {\mbox{and}}\,<\!2,\,1\!>\ \in \ I_{\mathfrak {M}}(\mathrm {F} )\ .\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d0da9d019741f2176986a0cd044c07b8bb10a44f)
Thus (13) is true.