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.

  • $\begingroup$ Thanks, do you mean that even if I were to be more formal (if you can expound a little more on what that would entail I'd appreciate it) I would always require induction? $\endgroup$ – Mike Mar 25 at 0:56
  • $\begingroup$ @Mike Yes, you need induction ... the statement does not follow from axioms 1 through 10. And to make things more formal: that all depends on what formal proof system you are supposed to work with.... $\endgroup$ – Bram28 Mar 25 at 2:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.