satisfaction relation
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 π be a structure with signature Ο.
Suppose β is an interpretation
, 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)ββ | ||
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 :
Here
In case for some of , we have , we say that models, or is a model of, or satisfies . If has the free variables , and , we also write or instead of . In case is a sentence (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 |