Is there a way to deduce Zorn's lemma from Zermelo theorem (that any set may be well ordered), which is essentially shorter then deduction of Zorn's lemma from the usual form of Axiom of Choice? 



Zorn's lemma via Zermelo theorem
*I assume the "usual proof" goes by defining the obvious chain of elements $p\_\eta$ by induction on $\eta$, and then arguing that that constitutes a chain with no upper bound.*


I'm not sure if this counts, but: let $<$ be a well-ordering of the set of chains through $\mathbb{P}$. Now we can define a sequence of chains $C\_\eta$ as: $C\_\eta$ is the $<$-least chain such that $$\forall \beta<\eta, C\_\beta\subsetneq C\_\eta.$$ If we assume that $\mathbb{P}$ satisfies the hypothesis of Zorn's lemma but has no maximal elements - equivalently, that every chain $C$ through $\mathbb{P}$ has an upper bound not contained in $C$ - then $C\_\eta$ exists for every ordinal $\eta$, which is a clear contradiction once we let $\eta$ exceed the cardinality of the set of chains.


Of course this still hinges on a transfinite induction/recursion argument - as Asaf comments, transfinite recursion is basically the only technique we have for utilizing well-orderings, so I don't think there's going to be a proof which avoids it. But notice that in this proof these arguments are pretty easy: 


* The recursion defining $C\_\eta$ is very short.
* To argue that $C\_\eta$ always exists, only the limit case is at all interesting, and even then we only need the fact that $\bigcup\_{\beta<\eta} C\_\beta$ is a chain.


Additionally, to me at least this seems more direct than the usual one - in particular, we never need dirty our hands with individual elements of $\mathbb{P}$.


I'm not sure this satisfies the OP, though.




---


Having just written this, now let me argue that it stinks, at least in one respect dear to my heart:


The usual proof uses a well-ordering of $\mathbb{P}$, whereas this one uses a well-ordering of $Chain(\mathbb{P})$, the set of chains through $\mathbb{P}$. Clearly a well-ordering of the latter yields a well-ordering of the former (even "effectively," although some care must be taken to pin down what "effectively" means here); meanwhile it is consistent with $ZF$ that $\mathbb{P}$ is well-orderable but $Chain(\mathbb{P})$ is not (e.g., take $\mathbb{P}$ to be the usual ordering on $\omega$).


So, if we are interested in the *inherent logical strength* of Zorn's lemma, and not just its truth, then this proof is extremely bad.


This interest in logical strength, and in proofs which are "efficient" in terms not of length but of axioms used, is the driving force behind *reverse mathematics*, which has been investigated extensively over the last few decades. Unfortunately for us, reverse mathematics lives in the realm of second-order arithmetic, that is, it focuses only on natural numbers and sets of natural numbers. This is really the wrong setting for Zorn's lemma. So, even though we can give an intuitive reason for the proof above being "bad" from the point of view of reverse math, it's not clear that we can make this precise.


Fortunately, we're getting there! Over the last few years, interest in *higher-order* reverse mathematics has developed: for example, see <http://www.brics.dk/RS/00/49/BRICS-RS-00-49.pdf> which introduced HORM, <http://arxiv.org/abs/1502.03618> on HORM and nonstandard analysis, and <http://arxiv.org/abs/1109.3902> for a study of ultrafilters in HORM. This provides a system and base theory over which we can reasonably study actual choice principles. So far this has not been investigated very much; however, let me mention one result you may find interesting.


Consider the following two choice principles: (1) "The reals are well-ordered" and (2) "Every real-indexed family of nonempty sets of reals has a choice function." The former clearly implies the latter - just pick the least element out of each set - but this proof requires a nontrivial amount of comprehension (specifically, ($\Pi^1\_1$ with type-2 parameters)-comprehension for type-2 functionals). From the effective point of view, the situation is far from clear. It turns out that this implication is false: over any reasonable$^1$ (from the point of view of effective mathematics) base theory, (1) does not imply (2), in fact (1) and (2) are incomparable. This proof isn't really written up yet, but a typo-y version can be found in my paper <http://arxiv.org/pdf/1310.5792v1.pdf> (page 16).


The natural question to ask at this point is: "Is there a reasonable base theory for higher-order reverse mathematics which proves the implication 'well-ordering implies Zorn' but not 'well-ordering implies choice'?" I strongly suspect the answer is "no."




---


$^1$Okay yes this is provocative nonsense, but one can isolate hypotheses on the base system which are fairly convincing from the point of view of computability theory and which imply the separation mentioned.


