Semantics of first-order logic
From Learning Logic for Computer Science
Every first-order formula evaluates to a truth value in a structure under a variable assignment.
Contents
Preparation: variable assignments
Variables are an important ingredient of first-order formulas. So interpreting a first-order formula only makes sense in a context where variables are assigned values. Given a structure $\mathcal A$, an $A$-assignment (or $\mathcal A$-assignment or $A$-variable assignment or $\mathcal A$-variable assignment) is a function $\{x_0, x_1, \dots \} \to A$.
In the definition of the semantics of the quantifiers $\forall$ and $\exists$, variable assignments need to be modified in one place. The notation for this is as follows. If $\beta$ is an $\mathcal A$-assignment, $i \in \mathbf N$, and $a \in A$, then $\beta\left[\frac{x_i}{a}\right]$ is the $A$-assignment defined by \begin{align} \beta\left[\frac{x_i}{a}\right](x_j) & = \begin{cases}a & \text{if } i = j\\ \beta(x_j) & \text{otherwise}\end{cases} \end{align}
Interpretation of terms
Let $\mathcal S$ be a signature and $\mathcal A$ an $\mathcal S$-structure. For a given $A$-assignment $\beta$, the value of any $\mathcal S$-term $t$ in $\mathcal A$ under $\beta$, denoted $\llbracket t\rrbracket_\beta^\mathcal A$, is defined by induction.
Base mapping.
- For every $i \in \mathbf N$, \begin{align}\llbracket x_i \rrbracket_\beta^\mathcal A = \beta(x_i) \enspace.\end{align}
- For every $c \in \mathcal C$, \begin{align}\llbracket c \rrbracket_\beta^\mathcal A = c^\mathcal A \enspace.\end{align}
Inductive rule.
- For every $f/\!/n \in \mathcal F$ and $\mathcal S$-terms $t_0, \dots, t_{n-1}$, \begin{align}\llbracket f(t_0, \dots, t_{n-1})\rrbracket_\beta^\mathcal A = f^\mathcal A(\llbracket t_0\rrbracket_\beta^\mathcal A, \dots, \llbracket t_{n-1}\rrbracket_\beta^\mathcal A) \enspace.\end{align}
Interpretation of formulas
Let $\mathcal S$ be a signature and $\mathcal A$ an $\mathcal S$-structure. For a given $A$-assignment $\beta$, the value of any $\mathcal S$-formula $\varphi$ in $\mathcal A$ under $\beta$, denoted $\llbracket \varphi\rrbracket_\beta^\mathcal A$, is defined by induction.
Base mapping.
- For the boolean constant symbols,\begin{align}\llbracket \bot \rrbracket_\beta^\mathcal A & = 0\\ \llbracket \top \rrbracket_\beta^\mathcal A & = 1\enspace.\end{align}
- For all $\mathcal S$-terms $t_0, t_1$, \begin{align}\llbracket t_0 \doteq t_1 \rrbracket_\beta^\mathcal A = \begin{cases}1 & \text{if } \llbracket t_0 \rrbracket_\beta^\mathcal A = \llbracket t_1 \rrbracket_\beta^\mathcal A\\ 0 & \text{otherwise}\end{cases} \enspace.\end{align}
- For every $R/n \in \mathcal R$ and $\mathcal S$-terms $t_0, \dots, t_{n-1}$, \begin{align}\llbracket R(t_0, \dots, t_{n-1})\rrbracket = \begin{cases}1 & \text{if } \langle \llbracket t_0 \rrbracket_\beta^\mathcal A, \dots, \llbracket t_{n-1} \rrbracket_\beta^\mathcal A\rangle \in R^\mathcal A\\ 0 & \text{otherwise}\end{cases} \end{align}
Inductive rules.
- For every $n$-ary connective $C$ and $\mathcal S$-formulas $\varphi_0, \dots, \varphi_{n-1}$, \begin{align}\llbracket C(\varphi_0, \dots, \varphi_{n-1})\rrbracket_\beta^\mathcal A = f_C(\llbracket \varphi_0 \rrbracket_\beta^\mathcal A, \dots, \llbracket \varphi_{n-1} \rrbracket_\beta^\mathcal A)\end{align}
- For every $\mathcal S$-formula $\varphi$ and $i \in \mathbf N$, \begin{align} \llbracket \exists x_i \varphi \rrbracket_\beta^\mathcal A & = \begin{cases}1 & \text{if there exists some $a \in A$ s.th. }\llbracket \varphi\rrbracket_{\beta\left[\frac{x_i}{a}\right]}^\mathcal A = 1\\ 0 & \text{otherwise}\end{cases}\\ \llbracket \forall x_i \varphi \rrbracket_\beta^\mathcal A & = \begin{cases}1 & \text{if for all $a \in A$: }\llbracket \varphi\rrbracket_{\beta\left[\frac{x_i}{a}\right]}^\mathcal A = 1\\ 0 & \text{otherwise}\end{cases} \end{align}
Example Let $\mathcal S = \{\text{one}, \text{add}/\!/2, \text{LT}/2\}$ and $\mathcal A$ the structure given by \begin{align} A &= \mathbf N\\ \text{one}^\mathcal A & = 1\\ \text{add}^\mathcal A & = {+}\\ \text{LT}^\mathcal A & = {<} \end{align} where $+$ denotes addition on the natural numbers and $<$ denotes the "less-than" relation on the natural numbers. Further, let $\varphi$ be defined by \begin{align} \varphi & = \exists x_1 \text{LT}(\text{add}(x_1, \text{one}), x_0) \enspace. \end{align} In order to determine $\llbracket \varphi \rrbracket_\beta^\mathcal A$, the first step is to interprete the terms in $\varphi$. Let $\beta$ be any $A$-assignment. Then \begin{align} \llbracket \text{add}(x_1, \text{one}) \rrbracket_\beta^\mathcal A & = \llbracket x_1 \rrbracket_\beta^\mathcal A + \llbracket \text{one} \rrbracket_\beta^\mathcal A && \text{inductive rule in def. of semantics of terms}\\ & = \beta(x_1) + 1 && \text{base mapping in def. of semantics of terms} \end{align} In the same way, one obtains \begin{align} \llbracket x_0 \rrbracket_\beta^\mathcal A & = \beta(x_0) \enspace. \end{align} Next, the definition of the semantics of formulas tells us that \begin{align} \llbracket \text{LT}(\text{add}(x_1, \text{one}), x_0) \rrbracket_\beta^\mathcal A & = 1 \end{align} holds if, and only if, \begin{align} \langle \llbracket \text{add}(x_1, \text{one}) \rrbracket_\beta^\mathcal A, \llbracket x_0 \rrbracket_\beta^\mathcal A \rangle \in {<} \enspace. \end{align} By the above, this is equivalent to \begin{align} \langle \beta(x_1) + 1, \beta(x_0) \rangle \in {<} \enspace. \end{align} The latter is typically written as \begin{align} \beta(x_1) + 1 < \beta(x_0) \enspace. \end{align}
Finally, according to the semantics of the existential quantifier, $\llbracket \varphi \rrbracket_\beta^\mathcal A = 1$ if, and only if, there exists some $a \in \mathbf N$ such that \begin{align} \llbracket \text{LT}(\text{add}(x_1, \text{one}), x_0) \rrbracket_{\beta\left[\frac{x_1}{a}\right]}^\mathcal A = 1 \enspace. \end{align} By the above, this is equivalent to: there exists some $a \in \mathbf N$ such that \begin{align} \beta\left[\frac{x_1}{a}\right](x_1) + 1 < \beta(x_0) \enspace. \end{align} The left-hand side can be simplified: \begin{align} a + 1 < \beta(x_0) \enspace. \end{align} An $a \in \mathbf N$ with such a property exists if, and only if, $\beta(x_0) \geq 2$.
Summing up, we have \begin{align} \llbracket \varphi \rrbracket_\beta^\mathcal A & = \begin{cases} 1 & \text{if }\beta(x_0) \geq 2\\ 0 & \text{otherwise.} \end{cases} \end{align}
Notation and terminology
Often, the condition $\llbracket \varphi \rrbracket_\beta^\mathcal A = 1$ is expressed as $\mathcal A, \beta \mymodels \varphi$. Then $\mathcal A$ together with $\beta$ is said to be a model of $\varphi$.
The same applies to sets of formulas: if $\Phi$ is a set of $\mathcal S$-formulas, $\mathcal A$ is an $\mathcal S$-structure, and $\beta$ an $A$-assignment, then $\mathcal A, \beta \mymodels \Phi$ means $\llbracket \varphi \rrbracket_\beta^\mathcal A = 1$ for all $\varphi \in \Phi$, and, in this case, $\mathcal A, \beta$ is said to be a model of $\Phi$.
Exercises
Exercise Die Signatur $\mathcal S$ sei definiert durch $\mathcal S = \{\text{in}, \text{out}, E/2\}$. Definieren Sie für jedes $i \in \{0, 1, 2, 3\}$ eine $\mathcal S$-Struktur $\mathcal A_i$, die den (ggf. undendlichen) Graphen $G_i$ mit Ein- und Ausgangsknoten modelliert.
Betrachten Sie die folgenden vier Graphen $G_0$, $G_1$, $G_2$ und $G_3$ von denen jeder genau einen Eingangs- und einen Ausgangsknoten hat.
| $G_0$ | $G_1$ | $G_2$ | $G_3$ |
|---|---|---|---|
|
|
|
|
For the signature $\mathcal S = \{\text{in}, \text{out}, E/2\}$ we define the following four $\mathcal S$-structures, which represent the graphs $G_0$, $G_1$, $G_2$ and $G_3$ :
\begin{align*} \mathcal{A}_0:\quad \text{universe: } A_0 &= \{0,\,1,\,2\}\\ \text{in}^{\mathcal{A}_0}&=0\\ \text{out}^{\mathcal{A}_0}&=2\\ \text{E}^{\mathcal{A}_0}&=\{(0,1),\,(1,2),\,(2,0)\} \end{align*}
\begin{align*} \mathcal{A}_1:\quad \text{universe: } A_1 &= \{0,\,1,\,2,\,3,\,4\}\\ \text{in}^{\mathcal{A}_1}&=0\\ \text{out}^{\mathcal{A}_1}&=2\\ \text{E}^{\mathcal{A}_1}&=\{(0,1),\,(1,3),\,(2,0),\,(2,4),\,(4,1),\,(4,2),\,(4,3)\} \end{align*}
\begin{align*} \mathcal{A}_2:\quad \text{universe: } A_2 &= \mathbb{N}_0\\ \text{in}^{\mathcal{A}_2}&=0\\ \text{out}^{\mathcal{A}_2}&=0\\ \text{E}^{\mathcal{A}_2}&=\{ (a,b)\in A_2^2 \mid a=b \text{ or } a+1=b\} \end{align*}
\begin{align*} \mathcal{A}_3:\quad \text{universe: } A_3 &= \{0,1\}^*\\ \text{in}^{\mathcal{A}_3}&=\varepsilon\\ \text{out}^{\mathcal{A}_3}&=\varepsilon\\ \text{E}^{\mathcal{A}_3}&=\{ (a,ab) \mid a\in A_3 \text{ and } b\in \{0,1\}\} \end{align*}
Exercise Sei $\mathcal S = \{\dot{\varepsilon}, \dot{0}, \dot{1}, \text{conc}/\!/2, L/1 \}$ eine Signatur. Zu den Sprachen $L_1=\{ww^\top\mid\Sigma^*\}$ und $L_2=\{w\in\Sigma^*\mid |w|_0 = 0 \}$ über dem binären Alphabet $\Sigma=\{0,1\}$ seien die $\mathcal{S}$-Strukturen $\mathcal{A}_1$ und $\mathcal{A}_2$ mit \begin{align*} A_i &= \{0,1\}^* \\ L^{\mathcal A_i} &= L_i \\ \text{conc}^{\mathcal A_i}(x,y) &= xy \text{ für $x,y\in\{0,1\}^*$} \\ \dot{\varepsilon}^{\mathcal A_i} &= \varepsilon \\ \dot{0}^{\mathcal A_i} &= 0 \\ \dot{1}^{\mathcal A_i} &= 1 \\ \end{align*} für $i\in\{1,2\}$ definiert.
Weiter sei $\beta\colon \{x_0, x_1, \dots\}\to \Sigma^*$ eine Belegung mit $\beta(x_0) = 10$ und $\beta(x_1)=0001$. Bestimmen Sie die Werte der folgenden Ausdrücke unter Rückgriff auf die Definition der Semantik von $\mathcal{S}$-Termen und $\mathcal{S}$-Formeln.
- $\llbracket \text{conc}(x_0,\text{conc}(\dot{1},x_1)) \rrbracket_{\beta}^{\mathcal{A_1}}$
- $\llbracket L(\text{conc}(x_0,x_1)) \rrbracket_{\beta}^{\mathcal{A_1}}$
- $\llbracket \exists x_0\; L(\text{conc}(x_0,x_0)) \rrbracket_{\beta}^{\mathcal{A_1}}$
- $\llbracket \forall x_0\; L(\text{conc}(x_0, \dot{1})) \rrbracket_{\beta}^{\mathcal{A_2}}$
\begin{align*} \llbracket \text{conc}(x_0,\text{conc}(\dot{1},x_1)) \rrbracket_{\beta}^{\mathcal{A_1}} &= \llbracket x_0 \rrbracket_{\beta}^{\mathcal{A_1}}\llbracket \text{conc}(\dot{1},x_1) \rrbracket_{\beta}^{\mathcal{A_1}} && \text{Semantik von Termen (Induktionsregel), Def. $\operatorname{conc}^{\mathcal A_1}$} \\ &= \llbracket x_0 \rrbracket_{\beta}^{\mathcal{A_1}}(\llbracket \dot{1} \rrbracket_{\beta}^{\mathcal{A_1}}\llbracket x_1\rrbracket_{\beta}^{\mathcal{A_1}}) && \text{Semantik von Termen (Induktionsregel), Def. $\operatorname{conc}^{\mathcal A_1}$} \\ &= \beta(x_0)(\dot{1}^{\mathcal A}\beta(x_1)) && \text{$3\times$ Semantik von Termen (Basisregel)} \\ &= 10 (\dot{1}^{\mathcal A}0001) && \text{$2\times$ Def. $\beta$} \\ &= 10 (10001) && \text{Def. $\dot{1}^{\mathcal A}$} \\ &= 1010001\\ \end{align*}
\begin{align*} &&\llbracket \text{conc}(x_0,x_1) \rrbracket_{\beta}^{\mathcal{A_1}} &= \llbracket x_0 \rrbracket_{\beta}^{\mathcal{A_1}}\llbracket x_1 \rrbracket_{\beta}^{\mathcal{A_1}} && \text{Semantik von Termen (Induktionsregel), Def. $\operatorname{conc}^{\mathcal A_1}$} \\ &&&= \beta(x_0)\beta(x_1) && \text{$2\times$ Semantik von Termen (Basisregel)} \\ &&&= 100001 && \text{$2\times$ Def. $\beta$} \\ &&&= 100(100)^{\top} && \text{Def. $w^{\top}$, $xy$ für $x,y,w\in\{0,1\}^*$}\\ &&&\in L_1 && \text{Def. $L_1$} \\ &\text{ dann gilt } & \llbracket \text{conc}(x_0,x_1) \rrbracket_{\beta}^{\mathcal{A_1}}&\in L^{\mathcal A_1} && \text{Def. $L^{\mathcal A_1} = L_1$}\\ &\text{ dann gilt } & \llbracket L(\text{conc}(x_0,x_1)) \rrbracket_{\beta}^{\mathcal{A_1}} &= 1 && \text{Def. $\llbracket L(\dots)\rrbracket$ (Induktionsregel)}\\ \end{align*}- Zunächst gilt für jedes $a\in A_1$: \begin{align*} &&\llbracket \text{conc}(x_0,x_0) \rrbracket_{\beta\left[\frac{x_0}{a}\right]}^{\mathcal{A_1}} &= \llbracket x_0 \rrbracket_{\beta\left[\frac{x_0}{a}\right]}^{\mathcal{A_1}}\llbracket x_0 \rrbracket_{\beta\left[\frac{x_0}{a}\right]}^{\mathcal{A_1}} && \text{Semantik von Termen (Induktionsregel), Def. $\operatorname{conc}^{\mathcal A_1}$} \\ &&&= \beta\left[\frac{x_0}{a}\right](x_0)\beta\left[\frac{x_0}{a}\right](x_0) && \text{$2\times$ Semantik von Termen (Basisregel)} \\ &&&= aa && \text{$2\times$ Def. $\beta\left[\frac{x_0}{a}\right]$} \\ \end{align*} Es folgt: \begin{align*} &\text{dann gilt }& \llbracket \text{conc}(x_0,x_0) \rrbracket_{\beta\left[\frac{x_0}{1}\right]}^{\mathcal{A_1}} &= 11 && \text{siehe oben, $1\in A_1$} \\ &\text{dann gilt }& \llbracket \text{conc}(x_0,x_0) \rrbracket_{\beta\left[\frac{x_0}{1}\right]}^{\mathcal{A_1}} &\in L_1 && \text{Def. $L_1$, $11=11^{\top}\in L_1$} \\ &\text{dann gilt }& \llbracket \text{conc}(x_0,x_0) \rrbracket_{\beta\left[\frac{x_0}{1}\right]}^{\mathcal{A_1}} &\in L^{\mathcal{A}_1} && \text{Def. $L^{\mathcal{A}_1}=L_1$} \\ &\text{dann gilt }& \llbracket L(\text{conc}(x_0,x_0)) \rrbracket_{\beta\left[\frac{x_0}{1}\right]}^{\mathcal{A_1}} &=1 && \text{Def. $\llbracket L(\dots)\rrbracket$} \\ &\text{dann gibt es ex. $a\in A_1$}& \llbracket L(\text{conc}(x_0,x_0)) \rrbracket_{\beta\left[\frac{x_0}{a}\right]}^{\mathcal{A_1}} &=1 && \text{Umgeschrieben mit $a=1$} \\ &\text{dann gilt }& \llbracket \exists x_0\; L(\text{conc}(x_0,x_0)) \rrbracket_{\beta}^{\mathcal{A_1}} &=1 && \text{Def. $\llbracket \exists x_0\;\cdot\;\rrbracket$} \\ \end{align*}
- Zunächst gilt für jedes $a\in A_2$: \begin{align*} &&\llbracket \text{conc}(x_0,\dot{1} \rrbracket_{\beta\left[\frac{x_0}{a}\right]}^{\mathcal{A_1}} &= \llbracket x_0 \rrbracket_{\beta\left[\frac{x_0}{a}\right]}^{\mathcal{A_1}}\llbracket \dot{1} \rrbracket_{\beta\left[\frac{x_0}{a}\right]}^{\mathcal{A_1}} && \text{Semantik von Termen (Induktionsregel), Def. $\operatorname{conc}^{\mathcal A_1}$} \\ &&&= \beta\left[\frac{x_0}{a}\right](x_0)\dot{1}^{\mathcal A_2} && \text{$2\times$ Semantik von Termen (Basisregel)} \\ &&&= a1 && \text{$2\times$ Def. $\beta\left[\frac{x_0}{a}\right]$, Def. $\dot{1}^{\mathcal A_2}$} \\ \end{align*} Daraus folgt für jedes $a\in A_2$:\[|\llbracket \text{conc}(x_0,\dot{1} \rrbracket_{\beta\left[\frac{x_0}{a}\right]}^{\mathcal{A_1}}|_0 = |a1|_0 = |a|_0.\] Nach Definition von $L^{\mathcal A_2} = L_2$ ist $\llbracket \text{conc}(x_0,\dot{1} \rrbracket_{\beta\left[\frac{x_0}{a}\right]}^{\mathcal{A_1}}\in L^{\mathcal A_2}$ genau dann wenn, $|\llbracket \text{conc}(x_0,\dot{1} \rrbracket_{\beta\left[\frac{x_0}{a}\right]}^{\mathcal{A_1}}|_0 = 0$, also genau dann wenn $|a|_0 = 0$. Weiter gilt dann nach der induktiven Regel der Definition der Semantik von Formeln, dass \[\llbracket L(\text{conc}(x_0,\dot{1} )\rrbracket_{\beta\left[\frac{x_0}{a}\right]}^{\mathcal{A_1}} = 1 \quad \text{gdw.}\quad |a|_0 = 0.\] Da $0\in A_2$, aber $|0|_0 = 1 \neq 0$ ist, gilt nicht für alle $a\in A_2$, dass $\llbracket L(\text{conc}(x_0,\dot{1} )\rrbracket_{\beta\left[\frac{x_0}{a}\right]}^{\mathcal{A_1}} = 1$. Nach der induktiven Definition der Semantik von Formeln für den Allquantor folgt damit, dass \[\llbracket \forall x_0\; L(\text{conc}(x_0, \dot{1})) \rrbracket_{\beta}^{\mathcal{A_2}} = 0\]
Exercise Die Signatur $\mathcal S$ ist definiert durch $\mathcal S = \{\text{one}, \text{mult}/\!/2\}$.
Betrachten Sie die folgenden drei Multiplikationstabellen.
| $M_0$ | 0 | 1 |
|---|---|---|
| 0 | 0 | 0 |
| 1 | 0 | 1 |
| $M_1$ | 1 | 2 |
|---|---|---|
| 1 | 1 | 2 |
| 2 | 2 | 1 |
| $M_2$ | 0 | 1 | 2 | ... |
|---|---|---|---|---|
| 0 | 0 | 1 | 2 | ... |
| 1 | 1 | 2 | 3 | ... |
| 2 | 2 | 3 | 4 | ... |
| ... | ... | ... | ... | ... |
Definieren Sie für jedes $i \in \{0, 1, 2\}$ eine $\mathcal S$-Struktur $\mathcal A_i$, die das Monoid $M_i$ modelliert. (Finden Sie dazu jeweils heraus, was das neutrale Element ist.)
Es sei $\beta$ eine auf $\{x_0, x_1, \dots\}$ definierte Funktion, für die $\beta(x_0) = 1$ gelte. Bestimmen Sie für jedes $i \in \{0, 1, 2\}$ den Wert \begin{align} \llbracket \text{mult}(\text{mult}(x_0,x_0),\text{mult}(\text{one}, x_0))\rrbracket_\beta^{\mathcal A_i} \end{align} unter Rückgriff auf die Definition der Semantik von Termen.
Exercise Sei $\mathcal S = \{\text{suc}/\!/1, \text{pred}/\!/1\}$ eine Signatur. Dann ist beispielsweise $\text{suc}(\text{pred}(\text{suc}(x_i)))$ ein $\mathcal S$-Term, für den wir auch einfach $sps(x_i)$ schreiben. Das heißt, wenn $u$ eine Folge ist, die aus den Buchstaben $s$ und $p$ besteht, dann steht $u(x_j)$ für einen $\mathcal S$-Term. Wir schreiben $|u|_s$ für die Anzahl der Vorkommen von $s$ und $|u|_p$ für die Anzahl der Vorkommen von $p$ in $u$. Beweisen Sie die folgende Behauptung per vollständiger Induktion:
Ist $\mathcal A$ eine $\mathcal S$-Struktur, für die $\mathcal A \mymodels \forall x_0\, \text{suc}(\text{pred}(x_0)) \doteq x_0 \wedge \forall x_0\, \text{pred}(\text{suc}(x_0)) \doteq x_0$ gilt, und sind $u$ und $v$ Wörter mit $|u|_s - |u|_p = |v|_s - |v|_p$, dann gilt $\llbracket u(x_0)\rrbracket_{\beta}^{\mathcal {A}} = \llbracket v(x_0)\rrbracket_{\beta}^{\mathcal {A}}$ für alle Belegungen $\beta$.
Anders ausgedrückt: Es gilt dann $\mathcal A \mymodels \forall x_0\, (u(x_0) \doteq v(x_0))$.
Zum Beispiel gilt etwa $spps(x_0) = sspp(x_0)$.
Hinweis Zeigen Sie dazu die Hilfsaussage, dass $\llbracket u(x_0) \rrbracket_\beta^{\mathcal A}=\llbracket w_u(x_0) \rrbracket_\beta^{\mathcal A}$ mit $w_u=\begin{cases}s^{|u|_s-|u|_p},&\text{ falls $|u|_s\geq |u|_p$}\\p^{|u|_p-|u|_s},&\text{falls }|u|_p >|u|_s\end{cases}$ gilt.