# Natural deduction proof (Fitch) - Alternative using disjunction exclusion

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

• Not clear... In your proof above you have proved something different (and the proof is unnecessary complicated). Now the question is: what are you trying to prove ? $\dfrac {\lnot \phi}{\phi \vdash 0}$ or $\dfrac {\phi \vdash 0}{\lnot \phi}$ ? Sep 30, 2020 at 13:28
• "A mathematical proof is an inferential argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion." This holds also in mathematical logic. Sep 30, 2020 at 13:34
• Maybe it will be helpful if you list the rules regarding $\lnot$ and $0$ that you are allowed to use: $(\lnot \text E)$, $(0 \text I)$ and $(0 \text E)$ Sep 30, 2020 at 14:38
• So what rules can you use? Sep 30, 2020 at 17:14
• Also, that second proof is still not a proper proof .. you can't have two assumptions in a subproof ... or at least there is no formal rule I know of that makes any practical use of something like that.... unless you do have such a rule? Again, we need to know the rules that you an use in order to answer your question Sep 30, 2020 at 17:29

$$\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\\ }$$