Richard Barrell3d ago
Slava Pestov
Everyone is posting jokes about constructive logic lately. I personally don’t think they’re funny, but I also don’t think they’re not funny, either
Aug 31, 2025 at 1:07amWeb
Show threadPer VognsenAug 31, 2025
@slava I like this old MO answer by @andrejbauer, https://mathoverflow.net/questions/25363/au-revoir-law-of-excluded-middle/25385#25385. Also, natural language jokes about LEM tend to accidentally be jokes about the law of non-contradiction.
Au revoir, law of excluded middle?

In what way and with what utility is the law of excluded middle usually disposed of in intuitionistic type theory and its descendants? I am thinking here of topos theory and its ilk, namely synthetic

MathOverflow
Show threadVicente ⁂Oct 10
@slava made me groan but in a good way