# 13.3 #Intro and #Elim

Since we've added ⊥ (or #) 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:

- Only a contradiction can entail ⊥.
- 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 it's negation, ~P.

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.

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). A sketch of the proof looks like this:

See if you can complete the proof.

Be careful not to read below until you've finished the problem. As you know about active learning, if you don't work through the textbook problems you won't learn the material.

The complete proof looks like this:

Now 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 ⊥.

Now let's see a full proof that uses ⊥Intro and ⊥Elim. The premise is (P&~~Q)&~Q and the conclusion is R. You have to match the rules with each step.

There is always more than one way to do a proof. For example, it doesn't matter whether you bring down P&~~Q or ~Q first from the premise. But it * does* matter that you bring down P&~~Q before you can bring down ~~Q: you always have to pay attention to what the main connective is.

It also does not matter whether you solve the proof in the fewest possible lines, like we did here. 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: 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'll understand ⊥Intro better, for example, once you realize that ~~Q and ~Q make for a contradiction just as much as Q and ~Q.

Here's what the completed proof looks like:

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

1. (P&~P)v~~R

Thus,

2. R

First, construct the proof yourself on a piece of paper. Then answer the question below.

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.

Here's what our proof looks like:

Your proof might look slightly different from ours: lines 3 and 4 could be reversed, for example. But you would still get the same citation for the final line.

You might get a different answer, though, if you took a different approach. For example, on line 6, you could have written ~~R from the ⊥Elim. And then you could export ~~R from the subproofs with vElim. Then you would get to the conclusion with ~Elim. That's great too: what matters is that the proof checks out correctly, not that you solve it exactly like our example.