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.
  • $\begingroup$ No reason to avoid them. In classical logic, Contraposition is a valid rule. $\endgroup$ May 25, 2021 at 10:42
  • $\begingroup$ In Intuitionistic logic the part $P \to Q \vdash \lnot Q \to \lnot P$ is valid, while the other part: $\lnot P \to \lnot Q \vdash Q \to P$ is rejected. $\endgroup$ May 25, 2021 at 10:44
  • $\begingroup$ "Is there any proof, in classical logic, for the law of contraposition that proves both sides of the equivalence without using double negation elimination or the law of excluded middle?" No; we need LEM, DN or other equivalent. $\endgroup$ May 25, 2021 at 10:51
  • 1
    $\begingroup$ I just want to say one thing about ¬¬elim. If you only deal with statements that have well-defined (boolean) truth-values, then ¬¬elim is trivially sound and there is no valid reason to feel uncomfortable or unconvinced. If you are not dealing with statements that have well-defined truth-values, then I must ask you, what on earth are you dealing with? This question is not meant to be dismissive; instead it is meant to help you truly understand classical logic and why it is sound for all real purposes. Intuitionistic logic, on the other hand, is simply not about truth. $\endgroup$
    – user21820
    Jan 4, 2022 at 15:32

1 Answer 1


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.
  • $\begingroup$ that's assuming CP's restricted applicability on a per-statement case-by-case basis in intuitionistic logic, right? if CP is provable for that statement then DNE and LEM follow. but to extend this case further, are DNE and LEM equivalent? $\endgroup$
    – msaa
    May 26, 2021 at 10:39
  • $\begingroup$ @msaa There is nothing restricted about CP here. Or maybe you can elaborate on what you would mean with an unrestricted way to formulate CP. Yes, DNE and LEM are equivalent and I can close the circle in the implication chain if you like. $\endgroup$
    – Léreau
    May 26, 2021 at 12:07
  • $\begingroup$ that would be very appreciated. but for the restricted part, isn't the intuitionistic CP, as a law, slightly different than the classical one (as shown here math.stackexchange.com/questions/838184/…)? if it were to have the exact same classical effect, I assumed that would may possible in a special case. $\endgroup$
    – msaa
    May 26, 2021 at 12:42
  • $\begingroup$ @msaa The post you have linked is not about a difference between formulations of CP in classical/intuit. logic. In a nutshell the post asks: "When does an instance of CP is true in intuit. logic?" and the answer is "It depends". And this is what I also mentioned in the answer to the second bullet point. The answers go a bit further by discussing some conditions of when instances of CP hold. For example the second answer states that if $B$ is stable (i.e. $\neg \neg B \rightarrow B$) then for every $A$ we have $(\neg B \rightarrow \neg A) \rightarrow (A \rightarrow B)$. $\endgroup$
    – Léreau
    May 26, 2021 at 20:53
  • $\begingroup$ for completion, can you prove DNE from LEM directly? also, from the provided proofs in en.wikipedia.org/wiki/Modus_tollens looks like MT isn't int. valid nor is material implication but it would be great if there's a proof for their invalidity as well. $\endgroup$
    – msaa
    Jun 7, 2021 at 10:53

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .