# 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?

• We may be interested by Kripke models of intuitionistic logic. Finding a Kripke model in which the second formula is satisfied but not the first one, proves (using the completeness theorem) that you can't prove syntactically the contraposition in intuitionistic logic. Aug 21, 2016 at 12:20
• Also discussed on mathoverflow.net/a/12349/65810 (but without proofs). Mar 4, 2021 at 17:54

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)$.

• well, yes, I thought the answer made it clear that some aspects of contraposition remain valid. But contraposition itself is not a valid principle in intuitionism. Unless I'm missing something in your comment @CarlMummert please correct me. Jun 18, 2014 at 10:46
• My concern is that the question asked when it can be used, and the first sentence of the answer is "it can't be used in intuitionistic logic", which seems to me to suggest "it can never be used", when actually it can be used in certain circumstances and not in others. Indeed, reading between the lines of the last paragraph shows one time it can be used. But I am afraid the headline may cause some readers to misunderstand Jun 18, 2014 at 10:59
• ah, I see and I agree with you. I now changed the first line to clarify matters. Thanks! Jun 18, 2014 at 12:08
• The $(P → Q) ⊢ (¬Q → ¬P)$ thing is called “modus tollens” (or “modus tollendo tollens”). It is important to understand that it has nothing to do with proofs by contradiction. Because it is confusingly perceived as a flavour of proof by contradiction, silly people frequently write that there is no modus tollens in intuitionism, although there is. Aug 31, 2014 at 20:20
• Basically $(\neg Q \to \neg P)\to (P\to Q)$ iff $\neg \neg Q \to Q$, which is sometimes termed that $Q$ is "stable" (under double negation). Or otherwise put it, its corresponding Heyting algebra element is called "regular". This doesn't hold for every element in a Heyting algebra unless it's downright a Boolean algebra... which is basically Carl's point below. Mar 4, 2021 at 6:06

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$.

• The first line $(\lnot R \to \lnot S) \to (S \to R))^N$ is missing a parenthesis, i.e. should probably be $((\lnot R \to \lnot S) \to (S \to R))^N$. For some reason, I can't seem to propose just that change via a regular edit. Mar 4, 2021 at 3:58