Gaëtan Gilbert (Oct 06 2022 at 16:03): Gaëtan Gilbert (Oct 06 2022 at 16:03):What can you say about this type? forall A B, (forall x:A, notnot (B x)) -> notnot (forall x, B x)
Is it inhabited, equivalent to some well known axiom, etc
Gaëtan Gilbert (Oct 06 2022 at 16:04):where Definition notnot A := (A -> False) -> False.
Olivier Laurent (Oct 06 2022 at 20:19):Isn't it Double-Negation Shift?
James Wood (Oct 10 2022 at 08:23):It's something like choice, but must be weaker because it follows from excluded middle/double-negation elimination (rather than the other way round).
Pierre-Marie Pédrot (Oct 10 2022 at 08:27):@James Wood not quite. With B : A -> Type (as opposed to B : A -> Prop) this is not a consequence of excluded middle in Prop.
Last updated: Oct 12 2024 at 12:01 UTC