5.1.5 The Satisfaction Definition

Having established this, we now are ready to define satisfaction. Let be a formula, let be a model, and let be an assignment of values in to variables. Then the relation ( is satisfied in with respect to the assignment of values to variables ) is defined inductively as follows:

(Here `iff' is shorthand for `if and only if'.) Note the crucial - and indeed, intuitive - role played by the x-variants in the clauses for the quantifiers. For example, what the clause for the existential quantifier boils down to is this: is satisfied in a given model, with respect to an assignment , if and only if there is some x-variant of that satisfies in the model. That is, we have to try to find some value for x that satisfies in the model, while keeping the assignments to all other variables the same.