Interpretation von Termen

Einfache Sprache

Def. Interpretation von Termen

Sei $\mathcal S$ eine Signatur und $\mathcal A$ ein $\mathcal S$-Struktur.

Eine $\mathcal A$-Belegung (auch $A$-Belegung oder auch Interpretation von $A$) ist eine Funktion $\mathbf V_\mathrm{PL}\to A$.

Für jeden $\mathcal S$-Term $t$ wird dessen Bedeutung in $\mathcal A$ unter der $\mathcal A$-Belegung $\beta$, geschrieben $\textlbrackdbl t\textrbrackdbl^\mathcal A_\beta$, induktiv definiert.

Basiselemente:

• Ist $t = c$ für ein $c\in\mathcal C$, dann gilt $\textlbrackdbl t\textrbrackdbl^\mathcal A_\beta = c^\mathcal A$.
• Ist $t = x_i$ für ein $i\in\mathbb N$, dann gilt $\textlbrackdbl t\textrbrackdbl^\mathcal A_\beta = \beta(x_i)$.

Induktive Regel: Für jedes Funktionssymbol $f\in\mathcal F$ mit der Stelligkeit $n = \Sigma(f)$ und $\mathcal S$-Terme $t_0,\ldots,t_{n-1}$, dann gilt

$$\textlbrackdbl f(t_0,\ldots,t_{n-1})\textrbrackdbl^\mathcal A_\beta = f^\mathcal A(\textlbrackdbl t_0 \textrbrackdbl^\mathcal A_\beta,\ldots,\textlbrackdbl t_{n-1}\textrbrackdbl^\mathcal A_\beta)$$