Homework # 1
due September 9

Reading

Please read Chapters 1-2 in your textbook.

Problems

Please do the following problems from the book:

2.2.7 (transitive closure) full natural language proof required

Natural Numbers

Using the following definition of ``greater than''

judgment gt: n > n

------- gt-one
s n > n

n1 > n2
--------- gt-more
s n1 > n2

Prove the following theorems in SASyLF:

  1. For any $n$, we have $(s n) > 0$.
  2. If $s n_1 > s n_2$ then $n_1 > n_2$.
  3. ``Greater than'' is transitive.
  4. If $n > n$ then we have a contradiction.

Submission

Turn in the natural language proof on paper at the beginning of lecture. The SASyLF proofs should be placed in the file homework1/homework1.slf of your AFS volume.

About this document



John Tang Boyland 2008-08-30