# 33.3 Key Pattern ~ExP(x)

You’ve already learned how to handle wide-scope quantifiers both in premises and conclusions.

You might have seen this coming next: now we have to learn about negation around a quantifier!

~ExP(x) and ~AxP(x) present special challenges of negation around a quantifier.

Just like the patterns ~(PvQ), ~(P&Q), and ~(P->Q), the patterns ~ExP(x) and ~AxP(x) present special challenges that we need to deal with.

Let’s see if you can see when a wide-scope negation is an issue.

To handle negation around another connective, you have to do a reductio build it from the inside.

In some ways, dealing with a negation around a quantifier, such as ~ExP(x), is similar to the patterns you already know, such as ~(PvQ).

Let’s review the 5-step plan, so you recall what we’re talking about.

When we use the five-step plan on ~(PvQ), we assume P in a subproof, and then we use vIntro to build PvQ.

“Building it from the inside”: building whatever is inside the scope of the negation. Such as building PvQ to contradict ~(PvQ), or building P->Q to contradict ~(P->Q), or building ExP(x) to contradict ~ExP(x).

That is what we mean by “building it from the inside”. We build up the part which is inside the scope of the negation, because that will contradict the original sentence, ~(PvQ), to finish the reductio.

Applying this idea to ~ExP(x), we should expect to need reductio at some point. And we also know that we will get the # symbol to finish the reductio by building ExP(x).

If you’d like to try it now, before we discuss it further, take out a piece of paper and try to complete this proof of the DeMorgan’s for Quantifiers:

1. ~ExP(x)
Thus,
2. Ax~P(x)

If you’d like to read more discussion first, just continue below.

Here is our next hint: don’t just start the reductio right away. If you do a reductio, then you will assume ~Ax~P(x), which gives us another negation around a quantifier pattern. Not exactly progress!

Whenever your conclusion is a wide scope Ax, always start a AIntro proof.

Instead, notice that our conclusion is a universal quantifier. So we should apply what you learned in section 33.1. Start a AIntro proof.

With that in mind, let’s see if you can complete the proof.

After we start the AIntro proof by assuming @n, notice how similar the next part is to the 5-step plan.

We have the premise ~ExP(x), and we assume P(n), similar to assuming one of the disjuncts. Then we build the existential, which allows us to introduce #. Finally we finish the reductio by proving ~P(n).

That allowed us to get the final conclusion by AIntro.