For Peano Axiom, mathematical induction is equivalent to well order property.
But in well order property, what is the definition of "order"?
In detail, if we define the "order" $b\le c$ as:
$b = c$ or exist a finite (may be zero) number of natural numbers $a_1,… ,a_n$ such that: $(s(b)=a_1)\ \wedge\ (s(a_1)=a_2)\ \wedge \ …\ \wedge\ (s(a_n)=c)$
($s(i)=j$ means that, natural number $j$ is the successor of $i$.)
And the corollary:
$\forall i\in \mathbb N \setminus \{0\},\ \exists j\in \mathbb N$ such that $s(j)=i$
will be trivial, since $\mathbb N$ has minimum element $0$ and $\forall i\in \mathbb N$, $i\geq 0$ means that $i=0$ or $s(0)=a_1 … s(a_n)=i$, so we can prove that exist $a_n$ such that $s(a_n)=i$.
It seems so wired. Because if we don't use well order property, we need to prove the corollary using induction(proof by induction that every non-zero natural number has a predecessor), and the proof steps for me is not trivial.
Best Answer
In second order logic you can express the relation $m\le n$ by the formula $$\forall U(Um\land(\forall t (Ut\rightarrow U(St)))\rightarrow Un)$$ where $S$ stands for successor, U is a variable quantifying over all subsets of the domain of discourse, and lowercase variables quantify over objects in the domain.
In first order logic, AFAIK there is no formula $\Psi(x,y)$ with free variables $x,y$ such that $\Psi(x,y)\iff x\le y$. However, if you introduce a binary relation symbol $\le$ into the language you can axiomatize it as follows