"

Putting it all together

Using the above techniques, one can calculate the truth-value of any sentence in โ„’1\mathcal{L}_1, involving any number of quantifiers in any possible distribution. And in fact, one can also calculate the satisfaction of every formula of โ„’1\mathcal{L}_1 relative to an initial assignment ๐š\mathbf{a} in the structure ๐’\mathbf{S}, involving open formulas with quantifiers. At each step, one just has to apply the relevant definition for the quantifier or connective until none are left, and then calculate the satisfiability of each resulting atomic formula relative to the relevant assignments. As we shall see soon, there are various techniques that make this easier than it first appears. But first, letโ€™s formulate the semantics for our language โ„’1\mathcal{L}_1 as a whole.

Again, the semantics is compositional, where the meaning of more complex expressions will always be calculable from the meaning of their constituent parts. Thus, parallel to how we introduced the semantics above, our definition will also start with assigning meaning to the predicates and terms of the language, then to atomic formulas, and then to more complex formulas.

Returning to satisfaction and truth once more, truth will be defined as a special case of satisfaction. Namely, satisfaction is relativized to structures and variable assignments, while truth will be assigned to those formulas in a structure that are satisfied under every possible variable assignment in the domain of that structure. In other words, only some formulas satisfiable in a structure will be said to be true, those that are satisfied under every variable assignment in the domain of the structure.

Definition 7.3 (Semantics of โ„’1\mathcal{L}_1). A first-order structure ๐’\mathbf{S} is a pair โŸจ๐ƒ,IโŸฉ\langle\mathbf{D}, I\rangle where ๐ƒ\mathbf{D} is a non-empty set called the domain, and II is the interpretation function such that for every cโˆˆ๐–ข๐–ฎ๐–ญ๐–ฒโ„’1c \in \mathsf{CONS}_{\mathcal{L}_1}, I(c)โˆˆ๐ƒI(c) \in \mathbf{D}, and for every predicate of arity nn, I(Pn)โŠ†๐ƒnI(P^n) \subseteq \mathbf{D}^n.

The function ๐š:๐–ต๐– ๐–ฑโ„’1โ†’๐ƒ\mathbf{a}: \textsf{VAR}_{\mathcal{L}_1} \to \mathbf{D} is a variable assignment in ๐ƒ\mathbf{D}. If ๐šโ€ฒ\mathbf{a}' is a variable assignment in ๐ƒ\mathbf{D} just like ๐š\mathbf{a}, except possibly for some xx, ๐šโ€ฒ(x)โ‰ ๐š(x)\mathbf{a}'(x)\neq \mathbf{a}(x), we call ๐šโ€ฒ\mathbf{a}' an xx-variant variable assignment of ๐š\mathbf{a}. If ๐šโ€ฒ(x)=d\mathbf{a}'(x)=d (dโˆˆ๐ƒd \in \mathbf{D}), i.e., ๐šโ€ฒ\mathbf{a}' is the xx-variant variable assignment of ๐š\mathbf{a} such that xx is sent to dd by ๐šโ€ฒ\mathbf{a}', we may also write ๐šdx\mathbf{a}^x_d.

For each term tโˆˆ๐–ณ๐–ค๐–ฑ๐–ฌโ„’1t \in \mathsf{TERM}_{\mathcal{L}_1}, we define the value of tt in the structure ๐’\mathbf{S} relative to the variable assignment ๐š\mathbf{a} as follows:

  1. if t=xt=x for some xโˆˆ๐–ต๐– ๐–ฑโ„’1x \in \textsf{VAR}_{\mathcal{L}_1}, I(t)[๐š]=๐š(x)I(t)[\mathbf{a}]=\mathbf{a}(x);

  2. if t=ct=c for some cโˆˆ๐–ข๐–ฎ๐–ญ๐–ฒโ„’1c \in \textsf{CONS}_{\mathcal{L}_1}, I(t)[๐š]=I(c)I(t)[\mathbf{a}]=I(c).

We define satisfaction for a formula XX relative to ๐’\mathbf{S} under ๐š\mathbf{a}, in symbols, ๐’โŠจX[๐š]\mathbf{S} \models X[\mathbf{a}] as follows:

  1. For the base: if X=Pn(t1,...,tn)X=P^n(t_1, …, t_n), then ๐’โŠจX[๐š]\mathbf{S} \models X[\mathbf{a}] iff โŸจI(t1)[๐š],...,I(tn)[๐š]โŸฉโˆˆI(Pn)\langle I(t_1)[\mathbf{a}], …, I(t_n)[\mathbf{a}]\rangle \in I(P^n).

  2. For the connectives:

    1. if X=ยฌYX=\neg Y, ๐’โŠจX[๐š]\mathbf{S} \models X[\mathbf{a}] iff ๐’โŠจฬธY[๐š]\mathbf{S} \not\models Y[\mathbf{a}];

    2. if X=(YโˆงZ)X=(Y \wedge Z), ๐’โŠจX[๐š]\mathbf{S} \models X[\mathbf{a}] iff ๐’โŠจY[๐š]\mathbf{S} \models Y[\mathbf{a}] and ๐’โŠจZ[๐š]\mathbf{S}\models Z[\mathbf{a}];

    3. if X=(YโˆจZ)X=(Y \vee Z), ๐’โŠจX[๐š]\mathbf{S} \models X[\mathbf{a}] iff ๐’โŠจY[๐š]\mathbf{S} \models Y[\mathbf{a}] or ๐’โŠจZ[๐š]\mathbf{S}\models Z[\mathbf{a}] (or both);

    4. if X=(Yโ†’Z)X=(Y \rightarrow Z), ๐’โŠจX[๐š]\mathbf{S} \models X[\mathbf{a}] iff if ๐’โŠจY[๐š]\mathbf{S} \models Y[\mathbf{a}], then ๐’โŠจZ[๐š]\mathbf{S}\models Z[\mathbf{a}].

  3. For the quantifiers:

    1. if X=โˆƒxYX =\exists x Y, then ๐’โŠจX[๐š]\mathbf{S} \models X[\mathbf{a}] iff there is an xx-variant assignment ๐šโ€ฒ\mathbf{a}' such that ๐’โŠจY[๐šโ€ฒ]\mathbf{S} \models Y[\mathbf{a}'];

    2. if X=โˆ€xYX =\forall x Y, then ๐’โŠจX[๐š]\mathbf{S} \models X[\mathbf{a}] iff for every xx-variant assignment ๐šโ€ฒ\mathbf{a}', ๐’โŠจY[๐šโ€ฒ]\mathbf{S} \models Y[\mathbf{a}'].

We say that a formula XX is true in (or relative to) ๐’\mathbf{S} iff for every assignment ๐š\mathbf{a} (in ๐ƒ\mathbf{D} of ๐’\mathbf{S}), ๐’โŠจX[๐š]\mathbf{S} \models X[\mathbf{a}]. We say that a formula XX is false in (or relative to) ๐’\mathbf{S} iff for every assignment ๐š\mathbf{a} (in ๐ƒ\mathbf{D} of ๐’\mathbf{S}), ๐’โŠจฬธX[๐š]\mathbf{S} \not\models X[\mathbf{a}].

You may see something strange with this definition of falsity. In particular, we defined a formula XX being false not as it not being true, but as a separate condition (namely, being unsatisfied under every assignment in ๐’\mathbf{S}). The reason why this is the case is precisely because some formulas cannot be said to be true or false, as they depend on the assignment function for their evaluation. Accordingly, if we specified that the formulas that are not true are false, we would have had to deem false those formulas that are sometimes satisfied, sometimes arenโ€™t in ๐’\mathbf{S}. It should be noted however that as far as sentences are concerned, a sentence not being true does entail it being false, so we are not violating the Law of Excluded Middle.

License

Icon for the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License

Learning Logic Backwards Copyright © by Peter Susanszky is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License, except where otherwise noted.