Homework # 2
due September 20

Reading

Please read Chapter 3 through the end of 3.3 in your textbook.

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.

Put your SaSyLF text in a file gt.slf in your AFS directory.

Terms

Define the boolean term language (true, false and if) and define equality over the terms and then prove the following theorems:

1. If if $t_0$ then $t_1$ else $t_2$ == if $t'_0$ then $t'_1$ else $t'_2$, then $t_0$ == $t'_0$.
2. If $t_0$ == $t'_0$, $t_1$ == $t'_1$, and $t_2$ == $t'_2$ then if $t_0$ then $t_1$ else $t_2$ == if $t'_0$ then $t'_1$ else $t'_2$.

Graduate Students

For each of the following proof systems, explain whether they support the ``law of excluded middle'' and why or why not:

1. Twelf
2. Coq
3. Isabelle

Write your answers on paper.

Submission

The SASyLF proofs should be placed in the files gt.slf and term.slf in the homework2 directory of your AFS volume.

About this document