Trouble with negation introduction with Fitch natural deduction proof

Question

I've recently posted another question regarding natural deduction proofs and I've definitely made some progress, but I'm now stuck with a proof which seems like it could be flawed.

Now as you can see, it looks like I've got it all figured out, however you can see an error is returned for incorrect use of negation introduction. Now there seems to be a contradiction in the premises on lines 4 and 5: as per lines 9 and 10, R is true and P is false. I went with P being false (line 10) which leads to a contradiction, seemingly making the proof work out. However, I could just as well have gone with R being true (line 9), which, according to line 5, would not prove my contradiction as I must prove Q.

Am I missing something obvious here or do you think the proof is broken?

Thank you!

Answer 1

The justification for line 13 should be indirect proof (IP) rather than negation introduction. Here is a correct proof using what you have done and the same proof checker:

Indirect proof can be found on page 118 of forallx.

---

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/

Answer 2

Tip: the rule of $\lnot\rm I$ introduces a negation.

So if a contradiction is derived from assuming a negation, we infer that a double negation is the case.   That is $\lnot Q\vdash\bot$ allows us to infer: $\vdash \lnot\lnot Q$.

Having done so, invoke the rule of double negation elimination (denoted: DNE, or $\lnot\lnot\rm E$), and infer that $\vdash Q$.