Lesson 10

For certain expressions we have to struggle to find a model that satisfies them. If such a model exists, we say the expression is satisfiable. Some other expressions, however, are satisfied by any model (as long as it is appropriate to their vocabulary). Those expressions are called valid. If \(\phi\) is valid, we write \(\models \phi\), with no reference to models.

Intuitively, a valid expression is a statement that is true for very basic reasons, having to do with general properties of functions, quantifiers, equality, etc., and not with the particular mathematical domain (for example \((\exists y \forall x (x = y + 1)) \Rightarrow (\forall w \forall z (w = z))\)). Then, an expression is unsatisfiable if and only if its negation is valid.

We have equipped our system for expressing mathematical reasoning with syntax and semantics. Surely there is something missing: A systematic method for revealing truth. But first, what is truth? One possible answer is that truth in first-order logic coincides with the concept of validity. Let us therefore introduce a systematic way for revealing the validity of expressions. Our system is based on the three basic kinds of validity that we know: Boolean validity, the properties of equality, and the properties of quantifiers.