# Definition:Value of Formula under Assignment

## Definition

Let $\mathbf A$ be a WFF in the language of predicate logic $\LL_1$.

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

Let $\sigma$ be an assignment for $\mathbf A$ in $\AA$.

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

If $\mathbf A = \map p {\tau_1, \ldots, \tau_n}$ with $\tau_i$ terms and $p \in \PP_n$ an $n$-ary predicate symbol:
$\map {\operatorname{val}_\AA} {\map p {\tau_1, \ldots, \tau_n} } \sqbrk \sigma := \map {p_\AA} {\map {\operatorname{val}_\AA} {\tau_1} \sqbrk \sigma, \ldots, \map {\operatorname{val}_\AA} {\tau_n} \sqbrk \sigma}$
where $p_\AA$ denotes the interpretation of $p$ in $\AA$ and $\map {\operatorname{val}_\AA} {\tau_i} \sqbrk \sigma$ is the value of $\tau_i$ under $\sigma$.
If $\mathbf A = \neg \mathbf B$ with $\mathbf B$ a WFF:
$\map {\operatorname{val}_\AA} {\neg \mathbf B} \sqbrk \sigma := \map {f^\neg} {\map {\operatorname{val}_\AA} {\mathbf B} \sqbrk \sigma}$
where $f^\neg$ denotes the truth function of $\neg$.
If $\mathbf A = \paren {\mathbf B \circ \mathbf B'}$ with $\mathbf B, \mathbf B'$ WFFs and $\circ$ one of $\land, \lor, \implies, \iff$:
$\map {\operatorname{val}_\AA} {\mathbf B \circ \mathbf B'} \sqbrk \sigma := \map {f^\circ} {\map {\operatorname{val}_\AA} {\mathbf B} \sqbrk \sigma, \map {\operatorname{val}_\AA} {\mathbf B'} \sqbrk \sigma}$
where $f^\circ$ denotes the respective truth function of $\circ$.
If $\mathbf A = \left({ \exists x: \mathbf B}\right)$ with $x \in \mathrm{VAR}$ and $\mathbf B$ a WFF:
$\map {\operatorname{val}_\AA} {\exists x: \mathbf B} \sqbrk \sigma := \begin{cases} \T & \text{if } \exists a \in A: \map {\operatorname{val}_\AA} {\mathbf B} \sqbrk {\sigma + \paren {x / a} } = \T \\ \F & \text{otherwise} \end{cases}$
where $\sigma + \paren {x / a}$ is the extension of $\sigma$ by mapping $x$ to $a$.
If $\mathbf A = \left({\forall x: \mathbf B}\right)$ with $x \in \mathrm{VAR}$ and $\mathbf B$ a WFF:
$\map {\operatorname{val}_\AA} {\forall x: \mathbf B} \sqbrk \sigma := \begin{cases} \T & \text{if } \forall a \in A: \map {\operatorname{val}_\AA} {\mathbf B} \sqbrk {\sigma + \paren {x / a} } = \T \\ \F & \text{otherwise} \end{cases}$
where $\sigma + \paren {x / a}$ is the extension of $\sigma$ by mapping $x$ to $a$.

### Sentence

Let $\mathbf A$ be a sentence in the language of predicate logic.

The value of $\mathbf A$ in $\AA$, denoted $\map {\operatorname{val}_\AA} {\mathbf A}$, is defined as:

$\map {\operatorname{val}_\AA} {\mathbf A} := \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk \O$

where $\O$ is the empty mapping considered as an assignment for $\mathbf A$ and $\map { \operatorname{val}_\AA} {\mathbf A} \sqbrk \O$ is the value of $\mathbf A$ under $\O$.