In this video we're going to learn some more rules for ...
proof: wedge-in,
double negation, and the rules for the double arrow.
Let's start with wedge in.
Here's the formula for it: if you have A,
you can add B to it on either side, with a wedge.
So you can add anything whatsoever to either side of ...
anything you already have as long as you join it on with a wedge.
If you have P
You can get P v Q by vI
or you could add the Q on the other side and get Q v P
or you could add something totally arbitrary like this.
The idea is that, if we know it's hot,
we know it's hot or raining. Since we know it's hot.
It doesn't matter what else you put on--if you already ...
know it's hot, you know it's hot OR whatever.
The main use for vI is when you have a wedge before an arrow.
Let's say we have (P v Q) -> R
and we've also been able to get Q.
Then we can use vI on Q to make it P v Q.
We added the P on the left side with a wedge.
Now we've exactly matched what's before the arrow in line ...
1, so we can use modus ponens and get R.
So we want to use vI to build the thing that's before the ...
arrow, to set us up for the modus ponens.
We only need one side of the wedge to do it.
Our next rule is double negation.
Here's the formula for the rule.
We can add two negations to anything we have,
or if we have something that already has two negations,
we can take them away.
One thing to note here, if you have ~P and you want ...
to apply the DN rule to it
you get three negations in front of P.
There was one there, and you added two more.
A main use for double negation
is to get the right input for rules whose inputs require ...
negations, like vO and MT.
So if we have P->~Q and Q, we can't do MT right away ...
because the other input for MT is supposed to be an ...
extra negation of what's after the arrow.
Q is one negation short of what's after the arrow.
But we can use double negation to add two negations ...
to Q, so we have an extra negation ...
of what's after the arrow.
Then we can do MT, which gives us the negation of ...
what's before the arrow: ~P.
Similarly, if we have P v ~Q and Q,
we need the negation of one side of the wedge to do vO.
Q isn't quite there yet.
But we can double negate Q, which gives us an extra ...
negation of one side of the wedge
so we can do vO and get the other side as is: P.
Now let's learn the rules for the double arrow.
The main one we'll use is <->O [double arrow out].
Here's the formula.
When you have a double arrow,
you can turn it into an arrow going either way,
forwards or backwards.
We don't need any other input;
we can do that from the double arrow alone.
But the challenging thing is to choose an arrow going in the ...
right direction.
Here's how we can use the double arrow.
Let's say we have P <->Q [double arrow]
and we have P.
Then we can use double arrow out to get P->Q.
Now we've matched what's before the arrow
and we can do MP to get Q.
If we had P <->Q [double arrow]
and Q
we'd want to turn the double arrow into Q -> P,
so we'd have matched what's before the arrow
and we could do MP to get P.
For some more cases
let's assume we have P <-> Q [double arrow]
and ~Q.
Now we want to get P->Q, so we'll have the negation of ...
what's after the arrow.
Then we can do MT and get the negation of what's before ...
the arrow, ~P.
But if we have P <-> Q [double arrow]
and ~P
we'll want to get Q -> P, again so we have the ...
negation of what's after the arrow
and we can do MT to get the negation of what's before the ...
arrow, ~Q.
To sum up how to deal with double arrows
if you've been able to get an exact match for what's on one ...
side of the <-> [double arrow]
then you want to put that side first when you get a single ...
arrow from it, so you can do MP.
If you can get the negation of one side of the <-> [double arrow]
you want to put that side second when you get a single ...
arrow from it, so you can do MT.
The other rule for double arrows is <->I [double arrow in].
Here's the formula; if you have an arrow from A to ...
B, and vice versa an arrow from ...
B to A, you can make a double arrow.
But this rule won't be much use until we can actually get ...
arrow statements like that! And we don't have an ->I rule,
so we aren't going to be able to do that yet.
In fact, to make arrow statements,
we're going to have to learn a whole different kind of rule.
That's what we'll be discussing in future videos!