can you help me with these questions?
math Jeff Edmonds York University Assignment 4 MATH1090 Informal and Formal Proofs 1.110 1.210 1.310 2.110 2.2a20 2.2b20 2.3a10 2.3b10 100 1 I really like this proof system If these are ALL true. Then at least ONE of these is true. Each line of the proof is a “sequent”: α1 ... αk β1 ... βl Each clause is a 1st order formula. Toniann Pitassi Q1 Sequent Calculus The following is called the cut rule. From γ(αβ) and (γα)β, conclude γβ. Note that α is cut out. Every valid statement can be proved without this rule, but Toni for her PhD proves the size of the proof without it might be exponentially bigger. 2 Q1 Sequent Calculus Prove or give a falsifying model 1. From γ(αβ) and (γα)β, conclude γβ. 2. ("w [α(w) iff β(w)]) ⌐$x [α(x)⌐β(x)] 3. (("w [α(w) iff β(w)]) ($x [α(x)⌐β(x)])) ["y β(y)] Q2 Ooops, since teaching you the game via parsing I changed my coloring system (which helps with the understanding) Then I changed the parsing AGAIN! Then I realized that I have not really covered syntax and parsing quite enough. Then in a 2am panic, I realized that though my method works for the problem at hand, another method is sometimes needed. My goto solution is to make more slides. Ooops. What I put on tests tends to be what excites me. This tends to be what is on the edge of my own understanding. Sometimes this make the problems too hard for students. Sorry. To compensate, give hints. 4 Assume that the parts in orange are indivisible “facts”. Change from orange to yellow, those facts that are assumed by some oracle. Change from orange to blue, those facts that the prover needs prove. Give a screen shot of a page of my slides that say you can rearrange the above statement into [yellow things blue things ] Argue in words (or even one word) the validity of this rearrange statement. Q2 [AB] ( [BC][AC] ) 5 Proving LHS of Oracle’s Consider the part circled in blue. It is talking about the case in which the oracle’s subtree contains LHSRHS. The oracle assures us all that if the prover can prove the LHS, then she will assure him of the RHS. Hint: The following example is one in which the prover has to work a bit to prove this LHS. Q2 6 Q2 2a. ("w [α(w)β(w)]) ( [("y β(y))("z γ(z))][("x α(x))("z γ(z))]) Hint: This statement is valid as its structure is similar to the last one and the " are distributed within/without the in a way that does not cause problems. Give its full parse tree (ie also parse within the oracle’s subtree) Color (model, oracle, prover, adversary) each statement according to who assures/proves it each free variable according to who provides it Prove the statement is valid by following the oracle, prover, adversary game. Hint: In the prover’s first attempt, he focuses on his own needs and fails. He quickly realizes that he must satisfy the needs of his highest maintenance oracle first. 7 Give a formal proof. Q2 2b. ("w [α(w)β(w)]) ( [("y β(y))("z γ(z))][("x α(x))("z γ(z))]) 8 Hint: This statement is not valid. Though its structure is similar to the previous two, the " are distributed within/without the in a way that causes problems. Give a model in which it is not true. Hint: First see which values of the model have their values forced For example, To make LHSRHS false, you must make the LHS true and the RHS false. What you hand it, is the model and the evaluation. Q2 3a. [("x α(x))("y β(y))] "z ( [β(z)γ(z)][α(z)γ(z)] ) 9 Give a formal proof, just as done in the last question. Then point out what goes wrong with the proof. Q2 3b. [("x α(x))("y β(y))] "z ( [β(z)γ(z)][α(z)γ(z)] ) 10 NEW SLIDES ‹#› 11 Three players: Adversary: prover: Oracle: If there is an implied "M, I go first providing worst case U, functions, relations and free vars. I prove formula is true with the Adversary’s choices and the Oracle’s help. If "x, If $y, If or, If , I assure A from AB. If "x, If $y, If or, If , provides worst x. constructs best y. chooses which side to prove. get new oracle to assure LHS. queries about his favorite x. provides best y. chooses which side to prove. assures LHS, then assures the RHS. or use modus ponens. Too many cooks. Who plays when? They each do their job when the structure of the sentence dictates. Follow the Parse Tree ‹#› 12 eg "x, $y, y=x+1 x" =)(2 A sentence has the correct syntax if it can be parsed into parse trees. well formed badly formed Syntax dictates which strings of characters are well formed Predicate logic formulas. Follow the Parse Tree 23+4 In addition to verifying that the syntax is correct, these also help explain the meaning i.e. syntax. First add then multiply. = 14 3+4 2 + 4 3 = 7 Ooops. That is wrong. ‹#› 13 eg "x, $y, y=x+1 x" =)(2 A sentence has the correct syntax if it can be parsed into parse trees. well formed badly formed Syntax dictates which strings of characters are well formed Predicate logic formulas. Follow the Parse Tree 23+4 In addition to verifying that the syntax is correct, these also help explain the meaning i.e. syntax. One parses using a Context Free Grammar. (See EECS 2001) First multiply then add. = 6 = 10 First add then multiply. + 4 23 2(3+4) = 14 3+4 2 3 2 + 4 3 = 7 ‹#› 14 Follow the Parse Tree Contest Free Grammar S "x S(x) | $x S(x) | SS | SS | SS | R(T,T) | … T f(T,T) | (T+T) | b | g | d R Loves represents “can be a” | represents “or” S represents any sentence eg "b,$g,Loves(b,g,d) returns true/false T represents any term eg father(b) returns objects R represents any relation: eg Loves maps tuples of terms to true/false ‹#› 15 Follow the Parse Tree Contest Free Grammar S "x S(x) | $x S(x) | SS | SS | SS | R(T,T) | … T f(T,T) | (T+T) | b | g | d R Loves Build the Parse Tree. Color (model, oracle, prover, adversary) each statement according to who assures/proves it each free variable according to provides it ‹#› 16 Follow the Parse Tree Contest Free Grammar S "x S(x) | $x S(x) | SS | SS | SS | R(T,T) | … T f(T,T) | (T+T) | b | g | d R Loves The highest president operation is "b. Hence, we use this rule. Parsing it as follows: "b,$g,Loves(b,g,d) Red indicates that the adversary provides it. Blue indicates the prover wants to prove it. "b $g,Loves(b,g,d) Recall, I prove a "b by getting my adversary to provide me with the worst case one b. The rest is blue because prover must prove it with the adversary's value b plugged in. ‹#› 17 Follow the Parse Tree Contest Free Grammar S "x S(x) | $x S(x) | SS | SS | SS | R(T,T) | … T f(T,T) | (T+T) | b | g | d R Loves The highest operation is $g. Hence, we use this rule. Parsing it as follows: Then we “recurse”. $g,Loves(b,g,d) Recall, I prove a $g by providing a suitable g. Loves(b,g,d) $g Then prover must prove the rest for this value g. ‹#› 18 Follow the Parse Tree Contest Free Grammar S "x S(x) | $x S(x) | SS | SS | SS | R(T,T) | … T f(T,T) | (T+T) | b | g | d R Loves This sentence is a relation. Hence, we use this rule. b, g, and d are terms (objects). Loves is a relation. Then we “recurse”. Loves(b,g,d) ‹#› 19 Follow the Parse Tree Contest Free Grammar S "x S(x) | $x