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:
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!).
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.
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:
Work it out on paper before proceeding.
Below we show you the finished proof, so don't scroll down until you're ready.
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!