I have been studying ordinals on my own for a few weeks now, and I have just gone through the proof for Hartogs' lemma, that given $S$ a set, $\exists \alpha$ an ordinal s.t. there is no injective function from $\alpha$ to $S$. My next step would be to show this implies $\exists g: \alpha \to S$ a surjection, which I believe requires the Axiom of Choice, since such a surjection should define a well ordering $S$, where $a,b \in S$ have $a<b$ if and only if $\min(g^{-1}(a)) < \min(g^{-1}(b))$.

I'm fairly certain I can show such a surjection exists if I start with any of the following formulations of AoC:

  1. If $S$ is a set, there exists a choice function on $S$.

  2. The Well-Ordering Theorem.

  3. Zorn's Lemma.

  4. Given $S,T$ are two nonempty sets, there exists an injection from $S$ to $T$ or an injection from $T$ to $S$

However, for personal preference, the statement of AoC I wish to use is the following:

$f:S \to T$ is a surjection if and only if $\exists g: T \to S$ s.t. $f \circ g = \text{id}_{T}$,

and I don't want to have to prove the result in a roundabout way by proving one of the 4 given formulations first.

I am having difficulty using the "surjection iff right inverse" statement to show that there are any injections or surjections between a set $S$ and an ordinal $\alpha$ guaranteed by Hartogs' lemma, since I only know that no injections exist from $\alpha$ to $S$, and not that any surjection exists. Any pointers in the right direction (or errors in my thinking) would be appreciated.

  • 3
    $\begingroup$ What does your proof from formulation 1 look like? The new formulation is morally very similar to formulation 1, so the same proof should still work. (proof it implies 1: let $S$ be a set of nonempty sets, and consider the surjection $\{(X, x) : X \in S, x \in X\} \to S$ given by $(X, x) \mapsto X$...). Even if you literally insert this as a step in the proof I think that's barely roundabout. (and it's hard not to have a similar proof, because the formulations are so similar.) $\endgroup$ Commented Oct 30, 2023 at 23:45
  • 1
    $\begingroup$ What makes you think there should be a proof using your formulation that does not pass through any of the other 4 formulations? $\endgroup$ Commented Oct 30, 2023 at 23:52

1 Answer 1


Greenspun's tenth rule:

Any sufficiently complicated C or Fortran program contains an ad hoc, informally-specified, bug-ridden, slow implementation of half of Common Lisp.

This is to mean that sometimes "the right tool is Common Lisp", and insisting on doing it in C or Fortran will invariably require you to implement Common Lisp, and it won't be as good or elegant.

The same thing applies to your situation. It is often the case that if you want to prove $\varphi\to\psi$, you end up proving $\varphi\leftrightarrow\varphi'$ and $\varphi'\to\psi$. Sometimes this will be done "openly" via some lemma or claim, and sometimes it is just embedded into the proof.

For example, the vast majority proofs that use Zorn's Lemma actually include an ad-hoc implementation of the Teichmüller–Tukey Lemma in them, which if you really think about it, tends to be the right tool for the job after all. Some authors who write about set theory and wish to avoid ordinals will write proofs of equivalences where you can see the bad and "bug ridden" implementation of ordinals come in.

Saying that you want to prove something directly and not in a roundabout way is fine. But will very often result in just an ad-hoc intermediate proof.

So, one such way, would be defining a surjection from $\{(T,s)\mid T\subseteq S, s\in T\}$ onto $\mathcal P(S)\setminus\{\varnothing\}$ given by the obvious projection map, then picking an inverse of that. Using this inverse defining by recursion an injection $S\to\alpha$, which will then give you a surjection from $\alpha$ onto $S$.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .