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 |