I give only maybe a 50% chance that any of the following adequately addresses your concern.
I think the succinct answer to your question is that it only matters if you happened to give me, e.g., a “2” (or anything else) and you asked me what it was and gave me your {0,1} set. In other words, you lose the ability to prove that 2 is 1 because it’s not 0, but I’m not that worried about that.
It appears to be commonly said (see the last paragraph of “Mathematical Constructivism”), that proof assistants like Agda or Coq rely on not assuming LoEM. I think this is because proof assistants rely on the principle of “you can’t prove something false, only true.” Theorems are the [return] types of proofs, and the “False” theorem has no inhabitants (proofs).
The law of the excluded middle also seems to me like an insistence that certain questions (like paradoxes) actually remain unanswered.
That’s an argument that it might not be true at all, rather than simply partially true or only not true in weird, esoteric logics.
Besides the one use-case for the paradoxical market: “Will this market resolve to no?” Which resolves to 1⁄2 (I expect), there may be also:
Start with two-valued logic and negation as well as a two-member set, e.g., {blue, yellow}. I suppose we could also include a xϵ{blue,yellow}. So including the excluded middle might make this set no longer closed under negation, i.e., ~blue = yellow, and ~yellow = blue, but what about green, which is neither blue nor yellow, but somehow both, mysteriously? Additionally, we might not be able to say for sure that it is neither blue nor yellow, as there are greens which can be close to blue and look bluish, or look close to yellow and look yellowish. You can also imagine pixels in a green square actually being tiled blue next to yellow next to blue etc., or simply green pixels, each seem to produce the same effect viewed from far away.
So a statement like “x = blue” evaluates to true in an ordinary two-valued logic if x = blue, and false otherwise. But in a {0, 1⁄2, 1} logic, that statement evaluates to 1⁄2 if x is green, for example.
It appears to be commonly said (see the last paragraph of “Mathematical Constructivism”), that proof assistants like Agda or Coq rely on not assuming LoEM. I think this is because proof assistants rely on the principle of “you can’t prove something false, only true.” Theorems are the [return] types of proofs, and the “False” theorem has no inhabitants (proofs).
Not clear what you mean by “because proof assistants rely on the principle of “you can’t prove something false, only true”. There’s a sense in which all math relies on this principle, and therefore proof assistants also rely on it. But proof assistants don’t rely on it more than other math does. If you make inconsistent assumptions within Agda or Coq, you can prove False, just as in any other math. And they follow the principle of explosion.
But yes, proof assistants often reject the law of excluded middle. They generally do so in order to obtain two properties known as the disjunction property and the existence property. The disjunction property says that if P∨Q is provable, then either P is provable or Q is provable. The existence property says that if ∃x.P(x) is provable, then there is an expression t such that P(t) is provable.
These properties reflect the fact that proofs in Agda and Coq carry a computational meaning, so one can “run” the proofs to obtain additional information about what was proven.
One cannot have both the disjunction property and the law of excluded middle, because together they imply that the logic is complete, and consistent logics capable of expressing arithmetic cannot be complete by Gödel’s incompleteness theorems.
Also if you are getting into proof assistants then you should probably be aware that they use the term “truth-values” in a different way than the rest of math. In the rest of math, truth-values are an external thing based on the relationship between a statement and the domain the statement is talking about. However, in proof assistants, truth-values are often used to refer to the internal notion of subsets of a one-element set; P({1}).
So while it is not equivalent to excluded middle to say that either a statement is true or a statement is false, it is equivalent to excluded middle to say that a subset of {1} is either Ø or is {1}. The logic being that if you have some proposition P, you could form the subset S={P|x in {1}}, and if P then by definition S is {1} and if not P then by definition S=Ø, so if P or not P then S={1} or S=Ø.
I give only maybe a 50% chance that any of the following adequately addresses your concern.
I think the succinct answer to your question is that it only matters if you happened to give me, e.g., a “2” (or anything else) and you asked me what it was and gave me your {0,1} set. In other words, you lose the ability to prove that 2 is 1 because it’s not 0, but I’m not that worried about that.
It appears to be commonly said (see the last paragraph of “Mathematical Constructivism”), that proof assistants like Agda or Coq rely on not assuming LoEM. I think this is because proof assistants rely on the principle of “you can’t prove something false, only true.” Theorems are the [return] types of proofs, and the “False” theorem has no inhabitants (proofs).
The law of the excluded middle also seems to me like an insistence that certain questions (like paradoxes) actually remain unanswered.
That’s an argument that it might not be true at all, rather than simply partially true or only not true in weird, esoteric logics.
Besides the one use-case for the paradoxical market: “Will this market resolve to no?” Which resolves to 1⁄2 (I expect), there may be also:
Start with two-valued logic and negation as well as a two-member set, e.g., {blue, yellow}. I suppose we could also include a xϵ{blue,yellow}. So including the excluded middle might make this set no longer closed under negation, i.e., ~blue = yellow, and ~yellow = blue, but what about green, which is neither blue nor yellow, but somehow both, mysteriously? Additionally, we might not be able to say for sure that it is neither blue nor yellow, as there are greens which can be close to blue and look bluish, or look close to yellow and look yellowish. You can also imagine pixels in a green square actually being tiled blue next to yellow next to blue etc., or simply green pixels, each seem to produce the same effect viewed from far away.
So a statement like “x = blue” evaluates to true in an ordinary two-valued logic if x = blue, and false otherwise. But in a {0, 1⁄2, 1} logic, that statement evaluates to 1⁄2 if x is green, for example.
Not clear what you mean by “because proof assistants rely on the principle of “you can’t prove something false, only true”. There’s a sense in which all math relies on this principle, and therefore proof assistants also rely on it. But proof assistants don’t rely on it more than other math does. If you make inconsistent assumptions within Agda or Coq, you can prove False, just as in any other math. And they follow the principle of explosion.
But yes, proof assistants often reject the law of excluded middle. They generally do so in order to obtain two properties known as the disjunction property and the existence property. The disjunction property says that if P∨Q is provable, then either P is provable or Q is provable. The existence property says that if ∃x.P(x) is provable, then there is an expression t such that P(t) is provable.
These properties reflect the fact that proofs in Agda and Coq carry a computational meaning, so one can “run” the proofs to obtain additional information about what was proven.
One cannot have both the disjunction property and the law of excluded middle, because together they imply that the logic is complete, and consistent logics capable of expressing arithmetic cannot be complete by Gödel’s incompleteness theorems.
Also if you are getting into proof assistants then you should probably be aware that they use the term “truth-values” in a different way than the rest of math. In the rest of math, truth-values are an external thing based on the relationship between a statement and the domain the statement is talking about. However, in proof assistants, truth-values are often used to refer to the internal notion of subsets of a one-element set; P({1}).
So while it is not equivalent to excluded middle to say that either a statement is true or a statement is false, it is equivalent to excluded middle to say that a subset of {1} is either Ø or is {1}. The logic being that if you have some proposition P, you could form the subset S={P|x in {1}}, and if P then by definition S is {1} and if not P then by definition S=Ø, so if P or not P then S={1} or S=Ø.