CS486 Applied Logic Assignment 7 Due Thursday, April 5, 2001

Reading: Please study all of Smullyan Chapter 5.

Exercises:

1. Prove by Refinement Logic

a. "xP(x)Ú$x.ØP(x)

b. ($y"xA(x,y) Þ $v"uB(u,v)) Þ
"y$v"u$x(A(x,y) Þ B(u,v))

2. Suppose that ℕ_n={0,1,2,...,n-1}. Show that if P(x) is a computable boolean expression, then there is a program to decide whether

"x:ℕ_n.P(x) or $x:ℕ_n.ØP(x).

What can you say about the relationship of this program to the proof in problem 1?

3. Solve the exercise on p. 63 of Smullyan.