How to derive ~(P → Q) → P?

Question

My book (An Exposition of Symbolic Logic with Kalish-Montague derivations) asks me to derive the theorem ~(P → Q) → P, but I have no idea how to derive it. The book gives no correction for theorems' proofs, and it doesn't tell the theorem's name, probably because it doesn't have a name.

So I ask: what is the derivation of ~(P → Q) → P step by step?

The book, at this point, already taught modus ponens, modus tollens, double negation, repetition (A, therefore, A), direct derivation, conditional derivation, indirect derivation, subderivations, and I am not allowed to use any other theorem to prove ~(P → Q) → P.

If it's not allowed to ask for derivations and proofs of things, please, tell me, and I delete this question.

Answer 1

this is a derivation using natural deduction rules from the textbook Gamut L.T.F. "Logic, language and meaning". It may help you with your derivation.

1. ¬(P→Q) - assumption
2. ¬P - assumption
3. P - assumption
4. ⊥ in 3,4
5. Q - EFSQ (explosion principle) (close assumption 3)
6. P→Q - Rule Introduction of → in 3,5
7. ⊥ in 1,6 (close assumption 2)
8. ¬¬P - Rule Introduction of ¬ in 2
9. P - Rule Elimination of ¬¬ in 8 (close assumption 1)
10. ¬(P→Q)→P - Rule Introduction of → in 1,9

Answer 2

the book only gives "modus tollens", "modus ponens", "douple negation", "repetion" (A, therefore A), direct derivation, conditional derivation, indirect derivation and subderivation.

You are asked to derive a conditional statement, $\neg (P\to Q)~\to~ P$ so use a conditional derivation.   So make a subderivation of the consequent, $P$, under the assumption of the antecedent, $\neg(P\to Q)$.

You have no way to directly derive $P$ under that assumption, so that calls for an indirect derivation. Thus make a subderivation of a contradiction under the assumption of the negation, $\neg P$.

Now derive a contraduction under the assumptions $\neg P$ and $\neg(P\to Q)$ will involve either deriving $P$ or $P\to Q$. Since if you could directly derive $P$ you would not be here... You are seeking to derive the conditional statement $P\to Q$, so ...

$$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{}{\fitch{\neg (P\to Q)}{\fitch{\neg P}{~~\vdots\\P\to Q\\\bot}\\P}\\\neg(P\to Q)\to P}$$

Answer 3

Hint: Start with an initial premise of $\neg (P \implies Q)$. Then apply the definition of '$\implies$'