# 33.5 Regular Routine for Quantifiers

At this point you’ve learned how to deal with wide-scope universals (section 33.1), wide-scope existentials (section 33.2), negation around existentials (33.3), and negation around universals (33.4).

Putting all the pieces together in complex proofs can still be challenging!

Those are all the basic patterns you can encounter, so now you’re ready for anything!

But sometimes putting all the pieces together in complex proofs is challenging. So in this section we’ll present a strategy for just that, synthesizing the knowledge of all the details that you’ve been learning.

Up to this point with formal proofs with quantifiers, we’ve been focusing on the trees. Now we’ll look at the forest.

For example, you know how to use wide-scope universals and existentials, but what if you have both in a proof? Which do you do first?

The routine tells you how to prioritize information, and what to do first.

What we will teach you is a regular routine that you can apply to any situation where you have many things happening at once. The routine tells you how to prioritize information, and what to do first.

We’ll first tell you the routine, and then we’ll elaborate with an example.

### The Regular Routine

1. Look at the conclusion for a wide-scope universal or negation. If you find one, start a AIntro or ~Intro proof.
2. Next, look to your premises for an existential. If you find one, start a EElim proof. (Use existentials before universals.)
3. Next, instantiate any universals.
4. Next, solve any proof sets that you can. Look for tactics like the 5-step plan or proving contradictions to finish reductios.
5. Repeat if necessary.

Here’s an example. Say we want to prove this:

1. Ax(P(x)->Q(x))
Thus,
2. ~Ex(P(x)&~Q(x))

Try it  now if you’d like, before reading below.

***Continuing***

The first thing we do is look at the conclusion. Since it is a wide-scope negation, we know to start with reductio.

That means that on line 2 we have Ex(P(x)&~Q(x)). So now we have two quantified sentences to work with, a universal and an existential.

Step two of the routine says to use the existential first.

Step two of the routine says to use the existential first, so we start an EElim proof by assuming @n P(n)&~Q(n).

You might want to bring down those conjuncts right away, since you know what to do with a wide-scope conjunction. The order is less important at this point.

But step three of the routine says to instantiate the universal, so we get P(n)->Q(n) by AElim;1.

Now there are no more quantifiers. We are just at a point where we have to use propositional logic to prove a contradiction and finish the reductio.

That’s what step four of the routine says. So in this case there is no need to repeat the process.

Let’s see if you can figure it all out.

If you understood that proof, then next you should do this one, to see how similar it is:

1. Ex(P(x)&~Q(x))
Thus,
2. ~Ax(P(x)->Q(x))

We left the negation in the conclusion, but otherwise we swapped the two quantified formulas.