\( \newcommand{\matr}[1] {\mathbf{#1}} \newcommand{\vertbar} {\rule[-1ex]{0.5pt}{2.5ex}} \newcommand{\horzbar} {\rule[.5ex]{2.5ex}{0.5pt}} \)
deepdream of a sidewalk
Show Answer
\( \newcommand{\cat}[1] {\mathrm{#1}} \newcommand{\catobj}[1] {\operatorname{Obj}(\mathrm{#1})} \newcommand{\cathom}[1] {\operatorname{Hom}_{\cat{#1}}} \newcommand{\multiBetaReduction}[0] {\twoheadrightarrow_{\beta}} \newcommand{\betaReduction}[0] {\rightarrow_{\beta}} \newcommand{\betaEq}[0] {=_{\beta}} \newcommand{\string}[1] {\texttt{"}\mathtt{#1}\texttt{"}} \newcommand{\symbolq}[1] {\texttt{`}\mathtt{#1}\texttt{'}} \)
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.