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.