CS 486 Applied Logic Assignment #7
Spring 1997 Due Date: Thurs., 3/13/97

Please read Suppes, Axiomatic Set Theory, pages 1-20.

1. Prove from Peano's axioms in Refinement Logic assuming equality as a primitive. Hint: try induction on .
2. Define .
   Prove in Refinement Logic with Arith rule.
3. Write a functional program to compute a function such that . Try to make the function match your proof in 2.
4. Use the monadic predicate calculus decision procedure to decide the validity of these formulas.
   1. 
   2. 

• About this document ...