Video 0-3: §0.1 Proof templates

0:00 Introduction to proofs

0:03 welcome to uh the unit zero on proof techniques this is a little primer on mathematical mathematical techniques and and tools that we will just use a little bit um on the side but they're just very useful to know in general it's a little bit of formal logic if you like uh don't don't be too scared it's it's not a lot and it's not very deep um but it's helpful to know the terms that that i will show you and it's helpful to know some of these proof techniques because they're used again in in research papers they're used in other classes and they're used a little bit also in some of the material i want to share with you later in this in this in this module

0:49 so let's get started with the the proof techniques i'll show you some templates for proofs and then specifically mathematical induction because that's one that's very heavily used in computer science and discrete mathematics and i'll briefly touch on how to prove formally that the program is correct that what you created in software is actually exactly doing the right thing that's again a whole big area of verification

1:20 people are studying this in much more detail i just want to give you a brief glimpse on it because again some of these questions will arise again when we discuss algorithms

1:35 Defining a formal proof

1:39 so what is a proof that's a a very deep question once you think about it and it has only really been settled in the early 20th century so it's a it's a fairly novel uh construction in this in this sense where you stress formal of course people have been doing mathematical proofs for decades and well dating back to ancient greece um but they might not have had the very strict notion of a proof that mathematics now has so what is a proof a proof is a sequence of statements statements that say something about a certain matter and each of these statements is either an axiom that's a statement that you accept outside of the mathematical system to be true so that's that's interesting to get mathematics going you have to accept you have to believe if you like in certain axioms to make sense or to hold true and there's no way for you to prove that these axioms are actually true or make any sense or or anything like this you have to accept them as given now then of course mathematicians wonder whether the the weakest axioms that you can start with and that's that's the um the subject of a formal logic but uh coming back out of the historical discussion a formal proof is a sequence

3:10 of statements and each statement is either something that you accept to be true god given or it follows from previous statements in this sequence using given inference rules and these are usually very very few rules that are allowed and they're specified by the logical systems all right what does that mean for you and for us usually among experts in a field often that's mathematicians but it can also be theoretically computer scientists or it can be programmers they often also argue about proofs

3:47 it's often accepted that it's enough to convince another expert human that a formal proof is possible that a formal proof is can be written down but you often don't write it down now how can you be sure how can you convince someone that this proof exists without writing it down that's actually a bit tricky sometimes it seems like a proof exists but it doesn't really exist and so what you have to do is use formal logic as guidance against faulty reasoning because that's something that easily happens especially for beginners so the easy way to prove to convince someone that a formal proof exists is to write it down and that's the only way to get bulletproof statements where you can absolutely be sure that it holds true so let's see some more concrete examples what that means and for that we need a little bit of notation so um i think this is this is big enough we will talk about statements so these are logical um sentences in in english or they can be um statements about numbers with variables so a simple statement could be a which which is the statement it rains which is is not true in my place at least and another statement could be the street is wet okay this is fairly awake what street i

4:44 Logical operators and notation

5:27 mean also it rains is is wake where when but let's suppose now and here where i am and the street is wet well the one outside of my window let's take this one uh it's not it's not really wet so both statements are are wrong for me at this point but at a different time they might be true they might be satisfied so usually statements are something where you can clearly say this is either true or false

5:59 it's hard to find examples in the in the physical world that are very clear-cut either true or false but in mathematics it's usually easier either a number is equal to 5 or it's not equal to 5 there's nothing in between really if we have a statement we can negate it that means we put this funny this funny symbol in front of it and that is a new statement which has just the opposite meaning so not a is the statement that uh in english we would say that it does not rain

6:40 but in more computerized speak you could just say it's not it rains well sounds not great but it's understandable then we can take two statements and use their conjunction the and between them that's written as this little little roof that's a and b so it rains and the street is wet which is true if and only if a is true and b is true that's what and usually means also in the in the natural language sense we can also put an or between the the two so uh this is true or this is true or both um

7:23 it's the non-exclusive or to use the the term uh from there which means it's allowed that both are true uh sometimes when we talk in in english and we say or we mean the exclusive or it's either this or that if you want to make the distinction clear that doesn't have in classical logic it doesn't have an extra symbol sometimes it's used and sometimes it's written as a with a

7:56 a plus with a circle around it and it's called xor that's the exclusive or but not both that's what i mean with either or these are usually the things that are fairly natural and easy to understand now slightly more controversial is is implication if a holds then b is also true if a then b if it rains the street is then the street is wet that would be the example for our a and b um i'll have a nice question about that in a second so i'll come back to that but i want to mention the last one the equivalence written as this double arrow

8:50 and that means statement a and b are logically equivalent in the sense that a holds holds true exactly if and only if b holds true and you can essentially define this as in terms of the other symbols

9:16 okay this is sometimes written as this we define this to be the same as a implies b and b implies a so that is the same thing as a is equivalent to b

9:42 the two are equivalent if one implies the other and the other implies the former okay let's see a more concrete example and for this i want to ask you this this question

9:45 Analyzing logical implications

10:02 so please have a think about this one is the following statement true if the earth is flat then ships can fall over its rim just tell me if that as a logical statement is true or false

10:30 i'll give you a sec to answer it and think about it okay i see 26 people answered so maybe another few seconds again remember it's about participation it's not about being correct about this i will tell you i haven't really told you what what the answer to this is at this point in time

11:53 okay let's see does anyone feel he needs more time to think about it then shout out in the lecture back channel doesn't look like it so um here are the results i think you can see them on the right but just in case um

12:21 so a lot of people say yes but there's also a few that say no and a few that say neither of the two is is true and i see this is again i can only show the correct answer if i leave it open that's fine so you can in principle still change your answer but not much is learned if you do so yes um the the statement is true and uh that's despite the fact that it talks about this nonsensical assumption i mean we know the earth is not flat by now we are pretty sure about this at least most of humanity are pretty sure that the earth is not flat but

13:04 for the logical statement this means the entire thing is trivially true so it's true because a implies b again is defined in terms of other things we already know a implies b is the same as either not a or b

13:40 so in this example a implies b a is the earth is flat now that means a implies b is the same as uh this thing not a or b now we can read out what that means in english

14:05 it says the earth is not flat or ships can fall over its rim well this is clearly not true but this is true and because it's an or in between the overall thing is true oops

14:31 all right so that's um just one important notion uh just to keep in mind this this formal definition of implication is maybe sometimes not completely intuitive you can totally make statements um when the precedent the thing in the if is not true you can claim anything and it's still a correct statement it's not a very useful statement in that the implication doesn't really do anything that's logically true

15:03 Proof strategies

15:05 okay i want to dive into a few more proof techniques templates so what these are for is um assume you have a statement that you would like to prove correct you have say you found a cool new observation in an algorithm and you'd like to show that a statement of the forum uh if a is true then b is true uh holds you want to convince someone that this is true uh what could be a more useful example um a useful example in in our context could be a is uh the input to your program

15:55 is valid and uh i mean this is whatever that means for you um say a list of numbers then b could be the output of your program is what it should be is correct

16:22 and then again that has to be substituted in a concrete instance by something that makes sense maybe the list has become sorted that's one of the topics that we will talk about in a couple of weeks so that's one instance now you might have this situation you want to make this statement about your program if the input is a valid list of numbers then the output is correctly sorted you would like to prove this then you have different strategies how you could do this you can do it a direct proof you assume that a holds and you show that then also b holds that's that's the obvious way to prove this but there are other alternatives so this is this is kind of um i only list it uh because it's sometimes the way to go it's sometimes the most convenient way to prove something but it's not very surprising the more interesting ones are the other ones because sometimes this is hard to do it seems not easy to show this and some of the other strategies are easier so one thing you can do is you assume that b is not true and then you show a has also been false so it's it's a proof by by contraposition it's similar to proof

17:45 by contradiction but it's slightly different in that you work your way strictly backwards so assume your output of the program is not sorted then you show that something in the input was fishy maybe the input contains an invalid number that cannot be compared with others

18:07 related is the proof by contradiction that means you assume a holds and b is violated and then you derive that this leads to a nonsensical statement so classic examples in mathematics for this kind of proof are are often um that uh the square root of two is is irrational

18:39 so you you can prove that the square root of two cannot be written as a fraction of two integers and one way to do is is to assume well assume it could be written like that and assume that the denominator numerator and denominator are relatively prime and then you can show by rearranging the equations that then actually they share a factor of two so that's a contradiction to your assumption

19:11 and lastly sometimes it helps to make the statement more complicated to make the proof easier so instead of just showing a implies b you take a different condition c and distinguish two cases when c holds and when it doesn't hold and if you can show in both cases that a and c implies b and a and not c implies b then a implies b either way and you can have more than two cases as well

19:47 that depends on the exact statement what is more convenient or more useful again uh a little question for you guys um an example and i would like you to to tell me what proof template has been used there so the example we're proving is if n squared is an even number then n is also even that is a correct statement and one way to show it is you show that when n is odd you assume n is odd and then you show that n squared is also odd what proof technique is that what template did you follow for this for this little proof and well just while you're voting this proof is actually fairly simple when n is odd that means you can write i shouldn't use that arrow

20:57 that means n can be written as 2 k plus 1 for some integer k say a natural number and if i now look at what happens to n squared well that's 2 k plus 1 squared that's nothing but 4k squared plus 4k

21:24 plus 1 and you see that this is even because it's divisible by 2 and so it can be written as 2 times or 2 times k prime plus 1 and k prime is again a natural number and it's it's just this divided by two so that's the proof um that also n squared is odd

21:59 so it's a simple statement and the proof is clearly correct though the statement is also true but what proof technique have we used maybe again just a couple of seconds because this was a bit more reading necessary

23:10 and out yourself in the back channel maybe we need this you can't post anonymously to the chat rooms unfortunately okay uh 46 so i'll show you the results now

23:30 so most people voted for indirect proof and we also have a couple of answers for the other things um the correct answer is indirect proof and let me go back to the slides to to show why um so that's again we should just identify a and b in this statement n squared is an even is an even number that's our a and is also even or is even that's our b and now if you see um we start with n is odd which was a bit mean because it's not um it's not directly uh the same thing as not b but this is effectively not b

24:21 because not even is the same as odd and same here this is again not a because again we flipped even an odd so the proof technique we used is indirect proof we showed the implication not b implies not a

24:48 all right um good thanks for other good participation in the question and let's move on there are other types of statements that we sometimes have to show and one example is equivalences we want to show that a is true exactly when b is true that was this so remember that was a if and only if b often written as as this so that's if and

24:52 Equivalence and set proofs

25:18 only if so we can often prove both implications we can often prove a implies b and b implies a as just two steps so it's two little sub proofs that together um show that a is the same as b is equivalent to b in this sense

25:43 and it often happens that one direction is much easier than the other but not always another type of statement that we will sometimes need is about two sets so we have a set s and another set r and we'd like to show that r is a subset of s

26:09 now and just to make sure this this notation here with the with the bar below this is somewhat similar to a lesser equal sign uh and it also means that r can be equal to s

26:29 and uh in in terms of in logical terms it means you show this implication whenever you have an element in r that same element is also an s so instead of arguing about sets what you really have to do is prove an implication and we've just seen how to do that scroll a couple of slides back and use one of the techniques from there

26:53 now this in isolation is not so uh is not so often what we want to prove it's more often that we want to prove that two sets are equal s and r are equal as sets and that again means um you prove two imp two inclusions s is a subset of r r is a subset of s if both is true then the two sets must be the same so again you have reduced proving set equivalence to set inclusion which will reduce to implication which you could reduce to one of the strategies that i've shown you that's how proofs are often get structured