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:
- \( \phi :\equiv Rt_1t_2...t_n \) and \( (\bar{s}(t_1), \bar{s}(t_2), ..., \bar{s}(t_n) ) \in R^{\mathfrak{u} } \).
- \( \phi :\equiv (\alpha \lor \beta) \) and \( \mathfrak{U} \vDash \alpha \) or \( \mathfrak{U} \vDash \beta \).
- \( \phi :\equiv \forall x \; (\alpha) \) and for each element \( a \in A, \; \mathfrak{U} \vDash \alpha[s(x|a)] \; \).
- \( \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 \).