1 0:00:00,000 --> 0:00:04,203 In this video we're going to learn some more rules for ... 2 0:00:04,203 --> 0:00:05,636 proof: wedge-in, 3 0:00:05,636 --> 0:00:09,839 double negation, and the rules for the double arrow. 4 0:00:09,840 --> 0:00:13,960 Let's start with wedge in. 5 0:00:13,960 --> 0:00:17,901 Here's the formula for it: if you have A, 6 0:00:17,901 --> 0:00:22,439 you can add B to it on either side, with a wedge. 7 0:00:22,440 --> 0:00:26,549 So you can add anything whatsoever to either side of ... 8 0:00:26,549 --> 0:00:31,519 anything you already have as long as you join it on with a wedge. 9 0:00:31,520 --> 0:00:35,840 If you have P 10 0:00:35,840 --> 0:00:40,800 You can get P v Q by vI 11 0:00:40,800 --> 0:00:46,000 or you could add the Q on the other side and get Q v P 12 0:00:46,000 --> 0:00:50,520 or you could add something totally arbitrary like this. 13 0:00:50,520 --> 0:00:53,387 The idea is that, if we know it's hot, 14 0:00:53,387 --> 0:00:57,401 we know it's hot or raining. Since we know it's hot. 15 0:00:57,401 --> 0:01:01,702 It doesn't matter what else you put on--if you already ... 16 0:01:01,702 --> 0:01:05,238 know it's hot, you know it's hot OR whatever. 17 0:01:05,240 --> 0:01:10,840 The main use for vI is when you have a wedge before an arrow. 18 0:01:10,840 --> 0:01:15,480 Let's say we have (P v Q) -> R 19 0:01:15,480 --> 0:01:19,000 and we've also been able to get Q. 20 0:01:19,000 --> 0:01:22,552 Then we can use vI on Q to make it P v Q. 21 0:01:22,552 --> 0:01:26,839 We added the P on the left side with a wedge. 22 0:01:26,840 --> 0:01:31,384 Now we've exactly matched what's before the arrow in line ... 23 0:01:31,384 --> 0:01:34,319 1, so we can use modus ponens and get R. 24 0:01:34,320 --> 0:01:38,335 So we want to use vI to build the thing that's before the ... 25 0:01:38,335 --> 0:01:41,279 arrow, to set us up for the modus ponens. 26 0:01:41,280 --> 0:01:45,760 We only need one side of the wedge to do it. 27 0:01:45,760 --> 0:01:49,360 Our next rule is double negation. 28 0:01:49,360 --> 0:01:52,960 Here's the formula for the rule. 29 0:01:52,960 --> 0:01:56,125 We can add two negations to anything we have, 30 0:01:56,125 --> 0:02:00,060 or if we have something that already has two negations, 31 0:02:00,060 --> 0:02:01,599 we can take them away. 32 0:02:01,600 --> 0:02:06,240 One thing to note here, if you have ~P and you want ... 33 0:02:06,240 --> 0:02:08,560 to apply the DN rule to it 34 0:02:08,560 --> 0:02:11,613 you get three negations in front of P. 35 0:02:11,613 --> 0:02:15,159 There was one there, and you added two more. 36 0:02:15,160 --> 0:02:19,120 A main use for double negation 37 0:02:19,120 --> 0:02:23,720 is to get the right input for rules whose inputs require ... 38 0:02:23,720 --> 0:02:25,920 negations, like vO and MT. 39 0:02:25,920 --> 0:02:30,230 So if we have P->~Q and Q, we can't do MT right away ... 40 0:02:30,230 --> 0:02:34,648 because the other input for MT is supposed to be an ... 41 0:02:34,648 --> 0:02:38,419 extra negation of what's after the arrow. 42 0:02:38,419 --> 0:02:42,837 Q is one negation short of what's after the arrow. 43 0:02:42,840 --> 0:02:46,772 But we can use double negation to add two negations ... 44 0:02:46,772 --> 0:02:49,299 to Q, so we have an extra negation ... 45 0:02:49,299 --> 0:02:51,358 of what's after the arrow. 46 0:02:51,360 --> 0:02:55,767 Then we can do MT, which gives us the negation of ... 47 0:02:55,767 --> 0:02:58,479 what's before the arrow: ~P. 48 0:02:58,480 --> 0:03:01,876 Similarly, if we have P v ~Q and Q, 49 0:03:01,876 --> 0:03:07,284 we need the negation of one side of the wedge to do vO. 50 0:03:07,284 --> 0:03:09,799 Q isn't quite there yet. 51 0:03:09,800 --> 0:03:13,490 But we can double negate Q, which gives us an extra ... 52 0:03:13,490 --> 0:03:15,920 negation of one side of the wedge 53 0:03:15,920 --> 0:03:21,760 so we can do vO and get the other side as is: P. 54 0:03:21,760 --> 0:03:24,977 Now let's learn the rules for the double arrow. 55 0:03:24,977 --> 0:03:28,359 The main one we'll use is <->O [double arrow out]. 56 0:03:28,360 --> 0:03:31,960 Here's the formula. 57 0:03:31,960 --> 0:03:33,961 When you have a double arrow, 58 0:03:33,961 --> 0:03:37,130 you can turn it into an arrow going either way, 59 0:03:37,130 --> 0:03:38,798 forwards or backwards. 60 0:03:38,800 --> 0:03:41,416 We don't need any other input; 61 0:03:41,416 --> 0:03:45,079 we can do that from the double arrow alone. 62 0:03:45,080 --> 0:03:49,520 But the challenging thing is to choose an arrow going in the ... 63 0:03:49,520 --> 0:03:50,879 right direction. 64 0:03:50,880 --> 0:03:54,600 Here's how we can use the double arrow. 65 0:03:54,600 --> 0:03:58,560 Let's say we have P <->Q [double arrow] 66 0:03:58,560 --> 0:04:01,240 and we have P. 67 0:04:01,240 --> 0:04:04,971 Then we can use double arrow out to get P->Q. 68 0:04:04,971 --> 0:04:08,599 Now we've matched what's before the arrow 69 0:04:08,600 --> 0:04:12,440 and we can do MP to get Q. 70 0:04:12,440 --> 0:04:16,080 If we had P <->Q [double arrow] 71 0:04:16,080 --> 0:04:18,880 and Q 72 0:04:18,880 --> 0:04:22,000 we'd want to turn the double arrow into Q -> P, 73 0:04:22,000 --> 0:04:25,120 so we'd have matched what's before the arrow 74 0:04:25,120 --> 0:04:29,200 and we could do MP to get P. 75 0:04:29,200 --> 0:04:32,880 For some more cases 76 0:04:32,880 --> 0:04:36,680 let's assume we have P <-> Q [double arrow] 77 0:04:36,680 --> 0:04:39,520 and ~Q. 78 0:04:39,520 --> 0:04:43,697 Now we want to get P->Q, so we'll have the negation of ... 79 0:04:43,697 --> 0:04:45,639 what's after the arrow. 80 0:04:45,640 --> 0:04:50,637 Then we can do MT and get the negation of what's before ... 81 0:04:50,637 --> 0:04:51,999 the arrow, ~P. 82 0:04:52,000 --> 0:04:55,720 But if we have P <-> Q [double arrow] 83 0:04:55,720 --> 0:04:58,520 and ~P 84 0:04:58,520 --> 0:05:02,020 we'll want to get Q -> P, again so we have the ... 85 0:05:02,020 --> 0:05:04,920 negation of what's after the arrow 86 0:05:04,920 --> 0:05:10,120 and we can do MT to get the negation of what's before the ... 87 0:05:10,120 --> 0:05:11,160 arrow, ~Q. 88 0:05:11,160 --> 0:05:15,480 To sum up how to deal with double arrows 89 0:05:15,480 --> 0:05:19,213 if you've been able to get an exact match for what's on one ... 90 0:05:19,213 --> 0:05:21,199 side of the <-> [double arrow] 91 0:05:21,200 --> 0:05:25,424 then you want to put that side first when you get a single ... 92 0:05:25,424 --> 0:05:27,719 arrow from it, so you can do MP. 93 0:05:27,720 --> 0:05:32,040 If you can get the negation of one side of the <-> [double arrow] 94 0:05:32,040 --> 0:05:36,087 you want to put that side second when you get a single ... 95 0:05:36,087 --> 0:05:38,439 arrow from it, so you can do MT. 96 0:05:38,440 --> 0:05:43,200 The other rule for double arrows is <->I [double arrow in]. 97 0:05:43,200 --> 0:05:47,139 Here's the formula; if you have an arrow from A to ... 98 0:05:47,139 --> 0:05:49,601 B, and vice versa an arrow from ... 99 0:05:49,601 --> 0:05:52,358 B to A, you can make a double arrow. 100 0:05:52,360 --> 0:05:56,154 But this rule won't be much use until we can actually get ... 101 0:05:56,154 --> 0:06:00,113 arrow statements like that! And we don't have an ->I rule, 102 0:06:00,113 --> 0:06:02,999 so we aren't going to be able to do that yet. 103 0:06:03,000 --> 0:06:05,310 In fact, to make arrow statements, 104 0:06:05,310 --> 0:06:09,213 we're going to have to learn a whole different kind of rule. 105 0:06:09,213 --> 0:06:12,559 That's what we'll be discussing in future videos!