# satisfaction relation

Let $\mathcal{A}$ be a structure with signature   $\tau$. Suppose $\mathcal{I}$ is an interpretation  , and $\sigma$ is a function that assigns elements of $A$ to variables, we define the function $\operatorname{Val}_{\mathcal{I},\sigma}$ inductively on the construction of terms :

 $\displaystyle\operatorname{Val}_{\mathcal{I},\sigma}(c)$ $\displaystyle=$ $\displaystyle\mathcal{I}(c)\qquad c\;\;\text{a constant symbol}$ $\displaystyle\operatorname{Val}_{\mathcal{I},\sigma}(x)$ $\displaystyle=$ $\displaystyle\sigma(x)\qquad x\;\;\text{a variable}$ $\displaystyle\operatorname{Val}_{\mathcal{I},\sigma}(f(t_{1},...,t_{n}))$ $\displaystyle=$ $\displaystyle\mathcal{I}(f)(\operatorname{Val}_{\mathcal{I},\sigma}(t_{1}),...% ,\operatorname{Val}_{\mathcal{I},\sigma}(t_{n}))\qquad f\text{ an }\;n\text{-% ary function symbol}$
 $\displaystyle\mathcal{A},\sigma$ $\displaystyle\models$ $\displaystyle t_{1}=t_{2}\text{ if and only if }\operatorname{Val}_{\mathcal{I},\sigma}(t_{1})=\operatorname{Val}_{\mathcal{I% },\sigma}(t_{2})$ $\displaystyle\mathcal{A},\sigma$ $\displaystyle\models$ $\displaystyle R(t_{1},...,t_{n})\text{ if and only if }(\operatorname{Val}_{% \mathcal{I},\sigma}(t_{1}),...,\operatorname{Val}_{\mathcal{I},\sigma}(t_{1}))% \in\mathcal{I}(R)$ $\displaystyle\mathcal{A},\sigma$ $\displaystyle\models$ $\displaystyle\neg\varphi\text{ if and only if }\;\;\mathcal{A},\sigma\not\models\varphi$ $\displaystyle\mathcal{A},\sigma$ $\displaystyle\models$ $\displaystyle\varphi\vee\psi\text{ if and only if either }\mathcal{A},\sigma% \models\psi\text{ or }\mathfrak{A},\sigma\models\psi$ $\displaystyle\mathcal{A},\sigma$ $\displaystyle\models$ $\displaystyle\exists x.\varphi(x)\text{ if and only if for some }\;\;a\in A,\;% \mathcal{A},\sigma[x/a]\models\varphi$

Here

 $\sigma[x/a](y)\begin{cases}a&\text{ if }\;\;x=y\\ \sigma(y)&\text{ else.}\end{cases}$

In case for some $\varphi$ of $L$, we have $\mathcal{A},\sigma\models\varphi$, we say that $\mathcal{A}$ models, or is a model of, or satisfies $\varphi$. If $\varphi$ has the free variables $x_{1},...,x_{n}$, and $a_{1},...,a_{n}\in A$, we also write $\mathcal{A}\models\varphi(a_{1},...,a_{n})$ or $\mathcal{A}\models\varphi(a_{1}/x_{1},...,a_{n}/x_{n})$ instead of $\mathcal{A},\sigma[x_{1}/a_{1}]\cdots[x_{n}/a_{n}]\models\varphi$. In case $\varphi$ is a sentence  (formula with no free variables), we write $\mathcal{A}\models\varphi$.

Title satisfaction relation SatisfactionRelation 2013-03-22 12:43:56 2013-03-22 12:43:56 CWoo (3771) CWoo (3771) 14 CWoo (3771) Definition msc 03C07 Model satisfaction satisfy