satisfaction relation (original) (raw)
Let 𝒜 be a structure with signature τ. Suppose ℐ is an interpretation
, and σ is a function that assigns elements of A to variables, we define the functionValℐ,σ 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 satisfaction. Again we have to take care of free variables by assigning temporary values to them via a function σ. We define the relation
𝒜,σ⊧φ by induction
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 sentence (formula with no free variables), we write 𝒜⊧φ.