CSC 2429S   Spring, 2002.   Assigned Problems.

1.  Prove the Anchored Completeness Theorem for PK, for the general case.
(See Exercise 5, page 10 in the Notes.)

2.  Show how to modify the proof of the Completeness Lemma to obtain
a proof of the Anchored LK Completeness Theorem.  (See Exercise 4,
page 24 in the Notes.)

3.  Show that the completeness direction of the Herbrand Theorem
follows from the Anchored LK Completeness Theorem.  (See Exercise 3,
page 30 in the Notes.)

4.  Show that the following are theorems of I-Delta-0 (See pp 34 and 35):
O3 (Associativity of multiplication)  (use O5)
D7 (Corrected to assert left-to-right implication only) (Use earlier results)
D10 (Cancellation Law for multiplication) (Use earlier results)

5.  Do Exercise 1 page 47:  Show that I-Delta-0 proves that every
power of two is divisible by all smaller powers of two.

6.  Show that the following results are provable in I-Delta-0:

a)  If y is a power of 2, then 2y is a power of 2.

b)  If x not= 0, then LenBit(y,x) holds for some y, where y is a power of 2.
Do not use the Theorem on page 47.

NOTE FOR 6a:
Your proof should follow in outline a natural proof in number
theory, where you may assume the usual laws of algebra and inequalities
(as presented on pp 33-35 in the Notes).  In order to make your proof
readable, you should use properties of numbers that we take for granted,
but justify them if they don't readily follow from the basic algebraic
laws.

Here are some basic principles that you may use (if you justify them
in ID0).

x|y iff xz=y for some z

Define the predicates even(x) and odd(x).  Prove that every number
is either even or odd, but not both.  Prove that the product of
two odd numbers is odd.

7.  In the corrected proof of Parikh's Theorem, carry out Case III
for forall-right, page 62. 

8.  Do Exercise 1, page 65 (special case of a proof based on
anchored LK that V0 is conservative over ID0).

9.  Do Exercise 1, page 71 (concerning justifying the case of cut
in the proof of the V0 witnessing theorem).

10. Do Exercise 2, page 79 (show explicitly that Parity(Y) is
Delta1B definable in V1).

11. Do Exercise 3, page80.  Show explicitly how V-tilde-1 can
Sigma1B define Numones(X).  (Use the techniques in the Leftarrow
direction of the Main Theorem, pp77,78.) Show V-tilde-1
proves property (i), but you need not bother with property (ii).

12.  Do Exercise 1, page 91 (the case of exists-right in the proof
of the V0 translation theorem).

13.  Do Exercise 2, page 97 (prove completeness of system G).