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.
 A: 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?)
A: 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$$
