Let us have a first order language $L=\{0,s\}$, where $0$ is a constant, $s$ is a function symbol of arity $1$. The first-order theory $T$ is axiomatized as follows:
How could I prove the following statement?
$$\forall a, b \left( s(s(a))=s(b) \implies s(a)=b \right)$$
I know how I could prove the converse using the substitution but I am not sure what I could use in the other direction.
On
We can make a model of your two axioms in which the result is false.
The model consists of the following objects:
(i) The ordinary natural numbers $0$, $1$, $2$, and so on with $s$ interpreted as the usual successor operation and
(ii) Distinct new objects $b_{0}$, $b_{-1}$, $b_{-2}$, and so on, where $s$ is interpreted by $s(b_0)=1$ and for all other $k$, $s(b_k)=b_{k+1}$.
Then the desired sentence fails. The successor of the successor of $b_{-1}$ is $1$, which is the same as the successor of $0$. But the successor of $b_{-1}$ is $b_0$, which is not $0$.
On
A simpler counter-example model is $\{0,1\}$ with $s(0)=1$ and $s(1)=1$. Then $s(s(0))=s(0)$ but $s(0)\neq 0$.
Note that your statement is one of the Peano Axioms.
You can't, as stated. Here's a model which satisfies these constraints. Let $\mathcal{M}$ have as its domain $\{0, 1, 2\}$. Let $s$ be the function that sends $0$ to $1$, sends $1$ to $2$, and sends $2$ to $2$.
In this model, both of the two axioms are true. Furthermore, letting $a = 0$ and $b = 2$, we have $s(s(a)) = s(s(0)) = s(1) = 2 = s(2) = s(b)$. But $s(a) = s(0) = 1 \neq 2 = b$.
In order to prove what you're looking for, then, you'll need to add an extra axiom. For instance, note that the reason this model works is because $s$ is not injective. That is $s(a) = s(b)$ doesn't imply $a = b$. Adding an axiom to the effect that $s$ is injective would certainly suffice to prove what you want to prove.