I'm getting a bit stuck in a tailspin on this one. I'm quite new to logic. I'm not sure how or when we use negation to get P. How then does that connect to (¬p ⇒ q) ⇒ ((¬p ⇒ ¬q)?
A truth table would show this is a tautology, so one can try deriving this without premises. Here is a proof using the proof checker associated with forallx. Something similar should work with Fitch:
On line 1, I assume the antecedent of the conditional I would like to derive. The consequent of that conditional is also a conditional so on line 2 I make another assumption assuming the antecedent of that conditional.
Then I notice that if I assume on line 3 ¬P I can derive a contradiction using modus ponens or conditional elimination (→E) which I do on lines 4 and 5. On line 6 I note that I have a contradiction. You may have to use a conjunction of lines 4 and 5 to show that in your proof checker.
With that contradiction I can use indirect proof (IP) on line 7 to discharge the assumption made on line 3 and derive P. On lines 8 and 9 I can use conditional introduction to derive the goal.
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf
You have assumed things in the worng order, and missed the significance of being able to derive both
In order to prove
(~ p > q) > ((~p > ~q) > p) you must first assume
(~p > q), aiming to derive
((~p > ~q) > p) , so that a conditional proof may be used (aka Implication Introduction in Stanford's Fitch system).
Likewise, in order to derive
((~p > ~q) > p) under that assumption, you must next assume
(~p > ~q) aiming to derive
Stanford's Fitch System takes allows
~~p to be derived from the two assumptions using their version of the Negation Introduction rule, and you can then use what they call Negation Elimination to derive
|_ | |_ ~p > q Assumption | | |_ ~p > ~q Assumption | | | ~~p Negation Introduction | | | p Negation Elimination | | (~p > ~q) > p Implication Introduction | (~p > q) > ((~p > ~q) > p) Implication Introduction