Stream: Coq users

Topic: ✔ How to derive strong excluded middle axiom?


view this post on Zulip Lessness (Oct 30 2021 at 19:48):

I was reading https://github.com/coq/coq/wiki/CoqAndAxioms, it says that strong excluded middle axiom is derivable from indefinite description and the excluded middle.
I'm trying but for now I'm unsuccessful. Any hints?

view this post on Zulip Pierre-Marie Pédrot (Oct 30 2021 at 19:51):

Use the fact that A + ~A is isomorphic to {b : bool & if b then A else ~A}, and then use choice to go between Prop and Type.

view this post on Zulip Gaëtan Gilbert (Oct 30 2021 at 19:52):

you can also use that ex (fun _ : A + B => True) is equivalent to A \/ B

view this post on Zulip Lessness (Oct 30 2021 at 19:58):

Thank you both.

view this post on Zulip Notification Bot (Oct 30 2021 at 19:58):

Lessness has marked this topic as resolved.


Last updated: Feb 06 2023 at 13:03 UTC