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 to variables, we define the function
inductively on the construction of terms :
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 |