 Show Question
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) = s(t)$$
• if $$t$$ is a constant symbol $$c$$, $$\bar{s}(t) = c^{\mathfrak{U} }$$
• if $$t$$ is $$ft_1t_2...t_n$$ for some function and term symbols, then $$\bar{s}(t) = f^{ \mathfrak{U} }(\bar{s}(t_1) \bar{s}(t_2) ... \bar{s}(t_n))$$

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 $$(\bar{s}(t_1), \bar{s}(t_2), ..., \bar{s}(t_n) ) \in R^{\mathfrak{u} }$$.
2. $$\phi :\equiv (\alpha \lor \beta)$$ and $$\mathfrak{U} \vDash \alpha$$ or $$\mathfrak{U} \vDash \beta$$.
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.

#### Extension: satisfaction for sets of $$\mathcal{L}$$-formula

Let $$\Gamma$$ be a sequence of $$\mathcal{L}$$-formulas, let $$\mathfrak{U}$$ be an $$\mathcal{L}$$-structure and let $$s$$ be a variable assignment function.

We say that $$\mathfrak{U}$$ and $$s$$ satisfy $$\Gamma$$ iff $$\mathfrak{U}$$ and $$s$$ satisfy all formula in $$\Gamma$$.

We write $$\mathfrak{U} \vDash \Gamma$$

### Meaning of $$\nvDash$$

Condition 4 introduces $$\nvDash$$ without much comment, specifically, without mentioning the excluded-middle. Does this condition work only for classical logic, and not for any logic that prohibits the excluded middle?

An argument supporting the cases that excluded-middle is not an issue: given that formulas are finite sequences of symbols (I think), it should surely be the case that an algorithm to check if a formula is satisfied by an $$\mathcal{L}$$-structure will finish in finite time. Having such a decider would allow us to define the negation without worry of an infinite loop. This seems like a reasonable justification for the definition of $$\nvDash$$.

#### Source

A Friendly Introduction to Mathematical Logic, Leary and Kristiansen