Is $(\neg q \rightarrow \neg p) \rightarrow (p \rightarrow q)$ equivalent to $p \vee \neg p$ in intuitionistic logic?

Question

I've heard mathematicians say that contrapositive arguments are usually preferable to proofs by contradiction, so I was curious if this was based on logical reasons (i.e. that $(\neg q \rightarrow \neg p) \rightarrow (p \rightarrow q)$ is not as strong of a logical assumption as $p \vee \neg p$ ).

Answer 1

Obviously $q \vee \neg q \vdash (\neg q \rightarrow \neg p) \rightarrow (p \rightarrow q)$ holds intuitionistically.

Conversely, substituting $\top$ for $p$ and $(r \vee \neg r)$ for $q$ in $(\neg q \rightarrow \neg p) \rightarrow (p \rightarrow q)$ yields $\neg \neg (r \vee \neg r) \rightarrow (r \vee \neg r)$. But $ \top \vdash \neg \neg (r \vee \neg r)$ just intuitionistically. So the particular case of the contrapositive law entails intuitionistically that $r \vee \neg r$. Thus, as axiom schemes they would be interchangeable when the intuitionistic rules hold (technically, this is different from saying the formulas are equivalent).

Answer 2

We can use the topological interpretation to show that the implication in the question is not provable in intuitionistic propositional logic.

Recall that, in the topological interpretation, we choose a topological space $X$ and associate each variable $P$ with an open set $[[P]]$ from $X$. There are rules for evaluating the open sets for more complicated formulas, in terms of the connectives. A formula is provable in intuitionistic propositional logic if and only if the formula always evaluates to the entire space. In particular we have the following rules:

• $[[P \land Q]] = [[P]] \cap [[Q]]$
• $[[P \lor Q]] = [[P]] \cup [[Q]]$
• $[[P \to Q]] = ([[P]]^c \cup [[Q]])^\circ$
• $[[\lnot P]] = (P^c)^\circ$
• $[[\bot]] = \emptyset$

Here $A^c$ is the complement and $A^\circ$ is the interior of a set $A$.

So, to make our counterexample, we can choose

• The space: $X = [0,1]$
• $[[Q]] = (0,1/2)$
• $[[P]] = [0,1/2)$.

Then we have

• $[[P \to Q]] = ([[P]]^c \cup [[Q]])^\circ = [1/2,1] \cup (0,1/2) = (0,1] \not = X$
• $[[\lnot P]] = ([[P]]^c)^\circ = (1/2,1]$
• $[[\lnot Q]] = ([[Q]]^c)^\circ = (1/2,1]$
• $[[\lnot Q \to \lnot P ]] = [0,1/2] \cup (1.2, 1] = [0,1] = X$
• $[[(\lnot Q \to \lnot P) \to (P \to Q)]] = (\emptyset \cup (0,1]) \not = X$

If we could prove intuitionistically that $(\lnot Q \to \lnot P) \to (P \to Q)$ then the set in the last line should have been all of $X$. So that formula is not intuitionistically provable.

Intuitively, with my choices of sets for $P$ and $Q$, knowing a point is not in $Q$ means having an open set around the point that is disjoint from $Q$ - which would also tell me the point is not in $P$. This is why $\lnot P$ and $\lnot Q$ are represented by the same set.

But knowing a point is in $P$ does not tell me that the point is in $Q$, which was expected because I chose the set for $P$ to not even be contained in the set for $Q$. That is how I constructed the example. With practice these examples are often easy to construct, which is why the topological interpretation is worth knowing.