That’s an interesting point, but I have a couple of replies.
First and foremost, any argument against ‘not not A’ becomes an argument against A if Alice translates back into classical logic in a different way than I’ve assumed she is. Bob’s argument might conclude ‘not A’ (because ¬¬¬A→¬A even in intuitionistic logic), but Alice thinks of this as a tricky intuitionistic assertion, and so she interprets it indirectly as saying something about proofs. For Alice to notice and understand your point would, I think, be Alice fixing the failure case I’m pointing out.
Second, an argument against an assumption need not be an argument for its negation, especially for intuitionists/constructivists. (Excluded middle is something they want to argue against, but definitely not something they want to negate, for example.) The nature of Bob’s argument against Alice’s claim can be quite complex and can occur at meta-levels, rather than occurring directly in the logic. So I guess I’m not clear that things are as simple as you claim, when this happens.
Arguing against A doesn’t support Not A, but arguing against Not Not A is arguing against A (while still not arguing in favor of Not A) - albeit less strongly than arguing against A directly. No back translation is needed, because arguments are made up of actual facts and logic chains. We abstract it to “not A” but even in pure Mathematics, there is some “thing” that is actually being argued (eg, my grass example).
Arguing at a meta level can be thought of as putting the object level debate on hold and starting a new debate about the rules that do/should govern the object level domain.
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.
That’s an interesting point, but I have a couple of replies.
First and foremost, any argument against ‘not not A’ becomes an argument against A if Alice translates back into classical logic in a different way than I’ve assumed she is. Bob’s argument might conclude ‘not A’ (because ¬¬¬A→¬A even in intuitionistic logic), but Alice thinks of this as a tricky intuitionistic assertion, and so she interprets it indirectly as saying something about proofs. For Alice to notice and understand your point would, I think, be Alice fixing the failure case I’m pointing out.
Second, an argument against an assumption need not be an argument for its negation, especially for intuitionists/constructivists. (Excluded middle is something they want to argue against, but definitely not something they want to negate, for example.) The nature of Bob’s argument against Alice’s claim can be quite complex and can occur at meta-levels, rather than occurring directly in the logic. So I guess I’m not clear that things are as simple as you claim, when this happens.
Arguing against A doesn’t support Not A, but arguing against Not Not A is arguing against A (while still not arguing in favor of Not A) - albeit less strongly than arguing against A directly. No back translation is needed, because arguments are made up of actual facts and logic chains. We abstract it to “not A” but even in pure Mathematics, there is some “thing” that is actually being argued (eg, my grass example).
Arguing at a meta level can be thought of as putting the object level debate on hold and starting a new debate about the rules that do/should govern the object level domain.
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.