alternative rule for negation introduction

I have the standard rule for negation introduction, namely:

$$\frac{P\Rightarrow Q\quad P\Rightarrow\neg Q}{\neg P}\quad\text{[Proof by negation]}$$

Now I need a slightly different rule (I'm not sure whether you'd say it's stronger or weaker):

$$\frac{P\Rightarrow Q\quad\neg Q}{\neg P}\quad\text{[Modus tollens]}$$

Can I derive the former from the latter? I'm guessing you can do it if you assume something like the law of the excluded middle. If you can get $P\Rightarrow\neg Q$ of course then you'd be done.

• Excluded Middle is not necessary: a standard rule of natural Deduction is $\to$-intro, that licenses the derivation: $A \vdash B \to A$. Thus, in your case: 1) $P \to Q$ : premise; 2) $\lnot Q$ : premise; 3) $P \to \lnot Q$ : from 2) by $\to$-intro; 4) $\lnot P$ : from 1) and 3) by your negation intro. – Mauro ALLEGRANZA Jun 10 '16 at 11:42
• Mauro, hi, thanks for the comment. I don't doubt the veracity of your rule (given your reputation!) but I cannot find it anywhere. It kind of makes sense, if $\neg Q$ holds then anything implies $\neg Q$. Am I supposed to just take it at face value? I don't think it is a special case of the standard $\rightarrow$-intro rule, right? – James Smith Jun 10 '16 at 13:56
• Exactly: $Q \to (P \to Q)$ is a tautology: in Hilbert-style proof systems is often adopted as a logical axiom. Thus, from it and the premise $Q$, by modus ponens we have $P \to Q$, that amounts to: $Q \vdash P \to Q$. – Mauro ALLEGRANZA Jun 10 '16 at 13:59
• – Mauro ALLEGRANZA Jun 10 '16 at 14:03
• so much to learn...interesting to see that others find this not quite easy to digest either – James Smith Jun 10 '16 at 14:04

The trick is to realise that $B\Rightarrow(A\Rightarrow B)$ is a tautology. To see this:

Suppose
B
Hence
Suppose
A
Hence
B // because B holds by the outer supposition
A=>B
B=>(A=>B)


I'm not entirely happy with this, because it seems that you are not deriving that B holds by applying any rule whose premises include A, you are simply restating the outer supposition. Apparently though this is fine. As Von Neumann once said, in mathematics you don't understand things, you just get used to them.

Now the result follows directly from modus ponens. Formally:

$$\frac{B\Rightarrow(A\Rightarrow B)\quad B}{A\Rightarrow B}$$

Again, since the left hand premise is a tautology you can leave it out, so you get:

$$\frac{B}{A\Rightarrow B}$$

This means that $\neg Q$ can be replaced with $P\Rightarrow\neg Q$ in the question, in which case the rule just becomes the standard one for proof by negation.

Together with the proof given in @Hailey's answer, it only remains to show that $\neg P\vee Q$ can be derived from $P\Rightarrow Q$. For this you need the law of the excluded middle.

For the proof we have the premise $P\Rightarrow Q$. Now suppose $P$ holds, then by modus ponens and the premise we have that $Q$ holds. From this $\neg P\vee Q$ holds by conjunction introduction. Therefore $P\Rightarrow\neg P\vee Q$. Now also $\neg P\Rightarrow\neg P$. Therefore $\neg P\Rightarrow\neg P\vee Q$ again by conjunction introduction. From these two implications $P\vee\neg P\Rightarrow\neg P\vee Q$ can be derived, which is a form of disjunction introduction which I leave out here. Lastly by the law of the excluded middle we can take $P\vee\neg P$ and together with modus ponens we have $\neg P\vee Q$, as required.

[Note: This has been voted up, however the fully correct answer is the one that begins 'The trick is...'.]

• Yes: the equivalence does not hold intuitionistically; in intuitionistic logic we have: $\lnot P \lor Q \vdash P \to Q$ but in order to prove: $P \to Q \vdash \lnot P \lor Q$ we need Exclude Middle or equivalently Double Negation. – Mauro ALLEGRANZA Jun 10 '16 at 14:55
• Thanks for confirming this, I'm glad I've gotten something right. Although your comments above make this answer moot, of course. – James Smith Jun 10 '16 at 15:09

$P\implies Q$ is equivalent to $\neg P ∨Q$

So, $(\neg P ∨ Q )∧\neg Q=(\neg P∧\neg Q )∨(\neg Q ∧ Q)=(\neg P∧\neg Q )\quad$ [As $(Q∧\neg Q)=false$]

Now, $\neg Q$ is given that means,it implies $\neg P$

• Hi, unless I'm very much mistaken this isn't quite right. Intuitionistically the statement $P\Rightarrow Q$ says nothing about the truth values of $P$ and $Q$ so there can be no equivalence. – James Smith Jun 8 '16 at 11:54
• Sorry I made a mistake – Hailey Jun 8 '16 at 11:55
• Okay, thanks for the correction. I alluded to other mistakes in your answer although I've gratefully taken that sentence out. I should make myself clear, though. Forgive me for sounding like a maths teacher for a second! But you're using equality here for punctuation and this is a bit questionable. You could separate the steps in the derivation with commas, say, and in this instance that would be okay. But you can't really equate all the statements, I think. Sorry to be a pedant. – James Smith Jun 8 '16 at 12:05
• Now it just remains to show that logical consequence and the material conditional are equivalent in classical logic, in fact all we need is that the latter can be derived from the former, and we're done. I should also correct myself here and say that logical consequence does say something about the truth values of $P$ and $Q$ in a classical setting, as you've rightly pointed out. – James Smith Jun 8 '16 at 12:07