You are right that for a particular formula p, the implication (~p ∨ p) ⇒ (¬¬p ⇔ p) is an intuitionistic tautology and that the reverse implication is not (in general).

However the situation is different when you quantify over all formulas. If you have (¬¬p ⇔ p) for _any_ formula p, you also have (~q ∨ q) for any formula q (written with a different letter to not get lost in variable capturing issues).

This is because, for any formula q, we have the intuitionistic tautology ~~(~q v q). (Proving this is a fun exercise. If you get stuck, see page 26 of https://github.com/iblech/talk-constructive-mathematics/raw/... or elsewhere on the Internet.) So, if you assume the principle of double negation for all formulas, then in particular you assume that, for any formula q, the implication ~~(~q v q) ⇒ (~q v q) holds. Since the antecedent is unconditionally valid, the consequent is as well. Thus you have the law of excluded middle for q.

I highly recommend Andrej Bauer's blog for such matters. The post http://math.andrej.com/2008/08/13/intuitionistic-mathematics... is a good starting point.

You melted my brain. What does “quantify over all formulas” mean?

From the way you state it, that's an interesting perspective. But it seems to be from a perspective of totality which I'm wary of. Not saying you're wrong, going to check out those links. Andrej Bauer was very kind to answer an out-of-the-blue email query of mine once :)

Seriously appreciative of your response, a thousand thanks!

EDIT: Ok, I've read your paper/slides. Very interesting. Don't you show that for specific constructions you can make LEM work for classical proofs with continuation monads? How does that show that _in general_ in constructive mathematics that the implication (~p ∨ p) ⇒ (¬¬p ⇔ p) holds but not its inverse? Also, your bit about rewinding time makes complete sense imho because classical logic is atemporal and continuation monads inject the idea of flowing time into those proofs in a controlled manner.

EDIT 2: I _highly_ reccommend Dennis E. Hesseling's Gnomes in the Fog: The Reception of Brouwer's Intuitionism in the 1920s which I think gives a different slant on what Brouwer actually claimed than what you might imagine if you go with Andrej Bauer's interpretation. I can shoot you a copy if you can't lay your hands on it online :)

Sorry, didn't intend to use so much jargon. By "quantifying over all formulas" I just meant that one has to distinguish between the following two statements:

1. The law of excluded middle holds for a particular formula p.

2. The law of excluded middle holds for _all_ formulas p.

Also note that "formula" just means "formal logical statement", i.e. structured string consisting of v, ==>, and so on.

What do you mean by "perspective of totality"?

Regarding your first edit: There is indeed a metatheorem which says "any classical proof can be turned into a constructive proof". The catch is that this does _not_ apply to all formulas (of course, else the discussion would be moot), but only to formulas of a special kind. Not many formulas are of this kind, but for instance "There exist infinitely many prime numbers" and "A particular Turing machine halts" are (when suitably formulated). If you want to lookup the details, look for "Friedman's Trick".

That the implication (~p ∨ p) ⇒ (¬¬p ⇔ p) holds is because there is a direct proof of this. I didn't show (here or in the slides) that the reverse implication is not intuitionistically valid. A simple way to do this would be to proceed along your lines, that is construct a Heyting algebra in which (¬¬p ⇔ p) holds for a particular element p but in which (~p v p) does not holds for this p. A fancier way would be to look at toposes arising "in nature", not specifically constructed for giving a counterexample.

Thanks for the book recommendation! I'll check it out. I won't have Internet over the weekend but I'd be glad to continue the discussion later.

I too would be glad, it's been enlightening already. We have common interests it seems :)

By structured string you mean well-formed formula I guess.

"perspective of totality" means taking all `things' together at once (if that were possible)

Careful: https://en.wikipedia.org/wiki/Principle_of_bivalence#Relatio...

In other words, what you wrote is that every value when negated twice returns to itself. Here's a truth table of 3 values for the negation operator

     v | 0 | 1 | 2
    --------------
    ¬v | 1 | 0 | 2

So ¬¬0 ⇔ 0 and ¬¬1 ⇔ 1 and ¬¬2 ⇔ 2 which satisfies the principle of double negation but not LEM. Correct?

Your counterexample could work, but it is not obvious that it does so. This is because you also have to give definitions of ∧, v, and ==>, and then check that your definitions satisfy the axioms of intuitionistic logic.

As stated, your example only shows that one can define a function f on a set which contains more than two elements such that f . f = id. But this by itself is a trivial statement.

Once those definitions are given then my trivial example holds though, correct?

Which are you saying; that it is, or, it is not possible to give those definitions?

I didn't check it. If you want to do it (the key step being to verify that the axioms of intuitionistic logic holds for your definitions of AND and OR), you can check Wikipedia for the list of axioms to verify: https://en.wikipedia.org/wiki/Heyting_algebra