# 13.4 ~Intro

It’s time to finally learn ~Intro. Intro rules are for creating a new instance of a connective. ~Intro allows us make a wide-scope negation, like ~P.

~Intro = Reductio. To prove ~P, we temporarily assume P and prove #.

It works just like reductio: to prove ~P, we temporarily assume P and prove #.

When we learned proof by cases, we used subproofs for temporary assumptions. We’ll do the same thing here: in order to temporarily assume P, just put P in a subproof, and end the subproof with #. That allows you to move out of the subproof and write ~P.

For example, consider this proof.

This rule is unique because you just cite the subproof where you assume the opposite of your conclusion. There is not also a specific line to cite. That’s why the answer is ~Intro;2-4.

By contrast, when we do subproofs with vElim, we have to cite not just the subproofs but also the line number with the disjunction. That’s because when you do vElim, you need a disjunction you are eliminating.

Now let’s try a harder example. Here’s an argument:

1. ~(P&Q)
2. P
Thus,
3. ~Q

Since the conclusion is a wide-scope negation, it’s a great plan to use reductio. If you can assume the opposite and prove a contradiction, then you’ll get the conclusion by ~Intro.

Let’s take it one step at a time.

Once you start a reductio, you don’t need to think about how to prove your final conclusion. Your new goal is to end the subproof with #.

Once you start that subproof, you should already have a new plan in mind.

You don’t need to think about how to get to ~Q now. You know how you’ll prove ~Q: with ~Intro, citing the subproof you just created.

The only thing to think about now is how do you finish that ~Intro proof. That requires your subproof end with #.

So now you have a new goal: figure out how to prove # inside the subproof. Then you can just end the subproof and justify the conclusion.

Whenever you have a wide-scope negation conclusion, working backwards by setting up a ~Intro is almost always the best way to go.

The plan we used in this proof generalizes: anytime you have a conclusion with a wide-scope negation, you can start by assuming the opposite and proving a contradiction.

But it’s important to know that you will often use ~Intro in other scenarios too. Just like the informal method of reductio, ~Intro is a general proof method that can prove negative and positive conclusions.

~Intro is a general proof method that can prove negative and positive conclusions.

How can that be?

Since ~Intro requires introducing a negation symbol, you might think that it cannot prove something other than a negation.

Solution: you just use ~Elim to get rid of two negations.

For example, let’s try this proof now:

1. ~(P&~Q)
2. P
Thus,
3. Q

Notice that premise 1 is slightly different than before!

Shortcut: drop the step with ~~, and cite the final conclusion as ~Intro. (There’s no ~Elim citation with the shortcut.)

In fact, it is so common to use ~Intro/reductio even when the conclusion isn’t a negation, we follow common practice of allowing a shortcut.

You can cut out the penultimate step that has ~~Q, and just cite the final line Q with ~Intro;3-5.

Here’s how it looks:

1. ~(P&~Q)
2. P
3. | ~Q
4. | P&~Q
5. | #
6. Q

Premise
Premise
Assume
&Intro;2,3
#Intro;1,4
~Intro;3-5

When you take the shortcut, remember to drop the sentence with ~~ and the use of ~Elim. It might seem odd to cite ~Intro for Q since there is no negation. But once you practice it, it will become completely natural.