Here's a first draft of an answer.

Induction will be used as the proof technique. Since Mathematica uses an equational prover, there's no direct way to use induction. What will be ventured here are just two first-order proofs, one for the basis case and the other for the induction step.

axioms = { ForAll[x, plus[x, zero] == x], ForAll[{x, y}, plus[x, next[y]] == next[plus[x, y]]]} 

Basis case:

FindEquationalProof[ForAll[x, plus[zero, zero] == zero], axioms] 

Induction assumption:

assertion = {ForAll[x, plus[zero, x] == x]} 

Induction step:

FindEquationalProof[ForAll[x, plus[zero, next[x]] == next[x]], Union[axioms, assertion]] 

Here's a first draft of an answer.

Induction will be used as the proof technique. Since Mathematica uses an equational prover, there's no direct way to use induction. What will be ventured here are just two first-order proofs, one for the basis case and the other for the induction step.

axioms = { ForAll[x, plus[x, zero] == x], ForAll[{x, y}, plus[x, next[y]] == next[plus[x, y]]]} 

Basis case:

FindEquationalProof[ForAll[x, plus[zero, zero] == zero], axioms] 

Induction assumption:

assertion = {ForAll[x, plus[zero, x] == x]} 

Induction step:

FindEquationalProof[ForAll[x, plus[zero, next[x]] == next[x]], Union[axioms, assertion]] 

EDIT: As requested in the comments, the following is a proof of $2+2=4$. The axioms are the same as above:

FindEquationalProof[ plus[next[next[zero]], next[next[zero]]] == next[next[next[next[zero]]]], axioms]