Use Fitch system to proof ((p ⇒ q) ⇒ p) ⇒ p without any premise. ONLY FOR FITCH SYSTEM. I know here has few similar questions, but I cannot figure out with those answer. Since for Fitch system, I can only use And Intro, And Elim, Or Inro, Or Elim, Neg Intro, Neg Elim, Impl Intro, Impl Elim, Biconditional Intro, and Biconditional Elim.
I know I need to assume (p=>q)=>p then for next I need to prove p, at the end I can use Imlo Intro. But I don't know how to prove p...
I saw some answers like:
(p=>q)=>p  assume 1
p          assume 2
~p         assume 3
q          neg Elim with 2 or 3
I stop at this step..NOt sure why I can get q from 2 and 3? Since Neg Elim follows this form ( ~~p get p) and also Neg Intro follows (p=>q, p=>~q, get ~p). But from what I learn I can not get the q from just assume 2 and 3...
I tried in Fitch system, But it doesn't work with the answer from other questions. So that's right I post here again. Wish someone can help me. 
 A: $\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$ 
Maybe this works for your rules?
$\fitch{}{
\fitch{
1. (p \rightarrow q) \rightarrow p \quad Assumption}{
\fitch{
2. \neg p \quad Assumption}{
\fitch{
3. p \quad Assumption}{
\fitch{
4. \neg q \quad Assumption}{
5. p \quad Reiteration \ 3}\\
6. \neg q \rightarrow p \quad \rightarrow  Intro \ 4-5\\
\fitch{
7. \neg q \quad Assumption}{
8. \neg p \quad Reiteration \ 2}\\
9. \neg q \rightarrow \neg p \quad \rightarrow Intro \ 7-8\\
10. \neg \neg q \quad \neg  Intro \ 6,9\\
11.   q \quad \neg Elim \ 10}\\
12. \quad \quad p \rightarrow q \quad \rightarrow Intro \ 3-11\\
13. \quad \quad p \quad \rightarrow  Elim \ 1,12}\\
14. \quad \neg p \rightarrow p \quad \rightarrow  Intro \ 2-13\\
\fitch{
15. \quad \quad \neg p \quad Assumption}{
16. \quad \quad \neg p \quad Reiteration \ 15}\\
17. \quad \neg p \rightarrow \neg p \quad \rightarrow  Intro \ 15-16\\
18. \quad \neg \neg p \quad \neg Intro \ 14,17\\
19. \quad p \quad \neg Elim \ 18}\\
20. ((p \rightarrow q) \rightarrow p) \rightarrow p \quad \rightarrow Intro \ 1-19
}$
A: The issue with this problem seemed to be Stanford Fitch's approach to the negation rules, and their lack of a falsum symbol.

To prove the conditional $(p\to(p\to q))\to p$, assume $(p\to q)\to p$ aiming to derive $p$.  IE a conditional proof.
To derive $p$ from that assumption, assume $\lnot p$ aiming to derive a contradiction. Ie a proof by contradiction.
To derive a contradiction from $\lnot p$ and $(p\to q)\to p$, seek to derive $p\to q$.
To derive $p\to q$ from those assumptions, use a conditional proof. Ie: now assume $p$.
To derive $q$ from the assumptions of $p$, $\lnot p$, and $(p\to q)\to p$, well, we have assumed a contradiction so explode it.
Discharge the assumptions and we are done.
$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}}\fitch{}{\fitch{~~1.~(p\to q)\to p\hspace{5ex}\text{Assume}}{\fitch{~~2.~\lnot p\hspace{11ex}\text{Assume}}{\fitch {~3.~p\hspace{10ex}\text{Assume}}{~~4.~\bot\hspace{8ex}\lnot\,\mathsf E, 2,3\\~~5.~q\hspace{9ex}\text{EFQ}}\\~~6.~p\to q\hspace{7ex}\to\mathsf I,3{-}5\\~~7.~p\hspace{12ex}\to\mathsf E, 1,6\\~~8.~\bot\hspace{12ex}\lnot\,\mathsf E,2,7}\\~~9.~\lnot\lnot p\hspace{13ex}\lnot\,\mathsf I,2{-}8\\10.~p\hspace{16ex}\lnot\lnot\,\mathsf E, 9}\\11.~(p\to (q\to p))\to p\hspace{2ex}\to\mathsf I,1{-}10}$$
Now, the Stanford Fitch implimentation's of the negation introduction rule isn't too cumbersome (and what they call negation elimination is usually known as double negation elimination), but the lack of a falsum symbol means they do not have an explicit ex falso quodlibet rule (EFQ).  You have to use a proof by contradiction using their negation rules.   It bloats the proofs somewhat.
$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}}\fitch{}{\fitch{~~1.~(p\to q)\to p\hspace{5ex}\text{Assume}}{\fitch{~~2.~\lnot p\hspace{11ex}\text{Assume}}{\fitch {~3.~p\hspace{10ex}\text{Assume}}{\color{red}{\fitch{~~4.\lnot q\hspace{5ex}\text{Assume}}{~~5.~\lnot p\hspace{5ex}\mathsf R, 2}\\~~6.~\lnot q\to\lnot p\hspace{2ex}\to\mathsf I, 4{-}5\\\fitch{~~7.~\lnot q\hspace{5ex}\text{Assume}}{~~8.~p\hspace{7ex}\mathsf R, 3}\\~~9.~\lnot q\to p\hspace{3ex}\to\mathsf I, 7{-}8\\10.~~\lnot\lnot q\hspace{6ex}\lnot\,\mathsf I,6,9}\\11.~q\hspace{9ex}\lnot\lnot\,\mathsf E,10}\\12.~p\to q\hspace{7ex}\to\mathsf I,3{-}11\\13.~p\hspace{12ex}\to\mathsf E, 1,12}\\14.~\lnot p\to p\hspace{9ex}\to\mathsf E, 2{-}13\\\fitch{15.~\neg p\hspace{12ex}\text{Assume}}{}\\16.~\lnot p\to\lnot p\hspace{7.5ex}\to\mathsf I,15{-}15\\17.~\lnot\lnot p\hspace{13ex}\lnot\,\mathsf I,14,16\\18.~p\hspace{16ex}\lnot\lnot\,\mathsf E, 17}\\19.~(p\to (q\to p))\to p\hspace{2ex}\to\mathsf I,1{-}18}$$
A: proof
GOAL:     ((p => q) => p) => p                     conclusion 

When trying to prove a conditional:


*

*Assume the antecedent


*Try and derive the consequent from your assumption.

In our case (p => q) => p is the antecendent.
p is the consequent.
So now we created a separate sub-problem which we have to solve in order to solve our main problem.

Sub-proof
1. (p => q) => p             premise

...

GOAL:   p                     conclusion  

How do we prove an atom p when given a conditional?
Well we have to use reductio ad absurdum.
We assume the negation of our atom ~p. And we attempt to derive a contradiction.
So now we have created a sub-sub-problem.

Sub-sub-proof
1. ~p             premise

...

GOAL:   ~p => z
        ~p => ~z                    conclusion

where z is some expression.
Instantiating our sub-sub-proof
0. (p => q) => p          premise (we are allowed to reuse this information from the main proof in this subproof)

1. ~p                     premise
2.     p                  assumption 
3.         ~q             assumption
4.         p              reiteration                 2
5.     ~q => p            implication introduction    4-5
6.         ~q             assumption
7.         ~p             reiteration                 1
8.     ~q => ~p           implication introduction    6-7
9.     ~~q                negation introduction       5,8
10.    q                  negation elimination        9
11. p => q                implication introduction    1-11
12. p                     implication elimination     0,11
~p => p

Combining the conclusion of our sub-sub-proof with the tautology ~p => ~p we get our desired contradiction.
All together
1.     (p => q) => p             assumption
2.         ~p                    assumption 
3.             p                 assumption
4.                 ~q            assumption 
5                  p             reiteration                 2
6.             ~q => p           implication introduction    4-5
7.                 ~q            assumption
8.                 ~p            reiteration                 2
9.             ~q => ~p          implication introduction    7-8
10.            ~~q               negation introduction       6,9
11.            q                 negation elimination        10
12.        p => q                implication introduction    3-11
13.        p                     implication elimination     1,12
14.    ~p => p                   implication introduction    2,13   
15.        ~p                    assumption
16.    ~p => ~p                  implication introduction    15,15
17.    ~~p                       negation introduction       14,16
18.    p                         negation elimination        17
  ((p => q) => p) => p           implication introduction    1,18

