coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] well-ordering axiom (aka Zermelo's theorem)

From: Daniel Schepler <dschepler AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] well-ordering axiom (aka Zermelo's theorem)
Date: Mon, 12 Sep 2016 10:13:57 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=dschepler AT gmail.com; spf=Pass smtp.mailfrom=dschepler AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f42.google.com
Ironport-phdr: 9a23:NwtephVtPSKn0jSPMLH444w1nwXV8LGtZVwlr6E/grcLSJyIuqrYZhSAt8tkgFKBZ4jH8fUM07OQ6PG5HzJQqs/Y6DhCKMUKDEBVz51O3kQJO42sNw7SFLbSdSs0HcBPBhdO3kqQFgxrIvv4fEDYuXao7DQfSV3VPAtxIfnpSMaJ15zkn8j7wZDYYh1JiTyhevsyaUzu9USC/vUR1KBlM+4azgbD6i9DfP0Tzmd1L3qSmQz974G+5sgw3T5XvqcN/shBXKGyRK84QKRcAS5uZ2wu783mrR3OVyOA43IdViMdlR8eUFuN1w3zQpqk6niyjeF6wiTPeJSuFb0=

On Mon, Sep 12, 2016 at 1:58 AM, Daniel de Rauglaudre
<daniel.de_rauglaudre AT inria.fr>
wrote:
> Hi all,
>
> This time, I have a problem to find a definition of the well-ordering
> axiom (for all types, not just nat), aka Zermelo's theorem.

Well, this isn't expanded in terms of only forall/exists as you asked,
but I did prove AC -> ZL -> WO here:

http://www.lix.polytechnique.fr/coq/pylons/contribs/files/ZornsLemma/trunk/ZornsLemma.WellOrders.html#well_orderable

Definition total_strict_order (R:relation T) : Prop :=
forall x y:T, R x y \/ x = y \/ R y x.

Record well_order (R:relation T) : Prop := {
wo_well_founded: well_founded R;
wo_total_strict_order: total_strict_order R
}.

...
Section WellOrderConstruction.

Variable T:Type.
...
Theorem well_orderable: exists R:relation T, well_order R.
--
Daniel Schepler

[Coq-Club] well-ordering axiom (aka Zermelo's theorem), Daniel de Rauglaudre, 09/12/2016
- Re: [Coq-Club] well-ordering axiom (aka Zermelo's theorem), Guillaume Melquiond, 09/12/2016
  - Re: [Coq-Club] well-ordering axiom (aka Zermelo's theorem), Daniel de Rauglaudre, 09/12/2016
- Re: [Coq-Club] well-ordering axiom (aka Zermelo's theorem), Daniel Schepler, 09/12/2016