Natural deduction proof (Fitch) - Alternative using disjunction exclusion

185 Views Asked by At

I have to build a fitch proof for the negation introduction rule

enter image description here

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:

enter image description here

The only way I found how to solve it is the following way:

enter image description here

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.

enter image description here

EDIT 3: Here are the rules I can use: https://drive.google.com/file/d/19WQOPuxyskq2s_eWXvR04sl6qMUG5CKx/view?usp=sharing

1

There are 1 best solutions below

0
On

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