CS 486 Applied Logic Assignment #5
Spring 1997 Due Date: Thurs., 2/27/97

Reading: Please read Smullyan Chapter V §3 and Chapter VIII p.79-82.
Estimated time: less than 5 hours.

1. Write tableau proofs of these first-order formulas from Smullyan page 56.
   1. 
   2. 
   3. 
2. Give counter-examples to the reverse implications in (b) and (c).
3. Convert (b) to a Refinement Logic proof. Does the proof require ?
4. Write a Refinement Logic proof of this formula where is closed.
   1. 
   2. Does your proof require Magic?
5. Solve the problem on page 57 of Smullyan.
6. In transforming Tableau proofs to Refinement proofs in the case of quantifiers, we handle the on the right case by trying to complete this suggested simulation with a lemma.
   

   

   The formula is where has no free .
   Show how to finish this Refinement proof under the assumption that is provable.

7. Solve exercise 1 on Smullyan p.82.
8. Optional extra credit.
   Let be the set of all Boolean valuations, i.e. all maps . Given a set of Boolean formulas , define the open sets, , on as
   Show that is a compact space in this topology, that is, given any open cover of for , there is a finite subcover .

• About this document ...