3 ms·
> that they have to give up law of excluded middle They have to give up the law of the excluded middle because the law of the excluded middle is false. Counter
by a1369209993 6y ago
> that they have to give up law of excluded middle
They have to give up the law of the excluded middle because the law of the excluded middle is false. Counterexample: "This statement is false.". You can pretend it's true by trying to outlaw self-reference, but Godel proved that that doesn't actually work if your logic is useful enough to support arithmetic.
- JoeCamel 6y agoI don't understand what "LEM is false" means. What are your starting assumptions that lead to the "LEM is false" conclusion? You can use/assume LEM in your system or not, most mathematicans assume LEM (without even thinking about it).
- kmill 6y agoI'm not sure what you're talking about, unless you're saying truth is provability. (Classical logic would disagree.) The Lean proof assistant, which has a pretty strong commitment to constructability, has the law of the excluded middle just fine: https://github.com/leanprover/lean/blob/master/library/init/classical.lean#L69 https://github.com/leanprover/lean/blob/master/library/init/... The caveat is that it only exists in Prop, and it's a consequence of proof irrelevance and functional extensionality. Types outside Prop don't have it for the simple reason that there's no sensible way to construct an element of Either A (A -> Void) in general (this is quasi-Haskell notation, where Void is a type with no terms). I'm not sure there's any need to bring Godel into this....