Skip to content

Instantly share code, notes, and snippets.

@JadenGeller

JadenGeller/LEM.idr

Last active March 29, 2018 18:56
Show Gist options
  • Save JadenGeller/ef18d5d85559785921358e78af366edb to your computer and use it in GitHub Desktop.
Save JadenGeller/ef18d5d85559785921358e78af366edb to your computer and use it in GitHub Desktop.
Download ZIP
Derivation of Law of the Excluded Middle from call/cc
Raw
LEM.idr
%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
@JadenGeller
Copy link
Author 

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))))

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment