Is $(p \to q) \to (\neg q \to \neg p)$ a theorem in (Johansson's) minimal logic?

Question

From a related question we know that $(P\to Q)\to (\neg Q \to \neg P)$ is a theorem in intuitionistic logic. I'm asking if that's also true for the positive fragment of intuitionistic logic aka minimal logic. Note that minimal logic does allow a notion of negation, because it does allow one to define negation relative to a (an arbitrarily chosen) false element $\bot$, i.e. ($\neg P =_{\mathrm{def}} P \to \bot $), it's just that the axiom $\bot \to X$ is not included in minimal logic.

Interestingly, as Wikipedia says

The propositional form of modus ponens, $(A \land (A\to B))\to B$ is clearly valid also in minimal logic.

The proof of this latter claim (not included in Wikipedia) is actually slightly involved, at least in the Hilbert calculus (of minimal logic). Recall (only the axioms I'm going to use) in this proof:

• THEN-2: $(\phi \to (\chi \to \psi )) \to ((\phi \to \chi ) \to (\phi \to \psi ))$
• AND-1: $\phi \land \chi \to \phi$
• AND-2: $\phi \land \chi \to \chi$

Let $P = A \land (A\to B)$. By AND-1 and AND-2 we have that both $P \to A$ and $P \to (A\to B)$, but we really want to show that $P \to B$. However by MP application to $P \to (A\to B)$ and THEN-2 we get $(P \to A) \to (P \to B)$. And since (we had by AND-1 that) $P \to A$ it follows by another MP application to these last two formulas that $P \to B$.

As Wikipedia (also) says, from the fact that the propositional form of MP holds for minimal calculus, i.e. $(A \land (A\to B))\to B$ is a theorem, it also follows by simple substitution of $B$ with $\bot$ (and applying the definition of negation) that the propositional form of the law of non-contradiction

$\neg (A \land \neg A)$ can still be proven in minimal logic.

However, I don't quite see how/if one ca pull off a similar trick for $(P\to Q)\to (\neg Q \to \neg P)$. So, is the latter a theorem in minimal logic (too, somehow), or is there a proof that it isn't? (And if the later is the case, does minimal logic plus this propositional form of modus tollens result is some interesting logic?)

(I actually have not idea how to attempt a proof that something isn't a theorem in minimal logic. For intuitionistic logic one can easily use the 3-element linear lattice with the appropriate implication table [making it a Heyting algebra] to show e.g. that $(\neg Q \to \neg P) \to (P\to Q)$ is not a theorem in intuitionistic logic, by taking $P = 1$ and $Q = \frac{1}{2}$; that yields $(0 \to 0) \to (1 \to \frac{1}{2}) = (1) \to (\frac{1}{2}) = \frac{1}{2}$, proving that this formula is not a theorem in intuitionistic (or minimal) logic, but this is the "converse" of the formal I'm asking about. I have no idea what can serve as a similar device for minimal logic that can show that something is a non-theorem just in minimal logic.)

Answer 1

Yes, this is provable. Unwinding the definition, your formula is

$$(P\to Q)\to((Q\to\bot)\to(P\to\bot)).$$

This is an instance of the more general tautology

$$(P\to Q)\to((Q\to R)\to(P\to R)),$$

which is easily provable in minimal logic: for example, recalling that the deduction theorem holds for minimal logic, it suffices to show

$$P\to Q,Q\to R,P\vdash R,$$

which follows by two applications of modus ponens.

Answer 2

Yes it is.

The usual ND rules for managing $\to$ are available also in ML.

1. $(p \to q)$ --- premise

2. $(q \to \bot)$ --- assumed [a]

3. $p$ --- assumed [b]

4. $q$ --- from 3) and 1) by $\to$-elim

5. $\bot$ --- from 4) and 2) by $\to$-elim

6. $(p \to \bot)$ --- from 3) and 5) by $\to$-intro, discharging [b]

7. $(q \to \bot) \to (p \to \bot)$ --- from 2) and 6) by $\to$-intro, discharging [a]

---

In an Hilbert-style proof system, you need the two "THEN-axioms" to prove the Deduction Theorem.

With this and Modus Ponens you have the necessary resources to manage $\to$.

Answer 3

Here's another way to do this using the topological semantics for minimal logic, obtained by taking the topological Heyting algebra semantics here and changing the interpretation of $\bot$ from $\varnothing$ to a fixed nonempty open set like $(-1, 1)$.

Let $X^c$ be the complement of $X$ in $\mathbb{R}$. Let $X^i$ or $i(X)$ be the interior of the set $X$. Similarly, let $X^k$ or $k(X)$ be the closure.

Lemma 51: $P \to Q$ holds if and only if $P \subset Q$ .

Suppose $P \subset Q$. Then

$$ [P \to Q] = i(P^c \cup Q) = i\bigg(P^c \cup (Q \cap P) \cup (Q \setminus P)\bigg) = i\bigg(\varnothing^c \cup (Q \setminus P)\bigg) = i(\varnothing^c) = \varnothing^c $$

Suppose $[P \to Q] = \varnothing^c$.

• Then $i(P^c \cup Q) = \varnothing^c$.
• Thus $P^c \cup Q = \varnothing^c$.
• Thus $(P^c \cup Q) \cap P = \varnothing^c \cap P$.
• Thus $Q \cap P = P$.
• Thus $P \subset Q$.

Theorem: $(P \to Q) \to (\lnot Q \to \lnot P)$ is a tautology.

Suppose $P \to Q$ is a tautology.

Thus $P \subset Q$.

Let $f(X)$ be $(X^c \cup (-1, 1))^{ic}$. Note that $[(\lnot Q) \to (\lnot P)]$ is $i(f(P)^c \cup f(Q)^c)$.

$f(X)$ is equal to $k(X \cap (-1, 1)^c)$, applying de Morgan's laws and exploiting the duality of the interior and closure.

$f$ is a composition of two functions, $\cdot \cap (-1, 1)^c$ and then the closure function, which are weakly monotonic with respect to $\subset$. Therefore $f$ is weakly monotonic with respect to $\subset$.

Therefore $f(P) \subset f(Q)$.

Therefore $(\lnot Q) \to (\lnot P)$ is a tautology.

Discharging our initial hypothesis, therefore $(P \to Q) \to ((\lnot Q) \to (\lnot P))$ is a tautology.