I am supposed to prove that if a is a positive natural number then there exists exactly one number b, such that the increment of b is equal to a.
My idea was to induct from the base case a = 1, but I am I can't proceed this way because I haven't yet established that 1 is the smallest positive number (I don't even have the concept of 'greater than' defined.) I have the fact that 0 is not a successor of any natural number, so I tried to use that but without success.
Any idea how to proceed?
On
We have :
to prove that if $a$ is a positive natural number then there exists exactly one number $b$, such that the increment of $b$ is equal to $a$.
Assuming that "the increment of $x$" is the successor of $x$, i.e. $S(x)$, we have in symbols :
$\forall a (a \ne 0 \rightarrow \exists ! b (S(b)=a))$.
We prove it using first-order Peano's axioms, i.e. the theory $\mathsf {PA}$, and in particular I will follow Stephen Cole Kleene, Introduction to Metamathematics (1952), page 181-on.
Uniqueness follows from the axiom :
$∀x,y ( S(x) = S(y) \rightarrow x = y)$.
Assume that :
$\exists b_1 \exists b_2 (S(b_1)=a \land S(b_2)=a)$.
Then, by property of equality, $S(b_1)=S(b_2)$; thus, form the above axioms, we conclude with $b_1=b_2$.
For the existence of $b$, where $b$ is the successor of $a$, we have to prove that :
$\forall a (a \ne 0 \rightarrow \exists b (S(b)=a))$.
The proof is by Induction on $a$, where the induction formula is : $\mathcal A(a) := (a \ne 0 \rightarrow \exists b (S(b)=a))$.
Basis : $\mathcal A(0)$. We need the tautology : $A \rightarrow (\lnot A \rightarrow B)$, with $A := 0 = 0$ and $B := \exists b (S(b)=0)$.
Using the logical theorem : $\vdash 0 = 0$ [by substitution in the identity axiom : $\vdash x = x$], by modus ponens we derive :
$0 \ne 0 \rightarrow \exists b (S(b)=0)$ --- $\mathcal A(0)$
Induction step : $\mathcal A(S(a))$. Again from identity axiom we have $S(a)=S(a)$; thus, by $\exists$-intro :
$\exists b (S(b)=S(a))$.
Having proved it, from the logical axiom : $A \rightarrow (B \rightarrow A)$, by modus ponens we derive :
$S(a) \ne 0 \rightarrow \exists b (S(b)=S(a))$ --- $\mathcal A(S(a))$ .
We have proved : $\vdash \mathcal A(0)$ and $\vdash \mathcal A(S(a))$; but form the last one, by properties of derivability, we have : $\mathcal A(a) \vdash \mathcal A(S(a))$.
Thus, applying Induction schema : if $\Gamma \vdash \mathcal A(0)$ and $\Gamma, \mathcal A(x) \vdash \mathcal A(S(x))$, then $\Gamma \vdash \forall x \mathcal A(x)$, with $\Gamma = \emptyset$, we conclude with : $\forall a \mathcal A(a)$, i.e.
$\forall a(a \ne 0 \rightarrow \exists b (S(b)=a))$.
Added
Please, consider Robinson arithmetic, or $\mathsf {Q}$, which is a finitely axiomatized fragment of Peano arithmetic, first set out by R.M.Robinson (1950) : $\mathsf {Q}$ is essentially $\mathsf {PA}$ without the axiom schema of induction.
In $\mathsf {Q}$ we have the axiom :
$\forall x(x = 0 \lor \exists y(Sy = x))$
which is exactly :
$\forall x(x \ne 0 \rightarrow \exists y(Sy = x))$.
You probably need an axiom equivalent to $a=b$ iff $S(a)=S(b)$, which would be axiom 8 of the Peano axioms. In that case you should be able to find at least one predecessor using the definition of a natural number, and then it is easy to see that it is unique because all predecessors must be equal.