# Tricky Tautology

I'm having difficulty deriving the following tautology: $$\neg(p \rightarrow q) \rightarrow p.$$

The difficulty lies in that the proof needs to be constructed using only the following rules of inference: modus ponens, modus tollens, and double negation. Further, no other theorems/tautologies may be referred to in the derivation.

I've tried everything I can think of, without discernible progress. I figure there is some crucial insight that should resolve the derivation quite quickly, but I've yet to find it. It would be appreciated if someone should point me in the direction of a solution.

edit: the deduction theorem is assumed.

-
What should you derive this from? You have to apply the inference rules to something. – Michael Greinecker Jun 5 '12 at 12:03

Okay, so we have Modus Ponens, Modus Tollens, and Double-Negation Elimination $$\frac{p\to q \qquad p}{q}\text{MP} \qquad \frac{p\to q\qquad \neg q}{\neg p}\text{MT} \qquad \frac{\neg \neg p}{p}\text{DNE}$$ plus natural deduction: $$\begin{array}{c}p \\ \vdots \\ \frac{q}{p\to q} \end{array}$$

We want eventually to conclude $\neg(p\to q)\to p$. The natural way to conclude an implication is by deduction, so $$\tag{1} \textbf{Assume: } \neg(p\to q)$$

How are we going to get from there to $p$? The only way to pick apart a singly-negated premise with the tools we're given is to use MT, and for that we'd need to have something of the form $X \to (p\to q)$. We'd then get the $X$ in negated form, which does not look promising unless $X$ is already negated once, in which case we can use DNE on it. So it might be useful to see if we can produce $\neg p \to (p\to q)$. A bit of truth-tabling tells us that this indeed is a tautology, which is reassuring. But how to prove that? Again, the deduction theorem: $$\tag{2} \textbf{Assume: } \neg p$$ $$\tag{3} \textbf{Assume: } p$$

And we now want to conclude $q$ from $\neg p$ and $p$. Again the only way to make use of the $\neg p$ assumption is to use MT on it, so we need to have something of the form $Y\to p$ first. But we can get that for any $Y$ because we already have $p$, so we can just choose $Y$ with a view to being able to prove $q$ from $\neg Y$ -- i.e., let $Y$ be $\neg q$ and do

$$\tag{4} \textbf{Assume: } \neg q$$ $$\tag{5} \textbf{By assumption }(3): p$$ $$\tag{6} \textbf{Discharge assumption }(4): \neg q \to p$$ $$\tag{7} \text{MT}(4,2): \neg \neg q$$ $$\tag{8} \text{DNE}(7): q$$

And now we just have to carry out the rest of the plans we already made: $$\tag{9} \textbf{Discharge assumption }(3): p\to q$$ $$\tag{10} \textbf{Discharge assumption }(2): \neg p \to (p \to q)$$ $$\tag{11} \text{MT}(10,1): \neg \neg p$$ $$\tag{12} \text{DNE}(11): p$$ $$\tag{13} \textbf{Discharge assumption }(1): \neg(p\to q)\to p$$

-

It's not possible if you have only those three rules of inference, and no additional axioms. Each of those rules require you to have already proved at least one premise, so there are no proofs of anything that use only those rules, since nothing can legally be the first line of a proof.

I suspect that you're actually allowed to use one or more logical axioms in your derivations. Your task is now to find out which ones. (Or perhaps the deduction theorem is allowed?)

-
I think that the ROI are to be applied to the antecedent. That is, one's allowed to assume the antecedent, and from that derive the consequent. Also, indirect methods are allowed, so one might assume that the negation of the tautology, and from this derive a contradiction. – andy Jun 5 '12 at 12:20
Instead of telling us what you think the rules are, why not ask and find out what they really are? – GEdgar Jun 5 '12 at 12:27
what are they, really? I'm genuinely interested. – andy Jun 5 '12 at 12:33
@andy: How would we know? You're the one who knows what course you're following, which textbook (or notes) you're using, and precisely how that text defines the permitted rules in its particular setting. – Henning Makholm Jun 5 '12 at 12:50
However, with the information that we have the deduction theorem as a primitive (which results in a style usually known as "natural deduction") it sounds plausible that the tautology can actually be derived with these tools. – Henning Makholm Jun 5 '12 at 14:00