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<S(x_1) \leftrightarrow (x_0<x_1 \lor x_0=x_1)$$ 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)$$
Your proof is correct, though if they are looking for a formal proof, you have a bit more work to do formalizing those steps. And notice: you don't use any of the 10 axioms .... but you do need induction.