Stream: Miscellaneous

Topic: logic quiz


view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Oct 06 2022 at 16:04):

where Definition notnot A := (A -> False) -> False.

view this post on Zulip Olivier Laurent (Oct 06 2022 at 20:19):

Isn't it Double-Negation Shift?

view this post on Zulip 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).

view this post on Zulip 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: Jan 29 2023 at 18:03 UTC