Lessness (Oct 30 2021 at 19:48): 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?
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.
Gaëtan Gilbert (Oct 30 2021 at 19:52):you can also use that ex (fun _ : A + B => True) is equivalent to A \/ B
Lessness (Oct 30 2021 at 19:58):Thank you both.
Notification Bot (Oct 30 2021 at 19:58):Lessness has marked this topic as resolved.
Last updated: Oct 01 2023 at 19:01 UTC