5 ms·

I care about LEM because I'm not very happy with the computational content of LEM. I know it can be interpreted as "proceed according to $not-A$; if you find a

I care about LEM because I'm not very happy with the computational content of LEM. I know it can be interpreted as "proceed according to $not-A$; if you find a contradiction by building an $A$, wind back the universe and proceed with the resulting proof of $A$", but this feels unsettling to me. Ex-falso has trivial computational content, and we use it all the time: it's `panic!()`. (I agree that there are formulations which don't require LEM, but it's important to be precise, especially when writing to dismiss a common misconception among people who haven't got the concepts crisply in their minds. "Is this quantity computable?" is very close in spirit to "can I compute the value of this quantity?", and LEM is exactly the kind of axiom which shows the difference.)

denotational 2y ago
> I'm not very happy with the computational content of LEM > Ex-falso has trivial computational content, and we use it all the time: it's `panic!()`. I have major issues with the computational content of a bottom type; my interpretation of the BHK semantics would not admit ex falso as constructive. Of course this all of this really stems from one’s notion of semantic truth: any non-trivial semantic theory of truth can be argued as the “one true logic”, and there’s not much anyone can say otherwise! As I see it, it really comes down to how useful it turns out to be in modelling the particular domain of discourse. As it happens, I’m more than happy to accept classical logic: I believe the principle of bivalence is how the world works, and as a result I’m forced to admit LEM if I want my proof calculus to be complete. You are right that pointing out the connection to LEM is important and worthwhile, regardless of formulation.
- Smaug123 2y ago
  By the way, an argument for ex-falso which I found very compelling: Take "False" to be syntactic sugar for "0 = 1"; then you can prove by induction that if False then all numbers are equal. That gives you a great deal of quodlibet completely soundly (since by induction on list-length, all lists are then equal to the empty list, and so on).

denotational 2y ago

> I'm not very happy with the computational content of LEM > Ex-falso has trivial computational content, and we use it all the time: it's `panic!()`. I have major issues with the computational content of a bottom type; my interpretation of the BHK semantics would not admit ex falso as constructive. Of course this all of this really stems from one’s notion of semantic truth: any non-trivial semantic theory of truth can be argued as the “one true logic”, and there’s not much anyone can say otherwise! As I see it, it really comes down to how useful it turns out to be in modelling the particular domain of discourse. As it happens, I’m more than happy to accept classical logic: I believe the principle of bivalence is how the world works, and as a result I’m forced to admit LEM if I want my proof calculus to be complete. You are right that pointing out the connection to LEM is important and worthwhile, regardless of formulation.

Smaug123 2y ago
By the way, an argument for ex-falso which I found very compelling: Take "False" to be syntactic sugar for "0 = 1"; then you can prove by induction that if False then all numbers are equal. That gives you a great deal of quodlibet completely soundly (since by induction on list-length, all lists are then equal to the empty list, and so on).