In constructive mathematics, not (not A) doesn’t imply A: Given some (A → EmptySet) → EmptySet, you’d be hard-pressed to extract an A using the usual methods.
You could try to go: “The (A → EmptySet) → EmptySet must surely use its input, where else would it get an element of EmptySet? So I will attach a debugger to it and watch for when it tries to call its input with some A; then abort the proceedings and return the A it came up with.” But theoretically, you’d need an extra axiom to allow such a trick.
I suspect that the principle is true, but needs more axioms to prove than one would like.
In constructive mathematics, not (not A) doesn’t imply A: Given some (A → EmptySet) → EmptySet, you’d be hard-pressed to extract an A using the usual methods.
You could try to go: “The (A → EmptySet) → EmptySet must surely use its input, where else would it get an element of EmptySet? So I will attach a debugger to it and watch for when it tries to call its input with some A; then abort the proceedings and return the A it came up with.” But theoretically, you’d need an extra axiom to allow such a trick.
I suspect that the principle is true, but needs more axioms to prove than one would like.