4 ms·

Thank you ever so much. I only had to make a few changes to make it work. Providing a computer verified proof is quite a definitive way of winning an argument.

Thank you ever so much. I only had to make a few changes to make it work. Providing a computer verified proof is quite a definitive way of winning an argument. LEM : (x:Type) -> Type LEM x = Either x (x -> _|_) DN : (x:Type) -> Type DN x = ((x -> _|_) -> _|_) -> x notnotLEMproof : {x:Type} -> ((LEM x) -> _|_) -> _|_ notnotLEMproof {x} f = f (Right (\a => f (Left a))) DNimpliesLEM : ((x:Type) -> DN x) -> LEM y DNimpliesLEM {y} dn = dn (LEM y) notnotLEMproof

jules 14y ago
Yes, thank you, I made some stupid mistakes there. I find the last one slightly clearer if you change the argument order: DNimpliesLEM : ((x:Type) -> DN x) -> ((y:Type) -> LEM y) DNimpliesLEM dn y = dn (LEM y) (notnotLEMproof y) Although with the original formulation you could prove the slightly stronger version: DNimpliesLEM : (x:Type) -> DN (LEM x) -> LEM x DNimpliesLEM x dn = dn (notnotLEMproof x) so that you don't need DN z to be true for all z, but just on the z you need (i.e. z = LEM x). It was an interesting exercise, and I learned a lot. First I tried proving (((x:Type) -> LEM x) -> _|_ ->) _|_ to then apply double negation directly to this, but this is actually not possible (as far as I can see). The double negation needs to be inside the quantifier. Maybe you can even write it simply like this with implicit parameters: DNimpliesLEM : DN (LEM x) -> LEM x DNimpliesLEM dn = dn notnotLEMproof