Definition:Value of Term under Assignment

From ProofWiki
Jump to navigation Jump to search


Let $\tau$ be a term in the language of predicate logic $\mathcal L_1$.

Let $\mathcal A$ be an $\mathcal L_1$-structure.

Let $\sigma$ be an assignment for $\tau$ in $\mathcal A$.

Then the value of $\tau$ under $\sigma$, denoted $\mathop{ \operatorname{val}_{\mathcal A} \left({\tau}\right) } \left[{\sigma}\right]$, is defined recursively by:

If $\tau = x$, with $x \in \operatorname{dom} \left({\sigma}\right)$ a variable in the domain of $\sigma$:
$\mathop{ \operatorname{val}_{\mathcal A} \left({x}\right) } \left[{\sigma}\right] := \sigma \left({x}\right)$
If $\tau = f \left({\tau_1, \ldots, \tau_n}\right)$ with $\tau_i$ terms and $f \in \mathcal F_n$ an $n$-ary function symbol:
$\mathop{ \operatorname{val}_{\mathcal A} \left({f \left({\tau_1, \ldots, \tau_n}\right) }\right) } \left[{\sigma}\right] := f_{\mathcal A} \left({ \mathop{ \operatorname{val}_{\mathcal A} \left({\tau_1}\right) } \left[{\sigma}\right], \ldots, \mathop{ \operatorname{val}_{\mathcal A} \left({\tau_n}\right) } \left[{\sigma}\right] }\right)$
where $f_{\mathcal A}$ denotes the interpretation of $f$ in $\mathcal A$.

If $\tau$ contains no variables, one writes $\operatorname{val}_{\mathcal A} \left({\tau}\right)$ instead of $\mathop{ \operatorname{val}_{\mathcal A} \left({\tau}\right) } \left[{\sigma}\right]$.