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$.
Then
- $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.
Best Answer
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).