Video 1-2: Proof Templates

0:03 With that said, let's look at a few of these proof techniques. Um, starting simple. Uh, what is a formal proof? Even maybe these days it's a proof in lean that someone verified, but then you still need to understand lean and check that it actually proves what you wanted to claim. Uh basically a proof including lean and other such uh systems is a sequence of statements where each statement is either an accepted axiom of your logical system something where the world has come together and said we believe this is true and the uh term belief here is deliberate. There is no way to prove an axiom correct. You have to make a convention. uh but these are not very debated. This is I think not the problem. Either a statement is an axiom or it follows from some previous statements that you've already proven or derived and um it follows using a certain inference rule using a certain rule of logic that tells you if this is true and that is true then this follows logically without doubt.

1:18 This is if you want to be extremely formal and make a proof computer checkable among experts or those who want to become ones. Um we'll be a bit less strict. If you can convince your fellow humans then we'll be happy. Now that depends a bit on the fellow humans to do a careful checking. The point is that we want to write proofs in a way so that a capable human would be able to fill in all the details without too much problems and they would come to the full formal version of a proof if needed. But we don't always have to do this because we're doing the same kind of sequence of steps many many times. And after a very short while you see that you can leaprog over some of these. So we'll use the formal logic as guidance to um be careful not to make mistakes in our reasoning. But we won't um insist on a computer checkable proof because then uh this becomes a lecture of its own on how to do that.

2:28 A bit of notation to make this work and essentially the notation is is taken from from mathematical logic. There are statements. These are things that can be true or false. They will eventually be statements about our algorithms. But for a simpler example, let's take just English sentences that are hopefully unambiguous. And of course, it starts right there with it rains. Is a fine English drizzle already rain? Who knows? And the street is wet is of course equally ambiguous. But let's pretend like um very binary world. Then you can say things like not a so it doesn't rain not it rains uh you can make out what it means even though it sounds a bit wrong and an or is the combination of two. So uh both have to be true for A and B to be true. A or B it's enough if one of the two is true but it also is fine that both are true. It's the non-exclusive or.

3:38 Let me stress that because it's important for the next piece. An implication. If A holds then B also holds. Uh we write that with such an arrow. What it formally means is just not A or B in the meaning of the non-exclusive or. Okay. And the last piece of notation is equivalence. A is true if and only if B is true. That's a statement that we want very often because it completely characterizes one property in terms of another one. And that's formally just the same as saying A implies B and B implies A.

4:18 Easy peasy. Let's see. Here's a statement. And to the extent that this is unambiguous and so on, remember these slider questions are just for your personal elucidation. There's no right or wrong checked. Uh there's a right or wrong for this question, but I don't care who is who uh or what you answered. But it's more fun that way. and it forces you to to think about and commit to one of the outcomes.

6:09 Was that a no? Okay, then let's see. A rather strong majority is for yes. And you're right. Let's see why. So we have a statement of this if then flavor. So there's an if then comes one statement and there comes the uh conclusion. Now formally speaking this if a then b is nothing but not a or b and um let's pretend that not a is unambiguously true.

7:00 So no matter what b says the whole statement is true. And this is a a trick that you can also use in proofs. If you have a premise, this statement a after the if that is just false, you can logically deduce anything and it's a valid statement, it's not going to be very helpful because you can never apply that implication. But that's maybe besides the point. Uh so you can be the wise guy with this statement.

7:34 If we have such statements like an implication A implies B, how can we prove that? Now, of course, this will depend on what A and B really are about. And we'll see some examples, but there's still several different templates that you can apply completely superficially without thinking and try them one after the other. Sometimes one is easier than the other to make the argument. Um, the easiest is the the direct proof. you just somehow derive a start b starting from a. So again you write down your axioms and a and apply inference rules to arrive at b somehow. That's a direct proof. Uh another option is to prove this statement by contraosition. So you show instead of a implies b you show that not b implies not a. That sounds weird. Why is that? Why is that the same? Well, for that you just have to logically insert the definition. Remember A implies B was the same as not A or B. So this not B implies not A is the same as not not B or not A.

8:48 And of course this uh double negation cancels. We're going to write A in front and then B at the back. already cleverly rearranged and then you see it's a implies b. So these two statements are logically equivalent which sounds like it shouldn't make your proof easier but sometimes it does uh because this not be sometimes gives you something concrete to start with. We'll see some examples where you hopefully agree with my verdict here.

9:24 uh related is is a proof by contradiction. Maybe I should say another option a proof by contradiction just assumes that A is true and at the same time B is not true and then you somehow derive a contradiction from that. I don't know you have to arrive at some nonsensical conclusion. Hence your assumption must be wrong. And so this is the negation of A implies B if you check again what the definition says. And the last case that's um on the logical level it looks like it makes life just more complicated but it often gives you more to work with is a case distinction. And formally you can say instead of showing A to B in one step, I say I could have A and another property C and I show that these two together imply B or A and not C also imply B. Again, it feels like this doesn't help, but sometimes this additional property gives you more to work with and makes the proof easier even though longer.

10:53 Okay. Um, let's see an example. You're not asked to prove this. I'm going to read out the proof to you and you're just trying to recognize which template is it. So, we prove something about natural numbers. N is some natural number. And the statement is if n squared is an even number then n is also an even number. And uh for that we how do we prove this? Well, we show that if n is odd, then n^ squ is also odd. And maybe let's unfold this a bit. What is an odd number? A number that's not even. Haha. Uh you can write any odd number as 2 * k + 1 where k again is a natural number. I'm trying to be diligent with n0 means the natural numbers including the zero. If you ever spot on my slides an n without a zero or without some other subscript that tells you the range, you should treat this as a mistake and tell me, I'm trying to avoid this ambiguous notation. So n0 is with a zero. Any odd number n can be written as 2k + 1. Okay.

12:06 Now if this is odd, we want to show that n^2 is also odd. So I just insert this. Now you need these uh binomial laws from school, right? So or k^ 2 + 4k + 1.

12:28 Now it turns out that this you can write as 2 * k prime + 1 or k prime this thing divided by 2 2k 2 + 2k and since k was a natural number also 2k ^ 2 + 2k is a natural number. So what we've done here is we found a representation for n squ that also has this pattern of an odd number. So n^ squ is odd. That's what's behind this innocent line here. If you unfold it, you can do a little bit of arithmetic and then you find that it has the pattern of an odd number. But what was the proof template we used here?

13:55 [snorts] Okay. to not keep you um much longer at the end of our slot soon. Most people got this correct. Indeed, it was a proof by contraosition or an indirect proof where we started with the negation of the conclusion, right? N squ is an even number. Then n is also even. The only uh hidden fact here was that I already inserted that not even means odd. So we started with n odd and then derived that this is also negated.

14:37 Uh then we had this other form of statement that is very common in in algorithms and in mathematics in general. An equivalence a implies a if and only if b. And for that if you want to prove such a statement you just or you could try to do it directly but almost always it's easier to do if you just split the two statements that you're supposed to prove the two implications and show each of them separately. And there again because each of these statements is an implication of the form we've just covered. You can use any of the recipes for implications in the two parts. And so you see that often um these formal proofs are very schematic and that there's a certain template you follow. And if you apply this diligently enough times, what you arrive at in the middle is often a fairly easy argument. That's the hope anyways.