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 quantifierfree
. 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 S1S4 (
).
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 quantifierfree 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.