Intuitionistically, are these inequivalent? $P \rightarrow Q,\; \neg Q \rightarrow \neg P,\; P \wedge \neg Q \rightarrow \bot,\; \neg P \vee Q$

Question

Sometimes we get questions like this that essentially ask:

Okay, I know there's at least three different ways of proving an implication, namely:

• direct proof
• proof by contraposition
• proof by contradiction

But what, really, is the difference between them?

As I see it, there's at least two ways of answering this question. One way is to nominate your favorite proof calculus for classical logic and explain how it handles these different proof strategies differently. Another way might be to argue that:

• direct proof proves $P \rightarrow Q$
• proof by contraposition proves $\neg Q \rightarrow \neg P$
• proof by contradiction proves $P \wedge \neg Q \rightarrow \bot$
• there's another one whereby you prove $\neg P \vee Q$

and that all four of these formulae are intuitionistically inequivalent. Actually, is this even true? Unfortunately, I don't know a thing about intuitionistic logic. So I ask:

Question. Intuitionistically, are each of the following formulae inequivalent? $$P \rightarrow Q,\; \neg Q \rightarrow \neg P,\; P \wedge \neg Q \rightarrow \bot,\; \neg P \vee Q$$

Answer 1

There are three strengths in your list: from strongest to weakest,

1. $\neg P\vee Q$
2. $P\to Q$
3. $\neg(P\wedge\neg Q)$, equivalent to $\neg Q\to\neg P$ (and to $P\to\neg\neg Q$)

Note that if (2) implied (1), taking $P=Q$ would yield $\neg Q\vee Q$, which is famously intuitionistically invalid. If (3) implied (2), we could take $P=\neg\neg Q$; then (3) $\neg\neg Q\to\neg\neg Q$ would yield (2) $\neg\neg Q\to Q$, which is again famously intuitionistically invalid. So we definitely expect that these implications do not hold. (Of course this is just some kind of informal reductio... which is not intuitionistically valid.)

For the equivalence of $\neg Q\to\neg P$ and $P\to\neg\neg Q$: the first is $\neg Q\to P\to\bot$; the second is $P\to \neg Q\to\bot$; so their equivalence is an instance of permutation. For the equivalence of $\neg(P\wedge\neg Q)$ and $P\to\neg\neg Q$: the first is $P\wedge\neg Q\to\bot$; the second is $P\to\neg Q\to\bot$; so their equivalence is an instance of the currying principle, that $A\wedge B\to C$ is equivalent to $A\to B\to C$.

---

As for your goal of distinguishing between contraposition and proof by contradiction: in most systems of sequent calculus, the following derivation is valid both top to bottom and bottom to top: \begin{align*} \Gamma &\vdash \neg Q\to\neg P \\ \Gamma,\neg Q &\vdash \neg P \\ \Gamma,\neg Q &\vdash P\to\bot \\ \Gamma,P,\neg Q &\vdash \bot \\ \Gamma,P\wedge\neg Q &\vdash \bot \\ \Gamma &\vdash P\wedge\neg Q\to\bot \\ \Gamma &\vdash \neg(P\wedge\neg Q) \end{align*}

A logic which doesn't validate this derivation would, I think, have to have one of these properties:

1. No deduction theorem, or a weak one.
2. No adjunction, which means a weird notion of $\wedge$.
3. A definition of $\neg$ other than $\to\bot$.

Not that there aren't such logics, but their existence might not be very compelling for your intended audience, which I assume is a student learning classical logic for the first time.

Answer 2

In intuitionistic logic:

1. $$p \rightarrow q \vdash \neg(p \land \neg q)$$
2. $$ \neg(p \land \neg q) \nvdash p \rightarrow q$$
3. $$ \neg p \lor q \vdash p \rightarrow q$$
4. $$p \rightarrow q \nvdash \neg p \lor q$$
5. $$p \rightarrow q \vdash \neg q \rightarrow \neg p$$
6. $$ \neg q \rightarrow \neg p \nvdash p \rightarrow q$$
7. $$p \rightarrow q \vdash (p \land \neg q) \rightarrow \bot$$

Proof-theoretically speaking, the reason why (2), (4) and (6) do not hold intuitionistically is because you need the double negation elimination to complete the proof. Since in intuitionistic logic this rule is dropped, there are no means to prove those classic entailments. In contrast, the proofs of the remaining (1), (3) and (5) go as usual.

There is a list of other interesting properties of this logic in Van Dalen Logic and Structure, p.156.

This paper and the Stanford Encyclopedia of Philosophy entry on it can also be interesting.