Can intuitionistic propositional logic prove that if the negations of two statements are equivalent, so are the original statements?

Question

I know that classical propositional logic can prove the formula $(\neg P \leftrightarrow \neg Q) \rightarrow (P \leftrightarrow Q)$. But, can intuitionistic propositional logic prove it? If not, can someone give a countermodel?

Answer 1

It's not too hard to prove that in general, the triple negation of a proposition is equivalent to its single negation (see here). Thus, a countermodel is any model that fails to validate that the double negation of a proposition is equivalent to the original proposition.

The Heyting algebra of open subsets of the reals is a good model to think about these sorts of things. Negation is the interior of the complement, so for example, the negation of $\mathbb R \setminus \{0\}$ is the empty set, and the double negation is all of $\mathbb R$.

Answer 2

No. This is equivalent to double negation elimination. To see this, take $Q = \top$. Then $(\neg P \iff \neg Q)$ is equivalent to $\neg \neg P$, while $(P \iff Q)$ is equivalent to $P$.