1 0:00:00,000 --> 0:00:04,918 In this video we're going to learn direct derivation, 2 0:00:04,918 --> 0:00:07,650 a new way of setting up proofs. 3 0:00:07,650 --> 0:00:11,038 We'll also learn two rules, &O and &I. 4 0:00:11,040 --> 0:00:15,720 First I want to introduce direct derivation. 5 0:00:15,720 --> 0:00:19,089 Direct derivation is an alternate way of writing ... 6 0:00:19,089 --> 0:00:21,636 proofs. Up till now we've used simple ... 7 0:00:21,636 --> 0:00:24,265 derivation, in which we start with the ... 8 0:00:24,265 --> 0:00:27,716 premises and go on until you get to the conclusion, 9 0:00:27,716 --> 0:00:29,277 at the end of the proof. 10 0:00:29,280 --> 0:00:32,769 For direct derivation, you start by writing the ... 11 0:00:32,769 --> 0:00:36,869 conclusion on a SHOW line, after the premises and before ... 12 0:00:36,869 --> 0:00:38,439 you do any more steps. 13 0:00:38,440 --> 0:00:42,178 Then you make a box and use the rules to prove the ... 14 0:00:42,178 --> 0:00:43,999 conclusion in the box. 15 0:00:44,000 --> 0:00:48,320 Once you've proved the conclusion inside the box 16 0:00:48,320 --> 0:00:50,840 you close the box 17 0:00:50,840 --> 0:00:53,562 and cancel out the original SHOW: 18 0:00:53,562 --> 0:00:56,479 line by crossing out the word SHOW:. 19 0:00:56,480 --> 0:01:00,880 Here's an example of how that works. 20 0:01:00,880 --> 0:01:04,800 We write down our premises 21 0:01:04,800 --> 0:01:08,420 and after that we write down the conclusion on a separate ... 22 0:01:08,420 --> 0:01:11,038 SHOW line. (The conclusion will be given ... 23 0:01:11,038 --> 0:01:14,118 along with the premises as part of the problem.) 24 0:01:14,120 --> 0:01:18,160 Then we make a box to show Q in. 25 0:01:18,160 --> 0:01:20,928 Now we do rules to the premises. 26 0:01:20,928 --> 0:01:23,377 We can get P by vO from 2 and 3. 27 0:01:23,377 --> 0:01:28,168 Since ~R is the negation of one side of the wedge in line ... 28 0:01:28,168 --> 0:01:30,510 2, we apply vO and we get the ... 29 0:01:30,510 --> 0:01:33,598 other side of the wedge, which is P. 30 0:01:33,600 --> 0:01:36,606 Then we get Q by MP from 1 and 5. 31 0:01:36,606 --> 0:01:40,489 P is what's before the arrow in line 1, 32 0:01:40,489 --> 0:01:44,998 so we get what's after the arrow, which is Q. 33 0:01:45,000 --> 0:01:48,282 Now since we've shown Q in the box, 34 0:01:48,282 --> 0:01:51,682 we cancel out the line where we show 35 0:01:51,800 --> 0:01:56,106 and write DD next to it, to show that we showed Q ... 36 0:01:56,106 --> 0:01:58,599 using direct derivation. 37 0:01:58,600 --> 0:02:03,240 Some things to note about direct derivation. 38 0:02:03,240 --> 0:02:05,674 First, when you write something on ... 39 0:02:05,674 --> 0:02:06,597 a SHOW: line, 40 0:02:06,597 --> 0:02:10,459 you can't use it as an input to other rules if you haven't ... 41 0:02:10,459 --> 0:02:12,558 cancelled out the SHOW: line. 42 0:02:12,560 --> 0:02:16,203 The thing on the SHOW: line is something that needs ... 43 0:02:16,203 --> 0:02:19,239 to be shown. It's not shown until you close ... 44 0:02:19,239 --> 0:02:21,581 the box and cancel the show line, 45 0:02:21,581 --> 0:02:25,398 so you can't use it as an input to rules inside the box. 46 0:02:25,400 --> 0:02:27,561 Also, right now Direct Derivation ... 47 0:02:27,561 --> 0:02:31,139 doesn't let us prove anything we can't prove using simple ... 48 0:02:31,139 --> 0:02:33,971 derivation. It's just another way of writing ... 49 0:02:33,971 --> 0:02:36,505 proofs, with the conclusion explicitly ... 50 0:02:36,505 --> 0:02:38,517 stated just after the premises. 51 0:02:38,520 --> 0:02:40,681 However, later we'll learn some new ... 52 0:02:40,681 --> 0:02:44,283 rules that won't work unless you've written the conclusion ... 53 0:02:44,283 --> 0:02:45,219 on a SHOW: line. 54 0:02:45,219 --> 0:02:48,244 These rules are going to have to be used with Direct ... 55 0:02:48,244 --> 0:02:50,477 Derivation. So we might as well learn ... 56 0:02:50,477 --> 0:02:51,917 direct derivation now. 57 0:02:51,920 --> 0:02:54,138 Also, you don't have to draw the ... 58 0:02:54,138 --> 0:02:57,038 whole box. You can just draw the leftmost ... 59 0:02:57,038 --> 0:02:59,511 line. That's much more convenient ... 60 0:02:59,511 --> 0:03:01,558 if you're typing a proof out. 61 0:03:01,560 --> 0:03:04,458 Now let's learn some new rules. 62 0:03:04,458 --> 0:03:08,359 The first one we'll learn is the rule of &O. 63 0:03:08,360 --> 0:03:11,246 This rule only needs one input, 64 0:03:11,246 --> 0:03:15,131 whose major operator is &. If you have A&B, 65 0:03:15,131 --> 0:03:17,240 then you know A is true. 66 0:03:17,240 --> 0:03:21,925 You also know B is true. So you could get either one of ... 67 0:03:21,925 --> 0:03:23,559 those by using &O. 68 0:03:23,560 --> 0:03:26,570 The upshot is that you can break an & 69 0:03:26,570 --> 0:03:29,372 statement up into its two sides, 70 0:03:29,372 --> 0:03:32,278 as long as & is the major operator. 71 0:03:32,280 --> 0:03:34,339 No input is needed besides the & 72 0:03:34,339 --> 0:03:36,953 statement. This is the first rule we've ... 73 0:03:36,953 --> 0:03:39,488 learned that only requires one input; 74 0:03:39,488 --> 0:03:41,468 once you have the & statement, 75 0:03:41,468 --> 0:03:44,557 it doesn't require anything else to unlock it. 76 0:03:44,560 --> 0:03:47,649 This means that when we do a proof with an & 77 0:03:47,649 --> 0:03:51,919 statement in it, it's a good idea to start by doing the &O. 78 0:03:51,920 --> 0:03:57,360 Let's look at this proof. The second premise is an & statement. 79 0:03:57,360 --> 0:04:01,068 So we start by breaking it up, because that's something we ... 80 0:04:01,068 --> 0:04:02,458 can do. First we get P. 81 0:04:02,458 --> 0:04:06,088 Note that I'm just drawing a line down the left instead of ... 82 0:04:06,088 --> 0:04:07,478 making the whole box. 83 0:04:07,480 --> 0:04:12,240 And we also get the right half, ~R. 84 0:04:12,240 --> 0:04:15,742 Since P is what's before the arrow in 1, 85 0:04:15,742 --> 0:04:20,119 we can do MP and get what's after the arrow, Q->R. 86 0:04:20,120 --> 0:04:24,451 Now the ~R from line 5 is what's after the arrow in ... 87 0:04:24,451 --> 0:04:27,158 Q->R, so we can do MT and get the ... 88 0:04:27,158 --> 0:04:30,839 negation of what's before the arrow, ~Q. 89 0:04:30,840 --> 0:04:33,910 That's what we were trying to show, 90 0:04:33,910 --> 0:04:38,039 so we can cancel the SHOW line and label it as DD. 91 0:04:38,040 --> 0:04:42,105 Now let's look at the &I rule. This is our first introduction ... 92 0:04:42,105 --> 0:04:44,137 rule, which lets us make a more ... 93 0:04:44,137 --> 0:04:47,308 complex sentence out of simpler components by ... 94 0:04:47,308 --> 0:04:50,398 putting a new connective into the statement. 95 0:04:50,400 --> 0:04:54,039 The idea is that we have two inputs and we join them ... 96 0:04:54,039 --> 0:04:57,412 together with an &. Since we know they're true ... 97 0:04:57,412 --> 0:04:58,743 separately, the & 98 0:04:58,743 --> 0:05:00,518 statement must be true. 99 0:05:00,520 --> 0:05:05,412 The inputs can be anything. This lets us put any two things ... 100 0:05:05,412 --> 0:05:06,839 together with &. 101 0:05:06,840 --> 0:05:10,400 Here's one common use for this. 102 0:05:10,400 --> 0:05:12,454 We have an & before an arrow, 103 0:05:12,454 --> 0:05:15,134 as in line 3. And we manage to get each ... 104 0:05:15,134 --> 0:05:17,010 side of the & separately. 105 0:05:17,010 --> 0:05:19,690 We'd like to be able to do MP to line 3, 106 0:05:19,690 --> 0:05:23,174 but in order to do that, we need to exactly match ... 107 0:05:23,174 --> 0:05:25,318 what's in front of the arrow. 108 0:05:25,320 --> 0:05:30,180 We can use &I to put lines 1 and 2 together to get P&Q. 109 0:05:30,180 --> 0:05:35,040 That exactly matches what's in front of the arrow. 110 0:05:35,040 --> 0:05:38,880 So then we can do MP. 111 0:05:38,880 --> 0:05:42,800 So if you have an & in front of an arrow 112 0:05:42,800 --> 0:05:47,360 often you can try to get both sides of the & 113 0:05:47,360 --> 0:05:51,440 then use &I to put them together 114 0:05:51,440 --> 0:05:55,320 and you'll be ready to use MP. 115 0:05:55,320 --> 0:06:00,400 Let's look at how we can put these rules together to do a longer proof. 116 0:06:00,400 --> 0:06:03,211 Here's all the premises and the conclusion. 117 0:06:03,211 --> 0:06:06,478 It may be a bit intimidating to see so many premises. 118 0:06:06,478 --> 0:06:09,517 But we can get a handle on it by starting with the & 119 0:06:09,517 --> 0:06:13,240 statement and then taking the smallest statements we have ... 120 0:06:13,240 --> 0:06:16,279 and seeing if we can combine them with anything. 121 0:06:16,280 --> 0:06:19,534 So we have an & statement in 5, 122 0:06:19,534 --> 0:06:24,144 and we can use &O on it to break it up. We get 123 0:06:24,280 --> 0:06:27,983 and R. Now the P is what's before ... 124 0:06:27,983 --> 0:06:29,977 the arrow in line 125 0:06:30,120 --> 0:06:35,060 so we can get ~Q by MP. That's the negation of one ... 126 0:06:35,060 --> 0:06:37,593 side of the wedge in line 127 0:06:37,720 --> 0:06:40,026 so we get the other side, T, 128 0:06:40,026 --> 0:06:42,751 by vO. We can go back and see that ... 129 0:06:42,751 --> 0:06:43,799 R, in line 8, 130 0:06:43,799 --> 0:06:46,734 is what's before the arrow in line 131 0:06:46,840 --> 0:06:51,707 so we apply MP and get S. Now we have both halves of ... 132 0:06:51,707 --> 0:06:55,357 the & that's before the arrow in line 133 0:06:55,480 --> 0:07:00,480 so we put them together with &I to get S&T 134 0:07:00,480 --> 0:07:04,680 which lets us do MP to get U. 135 0:07:04,680 --> 0:07:07,761 Finally, what we need to show is ... 136 0:07:07,761 --> 0:07:10,842 ~Q&U. We have each half of that, 137 0:07:10,842 --> 0:07:14,398 so we can use &I to put that together. 138 0:07:14,400 --> 0:07:18,051 Now we've shown what we needed to show, 139 0:07:18,051 --> 0:07:23,071 so we cancel out the SHOW line and mark it as done using ... 140 0:07:23,071 --> 0:07:24,896 DD. And we're done! 141 0:07:24,896 --> 0:07:28,318 The argument has been proved valid.