I have to build a fitch proof for the negation introduction rule
with some constraints: I cannot use ¬¬E, ¬I, RAA (Reductio ad absurdum) and ¬¬I. There is also another constraint saying that I have to use the law of excluded middle (LEM).
There are two tips provided to solve the problem. First of all, I have to use ¬E (or 0I). Second of all, I have to use the disjunction elimination:
The only way I found how to solve it is the following way:
Does anyone have an idea on how to use the disjunction elimination? As my solution doesn't use it?
EDIT 1: Correction in proof
EDIT 2: Thank you so much to @MauroALLEGRANZA for the help. This is what I came up with.
EDIT 3: Here are the rules I can use: https://drive.google.com/file/d/19WQOPuxyskq2s_eWXvR04sl6qMUG5CKx/view?usp=sharing




How about something like:
$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$
$\fitch{ 1. \phi \vdash \bot \qquad \quad Assumption}{ 2. \phi \lor \neg \phi \qquad \quad \qquad LEM\\ \fitch{3. \phi \qquad \quad \quad Assumption} {4. \bot \qquad \vdash \ Elim \ (?) \ 3\\ 5. \neg \phi \qquad \bot \ Elim \ 4\\}\\ 6. \phi \vdash \neg \phi \vdash \ Intro \ (?) \ 3-5\\ \fitch{7. \neg \phi \qquad \quad \quad Assumption} {8. \neg \phi \qquad Reit \ 6\\}\\ 9. \neg \phi \vdash \neg \phi \vdash \ Intro \ (?) \ 6-7\\ 10. \neg \phi \qquad \qquad \lor \ Elim \ 2,6,9\\ }$