1
$\begingroup$

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

$\endgroup$
13
  • 1
    $\begingroup$ 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}$ ? $\endgroup$
    – Mauro ALLEGRANZA
    Sep 30, 2020 at 13:28
  • 1
    $\begingroup$ "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. $\endgroup$
    – Mauro ALLEGRANZA
    Sep 30, 2020 at 13:34
  • 1
    $\begingroup$ 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)$ $\endgroup$
    – Mauro ALLEGRANZA
    Sep 30, 2020 at 14:38
  • 1
    $\begingroup$ So what rules can you use? $\endgroup$
    – Bram28
    Sep 30, 2020 at 17:14
  • 1
    $\begingroup$ 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 $\endgroup$
    – Bram28
    Sep 30, 2020 at 17:29

1 Answer 1

Reset to default
1
$\begingroup$

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

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .