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)  ca constant symbol
Val,σ(x) = σ(x)  xa 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 aA,𝒜,σ[x/a]φ

Here

σ[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,,anA, 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