Proof of the infinite descent principle

Hi everyone I wonder to myself if the next proof is correct. I would appreciate any suggestion.

Proposition: There is not a sequence of natural numbers which is infinite descent.

Proof: Suppose for contradiction that there exists a sequence of natural numbers which is infinite descent. Let $(a_n)$ be such sequence, i.e., $a_n>a_{n+1}$ for all natural numbers n.

We claim that if the sequence exists, then $a_n\ge k$ for all $k, n \in N$.

We induct on $k$. Clearly the base case holds, since each $a_n$ is a natural number and then $a_n \ge 0$ for all $n$. Now suppose inductively that the claim holds for $k\ge 0$, i.e., $a_n\ge k$ for all $n \in N$; we wish to show that also holds for $k+1$ and thus close the induction. Furthermore, we get a contradiction since $a_n \ge k$ for all $k, n \in N$, implies that the natural numbers are bounded.

$a_n>a_{n+1}$ since $(a_n)$ is an infinite descent. By the inductive hypothesis we know that $a_{n+1}\ge k$, so we have $a_n>k$ and then $a_n\ge k+1$.

To conclude we have to show that the claim holds for every $n$. Suppose there is some $n_0$ such that $a_{n_0}<k+1$ so, $\,a_{n_0}\le k$. Then either $\,a_{n_0} = k$ or $\,a_{n_0} < k$ but both cases contradicts our hypothesis. Thus $a_n\ge k+1$ for all $n$, which close the induction.

Thanks :)

I would argue a different way.

By assumption, for all $n$, $a_n > a_{n+1}$, or $a_n \ge a_{n+1}+1$.

Therefore, since $a_{n+1} \ge a_{n+2}+1$, $a_n \ge a_{n+2}+2$.

Proceeding by induction, for any $k$, $a_n \ge a_{n+k}+k$.

But, set $k = a_n+1$. We get $a_n \ge a_{n+a_n+1}+a_n+1 > a_n$.

This is the desired contradiction.

This can be stated in this form: We can only go down as far as we are up.

Note: This sort of reminds me of some of the fixed point theorems in recursive function theory.

Your argument does seem to work. Note that the last paragraph, however, is unnecessary. In the second last paragraph you have shown that $a_n \ge k + 1$ for every $n$ ($n$ was arbitrary here).

Also, your argument seems to be unneccesarily complicated. Here is how I would argue:

Fix any sequence of natural numbers $\left\{a_n\right\}$. Then by definition of natural numbers there are only finitely many $m \le a_0$, therefore we cannot choose infinitely many distinct numbers below $a_0$ and $\left\{a_n\right\}$ does not have infinite descent.