3 ms·

Here is the thing you're looking for. LEM is law of excluded middle, DN is double negation elimination law. Lets define some type abbreviations: LEM = (x:T

by jules 14y ago

Here is the thing you're looking for. LEM is law of excluded middle, DN is double negation elimination law. Lets define some type abbreviations: LEM = (x:Type) -> Either x (x -> _|_) DN = (x:Type) -> ((x -> _|_) -> _|_) -> x We first constructively prove not not LEM: notnotLEMproof : (x:Type) -> ((LEM x) -> _|_) -> _|_ notnotLEMproof x f = f (Right (\a -> f (Left a)) Now we can use double negation to obtain a proof for LEM: DNimpliesLEM : DN -> LEM DNimpliesLEM dn x = dn (LEM x) (notnotLEMproof x) I hope this is correct, since I don't know Idris syntax. If Idris supports implicit parameters, you would not need the x's: notnotLEM f = f (Right (\a -> f (Left a)) DNimpliesLEM dn = dn LEM notnotLEMproof

DanWaterworth 14y ago
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

by jules 14y ago

DanWaterworth 14y ago

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