PlanetMath: satisfaction relation

Main Menu

sections Encyclopædia
Papers
Books
Expositions

meta Requests (200)
Orphanage
Unclass'd
Unproven (490)
Corrections (6)
Classification

talkback Polls
Forums
Feedback
Bug Reports

downloads Snapshots
PM Book

information News
Docs
Wiki
ChangeLog
TODO List
Legalese
About

Entry average rating: No information on entry rating

satisfaction relation

(Definition)

Alfred Tarski was the first mathematician to give a formal definition of what it means for a formula to be “true” in a structure. To do this, we need to provide a meaning to terms, and truth-values to the formulas. In doing this, free variables cause a problem : what value are they going to have ? One possible answer is to supply temporary values for the free variables, and define our notions in terms of these temporary values.

Let $\mathcal{A}$ be a structure with signature $\tau$ . Suppose $\mathcal{I}$ is an interpretation, and $\sigma$ is a function that assigns elements of 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\;\;$ a constant symbol
$\displaystyle \operatorname{Val}_{\mathcal{I},\sigma}(x)$	$\displaystyle =$	$\displaystyle \sigma(x)\qquad x\;\;$ 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$ an $\displaystyle \; n$ -ary function symbol

Now we are set to define satisfaction. Again we have to take care of free variables by assigning temporary values to them via a function $\sigma$ . We define the relation $\mathcal{A},\sigma\models\varphi$ by induction on the construction of formulas :

$\displaystyle \mathcal{A},\sigma$	$\displaystyle \models$	$\displaystyle t_1=t_2$ if and only if $\displaystyle \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)$ if and only if $\displaystyle (\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$ if and only if $\displaystyle \;\;\mathcal{A},\sigma\not\models\varphi$
$\displaystyle \mathcal{A},\sigma$	$\displaystyle \models$	$\displaystyle \varphi\vee \psi$ if and only if either $\displaystyle \mathcal{A},\sigma\models\psi$ or $\displaystyle \mathfrak{A},\sigma\models\psi$
$\displaystyle \mathcal{A},\sigma$	$\displaystyle \models$	$\displaystyle \exists x.\varphi(x)$ if and only if for some $\displaystyle \;\;a\in A,\; \mathcal{A},\sigma[x/a]\models \varphi$

Here

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

In case for some $\varphi$ of , 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 , 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$ .

"satisfaction relation" is owned by CWoo. [ full author list (3) | owner history (3) ]

(view preamble)