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


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.

  • $\begingroup$ Wikipedia actually gives a proof of the deduction theorem and reading it closely it only relies on THEN-1 and THEN-2 (as these are called in the wiki page for intuitionistic logic, and THEN-1 is only really used to prove $P\to P$). It seems to me that an assumption exchange rule is also needed on the sequent side, and that one follows from the AND-1 and AND-2 rules once one has deduction theorem for a linear sequent. $\endgroup$
    – Fizz
    Mar 4 at 15:20
  • 1
    $\begingroup$ Yes, as long as the only derivation rule is modus ponens, you only need THEN-1 and THEN-2 to prove the deduction theorem. You do need THEN-1 in full, not just $P\to P$; it is needed in the proof of the deduction theorem to take care of logical axioms and assumption other than the one being deducted. Indeed, both THEN-1 and THEN-2 follow from the deduction theorem: since (trivially) $P,Q\vdash P$, the deduction theorem gives $P\vdash Q\to P$ and $\vdash P\to(Q\to P)$. Also, note that this is not a sequent calculus; $X\vdash A$ means that $A$ has a derivation in the Hilbert calculus ... $\endgroup$ Mar 4 at 15:40
  • $\begingroup$ ... from assumptions that belong to the set of formulas $X$. Thus, analogues of the sequent calculus “structural rules” hold trivially for this notion. $\endgroup$ Mar 4 at 15:41

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]

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.