Context: This question arises from the unsuccessful search for a proof (that does not use induction) of a result used to prove the equivalency of the Well-Ordering Principle ("WO") and Induction. Assume the Dedekind-Peano Axioms with addition and the following basics:
(A1) $\forall x[x+1=S(x)]$
(A2) $\forall x\forall y[x+S(y)=S(x+y)]$
(O1) $\ \ x<y\ $ means $\ \exists z[x+z=y]$
(O2) $\ \ x\leq y\ $ means $\ x\!=\!y\vee x\!<\!y$
In particular, the question arises on a result (labeled Theorem 1 here) used in the proof of WO implies induction:
Theorem 0: The well-ordering principle implies the principle of induction.
Proof: Let $A\!\subseteq\!\mathbb{N}$ be a set with the properties: (i) $1\!\in\!A$, and (ii) $k\!\in\!A$ implies $S(k)\!\in\!A$. The proof proceeds by contradiction by supposing that $A\!\neq\!\mathbb{N}$ (i.e., $\mathbb{N}\backslash A$ is non-empty). According to WO, if $\mathbb{N}\backslash A$ is non-empty, then it must contain a least element, which can be denoted as $l$. By (i), $l\!\neq\!1$. Therefore, from Theorem 1, there exists some $m\!\in\!\mathbb{N}$ such that $m\!+\!1\!=\!l$, which implies $m\!<\!l$ by (O1). It must be that $m\!\in\!A$ (since assuming otherwise would contradict $l$ being the least element of $\mathbb{N}\backslash A$). By (ii) and (A1), it follows that $S(m)\!=\!m\!+\!1\!=\!l\!\in\!A$. But this contradicts the assumption that $l\!\in\!\mathbb{N}\backslash A$. Hence the set $\mathbb{N}\backslash A$ must be empty, so that $A\!=\!\mathbb{N}$.
Question: My question is not on the above proof (unless there is a way to prove that result without relying on Theorem 1), but on the proof of Theorem 1 itself. I also understand how to prove Theorem 1 using induction. But since Theorem 1 is used above to prove induction (Theorem 0), one is obviously excluded from using induction and limited to using WO to avoid circular reasoning.
Theorem 1: For all $n\!\in\!\mathbb{N}$, $n\!=\!1$ or $n$ is the successor of some $m\!\in\!\mathbb{N}$. In other words: $$\forall x\Big[\ x\!=\!1\ \vee\ \exists y[x\!=\!y\!+\!1]\ \Big]$$
However, I am at a loss as to how to prove this using just WO. I've attempted to use the method of "proof by minimum counterexample" as above, but only come as far as this:
Proof (incomplete): Consider the set $B\!\subseteq\!\mathbb{N}$ defined by: $$B\equiv\{\ n\!\in\!\mathbb{N}\ :\ n\!=\!1\vee\exists m\!\in\!\mathbb{N}[n\!=\!m\!+\!1]\ \}.$$ The proof proceeds by contradiction by supposing that $B\!\neq\!\mathbb{N}$ (i.e., $\mathbb{N}\backslash B$ is non-empty). According to WO, if $\mathbb{N}\backslash B$ is non-empty, then it must contain a least element, which can be denoted as $l$. It follows from the definition of $B$ that $l\!\neq\!1$ and $\neg\exists m\!\in\!\mathbb{N}[l\!=\!m\!+\!1]$.
Am I on the right track?