Zulip Chat Archive

Stream: maths

Topic: Zorn's Lemma


view this post on Zulip Kevin Buzzard (Feb 15 2020 at 16:38):

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 ?

view this post on Zulip Chris Hughes (Feb 15 2020 at 16:41):

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

view this post on Zulip Kevin Buzzard (Feb 15 2020 at 16:45):

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

view this post on Zulip Kevin Buzzard (Feb 15 2020 at 16:45):

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)

view this post on Zulip Chris Hughes (Feb 15 2020 at 16:52):

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

view this post on Zulip Kevin Buzzard (Feb 15 2020 at 16:59):

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?

view this post on Zulip Kevin Buzzard (Feb 15 2020 at 17:02):

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)?"

view this post on Zulip Chris Hughes (Feb 15 2020 at 17:07):

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.

view this post on Zulip Chris Hughes (Feb 15 2020 at 17:09):

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.

view this post on Zulip Kevin Buzzard (Feb 15 2020 at 17:10):

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?

view this post on Zulip Kevin Buzzard (Feb 15 2020 at 17:11):

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

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:11):

That's in the API for zorn.chain

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:12):

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

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:12):

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

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:13):

because it doesn't matter

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:13):

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

view this post on Zulip Chris Hughes (Feb 15 2020 at 17:16):

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

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:18):

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

view this post on Zulip Kevin Buzzard (Feb 15 2020 at 17:19):

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

view this post on Zulip Kevin Buzzard (Feb 15 2020 at 17:20):

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.

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:21):

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

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:21):

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

view this post on Zulip Chris Hughes (Feb 15 2020 at 17:21):

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

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:22):

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

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:22):

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

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:23):

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

view this post on Zulip Kevin Buzzard (Feb 15 2020 at 17:24):

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

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:24):

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

view this post on Zulip Kevin Buzzard (Feb 15 2020 at 17:25):

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.

view this post on Zulip Kevin Buzzard (Feb 15 2020 at 17:28):

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.

view this post on Zulip Kevin Buzzard (Feb 15 2020 at 17:29):

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

view this post on Zulip Kevin Buzzard (Feb 15 2020 at 17:30):

These computer guys are supposed to be good at induction.

view this post on Zulip Johan Commelin (Feb 15 2020 at 17:33):

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

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:38):

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

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:40):

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

view this post on Zulip Chris Hughes (Feb 15 2020 at 17:43):

What's the non-obvious extrinsic justification?

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:43):

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

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:44):

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

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:46):

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

view this post on Zulip Chris Hughes (Feb 15 2020 at 17:47):

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

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:47):

I mean a justification of why it should be true

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:47):

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

view this post on Zulip Chris Hughes (Feb 15 2020 at 17:48):

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

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:50):

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

view this post on Zulip Chris Hughes (Feb 15 2020 at 17:52):

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

view this post on Zulip Mario Carneiro (Feb 15 2020 at 17:54):

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

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 22:10):

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).

view this post on Zulip Chris Hughes (Feb 25 2020 at 23:35):

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

view this post on Zulip Reid Barton (Feb 26 2020 at 00:28):

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.

view this post on Zulip Reid Barton (Feb 26 2020 at 00:52):

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.

view this post on Zulip Mario Carneiro (Feb 26 2020 at 00:52):

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

view this post on Zulip Mario Carneiro (Feb 26 2020 at 00:55):

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


Last updated: May 06 2021 at 19:30 UTC