Section Progress:

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.

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.

Imagine, for example, that we assume P on line 5 and prove ⊥ on line 8, so it looks like this:

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;5-8.

By contrast, when we did 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 real example. Here's an argument:

1. ~(P&Q)
2. P
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.


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.

Here's a sketch of what your proof should look like:

See if you can fill in the blanks below (don't use the hint unless you need it!).

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?, you might be wondering, since ~Intro requires introducing a negation symbol. Answer: because you'll then just use ~Elim to get rid of two negations.

For example, you should be able to do this proof now:

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

Work it out on paper before proceeding.




Below we show you the finished proof, so don't scroll down until you're ready.

Shortcut: drop the step with ~~, and cite the final conclusion as ~Intro.

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:

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, so if you find the shortcut confusing, you can just do it the long way!

13.4 ~Intro