1.2.3 The Satisfaction Definition

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 to variables in . 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.


Aljoscha Burchardt, Stephan Walter, Alexander Koller, Michael Kohlhase, Patrick Blackburn and Johan Bos
Version 1.2.5 (20030212)