Skip to content

Instantly share code, notes, and snippets.

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

Embed
What would you like to do?
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
@JadenGeller

This comment has been minimized.

Copy link
Owner Author

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))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.