# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorTodd_Trimble
• CommentTimeAug 9th 2018

Indicated where to find (in the nLab) a proof of the equivalence with the axiom of choice and with Zorn’s lemma (<– it’s there).

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeAug 9th 2018

That seems slightly odd, but probably as long as it’s indicated where to find it it doesn’t matter.

1. Would it be OK to remove the discussion box on this page? Probably no need to copy it here; if it is announced on the nForum, we will be able to find it easily again if we ever needed to.

• CommentRowNumber4.
• CommentAuthorTodd_Trimble
• CommentTimeAug 9th 2018

I agree that it seems a little weird, Mike.

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeAug 9th 2018

Sure, the discussion can be removed.

2. Removed old discussion in query box.

• CommentRowNumber7.
• CommentAuthormartinescardo
• CommentTimeJul 22nd 2021

This page claims that the well-ordering principle doesn’t imply excluded middle. But the way the paragraph is written is a bit ambiguous, and it may be interpreted as saying that the well-ordering principle doesn’t seem to imply excluded middle. If the former, does anybody know a reference for this?

• CommentRowNumber8.
• CommentAuthormartinescardo
• CommentTimeJul 22nd 2021
• (edited Jul 22nd 2021)

I asked the same question in the Zulip HoTT chat. Andrew Swan’s answer is that the (inductive) well-ordering principle implies excluded middle (and hence choice, I believe): https://hott.zulipchat.com/#narrow/stream/228519-general/topic/inductive.20well-ordering.20gives.20excluded.20middle.3F/near/246881801

• CommentRowNumber9.
• CommentAuthormartinescardo
• CommentTimeJul 22nd 2021

My student Tom de Jong formalized Swan’s answer in Agda, by the way (also taking into account a question I made after his answer).

• CommentRowNumber10.
• CommentAuthorDavidRoberts
• CommentTimeJul 22nd 2021

Hi Martin, thanks for picking this up.

PS If you want urls to turn into links, you need to surround them with angle brackets, like <https://example.com>, and have the Markdown option selected, to get https://example.com

• CommentRowNumber11.
• CommentAuthormartinescardo
• CommentTimeJul 22nd 2021

Thanks for the angle-bracket hint. Done!

• CommentRowNumber12.
• CommentAuthormartinescardo
• CommentTimeJul 23rd 2021

Fixed an incorrect claim. The well-ordering principle is actually equivalent to the axiom of choice in constructive mathematics, as proved by Andrew Swan (and formalized in Agda by Tom de Jong).

• CommentRowNumber13.
• CommentAuthormartinescardo
• CommentTimeJul 23rd 2021

Fixed Zorn’s lemma as well.

• CommentRowNumber14.
• CommentAuthormartinescardo
• CommentTimeJul 23rd 2021

I’ve added a reference, by John Bell, that Zorn’s Lemma doesn’t imply excluded middle. How do I reference this reference in nLab syntax?

• CommentRowNumber15.
• CommentAuthormartinescardo
• CommentTimeJul 23rd 2021

Improved the reference to Bell.

• CommentRowNumber16.
• CommentAuthorUrs
• CommentTimeJul 23rd 2021
• (edited Jul 23rd 2021)

How do I reference this reference in nLab syntax?

Following the template here I’d do something like this:

• J. L. Bell, Zorn’s lemma and complete Boolean algebras in intuitionistic type theories, The Journal of Symbolic Logic, 62(4):1265–1279, 1997 (doi:10.2307/2275642)
• CommentRowNumber17.
• CommentAuthormartinescardo
• CommentTimeJul 23rd 2021

Removed “if one admits the principle of excluded middle” from the beginning of the page, an assumption which is no longer needed after Andrew Swan.

• CommentRowNumber18.
• CommentAuthormartinescardo
• CommentTimeJul 23rd 2021

Removed “classically” at the beginning of the file, as this assumption is no longer needed.

• CommentRowNumber19.
• CommentAuthorUrs
• CommentTimeJul 23rd 2021

Following up on #16:

In fact we already have a page John Lane Bell, so best to link to it, too.

• CommentRowNumber20.
• CommentAuthormartinescardo
• CommentTimeJul 23rd 2021

Thanks, Urs, for both comments. I will add it later after I study the template.

• CommentRowNumber21.
• CommentAuthormartinescardo
• CommentTimeJul 23rd 2021

Oh, I see that you already did it. Good.

• CommentRowNumber22.
• CommentAuthorUrs
• CommentTimeJul 23rd 2021

By the way, I would re-structure that entry, regarding the material that was already there before you came in:

• the section “Assessment” is hardly worth a section, this should be a \begin{remark} ... \end{remark} and I find even that is unnecessary, as that assessment is at best besides the point (famous as that quote may be)

• the section “History” should be moved down to right before the references, not to distract from genuine content

This way your material “In constructive mathematics” would be moved up to where it’s more relevant, and maybe it should be inside “statement and proof”.

• CommentRowNumber23.
• CommentAuthormartinescardo
• CommentTimeJul 23rd 2021

I agree. I found the “assessment” a bit odd, not in its contents, which is interesting, but in its title.

• CommentRowNumber24.
• CommentAuthormartinescardo
• CommentTimeJul 23rd 2021

• CommentRowNumber25.
• CommentAuthormartinescardo
• CommentTimeJul 23rd 2021

Actually, the “assessment” is better placed where it is, I think. This is because, in “In constructive mathematics” we are actually discussing the topics of the “assessment”. Namely that classically two things are equivalent to choice, about which in “In constructive mathematics” we learn that one is constructively equivalent to choice but the other isn’t. So perhaps I would keep things as they are, but changing the title “assessment”. Maybe “discussion”? Not perfect but perhaps less worse than “assessment”?

• CommentRowNumber26.
• CommentAuthorUrs
• CommentTimeJul 23rd 2021

Have moved the section “History” to right before “References” and turned the section “Assessment” into a remark inside “Statement and proof”.

• CommentRowNumber27.
• CommentAuthormartinescardo
• CommentTimeJul 23rd 2021

Looks good to me.

• CommentRowNumber28.
• CommentAuthormartinescardo
• CommentTimeJul 24th 2021