Can one prove by contraposition in intuitionistic logic? I read that contraposition $\neg Q \rightarrow \neg P$ in intuitionistic logic is not generally equivalent to $P \rightarrow Q$. If this is right, in what case can this contraposition logical-equivalence be used in intuitionistic logic?
 A: 
In what case can this contraposition logical-equivalence be used in intuitionistic logic?

This is not straightforward to answer. What needs to be true is that $P$ and $Q$ need to act sufficiently like classical formulas. Here are two examples:
1. The negative translation embeds classical logic into intuitionistic logic, sending a formula $S$ to a formula $S^N$. If we compute this for an instance of contraposition, we obtain:
$$(\lnot R \to \lnot S) \to (S \to R))^N\\
(\lnot R \to \lnot S)^N \to (S \to R)^N\\
((\lnot R)^N \to (\lnot R)^N \to (S^N \to R^N)\\
(\lnot R^N \to \lnot S^N) \to (S^N \to R^N)$$
Therefore $(\lnot R^N \to \lnot S^N) \to (S^N \to R^N)$ is intuitionistically valid for all $R,S$. In particular, if $P$ and $Q$ are equivalent to negative translations of other formulas, then contraposition holds for $P$ and $Q$.

2. Here is a different view. Suppose $Q_0$ is a fixed formula such that contraposition holds between $Q_0$ and all $P$:
$$(\lnot Q_0 \to \lnot P) \to (P \to Q_0)$$
Then, letting $P$ be $\lnot \bot$, we have $\lnot P$ equivalent to $\bot$, and so from
$$(\lnot Q_0 \to \lnot P) \to (P \to Q_0)$$
we obtain
$$(\lnot \lnot Q_0) \to (\lnot \bot \to Q_0)$$
which is equivalent to 
$$\lnot \lnot Q_0 \to Q_0$$
Thus if $Q_0$ satisfies contraposition with all $P$, then $Q_0$ is equivalent to $\lnot\lnot Q_0$.  The converse of this was shown by Ittay Weiss in another answer: if $Q_0$ is equivalent to $\lnot\lnot Q_0$ then $Q_0$ satisfies contraposition with all $P$.
A: Contraposition in intuitionism can, sometimes, be used, but it's a delicate situation.
You can think of it this way. Intuitionistically, the meaning of $P\to Q$ is that any proof of $P$ can be turned into a proof of $Q$. Similarly, $\neg Q \to \neg P$ means that every proof of $\neg Q$ can be turned into a proof of $\neg P$. 
If $P\to Q$ is true, and you are given a proof of $\neg Q$, can you construct a proof of $\neg P$ ? The answer is yes, as follows. Well, we are given a proof that there is no proof of $Q$. Suppose $P$ is true, then it can be turned into a proof of $Q$, but then we will have a proof of $Q\wedge \neg Q$, which is impossible. Thus we just showed that it is not the case that $P$ holds, thus $\neg P$ holds. In other words, $(P\to Q)\to (\neg Q \to \neg P)$.
In the other direction, suppose that $\neg Q \to \neg P$, and you are given a proof of $P$. Can you now construct a proof of $Q$? Well, not quite. The best you can do is as follows. Suppose I have a proof of $\neg Q$. I can turn it into a proof of $\neg P$, and then obtain a proof of $P\wedge \neg P$, which is impossible. It thus shows that $\neg Q$ can not be proven. That is, that $\neg \neg Q$ holds. In other words, $(\neg Q \to \neg P)\to (P\to \neg \neg Q)$.
