Second, an argument against an assumption need not be an argument for its negation, especially for intuitionists/constructivists.
Law of noncontradiction is still constructively valid, and constructive logic only rejects the principle of inferring A from ¬A⟹⊥, it doesn’t reject inferring ¬A from A⟹⊥.
(Excluded middle is something they want to argue against, but definitely not something they want to negate, for example.)
You don’t want to negate it in the sense of accepting ¬(A∨¬A), but depending on your variant of constructive math, you might be able to prove something like ¬∀A.(A∨¬A). This is no more mysterious than how you would not want to be able to prove ¬(x=1), as it is equivalent to ∀x.¬(x=1), even though it is true that ¬∀x.x=1. Unbound variables are a mess!
When it comes to constructive mathematics, there are basically two kinds. One is “neutral” constructive math which doesn’t add any nonclassical principles; it is a strict generalization of classical math, and so it doesn’t allow one to prove things like ¬∀A.(A∨¬A), but conversely it also means that all neutral constructive statements are valid classical statements.
The other kind of constructive math comes from the fact that neutral constructive math has models that are inherently incompatible with classical logic, e.g. models where all functions are computable, or where all functions are continuous, or where all functions are differentiable. For such models, one might want to add additional axioms to make the logic better capture the features of the model, but this rules out the classical models. In such logics, one can prove ¬∀A.(A∨¬A) because e.g. otherwise the Heaviside step would be a well-defined function, and the Heaviside step is not computable/continuous/differentiable.
Law of noncontradiction is still constructively valid, and constructive logic only rejects the principle of inferring A from ¬A⟹⊥, it doesn’t reject inferring ¬A from A⟹⊥.
You don’t want to negate it in the sense of accepting ¬(A∨¬A), but depending on your variant of constructive math, you might be able to prove something like ¬∀A.(A∨¬A). This is no more mysterious than how you would not want to be able to prove ¬(x=1), as it is equivalent to ∀x.¬(x=1), even though it is true that ¬∀x.x=1. Unbound variables are a mess!
When it comes to constructive mathematics, there are basically two kinds. One is “neutral” constructive math which doesn’t add any nonclassical principles; it is a strict generalization of classical math, and so it doesn’t allow one to prove things like ¬∀A.(A∨¬A), but conversely it also means that all neutral constructive statements are valid classical statements.
The other kind of constructive math comes from the fact that neutral constructive math has models that are inherently incompatible with classical logic, e.g. models where all functions are computable, or where all functions are continuous, or where all functions are differentiable. For such models, one might want to add additional axioms to make the logic better capture the features of the model, but this rules out the classical models. In such logics, one can prove ¬∀A.(A∨¬A) because e.g. otherwise the Heaviside step would be a well-defined function, and the Heaviside step is not computable/continuous/differentiable.