0
$\begingroup$

Natural numbers (including 0) and the successor function are defined as per the Peano Axioms (you can check them on wikipedia). Addition is defined recursively as follows:

$a+0=a$

$a+S(b)=S(a)+b$

With these definitions in mind, I need to prove that $a+S(b)=S(a+b)$

I tried using induction on b, and while proving the base case was trivial, I only end up with a circular argument when I try to prove the inductive step.

$\endgroup$
3
  • $\begingroup$ You should prove $\forall a (a + S(b) = S(a + b))$ by induction on $b$. $\endgroup$
    – Mark Saving
    May 23, 2022 at 23:15
  • $\begingroup$ @MauroALLEGRANZA I intenionally used a different (hopefully equivalent, though I have yet it prove this) definition for addition, which is why I am trying to prove all of additions's properties from scratch, i.e. I am not allowed to use any "preliminary lemmas" and similar things. At the end of your proof, you state that $Sb+Sa=S(Sb+a)$... Which is exactly what I am trying to prove, so I can't use this statement in the proof. Also, I am not allowes to consider addition commutative yet either. $\endgroup$
    – Dark Rebellion
    May 24, 2022 at 7:51
  • $\begingroup$ You should probably show your failed attempt. It might turn out to be correct, and anyway we can better see where exactly your confusion is. $\endgroup$
    – Trebor
    May 24, 2022 at 9:44

1 Answer 1

Reset to default
0
$\begingroup$

Hint: try to prove the stronger claim: $$ \forall x(a + S(x) = S(a+x)) $$

$\endgroup$
2
  • $\begingroup$ This is exactly what I am trying to prove, essentially that $\forall a\forall b(a+S(b)=S(a+b))$ $\endgroup$
    – Dark Rebellion
    May 24, 2022 at 7:34
  • $\begingroup$ No it isn't. You don't have the $\forall$, which is vital as you need to apply the inductive hypothesis with $S(b)$ in place of $b$.. @MauroALLEGRANZA leaves this implicit in his answer, but that is a sleight of hand. $\endgroup$
    – Rob Arthan
    May 24, 2022 at 17:34

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .