\( \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 Question
\( \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) = 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