"Any finite poset has a maximal element." How to formalize the proof that is given? For fun, I'm reading The Mathematics of Logic, and the author gives the following theorem
Theorem. Any finite poset has a maximal element.
and a proof thereof. But, I can't figure out how to formalize the proof. Help, anyone? I was thinking of using reductio ad absurdum.
Here's the proof (I've cut a bit of the fluff, but its more or less verbatim).
Proof. Let $X$ be our finite poset and let $a_0 \in X$. We're going to define a sequence of elements $a_n \in X$ such that $a_n < a_{n+1}$ for each $n$. Given $a_n \in X$, there are two possibilities. Either $a_n$ is maximal, in which case we're finished, or else there is some $b \in X$ with $a_n < b$. In the latter case, choose $a_{n+1}$ to be such a $b$.
Now the argument in the previous paragraph cannot give an infinite sequence of elements of $X$. This is because $X$ is finite and the sequence $a$ is strictly increasing, hence all the terms of $a$ are distinct. Therefore, we cannot always have the second option in the previous paragraph, so at some point the $a_n$ we have obtained will be maximal. That is, our finite poset has a maximal element, as required.
Remark. We're allowed to use Konig's lemma, since this has already been proved.
 A: The given proof glosses over some details, but it's basically complete.
You could use induction on the cardinality of $X$. If $|X|=1$ there's nothing to prove. So let's assume $|X|=n>1$ and that the result holds for posets having cardinality less than $n$.
Pick an element of $X$, call it $a$; if $a$ is maximal, then we're done. Otherwise there's at least an element $b$ such that $a<b$. Consider $Y=\{x\in X: a<x\}$. Then $Y$, with the induced order relation, is a finite poset and $a\notin Y$, so that $|Y|<|X|$. By the induction hypothesis, $Y$ has a maximal element $c$. Let's show that $c$ is also maximal in $X$. If $d\in X$ and $c<d$, then we have $a<c<d$, so $a<d$ and hence $d\in Y$, contradicting the fact that $c$ is maximal in $Y$.
A: Finite sets also allow constructions like "top element of a longest chain", or "element with largest number of descendants". 
A: Let $n(x)$ be the cardinality of $\{y \in X / x < y\}$. Since $X$ is finite, the $n(x)$ are natural numbers, and there is an $x_0$ such that $n(x_0)$ is minimal. Suppose $n(x_0)>0$. Then there is a $y \in X$ such that $x_0<y$, and then $n(y)$ is the size of $\{z \in X / y< z\}$, which is strictly included in $\{z \in X / x_0 < z\}$. Thus $n(y) < n(x_0)$, which contradicts the minimality of $n(x_0)$. Hence $n(x_0)=0$, which means that $x_0$ was a maximal element.
