Instantly share code, notes, and snippets.

# JadenGeller/LEM.idr Last active Mar 29, 2018

Derivation of Law of the Excluded Middle from call/cc
 %default total postulate callCC : ((a -> Void) -> a) -> a peirce : ((a -> b) -> a) -> a peirce f = callCC (f . (void .)) notExcludedMiddleImpliesExcludedMiddle : Not (Dec p) -> Dec p notExcludedMiddleImpliesExcludedMiddle notExcludedMiddle = No (notExcludedMiddle . Yes) excludedMiddle : Dec a excludedMiddle = peirce notExcludedMiddleImpliesExcludedMiddle
Owner Author

### JadenGeller commented Dec 8, 2017

 ```excludedMiddle : Dec a excludedMiddle = peirce notExcludedMiddleImpliesExcludedMiddle excludedMiddle = callCC (notExcludedMiddleImpliesExcludedMiddle . (void .)) excludedMiddle = callCC (\x => notExcludedMiddleImpliesExcludedMiddle ((void .) x)) excludedMiddle = callCC (\x => No (((void .) x) . Yes)) excludedMiddle = callCC (\x => No ((void . x) . Yes)) excludedMiddle = callCC (\x => No ((void . x) . Yes)) excludedMiddle = callCC (\x => No (\y => (void . x) (Yes y))) excludedMiddle = callCC (\assumption => No (\contradiction => void (assumption (Yes y))))```