# Using Peano Axioms Prove That Greater Than Holds For Successor Functions

In first order logic, $$\ge$$ can be defined as $$\exists x(u = x + w)$$.

I am trying to formally deduce a proof for:

$$\exists x(u = x + w) \vdash \exists x(s(u) = x + s(w))$$

I can use peano axioms and basic formal deduction rules. I'm just having a hard time figuring out how to start the question and always get confused if I should use induction or not. Kinda new to this and just looking for a hint on how to start or general guidance on how to approach the question.

If I'm replacing the bound variables with free variables to start, which I believe I should, I know my final step would most likely be to add the $$\exists x$$ back to the LSH of the proof.

Any help appreciated.

Edit: Forgot to just say domain is natural numbers

1. $$∃x(u=x+w)$$ ---premise

2. $$u=a+w$$ --- assumed [a] form 1) for $$\exists$$-elimination

3. $$s(u)=s(a+w)$$ --- from 2) by substitution axiom for equality

4. $$s(u)=a+s(w)$$ --- from 3) by axiom for $$+$$

5. $$\exists x (s(u)=x+s(w))$$ --- from 4) by $$\exists$$-introduction.

$$\exists x (s(u)=x+s(w))$$ --- from 2)-5) and 1) by $$\exists$$-elimination, discharging assumption [a].

• This makes a lot of sense, thanks so much! Just wondering as I said I'm new to this and have been having some trouble about knowing when to use the induction axiom to deduce things, do you know of any indications that would help me know when to use this axiom? Commented Nov 25, 2020 at 7:32
• @JohnOkley - maybe useful: First Order Arithmetic as well as Peano Arithmetic Commented Nov 25, 2020 at 7:38