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.)
Best Answer
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.