What is the definition of the "order" of well order property in Peano Axioms?

Question

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.

Answer 1

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

• $\forall x (x\le x)$
• $\forall x\forall y (x\le y \land y\le x\rightarrow x=y)$
• $\forall x\forall y\forall z (x\le y \land y \le z \rightarrow x\le z)$
• $\forall x\forall y(x\le y \lor y \le x)$
• $\forall x (0\le x)$
• $\forall x\forall y(x\le y\land x\ne y\leftrightarrow Sx\le y)$

Answer 2

Your definition of $\le$ does not work well because it seems to be an infinitary conjunction. The Peano axioms are supposed to be interpreted in a logic that is second (or higher) order but still finitary -- every formula is finite string of symbols.

The usual definition of $\le$ in this setting is $$ x \le y \iff \exists z(x+z=y) $$ after we have defined addition recursively, of course.

We can then phrase the well-ordering property as $$ \tag1 \exists y(y\in A) \to \exists y(y\in A \land \forall z(z< y\to z\notin A)) $$ which is logically equivalent to a second-order formulation of long induction: $$ \tag2 \forall y(\forall z(z<y \to z\in B) \to y\in B) \to \forall y(y\in B) $$ (Namely, let $A$ be the complement of $B$ (or vice versa) and contrapose the outermost $\to$).

It then takes a bit of footwork to prove (2) from the usual second-order mathematical induction axiom $$ \tag3 0\in C \land \forall y(y\in C\to S(y)\in C) \to \forall y(y\in C) $$ and the recursive definition of addition. Basically, to get (2) you would apply (3) with $C=\{y\mid \forall z(z<y\to z\in B)\}$.