Com S 641 --- Semantic Models of Programming Languages

		       HOMEWORK 4: Truth Values
		 (File $Date: 2002/03/11 19:40:44 $)

Due: problems 1-5, Mar. 6, 2002; the rest, Mar. 8, 2002.

The following are exercises from chapter 6 of Back and von Wright's book.
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.  You may find it helpful to do
such proofs on the computer. 

1. (10 points) [6.3]
   Prove the correspondence rule for meet:
     |- t <= t' <==> (t \meet t' == t)
   using only the basic inference rules for lattices (Figure 6.1).

2. (10 points) [6.4]
   Prove the classical principle of double negation
     |- !(!t) <==> t
   using only rules given in chapter 6.  (Hint: use case analysis;
   first prove |- !T <==> F and |- !F <==> T.)

3. (10 points) [6.5]
   Prove that implication can be expressed with negation and disjunction:
     |- t ==> t' <==> !t \/ t' .

4. (10 points) [6.6]
   Prove the rule for focusing on a conjunct:
        Phi, t |- t1 <==> t2
      _____________________________
       Phi |- t /\ t1 <==> t /\ t2
   (hint: do case analysis on t).

5. (20 points) [6.7a,b]
a. Prove the rule for focusing on a conjunct under implication:
        Phi, t |- t1 ==> t2
      _____________________________
       Phi |- t /\ t1 ==> t /\ t2
b. Formulate and prove the corresponding rule for disjunction.

6. (10 points) [6.8a]
   Derive the rule for dropping vacuous universal quantifiers.

      |- (\forall v :: t) <==> t
      * v is not free in t

7. (10 points) [6.9]
   Derive the one-point rule for universal quantification:

      |- (\forall v :: v = t ==> t') <==> t'[v := t]
      * v is not free in t