satisfaction relation

Alfred Tarski was the first mathematician to give a formal definition of what it means for a formulaMathworldPlanetmathPlanetmath to be “true” in a structureMathworldPlanetmath. To do this, we need to provide a meaning to terms, and truth-values to the formulas. In doing this, free variablesMathworldPlanetmathPlanetmath 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 𝒜 be a structure with signaturePlanetmathPlanetmathPlanetmath τ. Suppose ℐ is an interpretationMathworldPlanetmath, and σ is a function that assigns elements of A to variables, we define the function Valℐ,σ inductively on the construction of terms :

Valℐ,σ⁡(c) = ℐ⁢(c)  c⁢a constant symbol
Valℐ,σ⁡(x) = σ⁢(x)  x⁢a variable
Valℐ,σ⁡(f⁢(t1,…,tn)) = ℐ⁢(f)⁢(Valℐ,σ⁡(t1),…,Valℐ,σ⁡(tn))  f⁢ an ⁢n⁢-ary function symbol

Now we are set to define satisfactionMathworldPlanetmath. Again we have to take care of free variables by assigning temporary values to them via a function σ. We define the relationMathworldPlanetmath 𝒜,σ⊧φ by inductionMathworldPlanetmath on the construction of formulas :

𝒜,σ ⊧ t1=t2⁢ if and only if ⁢Valℐ,σ⁡(t1)=Valℐ,σ⁡(t2)
𝒜,σ ⊧ R⁢(t1,…,tn)⁢ if and only if ⁢(Valℐ,σ⁡(t1),…,Valℐ,σ⁡(t1))∈ℐ⁢(R)
𝒜,σ ⊧ ¬⁢φ⁢ if and only if ⁢𝒜,σ⊧̸φ
𝒜,σ ⊧ φ∨ψ⁢ if and only if either ⁢𝒜,σ⊧ψ⁢ or ⁢𝔄,σ⊧ψ
𝒜,σ ⊧ ∃x.φ⁢(x)⁢ if and only if for some ⁢a∈A,𝒜,σ⁢[x/a]⊧φ


σ⁢[x/a]⁢(y)⁢{a if ⁢x=yσ⁢(y) else.

In case for some φ of L, we have 𝒜,σ⊧φ, we say that 𝒜 models, or is a model of, or satisfies φ. If φ has the free variables x1,…,xn, and a1,…,an∈A, we also write 𝒜⊧φ⁢(a1,…,an) or 𝒜⊧φ⁢(a1/x1,…,an/xn) instead of 𝒜,σ⁢[x1/a1]⁢⋯⁢[xn/an]⊧φ. In case φ is a sentenceMathworldPlanetmath (formula with no free variables), we write 𝒜⊧φ.

Title satisfaction relation
Canonical name SatisfactionRelation
Date of creation 2013-03-22 12:43:56
Last modified on 2013-03-22 12:43:56
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 14
Author CWoo (3771)
Entry type Definition
Classification msc 03C07
Related topic Model
Defines satisfaction
Defines satisfy