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.
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.