Context: I keep running into circular reasoning in attempting to derive strong induction (more generally "induction" whether it be weak or strong) from the well-ordering principle. Assume:
Peano Axioms w/ Well-Order: (I realize these are presented semi-informally)
(P1) $\ \exists x[x\!=\!1]$;
(P2) $\ $there exists an unary ("successor") function $S$ on $\mathbb{N}$ (i.e., $x\!\in\!\mathbb{N}\rightarrow S(x)\!\in\!\mathbb{N}$);
(P3) $\ \forall x[S(x)\!\neq\!1]$;
(P4) $\ \forall x\forall y[x\!\neq\!y\rightarrow S(x)\!\neq\!S(y)]$
(P5') $\ $Well-Ordering Principle: Every non-empty set includes a least-element: $$ \forall B\Big[\emptyset\!\subset\!B\!\subseteq\!\mathbb{N}\longrightarrow\exists m\big[m\!\in\!B\wedge\forall p[p\!\in\!B\rightarrow m\!\leq\!p]\big]\Big] $$
Note: Since I am trying to show the logical equivalency between Induction and the Well-Ordering Principle, I am assuming the latter as an axiom and treating the former as a theorem (below). The relation $\leq$ used above is defined next.Order Relation
(O1) $\ x\!<\!y\leftrightarrow\exists z[x\!+\!z\!=\!y]$
(O2) $\ x\!\leq\!y\leftrightarrow[x\!=\!y\vee x\!<\!y]$
Addition (since order above is defined with "$+$")
(A1) $\forall x[S(x)=x+1]$
(A2) $\forall x\forall y[x+S(y)=S(x\!+\!y)]$
With this as background, below is the theorem and proof I see most often (or some variation thereof) in textbooks and online forums.
Theorem: The Well-Ordering Principle (P5') implies the Strong Induction Principle.
Proof: Suppose $X\!\subset\!\mathbb{N}$ with: (1) $1\!\in\!X$, and (2) $\forall x[x\!<\!k\rightarrow x\!\in\!X]\rightarrow k\!\in\!X$. Assume $X'\!\equiv\!\mathbb{N}\setminus X$ is non-empty. From Well-Ordering Principle (P5'), $X'$ includes a least element $m$. From (1), $m\!\neq\!1$. Since $m$ is the least element of $X'$, then all $x\!<\!m$ must belong to $X$. However, property (2) implies that $m\!\in\!X$, a contradiction. Thus, $X'$ must be empty and $X\!=\!\mathbb{N}$.
My problem is with the highlighted sentence above, which appears to me to require the result that $\neg(m\!\leq\!x)\leftrightarrow x\!<\!m$, which I believe is based on the Trichotomy Property (exactly one of $x\!<\!y$, $x\!=\!y$, $x\!>\!y$ holds). However, the only proof of the Trichotomy Property (that I am aware of) based on the above axioms/definitions alone uses Induction (see Thm 4.1c). Thus, it appears the reasoning is circular (induction is used to prove an intermediate result that is then used to prove induction).
Question: Assuming my understanding above is correct, my question simply put is this: does a proof exist of the Trichotomy Property for $<$ as defined above that does not require a proof based on induction?
Best Answer
The axioms you listed (P1-P5') are not equivalent to Peano's. Replacing the (weak) induction axiom with the well-ordering axiom gives a weaker theory. The well-ordered sets that are not order-isomorphic to the natural numbers still obey the well-ordering axiom.
Before I come back to the trichotomy question, let's recall the role of induction in Peano's axioms. Like all the other axioms, induction is chosen so that the resulting theory may describe as well as possible the natural numbers. Induction, specifically, is there to exclude certain undesirable models.
For instance, without induction, one could easily build a "non-standard" model of arithmetic that, besides the natural numbers, contained two more elements, call them $\alpha$ and $\beta$, such that $s(\alpha) = \beta$ and $s(\beta) = \alpha$. Such a model would satisfy P1-P4, but induction rules it out.
If Peano's axioms included strong induction instead of weak induction, the resulting theory would allow models whose order type is not $\omega$. For instance, $W = \{0,1\} \times \mathbb{N}$, with lexicographic ordering, satisfies P1-P5'. (In particular, it is a well-order.)
On the other hand, weak induction does not "work" on $W$, because starting from $(0,0)$, which is the least element of $W$, and working up to $(0,1), (0,2)$ and so on, one never reaches $(1,0)$. One could "prove" by weak induction that all elements of $W$ have first component equal to $0$. For $W$ one needs transfinite induction, which is essentially strong induction.
Now, for the trichotomy property. Note that Mendelson introduces $x < y$ as a "purely abbreviational definition" in terms of $+$. Therefore, $<$ must be proved a total order. For that, induction is used; specifically, to show that the trichotomy property holds.
When proving that a well-ordered set satisfies the strong induction principle, the ordering of the set is supposed to be given, and to be a strict total order. No property of strict total orders needs to be proved.