Com S 641 --- Semantic Models of Programming Languages HOMEWORK 5: Proofs and Predicates and Sets (File $Date: 2002/03/23 21:06:02 $) Due: problems 1-10, March 25, 2002, the rest April 1, 2002. The following are exercises based on Cohen's book (chapters 2-3) and Chapter 7 of Back and von Wright's book. The ability to manipulate boolean formulas and to do proofs using the formal proof system of higher-order logic will be important for dealing with specifications and for reading the rest of the textbook. I sense we are getting the hang of this, but it's not quite solid yet. So I'm assigning several more exercises of this flavor. Please use the proof format described in chapter 4 for all of your proofs, and do the proofs formally, building up from the formal material in the book that we've seen so far. Please also do your proofs on the computer with an editor. If you use ASCII, please write write ``=='' for equality (=), ``==>'' for implication, ``<=='' for consequence, ``<==>'' for equivalence, ``!'' for negation, and != for inequality; also write the quantifiers as ``(\forall v :: t)'' and ``(\exists v :: t)'' and bounded quantification as ``(\forall v : b : t)'' and ``(\exists v : b : t)''. (Of course, you can use a text editor that has a symbol font with the proper symbols if you want; but I find this takes extra time.) Please also take a bit of time to go over your proofs to check them for following the proof format, for clarity, and check each step for validity. You can use lemmas I have proved in the truth-values/cohen.txt and truth-values/cohen-predicates.txt files in the course lecture notes directory, but if I stated a lemma without a proof, and if it's not in the Back and von Wright book, then you need to also prove that lemma. Of course, you can create your own lemmas (with proofs!) as well. 1. (15 points) This is a problem related to the focusing rules. a. What formula has to be valid for a proof step of the form P <== { some reason } Q to be a valid proof step (given assumptions Phi)? (See Cohen's chapter 6.) b. Consider the following proof step. "(X \/ Y <==> Y) \/ Z" <==> (X \/ Z <==> Z) <== { by \/ introduction } X \/ Y <==> Y <==> (X \/ Z <==> Z) Is this valid (i.e., without any assumptions)? If it is, prove the associated formula. If it is not, give a counterexample to the associated formula. 2. (10 points) [Cohen's 2.0d] Prove the first absorption law: |- X \/ (X /\ Y) <==> X . 3. (15 points) [Cohen's 2.1e] Prove the currying law: |- X ==> (Y ==> Z) <==> X /\ Y ==> Z 4. (15 points) [Cohen's 2.1f] Prove the following: |- (X ==> Y) \/ (Y ==> Z) 5. (20 points) [Cohen's 2.1i] Prove the following: |- (X ==> (Y <==> Z)) ==> (X /\ Y ==> Z) (Hint: I found it useful to use /\-elimination when focusing on the conclusion of an implication.) 6. (15 points) [Cohen's 2.2f] Prove the shuffle rule: |- (X /\ Y ==> Z) <==> (X ==> !Y \/ Z) 7. (15 points) [Cohen's 2.4c] Prove the following: |- (X ==> Y) <==> (Y ==> X) <==> X <==> Y Hint: I got an elegant proof by using problem 4 above as a lemma. 8. (20 points) Prove "trading" for bounded quantifiers. |- (\forall i : R.i /\ S.i : U.i) <==> (\forall i : R.i : S.i ==> U.i) 9. (20 points) Prove the following "nesting rule", assuming that j does not occur free in P.i: |- (\forall i : P.i : (\forall j : Q.i.j : U.i.j)) <==> (\forall i :: (\forall j : P.i /\ Q.i.j : U.i.j)) 10. (15 points) Prove the generalized de Morgan law: |- (\exists i : R.i : U.i) <==> !(\forall i : R.i : !(U.i)) Hint: use the de Morgan laws in Back and von Wright's book on page 118. 10b. (40 points; extra credit) Prove the generalized de Morgan law: |- (\exists i : R.i : U.i) <==> !(\forall i : R.i : !(U.i)) without using the generalized de Morgan laws for quantifiers in Back and von Wright's book on page 118. Hint: To do this, I used a proof rule for focusing within negation, which I had to develop and justify. I also found that the only way to satisfy the side conditions of the \forall-introduction and \exists-elimination rules was to use the other quantifier in the formula "s" that appears in these rules (on pages 116-117). For example, when using the \forall-introduction rule, in the subproof, the formula that plays the role of s was existentially quantified. Thus the uses of the quantifier rules "mixed" (one was used in the subproof for the hypothesis of the other) rather more than I expected at first. 11. (20 points) [7.1] A set B over a type S is identified with its characteristic predicate p_B : S -> Bool. So by abuse of notation, we consider B itself to have type S -> Bool. This means that we can talk about the image im.B.A of another set A under B. This image is a set of truth values. (a) Prove that im.B.B == {T}, if B != {}. (b) Prove that im.B.{} == {}. (c) Under what conditions is im.B.A == {F}? (d) Under what conditions is im.B.A == {F,T}? 12. (20 points) [7.5] In first-order logic it is common to introduce a Skolem function when one has proved a theorem of the form (\forall v :: (\exists w :: t)). Such a function f is assumed to satisfy the property (\forall v :: t[w := f.v]). In higher-order logic, the introduction of a Skolem function can be based on a derived inference rule: Phi |- (\forall v :: (\exists w :: t.w)) ____________________________________________ (skolemization) Phi |- (\exists f :: (\forall v :: t.(f.v))) * w not free in t Derive this inference rule using only the rules given in the text.