A WFF isn’t true or false until you specify a truth assignment for its variables. Similarly, a first order formula isn’t true or false on its own. Before we can get a truth value we have to give an interpretation.
An interpretation of a first order formula consists of a set , called the domain of the interpretation, and a relation on for each relation symbol in the formula.
In the interpreted formula, the variables can be elements of the domain of the interpretation. We write to mean “for every in ”, and to mean “there exists an element .”
Once we’ve given an interpretation, we can try to decide if the formula is true or false in that interpretation.
Here are some interpretations of the first order formula
The notation means the set of all natural numbers .
Domain , relation is . The interpreted formula is written
The interpreted formula is true. For every natural number there does exist a natural number with , e.g. could be the natural number .
Domain , relation is . The interpreted formula is written
The interpreted formula is false. It’s not true that for every natural number there exists a natural number such that . For example, could be 0 in which case no natural number satisfies .
This is a slight variation on the formula from the previous example.
Again, to give an interpretation we have to give a domain — a set for the elements represented by and to belong to — and a relation on . The interpreted statement will be true if and only if there is an element such that every is related to by the interpretation of the relation .
Is this formula true in the following interpretations?
Domain , relation is .
Domain , relation is .
(The answer is no for the first one and yes for the second.)
We already know how to determine the truth value in a particular interpretation of a formula just involving the logical connectives.
The rules for deciding whether a formula containing a quantifier is true in an interpretation with domain are:
An interpreted formula is true if for every element of , substituting into in place of gives a true statement.
An interpreted formula is true in an interpretation if there is an element of such that substituting into in place of gives a true statement.
(There are some subtleties in doing substitution into logical formulas caused by the concepts of free and bound variables, but they are beyond the scope of MATH0005. If you want to learn more, take MATH0037 Logic in your third year or read the book by Goldrei in the further reading for this chapter.)
Here are two first order formulas:
Let’s try and determine whether and are true in some interpretations.
Consider the interpretation with domain and where the relation is interpreted as .
is interpreted as saying there is an such that it is not the case that there is a in such that . That’s true: if then it is not the case that there is a in with .
is interpreted as saying for every it is not the case that for all we have . We could find if this is true by checking each in turn. But it’s simpler to just notice that whatever is, could take the same value, and then will be false. So is also true.
Next, consider the interpretation with domain and where the relation is interpreted as .
is interpreted as saying there is an such that it is not the case that there is a in such that . That’s false: can always take the same value as , and then .
is interpreted as saying for every it is not the case that for all we have . But when , it is the case that for all we have . So is false in this interpretation.
Finally, consider the interpretation with domain and where the relation is interpreted as .
is interpreted as saying there is an such that it is not the case that there is a in such that . That’s false: for every the number is in too, and .
is interpreted as saying for every it is not the case that for all we have . This is true: whatever is, we can take and then it is not the case that .
It was awkward to determine the truth or falsity of these formulas in the given interpretations. One thing that would be helpful would be to transform them into equivalent, simpler formulas. We know about logically equivalent WFFs for propositional calculus, but right now we don’t know how to define logical equivalence in first order logic.