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 ) c β’ a constant symbol |
| Val β , Ο β‘ ( x ) | = | Ο β’ ( x ) x β’ a variable |
| Val β , Ο β‘ ( f β’ ( t 1 , β¦ , t n ) ) | = | β β’ ( f ) β’ ( Val β , Ο β‘ ( t 1 ) , β¦ , Val β , Ο β‘ ( t n ) ) 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 :
| π , Ο | β§ | t 1 = t 2 β’ if and only if β’ Val β , Ο β‘ ( t 1 ) = Val β , Ο β‘ ( t 2 ) |
| π , Ο | β§ | R β’ ( t 1 , β¦ , t n ) β’ if and only if β’ ( Val β , Ο β‘ ( t 1 ) , β¦ , Val β , Ο β‘ ( t 1 ) ) β β β’ ( R ) |
| π , Ο | β§ | Β¬ β’ Ο β’ if and only if β’ π , Ο β§ΜΈ Ο |
| π , Ο | β§ | Ο β¨ Ο β’ if and only if either β’ π , Ο β§ Ο β’ or β’ π , Ο β§ Ο |
| π , Ο | β§ | β x . Ο β’ ( x ) β’ if and only if for some β’ a β A , π , Ο β’ [ x / a ] β§ Ο |
| Ο β’ [ 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 x 1 , β¦ , x n , and a 1 , β¦ , a n β A , we also write π β§ Ο β’ ( a 1 , β¦ , a n ) or π β§ Ο β’ ( a 1 / x 1 , β¦ , a n / x n ) instead of π , Ο β’ [ x 1 / a 1 ] β’ β― β’ [ x n / a n ] β§ Ο . 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 |
Generated on Thu Feb 8 19:55:31 2018 by LaTeXML
