I have the following premises:

$$A \Rightarrow B, (C \vee \neg A) \Rightarrow F, B \Rightarrow D, \neg D$$

I attempted to construct a proof for the conclusion $F$ using inference rules, but I'm not sure if my proof is correct. Here is the proof I came up with:

  1. $B \Rightarrow D$: Premise 1 (P1)
  2. $\neg D$: Premise 2 (P2)
  3. $\neg B$: Modus tollens on P1 and P2
  4. $A \Rightarrow B$: Premise 3 (P3)
  5. $ \neg A$: Modus tollens on 3. and P3
  6. $ (C \vee \neg A) \Rightarrow F $: Premise 4 (P4)
  7. $ \neg (C \vee \neg A) \vee F $: Implication elimination in 6.
  8. $ (\neg C \wedge \neg \neg A) \vee F $ DeMorgan Law
  9. $ (\neg C \wedge A) \vee F $ : Double negation in 8.
  10. $ F \vee (\neg C \wedge A) $ : Commutativity law
  11. $ (F \vee A) \wedge (F \vee \neg C) $ : Distributivity law
  12. $ F \vee A $ & $\wedge$-elimination through simplification rule
  13. $ F $: Disjunctive syllogism of 12. and 5. $(\neg A)$
  14. $ F $: Conclusion

Is this proof correct?

Any suggestions or corrections would be appreciated!

  • 1
    $\begingroup$ How about you say anywhere up front what you are trying to prove. It makes it a lot easier to read a proof if you know the goal. And the title is wrong - the proof is not "of" the premises. $\endgroup$ Commented May 19 at 10:57
  • 2
    $\begingroup$ Maybe after step 5 Addition will be useful: from $\lnot A$ to $C \lor \lnot A$. $\endgroup$ Commented May 19 at 13:02
  • 1
    $\begingroup$ Note that technically, your proof should be a semantic one since you use $\vDash$ as opposed to $\vdash$. Otherwise, it looks fine. $\endgroup$
    – PW_246
    Commented May 19 at 16:38


You must log in to answer this question.

Browse other questions tagged .