Section 3.1: Problem 3 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
The proof of quantifier elimination for showed how, given a formula , to find a quantifier-free . Show that without using the completeness of . (This yields an alternative proof of the completeness of , not involving -chains or the Łoś–Vaught test.)
Recall, that the proof of Theorem 31G considers a formula where each is atomic or the negation of an atomic formula, and provides a procedure to eliminate all quantifiers from it. We formalize this procedure (with a few more cases that we consider) and show the equivalence of the initial and resulting formulas under Axioms S1-S4 ( ).
First, we argue that if for wffs and there are wffs and such that does not contain and , then . Indeed, for every structure and such that , iff . Now, iff for some , iff for some , iff for some , and iff for some , and iff and iff .
(*) In particular, if , then , if , then , and if , then .
Let us call just , for simplicity, and let . is either or where , , and and can be a variable or a constant. We need to consider all possible cases for . To simplify things, suppose ’s are sorted in the following order: , ; ; , , ; , , ; (symmetrical cases such as , , are equivalent to corresponding cases we consider).
- where , . Then, does not contain , and we can simply take to obtain . We can now proceed with being the first formula in .
- If , then, obviously, is true in any structure with any assignment of , so that, according to (*), (and we can proceed with being the first formula in ), and (and we stop here).
- If , without loss of generality, suppose . Using deduction axiom group 2 (A2) for S4, . Using A2 and contraposition for S2, we further obtain . From here, using all the standard techniques for substitution, we obtain , and further . Overall, we see that , i.e. . Similarly, according to (*), (and we stop here), and (and we proceed with the new ).
- If , by using A2 for S1 and S2 and contraposition for S2, , and by using generalization and A2 and then times (as well as other substitution techniques), we obtain , i.e. , and, as before, according to (*), (stop).
- If , by S2 and A2, , and by applying this rule times, . Moreover, (see Example Eq5, page 122, for the idea of the proof). Hence, . Then, , and (stop). Indeed, for every structure and such that , iff for some , and iff iff (we used S2 at some point).
- If , then, similar to 3(b), we, first, conclude that . Then, for every structure and assignment such that , iff for some , and . Similar to 3(b), we argue that for any term in , and . So, let be in which we apply to each side of the equality of each term of . Then, in , all occurrences of can be represented as . Now we can proceed, iff for some , and iff for some , and (we used S1 and S3). Therefore, (stop).
- If , then, similar to 3(b), we, first, conclude that , and, then (stop). Indeed, for every structure and assignment such that , iff for some , and iff iff (we used S2 at some point).
- . All that we have left now, is terms that are negations of atomic formulas , . Consider any structure and such that . For every term , using S3, we can find such that , then let be greater than any for any such term, and let . Then, if we let , then, using S4, , i.e. . Since does not depend on the term, we conclude that the rest of the formula is satisfied in any structure that satisfies with any , and .
To conclude, we note that in our procedure, we did a few more steps compared to the proof in the text, and modified the formula in a slightly way in some common steps. Same as in the proof, we first move all formulas not containing out from the quantified expression (step 1). Then, similar to the text, we consider the case when a term contains on both sides (step 2). If , then, unlike the proof, we do not replace the term with or , but, equivalently, either remove it at all (instead of replacing with ) or conclude that the whole expression is equivalent to (instead of replacing just one term by ). If , then, similarly, we either conclude that the whole expression is equivalent to (instead of replacing a term by ) or remove the term (instead of replacing it by ). In steps 3 and 4, we, as in the proof, consider terms which are atomic formulas (not negations). Similar to the text, if there is at least one such term left, then we are going to obtain a quantifier-free formula right after this step. However, we consider four separate subcases here, which, of course, can be put together to form the one step in the proof. However, by doing this, we avoid unnecessary substitutions and new terms that are either always false or always true. For example, in step 3(a) we conclude that the whole formula is equivalent to instead of substituting it with a series of terms one of which would be . Similarly, in 3(b) we avoid unnecessary terms of the form for , as well as transformations of the remaining terms. In 4, we also consider two subcases, in one of which there is no need to check against for or transform the remaining terms. Finally, same as in the proof, we get to step 5 only if there were no terms in steps 3 or 4, i.e. if after steps 1 and 2 all remaining terms are negations.