Models & Soundness in Predicate Logic: Proof-Theoretic Verifcation

[00:00:00]in the last video I introduced proofs for predicate logic in this video we're going to look at models which are another way of analyzing arguments there are two great traditions in logic when it comes to asking what makes the argument from premises to conclusion good we've already seen one answer to this question the first option is to say that there is a proof which gets you from those premises to the conclusion but there's another option which says that an argument is good when there's no counter example to the argument when there's no way to make all of the premises true and the conclusion not be true we're going to have a look at one way of making this second option precise we're going to introduce a way of representing these ways to make things true in a very simple notion called a model we're going to introduce models to the language of predicate logic the key idea with the model is that it gives us all and only the information that we need to figure out whether or not a sentence in the language of predicate logic is true now if you think about the sentences in the language of predicate logic they're made out of predicates and terms and then they're combined using the connectives and the quantifiers the terms these are the things which represent objects and the predicates talk about the properties or relations that are that these objects might have so what we'll need to interpret the language to figure out whether or not a sentence is true is something to interpret the objects something to figure out what the objects represent and then what properties they might have so our models will involve a domain a domain is a collection of objects what kind of objects it doesn't matter we're not gonna say anything put any restrictions on what kind of objects how large the collection might be how small the collection might be all we need is some collection of objects for our names to name for our variables to range over then for each predicate in the language we need to interpret it and for each name in the language we need to interpret that what does that mean well for a name we need an object in the domain for the name to name and for a predicate we need a rule which provides a truth value for every appropriate number of things from the domain so for example if we have a one place predicate we need a truth value for every single object in the domain but if I have a two-place predicate I need a truth value for every pair of objects in the domain that's a 2-tuple if I had a three place predicate I'd need a truth value for every triple of objects in the drama and as I said if I have a name in my language I need to interpret that by selecting an object for that name tonight and I'll just bundle that stuff together and that is a model a model is a domain and an interpretation so let's take a look at an example let's select something where I've got a domain with three objects which I'll just call a B and C in a model like this on one place predicates can be interpreted just by a table that assigns a truth value for each object and a two-place predicate can be interpreted by a table assigning values for each pair of objects yes so my language contains a one place predicate F in this case I've represented what it is for F to be true in my model of the object I that's what this one here means against the a row and it's false of the object B and it's true of the object C so we can tell everything that we need to know about the predicate F in this domain so if we're only considering three objects a B and C then we know everything that F needs to tell us it's true of a and C and it's false of P and if L is a to place predicate we can do the same thing in this square table here which we read like this if I want to figure out whether L I I is true I see this value in the table and I see it because there's a one there well III it's true and L I'd B is false and l IC is true and L di as false and LB B is true and it will be C as false etc so here L is this to place predicate which describes a relation which holds of some pairs of things and files of others now given this definition I can figure out whether or not a sentence is pro using these rules I have a predicate earth which is an N place predicate applied to the terms a 1 up to a n this is true according to the model just when my interpretation of the predicate assigns the value true to whatever the term a 1 names that I made 2 names etc and the term a and so I just look up whatever the terms name and then I look in the value of the the interpretation of the predicate to see whether I've got a 1 or a 0 in that relevant slot of the table 1 true 0 false then a negation is true in my model just when the thing the gated is not true a conjunction is true just when both conjuncts a disjunction is true just when one or other may be both of the disjunctive through conditional is true just when the antecedent isn't true or the consequent is so the only way to make a conditional false is to make the antecedent true and the consequent that's a universally quantified sentence is true if and only if each instance is true where the name a is the standard name existentially quantified sentence is true if and only if some instance is true for some standard now no what's a standard a they're just our way of making sure that we've got a name for every object in a model so if I have a particular model that I'm wanting to reason about the standard names for that model are just selected so that each object in the model has got one and only one standard name and the interpretation of the name is going to be the particular object that that name picks out so it's just a collection where we use usually the same letters that we use in specifying that I made if I listed that I made out we'll just add to our language those letters as names for the objects in the dump in this way the crucifer universally quantified or an existentially quantified formula can be defined in terms of the truth of other formulas just the instances of the qualified formula where I plug in each of the standard names now in general languages aren't like this we don't have a name for every object in the universe we don't have a name for every object in our domain that I might have chosen but introducing standard names is just a very helpful shorthand for reasoning about whether or not a formula is true in a model so let's see how this works here I have my domain again my domain is just objects a B and C and I'm interested in the truth values of these three formulas that I have here for every XFX there is an X such that L X X and for every X there is a y L X Y and a Y X we'll start with for every X FX this formula is true if it's instances FIF Bay and FC are all true and we'll see here that fi is true so this gets a tick and FC is true so that gets a tick but f b is not true so that one isn't so we can say that for every X FX is false in our model or I might say it's negation is true so we'll say for every X FX is false in this model let's have a look at the next one there is an X such that LX x this is going to be true if one of these instances is true now III I'll be bait or LCC and if I look at this table here I'll say that Li is true I'll be B is true that LCC is not so this one isn't true this is and this one is so there is an x FX l XX is true since two of its instances are true now this last formula is a bit more complicated it's got two qualifiers so we'll take it quite slowly this formula is starts with a universal quantifier so we always do that bit first the universal quantifier in this case free that formula to be true each of its instances needs to be true so one instance is the I instance one instance is the B instance and one instance is the C instance we'll take them in turn I need there is a Y such that L iy + y I is struggling we just plugged in I for the variable X that was bound by the quantifier similarly the B instance is there is a Y such that lb y and ly B and the C instances there is a y LC y and Y C so there the three instances we need each of these to be true for my formula to be true now let's look at the first one this is an existentially quantified sentence and that also got three instances the first is Li I and I that's taking the value I for Y the second is Li B and I'll be a and the third is Li si and I'll see I remember existentially quantified formula for it to be true some instance has to be true and the instances are just found by substituting each of the standard names in so this even includes the case where the name a is used for both the variable X and the variable Y no ban on that that's good because this instance is true well III and Li is true because we've got this one here in the table so this is true so this one is true the I instance of the universal quantifier is true and similarly here we can say that el bebé is true so in particular the be instance of the the existential quantifier instance is true so I've get el bebé and el baby that's an instance of this one I don't even need to check the other Trobe because I know that's true but we can't do the same thing for C because LCC and LCC is not true so let's check the other instances and see whether we'll be all right here LC I and L I see is one I'll see thee and BC is a next and LCC and LCC we already know that one's false well I'll see I is true that's this slot LC I and L I see is true that's that slot so LC i-- and Lacs true so this a instance of our existentially quantified sentence use the highlighter this I instance is true because the I instance of that is true this be instance of the University one sentence is true because it's be instance is true and this see instance of the university quantified sentence is true because it's a instance is true and because each of these instances of the universally quantified statement is true the whole universally quantified statement is true so indeed this gets today so each of these sentences turns out to be true in our model no standard names are really handy when it comes to modeling quantifiers and it's the technique that we're going to use in this subject because it's very quick and easy but as I said these aren't the only way to deal with caught fires and be really bad if it was because there's no way we could use standard names in English because all of our natural languages don't have names for every object over which the language qualifies you know there's uncountably many different numbers and there's no way that we have names for each of them for example alfred tarski they're really important logician from the 20th century gave us an alternate way of dealing with quantifiers and if you've done logical methods in second year we've actually seen this well we can do some more work in defining what it is for things to be true in a model not just in terms of the truth values of their components but in terms of a relation of satisfaction where we say that for all X F X is and for some X F X in our model is to be analyzed in terms of the component F X without using names just using the variable X but we don't need to know whether F X is true but we need to know where there FX is true of this or whether it's true of that or whether it's true of each individual different object in the domain and that depends on the values of the variable extracts and the way that ASCII analyzed this was in terms of what he called assignments of values variables so in general a formula which might contain free variables is said to be sad as by the mortal relative to some assignment of values to those variables we won't go through the details of that but it's another way of giving truth value to formulas in terms of this relationship of satisfactory no in the first videos we had a look at proofs and proofs are one answer to the question what makes an argument from premises to conclusion good we can say that the argument is provable if there's a proof which leads us from the premises conclusion but now that we've got models we could say this we could say that the argument has got no counter example that there is no model or each member of the premises is true and the conclusion is not so we introduced these two similar but different notations for validity of arguments here here we've got proof ability and here we've got the absence of a counter example there Whitney with turnstiles but one is a single headed and the other is a double headed turnstile to give you a sense of how models theoretic validity this double headed turnstile works let's show for example that the argument from the premises something's F and something's J to the conclusion something is supposed F and J let's show that that does have a counter example so it's invalid so for this if I'm going to construct a model I need to interpret F and I need to interpret J and if I had a counter example to this I need some object in my domain for which F was true because I need some instance for this formula to be true I need some instance of the predicate F to be true so let's just call that object I and I need some instance of G to be true but what I really don't want is F ng to be true for anything so let's make F true of the object I bet she'd not be true of that object and if be false in the object babe G be true of the object babe and maybe I've got other objects like C and D for which they pass false doesn't really matter but here I've just constructed an interpretation where my names are a b c and d standard names for the objects a b c and d in the domain and I've interpreted efforts being true of I only I've interpreted genius been true of B only and now in this model there is an x FX is definitely true because fi is true and there is an X J axis true because GB is true but there is an X FX and GX is going to be false why because f ing I and F PNG bei are false Fi and GI is false because G is false and FB mg B is false because FB is false and FC and J say and F J and J they are also false for the same reason so we've constructed here a very simple counter example to this argument showing you that this argument is invalid it's got a counter example so now there are two different sorts of things that we can make what we've got for proofs if I can construct a proof from premises to a conclusion I know that the argument is good in the sense that it's provable and if I can construct a counter example to an argument a way of making the premises true and the conclusion false but I know the arguments bad it's got a counter example so if I think of the sort of field of arguments is sort of all represented out here in this you know great odd rectangle here it might be that I could see all of these little provable arguments over here you know this is provable that's possible that's provable and maybe over here I've got arguments which I've got a counter example this arguments got a counter example that arguments got a counter example that arguments gonna count for example now a question might be is every argument either provable or have a counter example and another question might be is there any argument that I can find a proof for and a counter example hmm that's two different questions one is is there a gap between they provable side and the counter example side are there any gaps between prove ability and having a counter example and the other is is there an overlap between prove ability and counter example is there some weird arguments where it's both provable and has a counter example that's the question that we're going to address in the rest of this video and also in the next one we're going to see that there's no gaps and there's no overlaps here the fact that there is no overlaps between proofs and counter examples is what's called a soundless theorem one way of describing what the soundness theorem says is is here in this very succinct claim it says that yes we've got a proof from X to a then there is no counter example the argument from X tie has got no counter example that's what's called the soundness theorem so if there is a proof from X Y then the argument doesn't have a counter example and then the converse is the completeness theorem which says that if we don't have a counter example of the argument then there is a proof from the premises to conclusion so if we don't have a counter example then there is a proof that's out there which could be found now these are two very interesting facts and we're going to explain why they're true or show that they are true we're actually going to prove these facts now there are very different facts because they give us different things to work with the soundness theorem tells us that if we have a proof from the premises to the conclusion then there is no counter example to be had and if we go to reason with this that's not going to be too hard to show because we've got a proof to work with we say that if there is this proof then we're going to show that there is no counter examples of itself you've got an argument and there is approach then we can just sort of verify that there's not a counter example made by checking the proof bit-by-bit completeness is the hard one because this says that if we've got an argument and there is no counter example to it then there must be a proof from the premises to the conclusion and that is quite another thing to prove so we're going to leave that for next time and in the rest of this video we'll explain why this soundness fact holds now the key thing which is going to enable us to verify soundness is this feature about proofs that we precisely defined what a proof is we did that in the previous section when we said is what it prefers it's made up from basic you know assumptions just by means of these rules this means that we can reason about them because we've precisely defined what they are and we can do what's called a proof by induction an inductive proof is consists of a base case where we want to show some property holds of things which we'll just call widgets for the moment we first show that it holds to the basic the atomic widgets the widgets which are the starting point of building new widgets these are the basic most fundamental ones then we show that this property if it holds of some widgets that I've got then it holds of any widgets I can make up out of those ones that I've already got so it turns out that any widget that I could build up from the atomic widgets by means of whatever the process of making widgets is has always got this property because the property holds in the base things and then if I build something up it holds of those two and if I build something from those at haunts of those two and if I keep on building new widgets the property is just kind of following along its kind of work this kind of proof works for many different sorts of widgets natural numbers for example I could think of them as starting from zero and continuing on just by adding one because I want to show that something holds of some all of the natural numbers have got some property if I then show that zero has that property and if a number has the property so does the next one then turns out all the natural numbers have got their property because that's just how the natural numbers made or define do the same thing for formulas if the atomic formulas have got some property and if a formulas got the property then the formulas conjunctions disjunctions negations conditional quantifiers etc I've got that property too then it turns out that all formulas have got that properly and this works for proofs as well because proofs are made out of our basic proofs which are just a single assumption and then builds up from proofs by means of the rules and it turns out there's lots of these things which are recursively constructed like that and this proof technique I will see again and again so to see how it works with proofs the smallest proof is just a single assumption single formula written down it's the premise it's the conclusion that's it and then each of the rules gives us ways to extend a proof for to prove source free proofs in the case of the disjunction elimination wall to make a new proof and every bit of proof is built up in this way in a finite number of steps that's just what it takes to be a proof it's a fight on tree made up out of these raw so to prove soundness we're going to use this sort of inductive argument sound this is the fact that if I've got a proof from X to I then I've got a no counter example to the argument from X time so we'll reason like this if pi is a proof from X to I then there is no counter example the base case is there soundness fact when PI is an assumption proof and then the inductive step is that if Selma's holds already for proof spy one and maybe PI 2 and PI 3 then it also holds for proofs constructed from these ones using the rules and then if I can show those two things the base case in the inductive step soundness holds for all of my props so is the base case if I is an assumption proof well it's a proof for the argument from eye to eye so we need to show that the argument from a to a doesn't have a counter example but a counter example to that argument would have to be a model where AI is true and I isn't and that's not how model what models work in every model either a is true or it isn't but not both so we never have a counter example to the argument from eye to eye so we have soundness for assumption proofs now there's lots of rules and I'm not going to explain how soundness works for each of them we'll do that in class I'm picking out four walls which will give you a good idea of how all of the rules work first look at the conjunction introduction law if my proof from x2i has no counter example and my proof from y2b has no counter example then any model where x and y are both true has got to be a model where AI is true because the argument from x die doesn't have a counter example and it has got to be a model where B is true because the argument from Y to be doesn't have a counter example so any model where x and y are true a and b has to be true too and if I and B are both true in my model given the rule for how injunction works I Andy it's true my model too so it follows that any model where x and y are true i and b is true so this is the simplest case it turns out that if my if i have no counter example to the argument from x to a and no counter example to the argument from y to be then indeed the argument from x and y to InP got no counterexample now many of the other rules have got this shape - these are rules which don't discharge premises don't have any funny business it's qualifiers all of those rules give you soundness in exactly the same way as this one here's a rule that discharges a premise though here my proof pie is a proof from X and I to be and I'm discharging some eyes and concluding I implies pay so if my pie is shows us that there is no counter example to the argument from xn A to B then in any model where each member of X is true and is true and B is true that's just what that means for that argument to have no counter example now that means if I've got a model where X is true and I'm leaving out then either a isn't true in my model or a is true in my model and in that case B is true in other words in those models either a isn't true or B is true if all of the things in etc but that's just the condition for a implies B to be true if you look back at the rules for when I implies being is true at a model it says when a isn't true or B is so it turns out that in a tables where X is true a implies B is true - and that's exactly what we needed because that's now the active assumptions in this proof for X discharge the eyes and now the conclusion is a implies B so sadness works for extending proofs with the conditional introduction Walter last connective rule that I look at is the disjunction in a disjunction elimination rule which is the most complicated one it's got three sub proofs by one PI 2 pi 3 if each of these proofs I've got no counter examples that means that in all the models where X is true I or B is true in all the models where Y in a are true C is true and if all the models where Zed and B is true C is true what we want is to show that in every model where and why Zedd are all true then see estra so tight the models where x y&z our trunk because X's are true I all be as straight and since I or B is true in these models if I take any of these models in that model either is true or B is true so in one case if it's a that's true then since Y is true and we're assuming a is true then C is got to be true too because the asar Givens got no counter example on the other hand if it's be in that disjunction that's true and then in that case because there destroy certain be a true so in that case C is true too so in either of those cases C is true so it turns out and sees true in my model whenever X and wines that are all true then C is true so that argument is valid to last thing I look at is this Universal quantifier introduction role I've got a proof from X to eye with the I instance that means that in any model where X is true I have a in strap and the name I doesn't apply up here in any formula in X that's the condition on actually being able to apply the universal quantifier introduction ball so it follows that in any model the domaine de interpretación i where each member of X is true so is I I so what I'm gonna do because I want to prove that for all X I of X is true we're gonna choose an object be in the domain day and I'm going to consider this new model where I just interpret the name I to refer to the object day instead of the name I so I've just chosen an object in the domain at random and I'm interpreting the name I to refer to that and I'm keeping everything else in the model exactly this now since the formulas ex don't feature the name I their interpretation is completely unchanged they're still true in this new model so since in every model where all the XS @ 4i is true the name I I am the formula III is truly miss model - because the argument from extra III is valid so this model can't be a counter example but either that they could have been any of the objects in the domain in our model and B is now in this new model the interpretation of the name right so that means that I of B holds in my original model for whatever standard name date I was wanting to use so it turns out that for every X I X is true in my model taupe because the B instance is true for any choice B that I used born so it turns out that if the formulas in exit row the universal in qualified formula is true - that was a lot of examples four of them and they were all of the different kinds of reasoning that you can get in these sorts of rules the other rules work in exactly the same way they're just gone slightly different shape but the reasoning works in exactly the same way so I'm going to leave them for us to do in class after we've mastered models and we've understood Sammis next step on our journey is to see how to prove completeness but that will be for the next class