Section 3.2: Problem 4 Solution
Working problems is a crucial part of learning mathematics. No one can learn... merely by poring over the definitions, theorems, and examples that are worked out in the text. One must work part of it out for oneself. To provide that opportunity is the purpose of the exercises.
James R. Munkres
Show that the theory of the real numbers with its usual ordering, , admits elimination of quantifiers. (Assume that the language includes equality.)
Solution 1. (see page 159). Now, according to Exercise 7-A of Section 3.1, admits elimination of quantifiers, i.e. for every wff there is a quantifier-free wff such that , hence, .
Solution 2. We can actually repeat the solution of Exercise 7-A of Section 3.1 here. This emphasizes the point that the two structures are elementarily equivalent, i.e. everything we said is true in one structure is true in the other.
Solution 3. In this exercise we are explicitly given that the language has the equality symbol, so there is no reason to get rid of the equality symbols from the conjunction to show a more general case. Instead, it will turn out to be more convenient to transform the formula so that there are no negations of atomic formulas in it, but we will do the transformation later in one of the steps. Each atomic formula in the conjunction is of the form or .
- If there is an atomic formula that does not contain at all, then , where does not contain (and we continue with ). Indeed, is logically equivalent to , and we can use Example Q2a, page 121.
- If there is an atomic formula that contains on both sides, then , (and we stop here), and , (continue).
- Now, for any negation of an atomic formula we note that and . We can now regroup the atomic formulas and use the fact that iff . From now on, we have atomic formulas only in .
- If there is an atomic formula (or, equivalently, ), then (stop). Indeed, for every model of and , iff for some , and iff iff .
- If all the remaining atomic formulas contain on the same side, that is they are all of the form , or all of the form , then (stop), as is unbounded.
- Otherwise, we have , and (both are true in a model of with iff there is some such that for and for iff for and ).
Example (same as in the solution of Exercise 7-A of Section 3.1). (intended to say ) becomes becomes becomes .