3 ms·
Go 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, bu
by waqf 16y ago
Go 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.