In section this week we largely proved things. I'll give you an example (note, I use a derivation system that is slightly different from Sean's. The difference between Sean's and mine is that mine is more explicit about the reasoning involved. For that reason it includes a few more steps. You can easily translate my derivations into Sean's by removing those extra steps. I like to include them for elementary logic so students can see all of the reasoning that goes on clearly. I've found once that's explicit, students start seeing that derivations are like arithmetic calculations in that they're very mechanical and rather easy):

1. A -> C
2. B -> (A v C)
3. SHOW (A v B) -> C

Note line 3 is something you've not seen. It's the thing you're being asked to prove. I like to include this in the proof directly so you can keep in mind your goal. Specifically, you know in line 3 you need to prove a conditional. You know that conditionals are only false if the antecedent is true and the consequent false. We're trying to show line 3 follows from lines 1 and 2. That means we're trying to show that if 1 and 2 are true, then so is 3. So we're trying to show 3 is true. To show line 3 is true, we essentially need to show it's not false. For that reason, we are warranted in assuming the antecedent is true in our proof. To do this, I like to add the following line:

4. SUPPOSE (A v B)
5. SHOW C

That is, I'm assuming the antecedent of line 3 is true. If I can show the consequent is derivable from 1, 2, and 4, then I'll have shown line 3 is entailed by lines 1 and 2. I've added a new SHOW line with "C" as our new target to make this clearer. You can think of this as a divide and conquer strategy. You assume some things to narrow down parts of the proof you need to apply rules to derive. At this point we've narrowed down our task to just having to prove "C" from lines 1, 2 and 4.

To be clear, it's not always the case that something of a conditional form is provable from premises. Just because we've assumed the antecedent of a conditional it doesn't mean we can derive a consequent. Put another way, in logic "assuming makes an ass out of you and me" doesn't apply. You can assume whatever you like, but it doesn't mean you can prove whatever you like. To this, just think about this attempt at a proof that won't work:

1* ~A
2* (B v C)
3* SHOW B -> C
4* SUPPOSE B
5* SHOW C
6* ?

There's no way to prove 3* follows from 1* and 2*, because there's no way to prove 5* follows from 1*, 2*, and 4*.

Again, this is just to say it's okay to assume the antecedent of a conditional when you're trying to prove it's true. If the antecedent is true and the consequent is false, you won't be able to prove it. If the antecedent is either false, or true and so is the consequent, then you'll be able to prove it. Hence, it's okay to assume it's true and focus on the consequent in derivations. Okay, now back to the other proof. We made it to:

1. A -> C
2. B -> (A v C)
3. SHOW (A v B) -> C
4. SUPPOSE (A v B)
5. SHOW C

Now we need to show "C". It might not seem obvious how. But note that we have line 4 available now. Moreover, it should be intuitive that the following holds:

(METHOD OF CASES): (A -> C) /\ (B -> C) |= (A v B) -> C

Consider: "If John goes to Home Depot then he buys batteries and if John goes to Target then he buys batteries, so it must be the case that if John goes to Home Depot or Target then he buys batteries." I hope that strikes you as true. But if not, let me prove it for you:

1** (A -> C)
2** (B -> C)
3**. SHOW (A v B) -> C
4**. SUPPOSE (A v B)
5**. SHOW C

There are many ways to show this, but I will show you how to do it by assuming the negation of "C" is true. Recall, everything in our language is either true or false. So, if "C" is true then "~C" is false, and vice versa. Moreover, in our language there are no contradictions. That means there is nothing of the form "C /\ ~C" outside a SUPPOSE line. Strictly speaking, we can suppose contradictions if we want. But - importantly - that's the only place a contradiction can live in our proof. In other words, we assume our language is consistent. All of this means that if I assume "~C" is true and get a contradiction, then it has to be the case that "C" is true. So:

6**. SUPPOSE ~C

But now look at line 1**. Recall, we have this rule:

(MODUS TOLLENS) (A -> B) /\ ~B |= ~A

We can apply that to lines 1** and 6** to get line 7**. We can do it again with lines 2** and 6** to get line 8**.

7**. ~A
8**. ~B

Now we can use line 4** and line 7** with the following rule:

(DISJUNCTION ELIMINATION) (A v B) /\ ~A |= B

That gives us line 9**.

9**. B

But lines 8** and 9** contradict each other. I like to write "!" to indicate that. Strictly speaking, "!" just means "B /\ ~B".

10**. !

Since I've a contradiction on the assumption of "~C" I must take back that assumption. That means I know "C" is true. The proof altogether is:

1** (A -> C)
2** (B -> C)
3**. SHOW (A v B) -> C
4**. SUPPOSE (A v B)
5**. SHOW C
6**. SUPPOSE ~C
7**. ~A
8**. ~B
9**. B
10**. !

Since my goal was to show line 3** followed from lines 1** and 2**, and I broke that down into me just having to show line 5** followed from 1**, 2**, and 4**, and since I just showed line 5** does follow from these premises, then I'm done. We now know the (METHOD OF CASES) works in our logic. Hence, we can use it whenever we want. We don't need to run through the proof again. We'll just label it and that'll be an abbreviation in our future proofs for the proof just above this paragraph.

Okay, so now we can finally return to our initial proof. Recall again where we left off, and let's apply (METHOD OF CASES). To do that, note we need to prove two things for this to apply, namely (A ->C) and (B -> C). Let's break that into two parts. starting with the first. I'm going to move a little faster now since we've covered all the tools we need to prove this:

Note at this point we need to show "C" follows from lines 1, 2, 4, 11, and 13. Importantly, we can't use line 7 anymore. This is because we already proved the thing we were trying to prove when we assumed "A" was true. We've "closed" that assumption off from the rest of the proof, when we derived "C" under it. This is analogous to moving from one nested line in Sean's proof system to a line just to the left of it. In any event, note in line 13 we have another disjunction and need to show "C" follows. We can apply (METHOD OF CASES) again:

14. SHOW (A -> C)
15. SUPPOSE A
16. SHOW C
17. C Modus Ponens, 1, 15
18. SHOW (C -> C)
19. SUPPOSE C
20. SHOW C
21. C Repetition, 20
22. (A v C) -> C Method of Cases, 14, 18
23. C Modus Ponens, 13, 22
24. (A v B) -> C Method of Cases, 6, 10
25. C Modus Ponens, 4, 24

And we're done. Here's the full proof altogether:

1. A -> C
2. B -> (A v C)
3. SHOW (A v B) -> C
4. SUPPOSE (A v B)
5. SHOW C
6. SHOW A -> C
7. SUPPOSE A
8. SHOW C
9. C Modus Ponens, 1, 7
10. SHOW B -> C
11. SUPPOSE B
12. SHOW C
13. (A v C) Modus Ponens, 2, 11
14. SHOW (A -> C)
15. SUPPOSE A
16. SHOW C
17. C Modus Ponens, 1, 15
18. SHOW (C -> C)
19. SUPPOSE C
20. SHOW C
21. C Repetition, 20
22. (A v C) -> C Method of Cases, 14, 18
23. C Modus Ponens, 13, 22
24. (A v B) -> C Method of Cases, 6, 10
25. C Modus Ponens, 4, 24

Next time we'll walk through the details of the justifications on the side of the proof more carefully. I'll also show you how to extract Sean's proof style from that above. If you prefer using Sean's proof system that's okay, it's equivalent to mine. Again, the only difference is mine makes every assumption and target in the proof explicit so you can understand the reasoning involved more easily. Once you've got the reasoning down, you won't need to see all those extra lines.