Are there uses of the sledgehammer Zorn's Lemma that are embedded in arguments similar to the more delicate one below, showing that the thing being constructed is actually unique?

Many uses of Zorn's Lemma are equivalent to Choice because it is actually necessary to choose one of many things, eg maximal ideals or points of a frame.

[Strictly, I should have said "unique up to unique isomorphism" in the title: Constructing the algebraic closure of a field may be done with Zorn's Lemma and is unique, but there is a (typically infinite) Galois group of automorphisms. Choice is needed essentially to pick the identity of this group, so this is not an example of what I'm looking for. Unfortunately I don't have a version of this order-theoretic argument generalised to categories with filtered colimits.]

This is a revised attempt to get feedback on the following question that I asked last year. I was led to formulating this fixed point theorem instead of a variation on the Knaster-Tarski one because my setting does not have binary joins. My suspicion is that this situation must occur frequently in algebraic constructions elsewhere.

To try to settle all the misunderstandings of this question, I'm trying to get MO contributors to do the kind of semantic literature search that is not possible with computers: in your knowledge of constructions that use Zorn's Lemma, ordinals, the Knaster-Tarski theorem etc, does the surrounding argument look like anything below? Is my fixed point theorem original, or have others used it before (even implicitly)? If it is original, are there proofs in the literature that could be improved by using it?

Algebraic applications of an order-theoretic idiom of recursion

Many algebraic constructions must surely use the following observation, probably disguised as one of its proofs:

Lemma Let $s:X\to X$ be an endofunction of a poset such that

  • $X$ has a least element $\bot$;
  • $X$ has joins of directed subsets (or chains, classically),
  • $s$ is monotone: $\forall x y.x\leq y\Rightarrow sx\leq s y$;
  • $s$ is inflationary: $\forall x.x\leq s x$;
  • $\forall x y.x=s x\leq y=s y\Rightarrow x=y$.


  • $X$ has a greatest element $\top$;
  • $\top$ is the unique fixed point of $s$;
  • if $\bot$ satisfies some predicate and it is preserved by $s$ and directed joins then it holds for $\top$.

Proof 1 Using the lemma for which Max Zorn denied responsibility, $X$ has at least one maximal element.

If $a$ and $b$ are maximal then there is also $c$ that is maximal with $a\geq c\leq b$. Then $a=s a$ and $b=s b$ since $s$ is inflationary. Since it's also mototone, $c\leq s c\leq s a,s b$, so $c=s c$. By the final condition, $a=c=b$.

This also explains why the "obvious" simple counterexamples aren't.

Proof 2 [added] If $X$ also has binary and therefore all joins, Tarksi's elaboration of Knaster's fixed point theorem says that there is a lattice of fixed points, but the final condition collapses this to just one.

Proof 3 Using ordinal recursion, not forgetting to cite von Neumann to justify that and Hartogs to say when to stop.

Using this argument, we could start from any basepoint, not just $\bot$, but by monotonicity and the final condition, the least fixed point over another basepoint must still be the same as the one over $\bot$.

Proof 4 Using the Bourbaki-- Witt Theorem, that the subset of $X$ generated by $\bot$, $s$ and joins of chains is itself a chain, indeed a well ordered set.

Comparing this with the previous argument, the fifth condition does a similar job as restricting to the subset generated by $\bot$, $s$ and joins of chains.

Proof 5 Using Pataraia's fixed point theorem. Just using composition, the set of monotone inflationary endofunctions of $X$ is directed and therefore has a join (greatest element) $t:X\to X$. Then $t$ is idempotent and its fixed points are also fixed by any $s$. Since $X$ is connected and the set of fixed points of $s$ is discrete, there can only be one of them, which must be the top element of $X$.

Proof of the induction principle The subset of elements satisfying the predicate has the same properties as $X$ itself, so includes $\top$.

This result has some superficial similarity to "Zorn's Lemma", but is superior to it because

  • it produces a unique result and proves properties of it; and
  • Pataraia's proof is constructive (it doesn't use the Axiom of Choice or Excluded Middle, although it is Impredicative).

I am looking for places where this result has been used, and maybe even where it has been identified as above.

The historical reasons for expecting to find it in algebra are:

  • well founded induction is sometimes (though questionably) attributed to Emmy Noether
  • Ernst Witt and Max Zorn were algebraists
  • a rambling proof of the Bourbaki-Witt theorem appears in an appendix to the 9th printing (but not the first) of Serge Lang's Algebra.

I am writing a paper about Well founded coalgebras and recursion. This is a categorical formulation of von Neumann's proof justifying recursion over ordinals, but in a generality without binary unions, which necessitated using Pataraia's theorem. However, it has taken me some months to learn how to use it and formulate the Lemma above.

The fifth condition is the less obvious part. Recall that Alfred Tarski's paper says that there is a lattice of fixed points (in the complete lattice case): this condition reduces the lattice to a single point.

It is common for binary unions to be very complicated or non-existent in algebraic constructions, which is why I believe this result may have occurred many times before.

Dito Pataraia presented his proof at the 65th PSSL in Aarhus in 1996 but never wrote it up before his death in 2011 at the age of 48. I never met him or saw the original version of his proof: I heard that it involved composition and reconstructed it myself, but I don't know what was the punchline of his argument. I am hoping Mamuka Jibladze (@მამუკაჯიბლაძე) will fill in some details.

Trying again to explain myself

My fifth axiom is the essential one, the part that seems to be original with me. It came from a lot of head-scratching: I knew that I had to use Pataraia's fixed point theorem, but it took me a long time to work out how. That is, the idiom.

My Lemma is simple, but sometimes the significance of the simplest things is the hardest to understand.

I asked this question to challenge others to find prior occurrences (to test my claim to originality, if you want to put it in competitive terms): in places where you use Zorn's lemma, ordinals or whatever, but thing is actually unique, what additional fact about your situation entails uniqueness? Is it that there cannot be two fixed points linked by the order?

Yes, I know about ordinals. However, if you make "full disclosure" of your proof using them, you will find that it is a very clumsy beast. It relies on von Neumann's recursion theorem, and Hartogs' Lemma for stabilisation. My observation is that many pure mathematicians do not know these things, even though most set theory textbooks include an (unattributed) proof of the recursion theorem. Stabilisation often goes without any proof at all.

Besides this, the traditional theory of ordinals uses excluded middle at every step. My notion of plump ordinal rectifies this. (@MikeShulman discovered it independently for his construction of the Conway numbers in Homotopy Type Theory). Hartogs' Lemma is apparently irretrievable.

Even if you don't care about excluded middle but you believe G.H. Hardy's maxim that "there is no permanent place in the world for ugly mathematics" you should want to eliminate use of the ordinals from your proofs.

I am asking this question here because I suspect that my Lemma has much wider application, but I came upon it in my (constructive categorical) work on recursion. I originally wanted a constructive account of the ordinals for my book. I built an intuitionistic theory of the ordinals to prove the fixed point theorem, but could not replicate Hartogs' Lemma. Then Pataraia came along with his far simpler proof, and I really "kicked myself", because I had known every step of it but had failed to put them in the right order.

The version of the recursion theorem in Section 7.3 of the book follows von Neumann's proof very closely, but in the setting of well founded coalgebras (which I introduced) for a functor that preserves inverse images. I then left the subject for a long time, but came back to it under provocation, because a certain person was trying to write me out of the history.

The new draft paper only requires the functor to preserve monos, and is applicable in many other categories besides $\mathbf{Set}$. However, several key steps in von Neumann's argument then fail, obliging me to find a more subtle proof using Pataraia's theorem, but not verbatim. I asked this question to try to find out whether anyone else had used my key argument.

Formulation of the Lemma

My first four conditions are familiar properties that are typically verified routinely. If the conclusion holds, the fixed point is unique, so the fifth property actually says that it is sufficient to test that two fixed points linked by the order are equal.

So the key ingredient to set up this situation is really the choice of the poset $X$, maybe as a subset of some other structure $Y$. The Bourbaki--Witt theorem takes $X$ to be the subset generated by $\bot$, $s$ and joins of chains, but I think this kind of begs the question. Section 10 of my draft paper (really an appendix) introduces a notion of "well founded element" $x$ $$ x\;\leq\; s x \quad\mbox{and}\quad \forall u:X.\ (s u \land x \;\leq\; u) \Rightarrow\ x\;\leq\; u, $$ which does the same job, but in a more elementary way. Under stronger hypotheses, $X$ has to be the subset of well founded elements of $Y$.

As I described, my setting is a categorical study of induction and recursion, but I tried to formulate this question without prejudicing the application. However, the previous remark suggests that my Lemma is necessarily about induction.

It would seem that my best hope of an application or previous occurrence of my Lemma outside my own subject is for Noetherian modules or something similar. So I would welcome an example of that.

  • $\begingroup$ Why isn't the flat domain $\{0,1\}_\bot$ with the constant endomap $s(x) = 1$ a counter-example to the claim that there is a greatest element in the poset? Am I misreading "greatest element"? I thought it meant "an element that is above all others". $\endgroup$ – Andrej Bauer Jun 2 '20 at 20:46
  • 2
    $\begingroup$ Without AC, the algebraic closure of a field is not in general unique up to isomorphism. In fact, it is consistent with ZF that the rational field has uncountable algebraic closures as well as countable ones. $\endgroup$ – Joel David Hamkins May 21 at 19:11
  • 1
    $\begingroup$ Isn't it simply incorrect historically to attribute well-founded induction to Noether? This concept is due to Cantor, significantly predating Noether. I said essentially the same in my answer to the post to which you link. $\endgroup$ – Joel David Hamkins May 21 at 19:14
  • 1
    $\begingroup$ I think I already did make them there. That is why I find it peculiar for you to cite that post as evidence that well-founded induction is to be attributed to Noether, since the evidence seems rather settled against that conclusion. $\endgroup$ – Joel David Hamkins May 21 at 19:22
  • 3
    $\begingroup$ Paul, I'm not sure I understand your question. If you are asking whether Zorn's lemma is ever used to prove the existence of something that is later shown to be unique (up to an iso), the answer is of course yes. If you are asking whether Zorn's lemma is ever used in situations where the axiom of choice was not necessary and we only needed well-founded recursion, then the answer is also of course yes. If you are asking about the setting of your lemma, it looks a lot like closure operator theory (but the last condition is extremely strong). $\endgroup$ – Pace Nielsen May 21 at 19:37

Background. Let $P$ be any set, and let $R$ be any reflexive binary relation on $P$. (The reflexive condition merely simplifies the following definition, since given any binary relation we can just pass to its reflexive closure.)

A map ${\rm cl}\colon P\to P$ is called a closure operator if for each $a,b\in P$ it satisfies the following three properties:

(1) extensive (or inflationary): $aR{\rm cl}(a)$,

(2) monotone: $aRb\Rightarrow {\rm cl}(a)R{\rm cl}(b)$, and

(3) idempotent: ${\rm cl}({\rm cl}(a))={\rm cl}(a)$.

Closure operators appear extensively (pun intended) in algebra. For example, as Gerhard Paseman mentioned, they occur prominently in some of George Bergman's work; see his free book "An Invitation to General Algebra and Universal Constructions". (They also occur in my free book "A Journey Through Formal Mathematics".)

Simplification assumption. Closure operators behave much better when $R$ is a poset relation on $P$, and so to simplify the remainder of this answer we will assume that $R=\leq$ is a poset relation.

Classical fact. Suppose $s\colon P\to P$ is any extensive and monotone function. Further suppose that least upper bounds exist for $\leq$-nondecreasing (ordinal-indexed) chains. Then there exists a (unique) closure operator ${\rm cl}\colon P\to P$ with the property that for any $a\in P$ we have ${\rm cl}(a)=a$ if and only if $s(a)=a$.

Proof idea. For each $x\in P$, recursively define the ordinal-indexed sequence $$ x_{\alpha} = \begin{cases} x & \text{ if }\alpha=0,\\ s(x_{\beta}) & \text{ if }\alpha=\beta+1\text{ is a successor, and}\\ \bigvee_{\beta<\alpha}x_{\beta} & \text{ if }\alpha\neq 0\text{ is a limit}. \end{cases} $$ It stabilizes, and we take ${\rm cl}(x)$ to be the stabilization. (After looking online, I see that this idea was also used by Amit Kumar Gupta in his answer to this linked question. I'm sure that this classical fact is proved in some textbook somewhere.)

This generalizes your lemma to avoid that extremely strong fifth axiom, as well as avoid the first axiom about a least element.

Is your lemma always in play? Now, you also asked whether there is any situation in which Zorn's lemma can be applied, the resulting object is unique, and we are not secretly using your lemma. To formalize this, suppose that $\mathscr{P}$ is some property on the elements of a poset $P$ to which Zorn's lemma applies.

Zorn's lemma requires the existence of at least one element $x\in P$ satisfying $\mathscr{P}$. Let $s(x)$ denote the unique(!) Zornification of $x$ (with respect to $\mathscr{P}$). Consider the subset $$ P'=\{x,s(x)\}\subseteq P. $$ It has a least element, all chains in $P'$ have joins, and there is a closure operator sending all elements to $s(x)$. Your fifth axiom is also (nearly vacuously) true.

Thus, a fortiori, we can turn any use of Zorn's lemma (where uniqueness occurs) into an application of your lemma, by modifying your poset.

If we are not allowed to modify the poset it is easy to come up with examples where your axioms 1, 2, or 3 fail (but not 4).

  • $\begingroup$ By the way, if you are interested in the entire poset having a unique closure, rather than locally every element having a unique closure, you can weaken your first axiom to "There is a lower bound (not necessarily a greatest lower bound) for any two element.". Then to show that ${\rm cl}(x)={\rm cl}(y)$, it suffices to consider the case when $x\leq y$. Now, monotonicity yields ${\rm cl}(x)\leq {\rm cl}(y)$. Idempotentence tells us these are ${\rm cl}$-fixed points (equivalently $s$-fixed points). Finally, your axiom 5 yields they are the same closure. $\endgroup$ – Pace Nielsen May 22 at 4:15
  • 1
    $\begingroup$ @PaulTaylor Perhaps my point was lost. Your axioms 2-4 give the existence of a unique closure operator corresponding to the fixed points of $s$. Thus, they are really all you need to obtain (local) unique closures. Your question, as originally expressed, asked whether such uniqueness was a common feature in algebra. As I said, YES, closure operators appear all over the place. Now, your axiom 1 is also a natural condition, because when constructing the closure of $x$ we can focus in on the subposet $\{y\in P\, : \, y\geq x\}$. (continued...) $\endgroup$ – Pace Nielsen May 22 at 15:16
  • 1
    $\begingroup$ But your axiom 5 is not common, because, generally, closure operators are not usually trivial. Closures are a local feature, not a global feature. For instance, in topology, you can have closed sets properly contain each other all the time. In algebra, closed sets (such as normal subgroups of a group, or ideals in a ring, or any other intersection closed subclass) has closed sets poperly containing other closed sets all the time. Thus, as an algebraist, I view your axiom #5 as very odd, which is what I tried to convey in my answer. (continued again...) $\endgroup$ – Pace Nielsen May 22 at 15:23
  • 1
    $\begingroup$ I tried to indicate in my addition that I am well versed in "general" mathematical techniques. I wish I hadn't mentioned algebraic closure, since it is not obtained by iterating some functor on the category of fields. In my setting, property 5 is provided by my notion of well founded coalgebra. So maybe the way to find another example, but in traditional algebra, is to pick up the "Noetherian" idea, although I was equally unsuccessful in getting responses on that. Are you familiar with examples of "Noetherian induction" (for rings or modules)? $\endgroup$ – Paul Taylor May 22 at 16:05
  • 1
    $\begingroup$ Yes, but in my field we also call it "well-founded induction" not Noetherian induction. $\endgroup$ – Pace Nielsen May 22 at 16:43

Let me answer the exact questions Paul asked:

"To try to settle all the misunderstandings of this question, I'm trying to get MO contributors to do the kind of semantic literature search that is not possible with computers: in your knowledge of constructions that use Zorn's Lemma, ordinals, the Knaster-Tarski theorem etc, does the surrounding argument look like anything below? Is my fixed point theorem original, or have others used it before (even implicitly)? If it is original, are there proofs in the literature that could be improved by using it?"

The answer to your first question is yes. As I mentioned in my previous answer, the three conditions "extensive, monotone, and joins of directed subsets exist" imply you are (implicitly) working with a closure operator. Closure operators in ((directed-)complete) posets are plentiful. (I'll give one specific example further below.)

The answer to your second question is no. I linked, in my previous answer, to a question on stackexchange back in 2011 on the matter. It is quite likely to date back much earlier.

The answer to your third question is (ignoring the issue of originality) that this will probably not improve the literature. Here is why. Suppose you are in a situation where you have an extensive, monotone map $s$ on a poset with a least element $x$ and with joins for directed subsets. As mentioned, it is classically known that you have a closure operator corresponding to the fixed points of $s$. Call the closure of your bottom element $\overline{x}$.

Let $y$ be an arbitrary element of your poset. Since $x\leq y$, we have by monotonicity that $\overline{x}\leq \overline{y}$.

Issue #1. To apply your lemma, you would need to verify your fifth axiom, so you'd at least have to prove that $\overline{x}=\overline{y}\geq y$, for every $y$. But, that's just the same thing as verifying that $\overline{x}$ is the top element after all.

To put this another way, verifying your fifth axiom is no different from verifying triviality of the closure operator, and may involve more work.

Issue #2. Your fifth axiom unnecessarily limits you to situations where it holds, whereas most natural situations don't have that fifth axiom even though some form of unique closure exists.

To give a concrete example: Suppose you have a specific group $G$ and a specific subgroup $H\leq G$. You could argue that $H$ has a "normal closure" (i.e., there is a normal subgroup of $G$ containing $H$ that is minimal with respect to those properties) using specifics of the situation. You might even be able to explicitly describe the normal closure of $H$, using transfinite recursion, depending on the specifics.

However, it is much easier to prove the existence of the normal closure by noting that normality is preserved by intersections, and thus there is a closure operator. (Note: Closure operators are in bijection with intersection/join closed subposets, when joins exist).

We can easily modify the situation so that $H$ is the minimal element of the poset at hand, but it is much more difficult to force your axiom 5 to hold (so that, somehow, the only subgroups of $G$ that are under consideration are the ones inside the normal closure of $H$).

By the way, you asked two additional questions: "I asked this question to challenge others to find prior occurrences (to test my claim to originality, if you want to put it in competitive terms): in places where you use Zorn's lemma, ordinals or whatever, but thing is actually unique, what additional fact about your situation entails uniqueness? Is it that there cannot be two fixed points linked by the order?"

The answers to the first question is that I merely use the existence of a closure operator (and the unique thing is then just the closure of the specific object in the poset you want to consider).

My answer to your second question is no. As in the case for normal closures of subgroups, there can be lots of different $s$-fixed points. But, still, for any given subgroup $H$, it has a unique closure. There is a unique minimal $s$-fixed point above every point.

You might object and say that you want to guarantee a unique $s$-fixed point. Even so, my point is two-fold. First, global uniqueness can be (naturally) separated from having a minimal $s$-fixed point (both in your framework, and in many other situations) by merely removing axiom 5. Second, as I previously mentioned, in the case where there is a minimal $s$-fixed point, verifying your fifth axiom is at best just as hard as verifying a unique $s$-fixed point (and, ultimately, they are equivalent using an easy-to-see argument using monotonicity and a bottom element).

  • $\begingroup$ The three conditions "extensive [inflationary], monotone, and joins of directed subsets exist" imply you are (implicitly) working with a closure operator. Wrong. In an application, the one-step operation $s$ may itself be very complicated and (unless it's trivial) we have no way of characterising its closure other than by saying it's the closure. In order theory, constructing the closure requires either your non-constructive ordinal recursion or Pataraia's constructive proof. $\endgroup$ – Paul Taylor May 22 at 21:30
  • $\begingroup$ The question that you linked is Knaster's fixed point theorem from 1927. It is not recorded what his proof was, but it was probably the simple constructive proof using intersections, not the clumsy non-constructive one using ordinal recursion. In fact, von Neumann published his recursion theorem the following year. This result and your subgroup examples depend on using complete lattices, whereas my and other applications lack binary joins. $\endgroup$ – Paul Taylor May 22 at 21:31
  • 1
    $\begingroup$ @PaulTaylor Those two sentences that you quoted and said are "wrong" are not wrong. True, I didn't mention easy characterizations of the corresponding closure operator, but you didn't ask about that, and the closure operator does indeed exist. $\endgroup$ – Pace Nielsen May 22 at 23:37
  • 1
    $\begingroup$ @PaulTaylor (1) When writing an answer on MathOverflow, I try to communicate not only with the question asker, but also with the multitude of readers. Many of those readers are not as familiar with the background information on closure operators; nor did I know exactly what you already knew. It was not my intention to lecture you. (2) One of your main questions was "Is my fixed point theorem original, or have others used it before (even implicitly)?" I don't mean offense when I then mention prior work that subsumes your lemma. $\endgroup$ – Pace Nielsen May 24 at 15:53
  • 1
    $\begingroup$ Yes, he's my coworker. Unfortunately, I don't know him that well, but I only hear very good things about him. $\endgroup$ – Andrej Bauer May 25 at 15:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.