Vtyjkyuk

Axiomatically, set $mathbbN$ is constructed via injective function $s:mathbbNrightarrow mathbbN$ and an element $1inmathbbN$ and we have that $forall ninmathbbN:s(n)neq1$. Together with this, we are given the axiom of mathematical induction, that is:

Axiom (PMI): Let $SsubseteqmathbbN$ satisfy following properties:
$$1in Stagi$$
$$nin SRightarrow s(n)in Stagii$$
then $S=mathbbN$.

Now, in order to talk about well ordering, we should define the ordering we wish to prove is well on $mathbbN$. We define addition:

Definition (addition): $+mathbbN^2rightarrow mathbbN$
$$a+1=s(a)tagiii$$
$$a+s(b)=s(a+b)tagiv$$

Then, we define strict order on $mathbbN$ by:

Definition (ordering):
$$a<bLeftrightarrow exists xinmathbbN:a+x=btagv$$
$$aleq bLeftrightarrow a<bvee a=btagvi$$

It is straightforward to show that $leq$ is total ordering. Now I wish to prove that $mathbbN$ is well ordered by $leq$. So, I proceed by showing that PCI, also known as Principle of Complete Induction, holds.

Theorem (PCI): Let $Ssubseteq mathbbN$ satisfy following properties:
$$1in Stagvii$$
$$1ldots nsubseteq mathbbNRightarrow s(n)in Stagviii$$
then $S=mathbbN$.

Proof: Proceed by induction. Because $1in S$ it follows that $1subseteq S$, so the base step holds. Now assume that $1ldots nsubseteq S$. By (viii) $s(n)in S$, thus $1ldots,n,s(n)subseteq S$. By PMI $S=mathbbN$.

So far so good, now I show that this implies the WOP also known as Well-ordering principle.

Theorem(WOP): $mathbbN$ is well ordered by $leq$, equivallently, any nonempty subset of $mathbbN$ has minimal element with respect to $leq$.

Proof: Assume there exists some $Ssubseteq mathbbN$ such that $S$ has no minimal element. We show that $S$ is empty. Let $P(n)$ be predicate:
$$P(n):nnotin S$$
and proceed by PCI.
$P(1)$ holds, because (It is straightforward to show by induction) $forall ainmathbbN:1leq a$ and if $1in S$ then $1$ is minimal element of $S$ which contradicts our assumption. So base step holds. Assume $forall kin 1ldots n:P(k)$. We wish to show that $P(s(n))$ holds. If $P(s(n))$ didn't hold, we would have that $s(n)in S$ but in that case $s(n)$ is the smallest element in $S$, which is impossible. So by PCI it follows, that $forall ninmathbbN:(n)$. But this shows that $S$ is empty. Thus any nonempty subset of $mathbbN$ must have minimal element.

Now, this looks very pretty, but as I red through this few times, i couldn't stop thinking about the set $1ldots n$. In fact, what do we mean by set $1 ldots n$? This is my "explanation": In fact
$$ 1ldots n=1,s(1),s(s(1)),ldots,s(s(s(ldots s(1))))$$ So $n$ is some finite composition of $s$ applied to $1$. Trivially $forall ninmathbbN:n<s(n)$. Denote $M=1ldots n$. Surely there exist some (unique) $n_1in M$ such that $s(n_1)=n$, next, there is some $n_2in M$ such that $n_1=s(n_2)$. By this process, we construct finite decreasing sequence $n_k$ ending at $1$ and we say that $forall kin M:k<s(n)$ by transitive property of the order. Most importantly, we are not able to construct any strict lesser number than $n$ itself by applying $s$ to it (because all these numbers are already in $M$) and thus (as said in the inductive step): $forall kin mathbbNsetminus M:s(n)leq k$ and thus $s(n)$ would be the least element in $S$.

If someone was thinking about the term finite, i can definite infiniteness as follows: A set $A$ is infinite if there is a bijection between its proper subset and the set itself. Then finite set is a set which is no infinite. But I am still unable to talk about numbers or how many times do i apply $s$. I could say that we apply $s$ to 1 $n$ times, but again, what is $n$? ... aand we run in circles.

Now, I am really curious about someone's opinion on that, because I see a very biig circular reasoning here. In fact, can i somehow rigorously show that $s(n)$ would be the least element in $S$ in the inductive step of the proof of WOP? Or am i actually completely wrong in something? Honestly, this argument seems weak to me and wouldn't persuade me. Thanks for any useful tips!

Recursively define $K(n) = 1,2,.. n$

$= 1, s(1), s(s(1)),.. s^n-1(1). $

$K(1) = 1 ; K(s(n)) = K(n) cup s(n).$

Similarly, for any other $n$ applications of $s.$