(And, refining the logical system to include bounds due to computational complexity, you need a path that is realistic in finite time.)
It also doesn't apply in Hegelian logic: ~A is literally everything that isn't A - and negating is likely undefined, since there is nothing in the universe that makes it necessary (regardless of sufficiency) for ~EverythingElse to necessarily mean that anything is left over, let along something as specific as A.
Unless A is somehow unspecific, in which case even ~A is likely defined and potentially meaningless.
I think the two worst intellectual holdovers in Western thought are Aristotelianism - and especially the law of the excluded middle - and Descartes' broader thinking - and especially his duality and "Cogito Ergo Sum": Both were really useful as developments in epistemology and logic, but both have outlived their then-value. We have moved on.
They are not even particularly useful as logical pablum for children, because it is too easy to assume forever that they are 100% reliable and valid - they are useful rules of thumb, they apply in many common, real world cases, but they are, logically, nothing more than extremely useful heuristics.
One can build vast systems with them, but one eventually hits Gödel and Aaronson, e.g., and one realizes the systems are built on less than sand.
Once one gets past them, one can begin to grok where mathematics and physics are now. But they are hard to break away from.
> The double-negation holds in propositional logic
Double-negation isn't a proposition, so don't know what this means. Double-negation elimination, that is, the proposition: for all A, ~ (~ A) -> A does not hold in constructive logic.
However, double-negation introduction, that is, the proposition: for all A, A -> ~(~ A) does definitely hold in constructive logic. Here is a proof in Coq:
Theorem A_implies_not_not_A : forall A : Prop, A -> ~ (~ A).
apply (H0 H).
So, not-not-provable doesn't necessarily imply provable (since it could just be an open question). But, provable does imply not-not-provable (since by definition it isn't unprovable).
So, I should have said, "do you believe not-not-A implies A?" without the initial assumption that A is true (which, ironically, I added later in a comment edit thinking I was adding clarity...)
(Which is correct, and what I was about to point out until I saw you already did!)
After explaining the difference between subset and strict_subset, they claim that for all A
empty_set strict_subset A
which obviously fails when A is itself empty.