Koinzidenzlemma
Einfache Sprache
Der Wahrheitswert einer Aussagenlogischen Formel unter einer Belegung $\beta$ hängt nur von den in der Formel vorkommenden Variablen ab.
Warum ist das Interessant? Weil es die Definition von Belegungen als partielle Funktionen, da es genügt, die Belegungen der in der Formel vorkommenden Variablen anzugeben.
Letztendlich ermöglicht es uns zu sagen das: eine passende Belegung $\beta$ ist genau dann ein Modell einer einer Formel $\varphi$, wenn die knappe Belegung $\beta|_{vars(\varphi)}$ (Eine Belegung die nur die in der Formel vorkommenden Variablen belegt) ein Modell von $\varphi$ ist.
#Def $vars(\varphi)$
Gibt die in der Aussagenlogischen Formel vorkommenden Variablen aus.
Sei $\text{vars}:\mathbf F_{AL} \to \mathcal P(\mathbf V_{AL})$ definiert durch die folgenden Regeln induktiv definieren.
Induktionsanfang. $\text{vars}(\top) = \text{vars}(\bot) = \emptyset$ und $\text{vars}(X_i) = \{X_i\}$ für alle $X_i\in\mathbf V_{AL}$.
Induktionsschritt. Seien $\varphi_0, \ldots, \varphi_{n-1}$ Aussagenlogischen Formelen und $C$ ein $n$-stelliger Junktor, dann gilt
$\text{vars}(C(\varphi_0,…,\varphi_{n−1}))=\underset{i Für jede Aussagenlogischen Formel $\varphi \in \mathbf F_{AL}$ und alle Belegungen $\beta_0,\beta_1$ mit $\beta_0 |_{\text{vars}(\varphi))} = \beta_1|_{\text{vars}(\varphi)}$ gilt $\textlbrackdbl\varphi\textrbrackdbl_{\beta_0} = \textlbrackdbl\varphi\textrbrackdbl_{\beta_1}$.
#TODO Finish lemma#Def Koinzidenzlemma