Stuck on a logic problem

Hi,

Can anyone give me some pointers for how to approach this problem?
I'm stumped and don't even know how one would begin.

(Exercise 3, Enderton 2nd ed., p. 223)
A theory T in a language with 0 and S is called w-complete if for any
wff phi and variable x, if phi(with x replaced by S^n(0)) is in T for
every n, then (forall x phi) is in T.
Suppose T is a consistent w-complete theory in the language (N,0,S,<,
+,*,exp). And suppose T contains all the following formulas:
1. forall x, x not= 0
2. forall x forall y (Sx = Sy -> x=y)
3. forall x forall y (x<Sy iff x <= y)
4. forall x, x is not less than 0
5. forall x forall y (x<y or x=y or y<x)
6. forall x, x+0 = x
7. forall x forall y x+Sy = S(x+y)
8. forall x, x*0 = 0
9. forall x forall y, x * Sy = x*y + x
10. forall x, exp(x,0) = S0
11. forall x forall y, exp(x,Sy)=exp(x,y)*x

Then show that T = Theory(N,0,S,<,+,*,exp).

The problem with the exercise is that there are just so so so many
hypotheses, all heuristics fall flat on their face. So I have no idea
how to begin either inclusion.

.

Relevant Pages