3 ms·
Implication is far less confusing if you are a constructivist.
by trurl 16y ago
Implication is far less confusing if you are a constructivist.
- waqf 16y agoGo on then: as a constructivist, does it follow from "n is even and n is odd" that "n = 17"? Show your work. (Comment: I'm fairly sure I know the answer, but I don't think it's so trivial as to not make for an interesting discussion on HN. In particular, I'm not sure that it's really less or more confusing to the sufficiently uninitiated.)
- trurl 16y agoI don't have time at the moment to give a proof in Coq or another constructive proof assistant, but it boils down to the fact that "n is even and n is odd implies n = 17" is a function that can never be executed.