Yes, they are the same assuming ¬¬ϕ = ϕ. But, one interpretation of mathematical truth is something like this: 1. A proposition is the name of a set/type whos

Yes, they are the same assuming ¬¬ϕ = ϕ. But, one interpretation of mathematical truth is something like this: 1. A proposition is the name of a set/type whose elements are proofs of the proposition. 2. A proposition is provable if its set/type is nonempty/inhabited. 3. Implication can be modeled as a function space X → Y. There is some restriction on the kinds of functions allowed, but "continuous" seems to be kind of the idea, in particular only compositions of known continuous functions. 4. The set for "contradiction" is ⊥, which ought to be empty. 5. For negation, we take ¬ϕ to mean ϕ → ⊥, that is, with the truth of ϕ we may construct a contradiction. 6. It is not hard to prove that ϕ → ¬¬ϕ, which is ϕ → ((ϕ → ⊥) → ⊥). In fact, rewriting this as ϕ → (ϕ → ⊥) → ⊥, we can just use "flip ($)" in Haskell, so to speak. 7. But, ¬¬ϕ → ϕ can't be proved directly. The double negation (ϕ → ⊥) → ⊥ as a function space is empty if ϕ is false and has exactly one element if ϕ is provable, so ¬¬ϕ → ϕ would mean that if ϕ is not false then one could obtain one of the proofs of ϕ. You can prove ¬¬(¬¬ϕ → ϕ) directly, though. ("It is not false that ϕ follows from ϕ being not false.") 7.5. I personally find that it is easier to think of ⊥ as an indeterminate set you don't know the elements of rather than just assuming it is empty, for the purpose of understanding the function space interpretation of implication. 8. If you care about classical logic, you can prove that double negation is a monad. It actually turns out that ¬¬¬¬ϕ → ¬¬ϕ, so you only ever need to have a single level of double negation. Double negation from the point of view of function spaces takes empty/nonempty sets to empty/singleton sets. Here's an answer to why stress the difference: sometimes you want to know if the best you can say about a proposition is that it isn't false. That way, you know whether its proof suggests an algorithm for calculating whatever the theorem was about. But if you don't care about the difference, then you can stay inside the double negation monad to get classical logic.