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 $\LL_1$.

Let $\AA$ be an $\LL_1$-structure.

Let $\sigma$ be an assignment for $\tau$ in $\AA$.

Then the value of $\tau$ under $\sigma$, denoted $\map {\operatorname{val}_\AA} \tau \sqbrk \sigma$, is defined recursively by:

If $\tau = x$, with $x \in \Dom \sigma$ a variable in the domain of $\sigma$:
$\map {\operatorname{val}_\AA} x \sqbrk \sigma := \map \sigma x$
If $\tau = \map f {\tau_1, \ldots, \tau_n}$ with $\tau_i$ terms and $f \in \FF_n$ an $n$-ary function symbol:
$\map {\operatorname{val}_\AA} {\map f {\tau_1, \ldots, \tau_n} } \sqbrk \sigma := \map {f_\AA} {\map {\operatorname{val}_\AA} {\tau_1} \sqbrk \sigma, \ldots, \map {\operatorname{val}_\AA} {\tau_n} \sqbrk \sigma}$
where $f_\AA$ denotes the interpretation of $f$ in $\AA$.

If $\tau$ contains no variables, one writes $\map {\operatorname{val}_\AA} \tau$ instead of $\map {\operatorname{val}_\AA} \tau \sqbrk \sigma$.