Zorn's Lemma

Stream: maths

[Kevin Buzzard]

theorem exists_maximal_of_chains_bounded
  (h : ∀c, chain c → ∃ub, ∀a∈c, a ≺ ub) (trans : ∀{a b c}, a ≺ b → b ≺ c → a ≺ c) :
  ∃m, ∀a, m ≺ a → a ≺ m :=

Have I just completely misunderstood or should that ≺ be something that a mathematician would usually call ≤?

[Chris Hughes]

It should be a transitive relation. $\le$ is a transitive relation.

[Kevin Buzzard]

Are you telling me that Zorn's Lemma is something weakerstronger than the statement that if $P$ is a partially ordered set with the property that all chains have upper bounds, then $P$ has at least one maximal element?

[Kevin Buzzard]

def zorn.exists_maximal_of_chains_bounded {α : Type u} {r : α → α → Prop} :
(∀ (c : set α), zorn.chain r c → (∃ (ub : α), ∀ (a : α), a ∈ c → r a ub)) →
    (∀ {a b c : α}, r a b → r b c → r a c) → (∃ (m : α), ∀ (a : α), r m a → r a m)

[Chris Hughes]

There's a stronger statement, that implies that version. The proof never uses reflexivity, and antisymmetry turns the final a ≺ m into a = m

[Kevin Buzzard]

The proof never uses reflexivity

As a mathematician I still feel slightly weird about this. Do we ever use this in mathematics when the relation is not reflexive? Is there some lemma saying that if we can prove it in the reflexive case then we can deduce it in the general case by applying the theorem to the reflexification of the relation or something?

[Kevin Buzzard]

I think I'm saying "Can one easily prove zorn.exists_maximal_of_chains_bounded (a statement about transitive relations) from Zorn's Lemma (a statement about partially ordered sets)?"

[Chris Hughes]

I suppose you could take the reflexive closure and quotient by a \le b and b \le a and then prove there's a maximal element in the quotient which can give you a maximal element in the set you started with. But that's kind of silly, you might as well prove it in the correct generality to start with if reflexivity and antisymmetry are never even mentioned in the proof.

[Chris Hughes]

I used the more general version in constructing algebraic closure. The set I was applying it to was partially ordered, but proving antisymmetry was messy and unnecessary.

[Kevin Buzzard]

But this is only because you have some definition of a chain which is also far too general, right? Do you think it would be possible to think of like 5 different definitions of "chain" that happened to work for transitive relations but were all equivalent when applied to partial orders -- which one do you choose for your definition of chain?

[Kevin Buzzard]

For example "for all a and b in the chain, r a b or r b a". That's also "the definition of a chain" for me

[Mario Carneiro]

That's in the API for zorn.chain

[Mario Carneiro]

it's that, when the relation is reflexive, and r a b \/ a = b \/ r b a when the relation is irreflexive

[Mario Carneiro]

mathematicians are also not consistent about whether strict orders can be considered partial orders

[Mario Carneiro]

because it doesn't matter

[Mario Carneiro]

but it so happens that zorn's lemma works with both < and <=

[Chris Hughes]

Isn't there some version of Zorn's lemma where the chains are all well ordered? Is that useful?

[Mario Carneiro]

I'm not sure, but that is another example of the </ <= inconsistency; generally partial orders and preorders are done with <= because that's more convenient, but when talking about well orders < becomes more convenient and authors retrofit that convention

[Kevin Buzzard]

I'm not sure proper mathematicians use well-orders.

[Kevin Buzzard]

Zorn doesn't need them and is probably the way AC is applied most of the time by "proper mathematicians", modulo lots of countable dependent choice done by the analysts.

[Mario Carneiro]

There are occasional constructions by transfinite induction, although maybe you consider it set theory just to use those words

[Mario Carneiro]

Like there is some topology thing where you apply the limit points operation transfinitely many times

[Chris Hughes]

https://www.math.uni-bonn.de/people/scholze/Condensed.pdf Peter Scholze isn't a proper mathematician. This mentions ordinals.

[Mario Carneiro]

or the iterative construction of the Borel sets (maybe that's "descriptive set theory"?)

[Mario Carneiro]

Also things like Hamel bases for vector spaces, dunno how you class that

[Mario Carneiro]

It's just really convenient when you want to say "do it over and over... and over and over until it's done"

[Kevin Buzzard]

Oh I ran into a great article about ideal mathematicians on Twitter!

[Mario Carneiro]

I think @Sebastien Gouezel had an example of this with midpoint construction in his talk in pittsburgh

[Kevin Buzzard]

His talk contained an extremely interesting and surprising (to me) application of the calculus of inductive constructions to do what looked to me like a very elaborate induction proof in an extremely clean way.

[Kevin Buzzard]

It's interesting isn't it. We just say "oh now this is just done by induction" and then people like Reid Barton come along and start saying "hey wait a minute" in his Pittsburgh talk.

[Kevin Buzzard]

@Reid Barton can you do your induction by writing some kind of crazy inductive type like Sebastien did?

[Kevin Buzzard]

These computer guys are supposed to be good at induction.

[Johan Commelin]

@Kevin Buzzard Do you mean this link: https://personalpages.manchester.ac.uk/staff/hung.bui/ideal.pdf

[Mario Carneiro]

Well, Sebastien's point was that the transfinite construction can be replaced by an inductive type, because inductive types do transfinite induction, and of course lean's support for the latter is much better than the former

[Mario Carneiro]

I don't think it's reasonable to argue that the mathematicians had it wrong though, because they are working in a different setting where that construction is not "obvious". I've always viewed the addition of inductive types in CIC as a huge cheat, a tremendous and complicated axiomatic extension with no intrinsic justification and a very non-obvious extrinsic justification

[Chris Hughes]

What's the non-obvious extrinsic justification?

[Mario Carneiro]

If you aren't steeped in belief in the lean way of doing things, it is a completely natural question to ask why the inductive type that Sebastien described should exist, or why it should have those recursion principles, and it amounts to relying on a very heavyweight theorem about inductive types

[Mario Carneiro]

The extrinsic justification is the proof of consistency of lean, which relies on some inaccessible cardinals and some messy set constructions in my thesis

[Mario Carneiro]

Those are the moves a set theory based mathematician would need to perform in order to justify the existence of all of lean's inductive types

[Chris Hughes]

By justification, I thought you meant a motivation for it being there.

[Mario Carneiro]

I mean a justification of why it should be true

[Mario Carneiro]

the motivation is some computer science thing that is probably not accessible to mathematicians

[Chris Hughes]

I guess it's also quite a hard theorem to state on paper, or to understand the statement of.

[Mario Carneiro]

If you are starting from a ZFC-esque foundation, it is a very circuitous route to the goal, and transfinite induction looks more direct

[Chris Hughes]

But that circuitous route has already been proven, so the mathematicians could have just cited that computer science paper when writing their proof.

[Mario Carneiro]

Yes, indeed they could. Kevin probably has a clearer idea of what would happen, but my guess is that the strange subject matter would be more off putting than the fact that the proof is requiring large cardinals for no reason

[Kevin Buzzard]

The Bonk and Schramm proof doesn't use inaccessible cardinals. I was surprised to see that it even needed transfinite induction, because this is rare in mathematics (I only saw it once in a commutative algebra proof in Matsumura's book, and Brian Conrad told me that he knew another proof which didn't use transfinite induction).

[Chris Hughes]

But you could do inductive types in set theory without inaccessible cardinals right?

[Reid Barton]

This is something I've been reading/thinking about recently. There are two well-known ways to construct inductive types in set theory, neither of which requires inaccessible cardinals.

The first is by a transfinite construction (along the lines of the small object argument): Imagine the ordinals index time. Roughly, at each ordinal, add all the terms you don't already have that you can form by applying a constructor to arguments which were added at previous stages. If every constructor has finite arity, you can stop at time omega. If there are constructors of infinite arity, you need to find an ordinal alpha for which any set of ordinals less than alpha indexed by the arity of a constructor has an upper bound which is again at least alpha (basically, a sufficiently large regular cardinal). In ZFC, this is easy: take alpha to be the successor of the sup of the arities of all constructors. In ZF only, this may not work (e.g. a countable union of countable sets may be uncountable) and it is in fact consistent (at least relative to some other mild consistency hypothesis) that no such alpha exists.

The second way is to represent a term of an inductive type as a certain kind of well-founded "tree" (this is where W in W-type comes from, I believe). Each constructor appearing anywhere in such a term has a location specified as a finite list of indices into the arities of the constructors which appear above it in the tree. The term can be recovered from the data of the constructor at every location, so you can define the inductive type to consist of a particular subtype of list I -> J where I is the sum of the arities of all constructors, and J indexes the constructors. This construction works in ZF, and even in any topos with a natural number object.

However, the first construction generalizes to free algebras for algebraic theories which can contain equations, and the existence of such is actually equivalent in ZF to the existence of a proper class of regular cardinals. The Bonk and Schramm proof probably needs something like this, because you need to identify equivalent Cauchy sequences to end up with a metric space (and not a pseudometric space or whatever). Anyways this is all significantly weaker than choice, which for all I know the Bonk-Schramm proof probably uses anyways.

To summarize, to roughly indicate the logical status of inductive constructions, the order of logical strength is something like

elementary topos (roughly, Lean without Type, recursive inductive types like the naturals, or axioms?)
natural number object <=> all inductive types
ZF
ZF + proper class of regular cardinals <=> ZF + free algebras for algebraic theories with equations
ZF + (certain weak forms of choice...)
ZFC
ZFC + there exist countably many inaccessible cardinals (roughly, Lean with everything)
ZFC+U (every set is contained in an inaccessible cardinal), etc.

[Reid Barton]

Based on Sebastien's description of the proof, I would guess it uses exactly ZF + countable choice and from the perspective of logical strength this would be the case whether it is presented using transfinite induction or using inductive types.

[Mario Carneiro]

Now this makes me wonder: Set.{0} biject with Type in lean? It's not exactly clear to me what kind of set Type actually needs to be; clearly it relates to an inaccessible cardinal but it doesn't necessarily have to be one itself. If you do lean without Type, all inductive types that can be constructed exist in ZFC

[Mario Carneiro]

although what exactly "lean without Type" means is not quite clear; you still need to allow Type in certain places, for example on the right hand of typing judgments like A : Type, as well as possibly "presheaves" like F : A -> Type where A : Type