# Prove that every nonzero element has an induction given the following axioms.

Given the following axioms for arithmetic with exponentiation, call them $$AE$$, what does it mean/how do you proceed to prove the following statement (that every nonzero element is a successor)?

$$AE \vdash \forall x_0 (x_0 \neq 0 \rightarrow \exists x_1(x_0=S(x_1))$$

This is a homework assignment, but I am confused by the turnstile $$\vdash$$ which makes me feel like there needs to be some sort of formal derivation from the axioms using logical rules of inference. I would consider the following to be a proof, but I am not really using any of the listed axioms explicitly, and I am also not sure that induction is allowed. Do you think this suffices, and the above is just a rather formal way for my instructor to ask me to provide this standard proof?

My Proof:

Let $$P(x) \equiv(x=0 \lor \exists x_1 (x = S(x_1)))$$

Base case: $$P(0)$$ holds.

Inductive step: Suppose $$P(n)$$ holds for some $$n$$. It is immediate that $$P(S(n))\equiv (S(n)=0 \lor \exists x_1 (S(n)=S(x_1)))$$ as witnessed by $$x_1=n$$. So by induction the result follows.

1) $$\forall x_0 \sim (S(x_0)=0)$$ 2) $$\forall x_0, \forall x_1 (S(x_0)=S(x_1)\rightarrow x_0=x_1)$$ 3) $$\forall x_0 \forall x_1 (x_0 4) $$\forall x_0 (\sim x_0<0)$$ 5) $$\forall x_0 \forall x_1 (x_0 < x_1 \lor x_0=x_1 \lor x_1 < x_0)$$ 6) $$\forall x_0 (x_0+0=x_0)$$ 7) $$\forall x_0 \forall x_1 (x_0 + S(x_1) = S(x_0 + x_1))$$ 8) $$\forall x_0 (x_0 \cdot 0 =0)$$ 9) $$\forall x_0 Exp(x_0,0)=S(0)$$ 10) $$\forall x_0 \forall x_1 Exp(x_0,S(x_1)=Exp(x_0,x_1)\cdot x_0)$$