Math and science::Theory of Computation::Modal theory

# Term and formula assignment

In a previous card, it was described how an $$\mathcal{L}$$-structure and a variable assignment fuction act together to identify a set theoretic interpretation for every symbol of a language. For terms and formulas, they have an interpretation assigned to them by a term assignment function and a formula assignment function. Terms get assigned to elements while (some) formulas get assigned "truth" (also called "satisfaction").

### Term assignment function

Let $$\mathcal{L}$$ be a language, and let $$\mathfrak{U}$$ be an $$\mathcal{L}$$-structure for the language. Let $$A$$ be the universe of $$\mathfrak{U}$$ and let $$s$$ be a variable assignment function.

The term assignment function, denoted $$\bar{s}$$, is a mapping of terms to elements of $$A$$. It is defined recursively and is fully determined by the combination of the $$\mathcal{L}$$-structure and the variable assignment function.

Let $$t$$ be a term, then:

• if $$t$$ is a variable symbol, [$$\bar{s}(t) = \, ? \,$$]
• if $$t$$ is a constant symbol $$c$$, [$$\bar{s}(t) = \, ? \,$$]
• if $$t$$ is $$ft_1t_2...t_n$$ for some function and term symbols, then [$$\bar{s}(t) = f^{ \mathfrak{U} }(\, ? \, )$$ ]

Formulas get a very different mapping.

### Formula assignment: truth/satisfaction

Let $$\mathcal{L}$$ be a language, and let $$\mathfrak{U}$$ be an $$\mathcal{L}$$-structure for the language. Let $$A$$ be the universe of $$\mathfrak{U}$$ and let $$s$$ be a variable assignment function (and $$\bar{s}$$ the resulting term assignment function).

Let $$\phi$$ be a formula valid in $$\mathcal{L}$$. We say that $$\phi$$ is true in $$\mathfrak{U}$$, or that $$\mathfrak{U}$$ satisfies $$\phi$$, and we write $$\mathfrak{U} \vDash \phi$$, iff one of the following conditions holds:

1. $$\phi :\equiv Rt_1t_2...t_n$$ and [$$\, ? \, \in \, ? \,$$].
2. $$\phi :\equiv (\alpha \lor \beta)$$ and [condition 1] or [condition 2].
3. $$\phi :\equiv \forall x \; (\alpha)$$ and for each element $$a \in A, \; \mathfrak{U} \vDash \alpha[s(x|a)] \;$$.
4. $$\phi :\lnot (\alpha)$$ and $$\mathfrak{U} \nvDash \alpha[s]$$.

$$\mathfrak{U} \nvDash \phi$$ means it's not the case that $$\mathfrak{U} \vDash \phi$$.

There is a discussion about the meaning of $$\nvDash$$ on the back side.