Section Progress:

10.3 ~Elim

Now that you know a bit about how the formal proof system in BOOL works, let' see if you can figure out what we call this rule:

~Elim is how we use a sentence with a wide-scope negation. But here's the catch: it only applies if you have two negations stacked up on each other.

That's because you can't eliminate a single negation: inferring P from ~P is clearly not valid!

So if you don't have two negations together, you can't use ~Elim.

You can only apply Intro and Elim rules to the main connective.

Also remember this key fact that you learned before: you can only apply Intro and Elim rules to the main connective. That means you can't go straight from Q&~~R to Q&R with ~Elim. This is a valid inference, but you have to do more work to prove it.

Let's see if you can figure it out.

Now let's see if you can figure out how to prove Q from ~~(P&~~Q).

10.3 ~Elim