I was thinking about LEM today. Without the oracle, you can prove that the double negation of the law of the excluded middle is true, which can be represented

I was thinking about LEM today. Without the oracle, you can prove that the double negation of the law of the excluded middle is true, which can be represented with the following type: negneg_lem :: ((Either a (a -> r)) -> r) -> r I'm using a polymorphic r to represent the void type, and I'm using the idea that "not a" is the same as "a -> r". The proof of negneg_lem is just negneg_lem f = (f . Right)(f . Left) No oracle there. If you had an oracle oracle :: ((a -> r) -> r) -> a then you would get the normal LEM as lem = oracle negneg_lem An interesting thing about the type (a -> r) -> r, i.e., double negation, is that it is the type for continuation-passing style. This suggests that a classical proof is something which is allowed to do backtracking search, but I'm still trying to understand exactly how that is. (Also, the oracle is somewhat absurd. Really, if you have a function which takes functions, you can produce an element of the function's domain? It might almost make more sense if r was a void type.)