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.

The proof

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!

  • $\begingroup$ Replace $\neg Q$ with another letter, say $A$. Now review negation introduction. What exactly does it allow you to conclude? $\endgroup$ – Git Gud Feb 9 at 22:03
  • 1
    $\begingroup$ HINT: The rule is called $\neg$ Introduction $\endgroup$ – Bram28 Feb 9 at 22:12
  • $\begingroup$ Ah I see...so by using ¬ Introduction I changed line 13 to ¬¬Q and then created line 14 which states Q with a DNE justification. That works out. Thanks so much! I am however still perplexed by the contradiction in the premises...I guess I should just always pick the premises that proves what I am trying to do... $\endgroup$ – Gerhardus Carinus Feb 9 at 22:21
  • $\begingroup$ @GerhardusCarinus I have no idea of what you mean with contradiction in the premisses. Still regarding your proof, some of the lines can be eliminated, they aren't doing anything at all. Work backwards from the end to try to find them. $\endgroup$ – Git Gud Feb 9 at 22:28
  • $\begingroup$ Thank you Git Gud - yes, I found the lines I'm not using :-) also, thank you for formatting my question properly! To explain what I mean by 'contradiction in the premises'. Looking at the example above, line 8 states R ∧ ¬P. Now, you can see I used the ¬P part of that conjunction to deduce Q (from line 4), which leads to the contradiction I am trying to prove. However, what if I decided to rather use the R part of R ∧ ¬P (which I should be able to do as it is a conjunction)? This leads to ¬Q (due to line 5) which would NOT prove my contradiction. Shouldn't all cases work out? $\endgroup$ – Gerhardus Carinus Feb 10 at 5:25

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:

enter image description here

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/


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$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.