Com S 641 Semantic Models for Programming Languages
			     Homework: 3

E. Cohen.  Programming in the 1990s. Springer-Verlag, 1990.  Chapters 2 and 3.

The aim of this homework is to gain fluency with the predicate calculus.
Note that (p. 31, and p. 41) the conjunction (/\) has the same precedence
as disjunction (\/).  Note also that the equivalence and discrepancy have
the lowest binding power.

(Chapter 2)
When you read this chapter, read each of the proofs carefully,
being sure that you understand each step.  A good way to do this
is to check each step as if it might not be correct (extra credit for
finding any errors).  Even better, try to do some of the proofs yourself,
without looking at the book's proof.  I will only require a subset of
Cohen's exercises, but you might want to start with some easier ones,
and do more if you're having trouble.  (See me if you're stuck.)

For the following exercises, we write ``==>'' for implication,
``<=='' for consequence, ``equiv'' for equivalence, ``diffs'' for discrepancy,
and ``~'' for negation;  you can use the same conventions if you use ASCII.
(These conventions have the pleasing property that the longer ones have lower
binding power, and the number of characters is inversely proportional to
the binding power.  Also ``equiv'' should remind you to say "equivalent"
or "equivales", and ``diffs'' should remind you to say "differs from".
But when writing by hand, use the symbols in the book.)
It may be helpful to use a text editor for these exercises;
I like to copy the formula from the last step to the next,
and then edit the formula in place, as this saves time and prevents
silly copying errors.

When doing a proof, you can cite axioms and theorems from Cohen's book,
but no appeals to models are allowed.  (Don't draw a truth table,
or anything like that.)  When proving a theorem found in the chapter,
you should only use axioms or theorems that appear strictly earlier
in the chapter, so that the proof could be placed in the text.
Note that most of Cohen's exercises are also theorems in the chapter,
and so this will help Cohen avoid circular reasoning (!).

a. (Cohen's 2.0(d)) Prove the Absorption law: X \/ (X /\ Y) equiv X
b. (Cohen's 2.1(d)) Prove: true ==> X equiv X
c. (Cohen's 2.1(e)) Prove: X ==> (Y ==> Z) equiv X /\ Y ==> Z
d. (Cohen's 2.1(f)) Prove: (X ==> Y) \/ (Y ==> Z)
e. (Cohen's 2.1(h)) Prove the implication distributes over the equivvalence:
			X ==> (Y equiv Z) equiv X ==> Y equiv X ==> Z
f. (Cohen's 2.1(i)) Prove: (X ==> (Y equiv Z)) ==> (X /\ Y ==> Z)
g. (Cohen's 2.2(a)) Prove: ~X \/ Y equiv X \/ Y equiv Y
h. (Cohen's 2.2(f)) Prove the Shuffle law:
			(X /\ Y ==> Z) equiv (X ==> ~Y \/ Z)
i. (Cohen's 2.3(b)) Prove the conjunction distributes over the discrepancy:
			X /\ (Y diffs Z) equiv X /\ Y diffs X /\ Z
j. (Cohen's 2.4(b)) Prove: (X ==> Z) \/ (Y ==> Z) equiv X /\ Y ==> Z
k. (Cohen's 2.4(c)) Prove: (X ==> Y) equiv (Y ==> X) equiv X equiv Y
l. (Cohen's 2.4(f)) Prove: Y \/ (X ==> Y) equiv X ==> Y
m. (Cohen's 2.4(g)) Prove: X \/ Y ==> X /\ Y equiv X equiv Y

(Chapter 3)
As below, in ASCII, write ``all'' for the universal quantifier, ``exists''
for the existential, and ``OP'' for Cohen's underlined ``OP''.
By hand use the standard symbols.
n. (Cohen's 3.1(a), p. 51) Using the laws (rules) for quantified expressions,
   prove the dummy elimination rule:
	(OP i,j : i = Z /\ R.i.j : T.i.j) = (OP j : R.Z.j : T.Z.j)
o. (Cohen's 3.2(b), p. 54) Prove the rule of instantiation for universal
   quantification: (all i :: f.i) ==> f.x
p. (Cohen's 3.3(b), p. 55) Prove the rule of instantiation for existential
   quantification: f.x ==> (exists i :: f.i)
q. (Cohen's 3.3(c), p. 55) Prove trading for existential quantification:
	(exists i : R : T) equiv (exists i :: R /\ T)
r. (extra credit only) do one or more of Cohen's exercises 3.11, 3.12, or 3.13.