Propositional Logic: Syntactic Consequence Relation

[00:00:10][Music] okay let's begin so uh we at the end of last lecture we asked this question so given a set of propositional formulas capital S and a single propositional formula t does there exist a purely syntactic way which means a way which can be taught to a machine to determine whether T is a logical consequence of s and one of the possible answers to that question is given by Hilbert style deductive calculus so what is calculus calculus is a set of rules and some axioms as you all may recall axioms are those statements which we do not question right and in this case uh these axium schemata yeah I mean I'm using the word schemata because there are different schemes and they themselves have variables in them so the important thing here is that uh I mean you have to verify when I start writing down these axium SCH uh schemes you have to remember that these are all toies I mean remember or verify yourself and I think nobody will have any objections in accepting tooies as axioms because they are always true so why not and the rule of inference there will be only one yeah so what is that modus ponents or for short we are going to call it MP okay so we will have this and in order to do this properly we are going to use a slightly different adequate set of connectives so when we defined propositional language and then prepositional formulas SL then we only used two symbols what were they negation and conjunction but uh just a momental thank you okay so uh now today onwards we are going to use a slightly modified set of adequate connectives adequate set of connectiv which uses negation and implication obviously there is no difference yeah implication and negation are adequate you can check that what do you need to do as soon as you can express conjunction using implication and negation you are done because we already know that conjunction and negation they are together adequate yeah so how do you express conjunction using implication and negation negation of P implies negation okay if you say so I'm going to believe that implic uh negation of P implies negation Q is same as using D Morgan it will be same as P conjunction Q okay so any questions about this this is the way we are going to do it there is another answer to this question that is natural deduction system or genen style system but we are not going to cover that in our course if you are interested please go and read about it in any good logic book I have given you lots of references okay uh that has very few axioms but mostly it contains rules of inference okay so what what are these axioms so we are going to call them logical axioms and short form is La so these logical aums there is four of them la1 is the statement s implies T implies s can you check quickly if you take this statement s and t are any formulas then can you check that this is a tooy if s is false then false implies anything is true if s is true then anything implies true is true so therefore the second part will be like T implies s will be true so this is a actually a toy yeah so I should uh well okay um here I should write for all s and t in SL this is la1 logical axium one but it is not a single axium please notice it is lot of axium put together because there is one axium for each s and t for each pair S and T right so there are infinitely many axm here that's why we are calling it axium schemata it's a scheme yeah s and t are variables they are not propositional variables they are formulas any arbitrary formula can be put in there and then still it will give us a logical axium because as you already confirmed that this is a tooy no matter what s and t are it's going to be remain a tooy okay so this is an axium scheme not just a single axum I did not write propositional variables for S and T I said any arbitrary formulas s and t this one is a logical axium okay this is called yeah I mean I'm going to write their names although you don't need to remember them at all this is called law of affirmation of consequent okay so affirmation of consequent consequent is s t is arbitrary and in general in formal proofs this particular axm is very useful because it allows you to talk about any like introduce any arbitrary T okay sir yes can we only use l instead of s if you only use l then your proof system won't be strong enough yeah so that's why you need the strength of all of them I'm going to write one extra thing but that's okay so uh now sorry uh I should add a u also here yeah St and U for all St and U the second one is something which you can already see what's happening what does it look like right so let me write its name it's is called self-d distributive law of implication okay so s implies T implies U implies s implies T implies s implies U so St and U are arbitrary Okay so so la3 now la3 is very simple this is called double negation elimination name is simple double negation elimination and finally we have la4 that is now you tell me what what it looks like contrapositive yes law of contraposition okay so if you know the Contra positive of a statement then you know the statement now here I'm going to give you an an exercise verify that all logical axioms are toies yeah just so that you can confirm this well okay now um the Only Rule is modus ponents but how to use these things yeah once we have these ingredients how to use them so there are actually uh we are going to use induction to construct a proof of formal proof yeah and in that induction there will be two basic steps first one is uh I mean base cases yeah first one is a logical axium the second one is a non-logical axium and the only inductive step is this so-called rule of inference modus ponents I'm going to write all these things down so using this we are going to define a sequent so there there is a bunch of terms but once I start writing a for an example of a formal proof all these things will be clear so let me go to the next slide and start talking about it so oh yeah uh just before we proceed modus ponents yeah so this is a rule of inference so for s and t in SL yeah I mean here I'm going to be a bit sloppy if we have S implies T and T then we have t s oh sorry yes here I'm supposed to write s if we have S implies T and S then we have t now I'm being sloppy in which word here we have yeah what does that really mean so I'm going to make that precise by defining a sequent okay given s subset of SL and S uh and T in SL say that now notice yeah is a deductive consequence of s yeah so read T is a deductive consequence of s if one of the following is true okay so now there are two base cases uh the first one is L A okay if T is a logical axium then T is a deductive consequence of s see logical axium means a tooy and tooy in the Boolean algebra where does it sit at the top so deductive consequence also think of it as less equal so anything implies top element implies or less equal top element right it's the top element after all so therefore logical axium is simple to deduce you are deducing a tooy so no problem yeah then the second one is non-logical axium nla is a non-logical axium so if P belongs to S then T is a const sequence deductive consequence of s if so basically this is a single Turn Style symbol whatever happens on the left we should affirm that whatever we assume we should affirm it you understand yeah I'm I'm trying to find out all the consequences of capital S so in particular everything in capital S is also a consequence sequence but it is not because of some logic that's why it's called non-logical axum it's because of my own assumption right so non-logical axm and third one is of course MP if we already have sequence s deduces s and s deduces s implies T then we have this so this is modus ponents and you have to use this rule on two previous lines you should have two previous lines one which says little s is a consequence and another one which says s implies T is a consequence then you can conclude that t is a consequence of capital S is this clear okay now the most important definition of proof or a formal proof yeah more precise L is a finite set of finite list maybe I should use the word list of sequence now yeah let's come to our senses properly if we are thinking about any proof do you go on and on and on you finish after a finite amount of time every single statement that you make in mathematics that either follows from the hypothesis which is a non-logical axium or something which is a logical axium it's always true it was proved elsewhere or it is always true because we have um like it's part of our Ma mathematical aums or it was deduced from two pre previous sentences we combine two previous arguments to give a new argument that's how every single mathematical proof is written of course in reality the rules of inference could change yeah we it might become more complicated our our ordinary mathematical proofs are much more complicated as I already mentioned we are studying propositional logic so this is the baby version of logic but you can understand the idea every formal proof has finite length I mean it could be 100 pages but 100 pages is still finite we cannot go on and on right whatever rules we have so for example induction we assume so we can write proof using induction but for any argument we either rely on our hypothesis or something that cannot be questioned and we deduce new things from existing things right so uh even uh let's recall canas theorem we start with some set and then we argue about that set that if this happens then that happens if this happens then that happens and then we conclude something using contradiction over there but this if and then all these things in a very crude sense they are one of these three either it's a rule of inference or it's a hypothesis or it's an axum okay so for the first time you are looking at the definition of a proof okay now just saying this is not enough I have to give you an example so let us do an example of a formal proof okay so suppose L is equal to P QR writing down formal proofs is notoriously hard in this particular Hilbert style calculus okay because you have to use your imagination how to introduce new variables yeah I'll show you with an example but proving completeness theorem is very easy with Hilbert style system that's why I have chosen this over natural deduction okay so suppose L is equal to pqr and we will show this if P implies Q and Q implies R are given then what would you like to show P implies R very good so whenever we are writing down a formal proof of this statement this sequent then it should be a finite list of sequence such that the last sequent is precisely this that is the meaning of writing a formal proof and we are going to label uh number not label number each line of the proof okay so let's write down the first line what can you say if you are given P implies q and Q implies R what can you conclude from there P imp q p p implies Q not both simultaneously yes we have to be very slow second one I'm not going to write this side I'm just going to put dto yeah I have to write a reason yeah I cannot proceed without reason so this is a non-logical axium because I assumed it I concluded it the second one is of course going to be okay what would be the third one I still cannot use anything like modus ponents because I don't have the right setup and I have already exhausted all nlas so now I have to rely on logical axioms now let me quickly take you back which logical AUM do you think could be useful here second one and tell me what are St and u p q and if I use P implies Q implies R implies P implies Q implies P implies R okay fine I'm just going to write down because she said so okay so P implies Q implies R implies well uh for for some time don't write it yeah let's experiment and then we will after finalizing we'll write it I mean this seems okay yeah because ultimately we are going to get P implies R and we will need two applications of modus ponents can you see that first application to get rid of this part and the second application to get of this part okay now this part can be gotten rid of because we already have line one but how to get rid of this part we have to use line two somehow so let me first write down this is la2 so we have to get rid uh we have to use this to obtain the first part of line three any ideas I'm going to go back here I already told you the first one is the magic one it introduces new things without any problem so what if I choose s to be Q implies R and P uh P to be t then I will get it can you see now this is something which you have to do yourself so Q implies R implies P implies Q implies R if I write this this is la1 then I'm done I mean now I can see the entire proof any questions why we chose this okay now you can start writing again so now uh now the rest of the proof is fairly straightforward I have to use uh I have to first conclude P implies Q implies R and this is by using mod ponents on previous two lines which two lines four and two two and four so we write mp24 do not write any single line without number and justification okay sixth one so once we have P implies Q implies R what can you conclude see this part is same as the first part of line three so I should use mod exponents so I should say p implies Q implies p implies R and I'm going to use MP 35 and then finally I'm going to use modus ponents again on line number one and six okay so we have concluded what we wanted and this is a proof it's a seven line proof okay those who like to solve puzzles this is the best way to solve puzzles yeah I in finding out formal proofs of statements which are obviously true it's notoriously hard believe me okay any questions about this yes less than seven lines only three lines only two lines I have no idea I mean this is the shortest proof that I can come up with so I I don't want to say anything about the length as long as the length is finite you are okay and there could be different proofs yeah there could be multiple proofs of the same statement okay now I'm going to write down some lemas yeah and those lemas will have numbers because we are going to refer to them later in the proof of completeness theorem so uh the first LMA is your tutorial ass problem okay so I'm going to write LMA 1 and it simply says this there is a proof of s implies s s implies s is that a toogy so now notice something it's a tooy so you want to derive a tooy from the given tooies because there are no nlas the left hand side is empty so no nlas only use logical axioms means only use tooies from the given set of toies to conclude other tooies so that's why this is called I mean this is also not an easy task yeah try this out before uh tomorrow tomorrow we'll see the solution anyway but try it out yourself this is a like possibil the simplest looking statement but the proof is not easy okay another thing yeah uh so finite character of proof LMA okay so what uh oh by the way I think this is a right time to talk about something some question that that's always in uh students minds but nobody answers it properly what is the difference between a theem a LMA and a proposition and a corer okay so uh if you are writing a book a paper if you are are studying for a course then arum is a statement which you should never forget it has independent value okay now this is not I'm not giving you any mathematical explanation I'm telling you how things normally work in the mathematical Community theorems are statements which you should never forget can you tell me any theorem from calculus course which you should always remember fundamental theorem of fundamental theorem of calculus yeah it's a theorem you should never forget that then roles theorem mean value theorem usually they also have some names now here we are going to write down several lemas so LMA the plural of LMA is Lata so uh I mean in practice this is the Greek plural sorry Latin in plural but we also use lemas so lemas are important steps they are key steps in the proofs of theorems but they are of independent interest uh they they use lot of notation so they are usually only of interest for writing the proof of a theorem so there are tools developed on the way so normally you call an argument a LMA you separate it out from the main proof If it is used at least twice yeah or it is of independent interest and propositions are those statements which are small results but they are independent okay so if you want to give something like suppose use and end up writing a paper then usually the important results will be called theorems while you are proving theorems you are giving some definitions and after those definitions you want to prove some consequences some simple things about the new terms you have developed those will be propositions and lemas are techniques or tools that you develop on the way in order to prove theorems corollaries are consequences yeah so if there is a statement of a theorem or a proposition or a LMA and then a simple consequence of that statement I mean simple doesn't really mean the proof is very short always it could be long but the essential ingredient is that statement the earlier statement in that proof then it is called a corer there is also some word which has been forgotten it's called a scholium s c l o uh s c h o l i u m scholium so scholium are usually consequences of proofs so basically it's a corer of the proof of the above statement yeah it doesn't follow from the statement alone it follows from the proof of the statement people generally don't use it but yeah one of my good friends and professors he he taught me about this that scholium used to be a thing in the past okay let's come back here so uh now I'm going to State this finite character of proof LMA so it says that if s is a subset of SL and T is in SL then there is a finite set s not containing uh contained inside s such that S pro T can you tell me a proof of this statement finite character of proof so capital S could be potentially infinite and if T is a consequence of capital S then actually T is a consequence of a finite subset of capital S why is that the case because the proofs are finite proofs are finite yes next statement length of a proof is finite obviously so therefore how many nlas can you use so done you only choose those elements of capital S which are used as nlas the rest of them are irrelevant right so I'm not writing a proof finite character of proof yeah I mean it only follows from a finite set of assumptions you don't need infinitely many of them okay let's do the next thing so monotonicity okay uh here we are talking about the set of consequences of a cap of a given set of propositional formulas so capital S is given okay then um there is is a bunch of consequences of capital S I'm going to use this notation yeah uh suppose s is a subset of S Prime and S Prime is a subset of SL and T is in SL if there is a proof of t from s then there is a proof of T from S Prime why is it called monotonicity yeah maybe I should explain that so in other words if these angular brackets denote the collection of all the things which can be proved from T then s subset of S Prime implies that the angular bracket of s is angular bracket of is contained inside angular bracket of S Prime this angular bracket this is called the deductive closure of s okay why deductive closure uh can you tell me what is the relationship between s and its deductive closure it's the filter generated by it's the filter generated by but s itself is contained inside deductive closure yes why loudly nla yes and n right so every single formula in capital S is a non-logical axium so you have a on line proof of that so therefore s is certainly contained inside its deductive closure and monotonicity says that if s is contained inside S Prime then deductive closure of s is also contained inside dedu closure of S Prime by the way this filter idea yeah that hasn't been shown yet you are when you say that uh this is this is precisely the filter generated by capital S you are using the logical con logical equivalence classes of s which is a totally semantic notion here we are still talking about purely syntax IC notion so once we prove completeness theorem then this thing will be same as the other monotonicity or this will be the filter generated by The Logical cons uh logical equivalence classes of formulas in capital S yeah so right now this doesn't mean anything it's simply the set of formulas which have a proof from capital s so completeness theorem will say that single Turn Style and double Turn Style are exactly the same yeah so in fact we started it here yeah LMA one is the first LMA which we need for the proof of the completeness theorem then finite character is also something very useful monotonicity which will need yeah so all these things we are going to uh write okay the uh you are supposed to write the proof of this yeah monotonicity for tutorial and I'll will give you the hint it's induction on the line number of the proof okay perhaps tomorrow also I will only say that okay now uh we will start with the proof of a next important result and that's why I'm calling it a theorem it's called deduction theorem so suppose we have already seen this semantic version of this yeah suppose s is a subset of SL s and t are elements of SL then uh there is a proof of s implies T from capital S if and only if there is a proof of T from s Union capital S single sorry capital S Union single T small s we have seen the double Turn Style version of this yeah I mean you are simply transferring this s back and forth and that is allowed but the semantic version has a very simple proof the syntactic version we have supposed to do lot of work here okay so uh I will finish proving one side today and next thing we'll do next week okay so uh we suppose we have a proof we have a proof of s implies T from capital S then I just want to increase the size of the left hand side what is the way to do that loudly no no no no not la1 just look here it's here monotonicity you want to add more hypothesis yeah so that is allowed so start with a proof and use mon monotonicity to replace the LHS of each line uh of each uh line by s Union singl tonus any problem here I'm just adding more one more hypothesis little less okay to obtain a proof of capital S Union Singleton small s proves s implies t now how do I obtain what do I want I want a proof of s Union Singleton S pro T how do I obtain it from here I have this huh modus ponents on what I don't have two statements yet we can use nla right so add two lines what is the first line S Union and then done so one side is quite simple yeah uh so this side of the proof is done now so we obtained a proof of just T from this okay the other side is what is more complicated okay so suppose I'm going to start it today s Union Singleton S pro t so uh the idea here is that now you have a proof a finite proof we are again going to use induction on the line and we are going to replace each line by finitely many lines okay we'll replace each line by finitely many other lines so that in total I will again have a finite Union of finite set of lines which means a finite proof yeah that is important I always need a finite proof but our idea would be that we don't want s Union Singleton s on the left hand side we always need just capital S on the left hand side okay so let me write down so we replace each line of the proof by uh finitely many uh lines with s in the LHS and use induction okay how many cases would there be what are the two base cases of this first thing would be there are two base cases LA and nla and then the inductive Cas is MP okay so let us do that so so base case one okay so that is La suppose line number I is the sequent every line is a sequent yeah I mean I'm uh using this then replace it with was there anything to be done here because logical axium is a consequence of anything yeah that's our um original idea so therefore there was nothing to be done uh but oh I mean uh sorry there is something to be done see what we need is this so we have to replace it with an appropriate line so let me just take two more more minutes so okay this is my la1 so TI was itself a logical axium and that was a consequence of s Union singl ton s now I'm using la1 for this and using la1 now I can conclude this mp on the above two lines so I replaced this particular sequent yeah I mean this underlined sequent by three lines I had s little s on the left hand side and I pushed it to the right hand side that's how we are going to do it with remaining base cases and inductive case okay so let us stop for [Music] [Music] today [Music]