Definition:Value of Formula under Assignment

From ProofWiki
Jump to navigation Jump to search

Definition

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

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

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


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

If $\mathbf A = p \left({\tau_1, \ldots, \tau_n}\right)$ with $\tau_i$ terms and $p \in \mathcal P_n$ an $n$-ary predicate symbol:
$\mathop{ \operatorname{val}_{\mathcal A} \left({p \left({\tau_1, \ldots, \tau_n}\right) }\right) } \left[{\sigma}\right] := p_{\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 $p_{\mathcal A}$ denotes the interpretation of $p$ in $\mathcal A$ and $\mathop{ \operatorname{val}_{\mathcal A} \left({\tau_i}\right) } \left[{\sigma}\right]$ is the value of $\tau_i$ under $\sigma$.
If $\mathbf A = \neg \mathbf B$ with $\mathbf B$ a WFF:
$\mathop{ \operatorname{val}_{\mathcal A} \left({\neg \mathbf B}\right) } \left[{\sigma}\right] := f^\neg \left({ \mathop{ \operatorname{val}_{\mathcal A} \left({\mathbf B}\right) } \left[{\sigma}\right] }\right)$
where $f^\neg$ denotes the truth function of $\neg$.
If $\mathbf A = \left({\mathbf B \circ \mathbf B'}\right)$ with $\mathbf B, \mathbf B'$ WFFs and $\circ$ one of $\land, \lor, \implies, \iff$:
$\mathop{ \operatorname{val}_{\mathcal A} \left({\mathbf B \circ \mathbf B'}\right) } \left[{\sigma}\right] := f^\circ \left({ \mathop{ \operatorname{val}_{\mathcal A} \left({\mathbf B}\right) } \left[{\sigma}\right], \mathop{ \operatorname{val}_{\mathcal A} \left({\mathbf B'}\right) } \left[{\sigma}\right] }\right)$
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:
$\mathop{ \operatorname{val}_{\mathcal A} \left({\exists x: \mathbf B}\right) } \left[{\sigma}\right] := \begin{cases} T & \text{if for some $a \in A$, $\mathop{ \operatorname{val}_{\mathcal A} \left({\mathbf B}\right) } \left[{\sigma + (x / a)}\right] = T$} \\ F & \text{otherwise} \end{cases}$
where $\sigma + (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:
$\mathop{ \operatorname{val}_{\mathcal A} \left({\forall x: \mathbf B}\right) } \left[{\sigma}\right] := \begin{cases} T & \text{if for all $a \in A$, $\mathop{ \operatorname{val}_{\mathcal A} \left({\mathbf B}\right) } \left[{\sigma + (x / a)}\right] = T$} \\ F & \text{otherwise} \end{cases}$
where $\sigma + (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 $\mathcal A$, denoted $\operatorname{val}_{\mathcal A} \left({\mathbf A}\right)$, is defined as:

$\operatorname{val}_{\mathcal A} \left({\mathbf A}\right) := \mathop{ \operatorname{val}_{\mathcal A} \left({\mathbf A}\right) } \left[{\varnothing}\right]$

where $\varnothing$ is the empty mapping considered as an assignment for $\mathbf A$ and $\mathop{ \operatorname{val}_{\mathcal A} \left({\mathbf A}\right) } \left[{\varnothing}\right]$ is the value of $\mathbf A$ under $\varnothing$.


Also see


Sources