Processing math: 17%

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)  
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]βŠ§Ο†

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,…,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