# 13.3 #Intro and #Elim

Since we’ve added # to BOOL, it will be helpful to have formal proof rules for it. These rules will then help us create the ~Intro rule.

Here’s what we know:

1. Only a contradiction can entail #.
2. Any contradiction can entail #.

Those facts allow us to figure out the #Intro rule. Any time we have some sentence, like P, and the negation of that sentence, like ~P, we can write #.

#Intro always requires citing two things: a sentence, such as P, and its negation, ~P.

For #Intro, you just need some sentence and its negation.

The sentence in the role of P does not have to be atomic. PvQ and ~(PvQ) would also justify # via #Intro. You just need some sentence, and that exact sentence with a negation in front.

#Intro requires citing two different lines, such as #Intro;1,2

Since we require you to cite two separate sentences for #Intro, if you already have a contradictory sentence like P&~P, you just have to bring down each conjunct and cite them to justify #.

For example, say you have to prove # follows from (P&~P)v(Q&~Q).

Next we need to learn #Elim. Welcome to the easiest rule in BOOL!

“Elimination” is how you use a symbol that you already have. You know that a contradiction entails anything, so if you already have a #, you get to write anything you want, and cite #Elim and the line with the #.

Let’s put the rules together and do a proof that uses #Intro and #Elim.

The premise is (P&~~Q)&~Q and the conclusion is R.

There is always more than one way to do a proof. For example, from a logical point of view, it doesn’t matter whether you first bring down P&~~Q or ~Q from the premise.

Our guidelines ask you to go from left to right for simplicity.

But when you do repeated operations like bringing down both conjuncts, our guidelines ask you to go from left to right for simplicity.

It is also important that you bring down P&~~Q before you can bring down ~~Q. You always have to pay attention to what the main connective is.

When you are solving proofs on your own with pen and paper, it does not matter whether you solve the proof in the fewest possible lines, like we did here.

For example, if you were doing this proof, it is very natural, when you get ~~Q, to infer Q with ~Elim. That is a great impulse! You can then use Q and ~Q for #Intro.

The most important thing is that the proof is correct, not that you solve it in the fewest possible lines. Every line needs to be properly cited, with the conclusion on the final line.

The most important thing is that the proof is correct: all the lines need to be properly cited, with the conclusion on the final line.

It can be very helpful, though, to try to solve proofs in as few lines as possible, because it gives you a more complete understanding of how the rules work.

You understand #Intro better, for example, if you realize that ~~Q and ~Q make a contradiction just as much as Q and ~Q.

You understand #Intro better if you realize that ~~Q and ~Q make a contradiction just as much as Q and ~Q.

Let’s practice one more example. Here’s the argument:

1. (P&~P)v~~R
Thus,
2. R

First, construct the proof yourself with pen and paper.

Working out proofs on your own, rather than just completing our skeleton proofs, is essential! Remember the importance of active learning: if you challenge yourself more now, the rest of the course will seem easier and you will have better long-term retention.

After you’ve worked it out, answer the question below.

Don’t look below until you’ve worked on the proof yourself!

Don’t look below until you’ve worked on the proof yourself! If you aren’t going to put in the effort to work out the proof yourself, you might as well be watching Netflix instead of reading this textbook.

This proof is an important example because there are several equally good ways of solving it.

There are several good ways to do this proof.

Hopefully you saw the disjunction premise and thought to do proof by cases.

But you could have exported the final conclusion out of each case, or you could have exported ~~R out of each case, and then done ~Elim last.

What matters is that the proof checks out correctly, not that you solve it exactly like we do.

If you’d like to see what both versions look like, here they are.