Math 314 Computer Lab II, Spring 2011Dr. HolmesFebruary 17, 2011In this lab, we will have a brief introduction to the logic of quantifiersunder Marcel – probably just enough to give the general idea that it reallycan be done. I do hope that this will serve to reinforce the strategies forusing quantified assumptions or lemmas and proving quantified goals.It is possible that I will have done an upgrade on the prover before Fridaymorning; I have one in mind. If I do this, running the compile command inthe instructions from the first lab will get the updated version, and I willbriefly explain what the difference is.- s "(Ax1.P1(x1)) & (Ax1.P1(x1)->P2(x1)) -> (Ax1.P2(x1))";Line number 1:|-1: (Ax1.P1(x1))& (Ax1.P1(x1) -> P2(x1))-> (Ax1.P2(x1))We start a simple Marcel proof. The setup is enough to introduce ournotation. The universal quantifier is just A (and the existential quantifier isjust E). We are stuck with ASCII notation. The series of symbols P1, P2, . . .can be used as variable predicates as well as propositional letters. The seriesof symbols x1, x2, . . . are used for bound variables: if a variable is quantifiedover it is bound. We will see shortly that there is a separate series a1, a2,. . . of free variables (constants) and another series U1, U2, . . . of ”unknowns”1(expressions for which we are allowed to introduce a further specificationlater).2- r();Line number 2:1: (Ax1.P1(x1))& (Ax1.P1(x1) -> P2(x1))|-1: (Ax1.P2(x1))- l();Line number 3:1: (Ax1.P1(x1))2: (Ax1.P1(x1) -> P2(x1))|-1: (Ax1.P2(x1))These commands and what happens when they are issued should be en-tirely unsurprising. This is at the level of propositional logic. We see auniversal goal. We know that our strategy for proving a universal goal isto introduce an arbitrary object and establish the statement for that object.Let’s see what that looks like in Marcel.3- r();Line number 4:1: (Ax1.P1(x1))2: (Ax1.P1(x1) -> P2(x1))|-1: P2(a1)This is exactly what we expect. Marcel is introducing a new constanta1 and telling us to prove the formerly universally quantified goal for thespecific value a1 of the original variable x1.The only thing we can do now is try to use the universally quantifiedhypotheses. We should all be able to see how the proof goes: the idea is toget the specific cases of these universal assumptions that we need. In theprocess, we will discover one more Marcel command.4- l();Line number 5:1: P1(U2)2: (Ax1.P1(x1))3: (Ax1.P1(x1) -> P2(x1))|-1: P2(a1)Marcel introduced a new piece of notation. We get an assumption P1(U2).The notation U2 stands for an ”unknown” – here we do not know what weneed when we apply the l(); command and Marcel allows us to replace U2with a different expression. We know what we want: we would prefer U2 tobe a1.- su 2 "a1";Line number 5:1: P1(a1)2: (Ax1.P1(x1))3: (Ax1.P1(x1) -> P2(x1))|-1: P2(a1)5The mnemonic su abbreviates ”set unknown”. The argument 2 tells usthat we are setting the second unknown U2 to a more specific value. Thevalue that we want to set it to is the second argument, and the effect isexactly what we expect. Now it is clear that we want to execute the samemaneuver on the universally quantified statement in line 2. You might noticethat the quantified statement we have already acted on is still there. Thereason for this is that we might need more than one special case of a universalstatement in an argument.There is a restriction on the su command. You can only replace Un(where n is some natural number) with objects we know about when Un isfirst introduced. That means we cannot have am or Um with m > n in theexpression we use to replace Un. I didn’t have this restriction when I firstimplemented unknown variables; you can imagine my surprise the first timeI proved a false theorem. . .- gl 3;Line number 5:1: (Ax1.P1(x1) -> P2(x1))2: P1(a1)3: (Ax1.P1(x1))|-1: P2(a1)- l();Line number 6:61: P1(U2) -> P2(U2)2: (Ax1.P1(x1) -> P2(x1))3: P1(a1)4: (Ax1.P1(x1))|-1: P2(a1)- su 2 "a1";Line number 6:1: P1(a1) -> P2(a1)2: (Ax1.P1(x1) -> P2(x1))3: P1(a1)4: (Ax1.P1(x1))|-1: P2(a1)Now we are back to the level of propositional logic: we can see that theconclusion follows by modus ponens from lines 1 and 3, and we know how toconvince Marcel of this.7- l();Line number 7:1: (Ax1.P1(x1) -> P2(x1))2: P1(a1)3: (Ax1.P1(x1))|-1: P1(a1)2: P2(a1)- gl 2; Done();Line number 7:1: P1(a1)2: (Ax1.P1(x1))3: (Ax1.P1(x1) -> P2(x1))|-1: P1(a1)2: P2(a1)8-Line number 8:1: P2(a1)2: (Ax1.P1(x1) -> P2(x1))3: P1(a1)4: (Ax1.P1(x1))|-1: P2(a1)- Done();Q. E. D.That completes our first proof with quantifiers. I haven’t done anythingwith the existential quantifier; this won’t require any new commands, but onehas to notice that what happens with the existential quantifier is in a sensethe reverse of what happens with the universal quantifier. An existentialassumption, like a universal goal, allows the introduction of a new constant (awitness). To prove an existential goal, we introduce a goal with an unknownreplacing the quantified variable: we have to decide later what the unknownis.The existential result we will prove is even more trivial than the precedingresult, and just serves to illustrate these points. We will however have aproblem (at least the way I choose to do it) which illustrates an importantpoint.9- s "(Ex1.P1(x1) & P2(x1)) -> (Ex1.P1(x1))";Line number 1:|-1: (Ex1.P1(x1) & P2(x1))-> (Ex1.P1(x1))- r();Line number 2:1: (Ex1.P1(x1) & P2(x1))|-1: (Ex1.P1(x1))This is obvious propositional logic work. Now we try to prove the con-clusion.- r();Line number 3:1: (Ex1.P1(x1) & P2(x1))2: ~(Ex1.P1(x1))|-1: P1(U1)10This should be what you expect. The negation of the original conclusionappearing as a hypothesis might be surprising. It’s actually there so that youcan introduce a new witness to the existential conclusion if you accidentallypick the wrong one or if you need to use different witnesses in different cases.We will see how it can be used to correct a mistake in proof strategy below!In any case remember that when proving C it is actually always safe to assume∼ C (changing your argument into a proof by contradiction).It’s obvious what the value of the unknown should be: it should be thewitness to the existential hypothesis! We use the l() command to introducethat witness. . .- l();Line number 4:1: P1(a2) & P2(a2)2: ~(Ex1.P1(x1))|-1: P1(U1)- l();Line number 5:1: P1(a2)2: P2(a2)3: ~(Ex1.P1(x1))|-1: P1(U1)11- su 1 "a2";Circularity error<hit enter>Line number 5:1: P1(a2)2: P2(a2)3: