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
Definition notnot A := (A -> False) -> False.
Isn't it Double-Negation Shift?
It's something like choice, but must be weaker because it follows from excluded middle/double-negation elimination (rather than the other way round).
@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: Dec 07 2023 at 09:01 UTC