Lecture 29

[Music] okay so look at this deduction theorem DT you can use it as a derived rule of inference modus ponents is one rule of inference yeah that was the only one rule and that was an original rule this one I'm saying you can use it as a derived rule of inference and make proofs shorter we are going to soon see an example yeah how to use DT as a derived rule of inference okay let me just add we will freely use DT in formal proofs as a derived rule of inference so a justification for a line a reason for a line can be DT Where We Are simply transferring something from left to right or right to left however okay do not use it for proving little s implies little s if you use DT there then what does it say little s proves little s which is nla we used that proof in the proof of DT so please don't do that don't convert LMA 1 into an obvious statement understood okay fine so now uh if you remember by this point in the semantic part we had defined valuation and we have also proven an analog of DT for semantic Turn Style yeah double Turn Style and at that time we decided to define a theory what was the theory the long weekend has wiped your memory what is a theory a satisfiable set a satisfiable set okay now that is a semantic concept satisfiability is a semantic concept what is its syntactic analog yeah that is called consistent so now we are going to Define what is a consistent Theory so definition but this this particular definition is negative yeah what is the meaning of a negative definition we do not Define what is consistent we Define what is inconsistent and whenever it is not inconsistent then we say it is consistent okay so let us look at the definition now so say that a subset of SL is inconsistent if for any T in SL we have a deduction of T from capital s so you can prove anything from capital s that is inconsistent so in particular you can prove one formula and its negation simultaneously yeah we say say to people yeah that oh your speech is incoherent you are not making sense that is an inconsistent Theory so say that s is consistent if it is not inconsistent i e there is T in SL such that there is no proof of t from s there is no deduction of T from s okay so uh I mean we would like to know some examples of DT of of a of an inconsistent Theory or a consistent Theory can you give me one example of an inconsistent Theory p and negation p and negation P yeah where p is a propositional variable or in general s and negation s where s is any formula because I mean in the filter language s and negation s by conjunction they generate Z zero the contradiction and from contradiction you can prove anything that's the idea so we are going to Simply do that yeah so we will prove we now show that s negation s is inconsistent okay how can we do that let us start we uh so let T be in SL so what do we want to show s comma negation s proves t t is arbitrary yeah t doesn't depend on S so we want to prove that so we are going to start with this the first line I will write what can I prove from this first from s and neg s s s okay good this is nla second line okay what else can I prove from this s meet s me negation is we don't use the word meet here do you mean conjunction but conjunction is not part of our set of connectives right now what are we using negation and implication huh so we can only use I mean from these two you obviously cannot apply any MP yeah you have to add something more what should you add s imp negation s implies s s implies negation s implies s and then you'll end up proving s by using MP twice not really helpful you have to introduce something so I'm just going to write this I'm going to make it a bit more complicated first this one is allowed yes so what is the reason okay good fourth one now what can I conclude negation T implies negation s and uh what is the reason for that MP 2 3 okay now contos contraposition law of contra position so s implies negation s so negation T implies negation s implies s implies T this is La 4 and after that I can use MP okay and then I will conclude s implies T by using MP 45 and and finally I can conclude T by using mp1 6 okay so we indeed proved any T from s and negation is just a re uh rewrite of this is LMA 2 okay so without any left hand side I can prove that s implies negation s implies T how do you do that how do you prove LMA 2 from this look at the first line 2 * d 2 * DT okay so I gave you a problem of uh I gave you a solution of the tutorial problem this is LMA 2 and here is a proof and I can also give you a proof of LMA 3 yes in both these cases use DT twice it just depends on in which order you are pulling terms in did anybody try to solve this problem LMA 2 and LMA 3 okay so I have spoiled it for you okay uh then they are other lemas which I mean they will be used later so let me just write them here so LMA 4 is also useful so that is s implies negation s implies negation s that is LMA 4 I'm not going to tell you any proofs at this point because they are tutorial problems so you should at least have some fun so LMA 5 this is called double negation introduction yeah s implies double negation s and finally there is LMA 6 okay and it says that s implies negation T implies negation s implies T okay these are the three statements where you can have fun trying to prove these things until Friday right so these are the statements we are going to use however we are not done with the concept of consistency yet we still need various different Notions uh various different results to conclude consistency or inconsistency or its characterizations so so far we have proven LMA 1 2 and 3 four five and six are exercises for now and now there will be three more 7 8 and n and they will be related to the notion of consistency so let's write that so LMA 7 okay LMA 7 says that given as subset of SL s is inconsistent if and only if for some little s in SL s proves negation of s implies s is this intuitive s implies s is a tooy and negation of s implies s is a contradiction so what we have saying is a set is inconsistent if and only if it proves a specific type of contradiction I mean it should be any contradiction really but in this proof we are only going to do one part okay any ideas on how to do this s already proves as simp so if s is is inconsistent yes if s is inconsistent then s proves t for any T so in particular s proves negation little s implies little s Okay so so one side is obvious what about the other side other implication that suppose you have a proof of a contradiction from capital S how do you show that you can imply anything no you can prove s simp as s also like because you can prove it from anything so how can you prove s simp as S I mean I want to a proof of s impli t for n no yeah like we have negation s s and s s we can use the previous and oh uh negation as simplies and as simplies and then you can prove any claim yeah but then you have to use a cut rule okay so capital S proves this capital s proves this and then you still need to obtain that capital S proves any consequence of this that is called a cut rule yeah so let's not go there we want to directly conclude something but now that we are on this page do you think any LMA would be able to help us okay let's uh do it in a nonlinear fashion sorry that was unnecessary actually let's do it in a slightly nonlinear fashion so s proves negation s implies s is given yeah don't write anything for now yeah this is hypothesis and we would like yeah want what do we want that s proves T okay then perhaps to trace back one step maybe we used reasoning MP here yeah most like we used MP this is not nla this is not La so we used MP so on which one did we use MP we only know two things so perhaps the previous sentence was this okay how do we and then the reason was mp on an on appropriate lines so enough to obtain this well this really doesn't sound useful I mean this doesn't look useful right now but what if we use its Contra positive yeah perhaps we can use something which is useful so at some point if we just have the Contra positive which is negation T implies double negation of s implies s then by using negation T implies double negation s implies s implies negation s implies s proves T implies T so this would be la4 and then this would be appropriate MP okay now we are getting closer how do we obtain something like this well this gives us the vibe of because T is arbitrary it gives us the vibe of la1 all right so if we have la1 then we just need this double negation s implies s implies negation T implies double negation s implies s this is la1 and then this is MP oh this is MP provided we have somewhere double negation s implies s yeah if we have this double negation as simplies then using these two things I can conclude this um sorry using these two I can conclude this yeah now how do I obtain this double negation as simple as this so because of some technical glitch we couldn't really save this part of the proof so let me share so here is the completed proof of LMA 7 the backward implication so let us try to look at this step three yeah I mean this step three we we had finished uh step four I mean we we had reached until this point that double negation s implies s we will need yeah we are doing this proof backwards well how do you obtain that we know double negation elimination is one of the logical axioms but here we don't need that we need its Converse double negation introduction which is precisely LMA 5 so LMA 5 and because you want capital S to be on the left hand side you would like it to have monotonicity as well so LMA 5 and monotonicity you get this s implies s implies double negation s implies S as the right hand side of the third line of the proof and already s implies s which is the left left hand side of the implication is our LMA 1 as well as use monotonicity because he wanted to increase the left hand side and uh the first line is the hypothesis that negation is simpli as s is true so do you understand all these things now so we have completed the proof of LMA 7 and this is a really good example of how a proof can be written backwards writing a formal proof as we have said on multiple occasions is a difficult process so we can perhaps start from the backward uh like from the last line and then work our way backwards as well as some way forward and then eventually we reach the point that we wanted okay so now let us look at this LMA 8 so our list of lemas is not yet complete in Lama 7 we just saw that a test for inconsistency now this is another test for inconsistency but notice that there is a slight difference here the slight difference comes from that we are not talking about the inconsistency or consistency of a given set but but we are talking about whether we can add a single extra formula to this particular set and then decide its inconsistency so let us look at what is written so suppose capital S is a subset of SL which means it is a set of formulas propositional formulas and little s is a single propositional formula so now s Union single t s is incon consistant if and only if negation s can be proven from capital S okay see here like the there is a usual chance of confusion that what if capital S itself is inconsistent well capital S is inconsistent means by monotonicity capital S Union Singleton small s is also inconsistent so capital S can prove anything so both sides are anywh true yeah so that's not really the question here we are trying to test the boundaries of a consistent set so usually whenever we we use this result we are interested in the case when capital S is consistent but adding a new element that will explode that will result in explosion yeah like it will become inconsistent the forward proof is quite simple if s Union single s is inconsistent then you can prove anything from it yeah so that's the that's the definition of inconsistency that s proves t for any T so that t happens to be negation s so that's our first line it's it's by inconsistency then by using DT we can transfer this little s to the right hand side of the Turn Style operator now this is a perfect setup for LMA 5 so use LMA 5 plus monotonicity because our left hand side is nonempty to get that capital S proves that s implies negation s implies negation s and then a simple application of MP will give you the necessary result okay so very uh Sleek use of the deduction theorem as a derived rule of consequence okay so for the next one suppose we are given that negation s is a logical con is a proof theerotic consequence of capital S it can be deduced it's a deductive consequence of capital S then s Union Singleton s like Singleton small s has got l s as well as negation S as uh deductive consequences one thanks to nla whereas the second one thanks to the hypothesis as well as monotonicity now we want to prove that capital S is inconsistent which means given any formula T we should be able to prove Little T from capital S and how do we introduce this unknown thing well our usual idea is uh la1 but we don't want to do la1 here yeah s impli t impli s is not what we are going to do we are in fact going to use the inconsistency part like we have shown you remember that we have shown that little s comma negation s this Two element set is inconsistent and using that we proved that uh Prov LMA 2 by applying deduction theorem twice so LMA 2 and monotonicity will give us line number three okay so s implies negation s implies T is a logical is a deductive consequence of s un single gen and then you simply apply mod exponents twice and you get the result okay so whenever you have both small s and negation s then the process is really easy there is now these uh if you uh understand LMA 7 is a proof uh is a is a test for inconsistency of a given set of formulas this is also a test of inconsistency for S Union single gen s but now we like so therefore both of them are necessary as well as sufficient conditions in the next LMA however we are going to obtain a sufficient condition so if there is a set from which we can prove Little T as well as negation T then s is inconsistent the proof is not very different from what we just saw but it is just a test of it's a just a sufficiency test okay and we are going to use all of these proofs later yeah so you you have t and negation t as hypothesis and I just changed the letter here like you start with U as your new formula and then you would like to prove s proves U again use LMA 2 and monotonicity and mod exponents that gives you the complete proof now after a small break we will return for uh looking at the proof of the soundness theorem important result in prepositional logic is the completeness theorem it's G's completeness theorem although GLE proved it for predicate logic first prepositional logic as I already told you it's a baby version of what can be done here we are going to gather ideas and then we will generalize them to the appropriate context so completeness theorem is the connection between sing single Turn Style and double Turn Style it says that they are exactly the same it is also connection between satisfiability and consistency it will say they are the same and when you say there are they are same actually there are two things one thing is that single Turn Style syta syntactic thing will imply the semantic thing and conversely one of them whenever there are two things to prove yeah usually it is the case that one is obvious or much more simpler than the other so the simpler part of this is the syntactic deduction implies semantic consequence this part is called soundness theorem have you heard the phrase sound sleep yeah sound sleep yeah I mean I'm peaceful I'm not bothered by anything so the simplest thing to expect because see this Hilbert style deduction system we introduced those four logical axium schema then we came up with modus ponents and we would like to verify that we are sound people we are we haven't gone insane right so in order to check that we must prove that whatever our understanding is whatever our semantics is that semantics does indeed follow from our syntax okay so we are going to first prove the easy part which is the soundness theorem and then we come the completeness theorem which is the converse Now by this time I have talked about these things so many times that the statement of soundness theorem is also not a surprise so suppose s is a subset of SL and T is a particular formula if there is a proof of T from capital s then T is a logical consequence this is soundness yeah single Turn Style implies double Turn Style okay what do we need to show here what do we need to show [Music] here Whenever there is a valuation V that makes capital S true then there the same valuation will also make small T true so assume that there is a proof of T from s and that V is a valuation such that it is a model of s so V is a mod uh V is something that witnesses that capital S is satisfiable which means V of capital S is true just to recall things so V of capital S is true means V of Lal s is true for all small s in capital S okay now we have a proof of T from capital s what should be our way of proving this we have a formal proof and where will this line be S proves T this sequent will lie at the end so we have to use are there any other ways of proving anything induction on line number okay we will show by induction on line number that if V of LHS is true oh I mean line number of a proof of t uh of s implies t s s d is T if V of LHS is true then V of rhs is true okay tell me what is base case one La yeah so uh line I is uh s through TI L then if there is a valuation V I mean that that particular valuation V that makes the left hand side true there is no cause cause and effect here TI is a logical axium so TI is a toy so V of T is true no cause and effect yeah since TI is La it is a toogy that's why that exercise verify that all logical aums are tooies it is a tooy and hence V of TI is true done so base case 2 line I is s proti nla since TI belongs to S and V of capital S is true V of TI is also true done because it belongs to capital S and V makes everything in capital S true inductive case line I is S pro TI MP and well I'm going to use a different notation JK for a change so J and K are smaller right so by induction hypothesis if uh line J is s proves TJ and line K is S pro uh TJ implies TI then V of TJ is true yeah because they were previous lines so we have already concluded something about their right hand sides so by induction hypothesis we of TJ uh is true and V of TJ implies TI is true okay if V of TJ is true and TJ implies TI is true what can you conclude about TI by the definition of valuation for implication yeah by the definition of valuation for implication V of TI is also true so we proved the inductive case now what is the last line of this this whole proof since S pro T is the last sequent in the proof or last line in the proof by induction we are done I mean it looks like a long proof but there is seriously nothing in it soundness is the easy part of the completeness theorem [Music] [Music] [Music]