Contraposition's value is rigorous logical reasoning I don't remember where but I read in the past that contrapositive proofs should be avoided when possible. fast forward and I became almost obsessed with why contraposition is still used when it has so many flaws (Hempel's raven for example).
For example, while there are some awfully simple proofs for the law of contraposition, proving both ways of the equivalence ultimately boils down to double negation elimination, which, by itself, doesn't feel very convincing. For example, the law of non-contradiction feels perfectly fine but the law of excluded middle is frowned upon by intuitionistic (aka constructive) logic (along with double negation elimination since both could be derived from each other in classical logic. please correct me if I'm wrong). So:

*

*Is there any proof, in classical logic, for the law of contraposition that proves, using pure logical constructs, both sides of the equivalence without using double negation elimination or the law of excluded middle? I'm not strictly a fan of intuitionistic logic but it will be reassuring if there is anything like an intuition-friendly proof in classical logic.

*Are contrapositive proofs really avoided in the real world?

*Any special cases (like statements of form X) that are perfectly fine to prove using contraposition without invoking logical leaps? like the case mentioned here.

 A: An answer to your question can be given in intuitionistic logic. If you are not a fan of intuitionistic logic and don't know much about it; it's enough to know that the law of excluded middle ($\mathsf{LEM}$) can not be shown in said logic.
What you can however show in intuitionistic logic is that $\mathsf{LEM}$ and and Contraposition ($\mathsf{CP}$) are equivalent and in this precise sense, $\mathsf{CP}$ is "just as bad" a $\mathsf{LEM}$.

Let me expand on my answer, more specifically addressing the bullet-points.

*

*Yes there is a proof of the equivalence between $\mathsf{LEM}$ and $\mathsf{CP}$ which, upon inspection, does not use double negation elimination ($\mathsf{DNE}$). Actually, from the start, we can slightly change our classical proof system and completely remove the possibility to use $\mathsf{DNE}$, which guarantees that we don't use it by accident. There is even a name for this variation of classical logic and you might have guessed it by now: it's intuitionistic logic.


*Yes. There are good reasons for people to avoid proofs which use $\mathsf{LEM}$ and since it is equivalent to $\mathsf{CP}$, this also means we are trying to avoide $\mathsf{CP}$.


*Yes there are instances where $(\neg B \rightarrow \neg A) \rightarrow (A \rightarrow B)$ can be proven and therefore be used, just as there are instances of a statement that has the form $X \lor \neg X$ which can be proven and therefore be used. For example, if you have the finite set $B = \{0, 1\}$ you can (without using $\mathsf{LEM}$ or the likes) show that $\forall x, y \in B : ~ x = y \lor \neg (x = y)$.

Here are proofs for $\mathsf{CP} \Rightarrow \mathsf{DNE} \Rightarrow \mathsf{LEM}$ and lastly $\mathsf{LEM} \Rightarrow \mathsf{CP}$ in intuitionistic logic. Rember that in intuitionistic logic (just like in classical logic) there are the always false proposition $\bot$ and the always true proposition $\top$ and negation is defined by $\neg P := P \rightarrow \bot$.

*

*Assume $\mathsf{CP}$. This means for any propositions $A, B$ we have $(\neg B \rightarrow \neg A) \rightarrow (A \rightarrow B)$.
So in particular for $A = \neg \neg X$ and $B = X$ we get
$$
  (\neg X \rightarrow \neg \neg \neg X) \rightarrow (\neg \neg X \rightarrow X)
$$
So $\neg \neg X \rightarrow X$ follows from $\neg X \rightarrow \neg \neg \neg X$ where this latter statement is true since by definition it is the same as $(\neg X) \rightarrow \neg (\neg X) \rightarrow \bot$ which is more obviously true.


*For the second implication we now assume $\mathsf{DNE}$. This means for every $A$ we have $\neg \neg A \rightarrow A$, which means in order to show $X \lor \neg X$ it suffices to show $\neg \neg (X \lor \neg X)$.
So assume $H_1 : \neg (X \lor \neg X)$ and try to get a contradiction to it. With $H_1$ we can show $H_2 : \neg X$ (since assume we had $X$, then we also have $X \lor \neg X$; in contradiction to $H_1$). Now that we have $H_2$ this too implies $X \lor \neg X$ and we therefore get the desired contradiction to $H_1$.


*Assume $\mathsf{LEM}$, meaning for every $X$ we have $X \lor \neg X$. We want to show $(\neg B \rightarrow \neg A) \rightarrow (A \rightarrow B)$, so we assume $H_1 : (\neg B \rightarrow \neg A)$ and $H_2 : A$ and try to show $B$. Because of $\mathsf{LEM}$ we either have $B$ or $\neg B$. In the first case it is trivial to show $B$. In the second case we have $\neg B$ which, by using $H_1$ gets us $\neg A$ which by $H_2$ gets us $\bot$. So by explosion we can again conclude $B$.

By request fom the comments, here is also the implication $\mathsf{LEM} \Rightarrow \mathsf{DNE}$.
We are trying to show $\neg \neg X \to X$, so assume $H : \neg \neg X$ and try to get $X$. By $\mathsf{LEM}$ we know that $X \lor \neg X$ so we get two cases:

*

*If $X$ then we are done.

*If $\neg X$ then we get $\bot$ because of $H$ and therefore $X$ by explosion.

