Is $(\neg q \rightarrow \neg p) \rightarrow (p \rightarrow q)$ equivalent to $p \vee \neg p$ in intuitionistic logic? I've heard mathematicians say that contrapositive arguments are usually preferable to proofs by contradiction, so I was curious if this was based on logical reasons (i.e. that $(\neg q \rightarrow \neg p) \rightarrow (p \rightarrow q)$ is not as strong of a logical assumption as $p \vee \neg p$ ). 
 A: Obviously $q \vee \neg q \vdash (\neg q \rightarrow \neg p) \rightarrow (p \rightarrow q)$ holds intuitionistically.
Conversely, substituting $\top$ for $p$ and $(r \vee \neg r)$ for $q$ in $(\neg q \rightarrow \neg p) \rightarrow (p \rightarrow q)$ yields $\neg \neg (r \vee \neg r) \rightarrow (r \vee \neg r)$. But $ \top \vdash \neg \neg (r \vee \neg r)$ just intuitionistically. So the particular case of the contrapositive law entails intuitionistically that $r \vee \neg r$. Thus, as axiom schemes they would be interchangeable when the intuitionistic rules hold (technically, this is different from saying the formulas are equivalent).
A: We can use the topological interpretation to show that the implication in the question is not provable in intuitionistic propositional logic.
Recall that, in the topological interpretation, we choose a topological space $X$ and associate each variable $P$ with an open set $[[P]]$ from $X$. There are rules for evaluating the open sets for more complicated formulas, in terms of the connectives. A formula is provable in intuitionistic propositional logic if and only if the formula always evaluates to the entire space. In particular we have the following rules:


*

*$[[P \land Q]] = [[P]] \cap [[Q]]$

*$[[P \lor Q]]  = [[P]] \cup [[Q]]$

*$[[P \to Q]] = ([[P]]^c \cup [[Q]])^\circ$ 

*$[[\lnot P]] = (P^c)^\circ$

*$[[\bot]] = \emptyset$


Here $A^c$ is the complement and $A^\circ$ is the interior of a set $A$.
So, to make our counterexample, we can choose


*

*The space: $X = [0,1]$

*$[[Q]] = (0,1/2)$

*$[[P]] = [0,1/2)$.


Then we have


*

*$[[P \to Q]] = ([[P]]^c \cup [[Q]])^\circ = [1/2,1] \cup (0,1/2) = (0,1] \not = X$

*$[[\lnot P]] = ([[P]]^c)^\circ = (1/2,1]$

*$[[\lnot Q]] = ([[Q]]^c)^\circ = (1/2,1]$

*$[[\lnot Q \to \lnot P ]] =  [0,1/2] \cup (1.2, 1] = [0,1] = X$

*$[[(\lnot Q \to \lnot P) \to (P \to Q)]] = (\emptyset \cup (0,1]) \not = X$


If we could prove intuitionistically that $(\lnot Q \to \lnot P) \to (P \to Q)$ then the set in the last line should have been all of $X$. So that formula is not intuitionistically provable. 
Intuitively, with my choices of sets for $P$ and $Q$, knowing a point is not in $Q$ means having an open set around the point that is disjoint from $Q$ - which would also tell me the point is not in $P$. 
This is why $\lnot P$ and $\lnot Q$ are represented by the same set. 
But knowing a point is in $P$ does not tell me that the point is in $Q$, which was expected because I chose the set for $P$ to not even be contained in the set for $Q$. That is how I constructed the example. With practice these examples are often easy to construct, which is why the topological interpretation is worth knowing.  
