5 ms·

I've tried to do so in Idris, but I haven't been able to: deriveExcludedMiddle : ((x:Type) -> ((x -> _|_) -> x) -> x) -> Either y (y -> _|_) So, perhaps I

I've tried to do so in Idris, but I haven't been able to: deriveExcludedMiddle : ((x:Type) -> ((x -> _|_) -> x) -> x) -> Either y (y -> _|_) So, perhaps I am relying on one of those logics where it doesn't hold.

jules 14y ago
Shouldn't that be ((x -> _|_) -> _|_) -> x) and the y's at the end should presumably x's. And shouldn't the quantification over x:Type be separately over each part?
- DanWaterworth 14y ago
  (((x -> _|_) -> _|_) -> x) would be the type of double negative reduction. I'm not entirely sure what the type should be. Perhaps, (((x -> _|_) -> (y, y -> _|_)) -> x) is more accurate. In any case, each of the three types are equivalent. I wanted: (forall x. ((~x) -> x) -> x) -> (forall y. y \/ (~y)) Rather than: (forall x. (((~x) -> x) -> x) -> x \/ (~x))
  - jules 14y ago
    Proof by contradiction goes like this: You assume ~x, and from this you derive a contradiction _|_. Then you conclude x. So from ~x -> _|_ we derive x. In other words: (~x -> _|_) -> x. That's the same as ((x -> _|_) -> _|_) -> x. But in any case, as you said, this is equivalent to (~x -> x) -> x because ~x -> x is equivalent to ~x -> _|_.
    - DanWaterworth 14y ago
      I think strictly speaking, _|_ isn't a contradiction, it's an absurdity. (x, x -> _|_) is a contradiction.
      - jules 14y ago
        Ah I see, that's where the terminological differences came from.
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

jules 14y ago

Shouldn't that be ((x -> _|_) -> _|_) -> x) and the y's at the end should presumably x's. And shouldn't the quantification over x:Type be separately over each part?

DanWaterworth 14y ago
(((x -> _|_) -> _|_) -> x) would be the type of double negative reduction. I'm not entirely sure what the type should be. Perhaps, (((x -> _|_) -> (y, y -> _|_)) -> x) is more accurate. In any case, each of the three types are equivalent. I wanted: (forall x. ((~x) -> x) -> x) -> (forall y. y \/ (~y)) Rather than: (forall x. (((~x) -> x) -> x) -> x \/ (~x))
- jules 14y ago
  Proof by contradiction goes like this: You assume ~x, and from this you derive a contradiction _|_. Then you conclude x. So from ~x -> _|_ we derive x. In other words: (~x -> _|_) -> x. That's the same as ((x -> _|_) -> _|_) -> x. But in any case, as you said, this is equivalent to (~x -> x) -> x because ~x -> x is equivalent to ~x -> _|_.
  - DanWaterworth 14y ago
    I think strictly speaking, _|_ isn't a contradiction, it's an absurdity. (x, x -> _|_) is a contradiction.
    - jules 14y ago
      Ah I see, that's where the terminological differences came from.

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