Proof following statement with interference rules ( without truth table) that

$$ (\neg C \wedge B \wedge (A \rightarrow C) \wedge (B \rightarrow D ) )\implies (\neg A \wedge D ) $$

Attempt to proof

  1. $B$ (premise)
  2. $B \rightarrow D$ (premise)
  3. $D$ (Modus ponens 1,2)
  4. $A \rightarrow C $ (premise)
  5. $\neg C$ (premise)
  6. $\neg A$ (Modus tollens 5,4)
  7. $\neg A \wedge D$ (Conjunction introduction 6, 3)

Is my proof correct?

  • $\begingroup$ your statement is missing a closing parenthesis $\endgroup$ – J. W. Tanner Jun 13 '19 at 17:46
  • $\begingroup$ @J.W.Tanner What do you mean by this? $\endgroup$ – Tuki Jun 13 '19 at 17:47
  • $\begingroup$ The first $($ is extraneous $\endgroup$ – Bram28 Jun 13 '19 at 17:48
  • 1
    $\begingroup$ Yes that would be typo, I'll fix that $\endgroup$ – Tuki Jun 13 '19 at 17:49
  • 1
    $\begingroup$ Since the $\Rightarrow$ is the meta-logical symbol for logical implication, rather than a logical operator (such as $\to$), you actually don't need that outside set of parentheses $\endgroup$ – Bram28 Jun 13 '19 at 17:51

You really have only one premise:

$$ \neg C \wedge B \wedge (A \rightarrow C) \wedge (B \rightarrow D )$$

Thus, you'll need to infer the statements that you have on lines 1,2,4, and 5 from this premise using the Simp rule (this is short for Simplification ... other textbooks call this conjunction elimination)

Also, for line 7, the name of the rule in your system is Conj (short for Conjunction) ... you call this conjunction introduction, and indeed many textbooks do, but in your system it is Conj

Otherwise, your proof looks to be fine!

| cite | improve this answer | |
  • $\begingroup$ Are you sure about that? $\endgroup$ – Bertrand Wittgenstein's Ghost Jun 13 '19 at 17:51
  • $\begingroup$ @BertrandWittgenstein'sGhost Good point (assuming this is what you mean): I can't be certain until the OP lets us know exactly what inference rules need to be used ... edited my answer $\endgroup$ – Bram28 Jun 13 '19 at 17:54
  • $\begingroup$ @Bram28 the exact rules I was suppose to use are here. i.imgur.com/qVTimfL.png, It's in Finnish but you can probably understand it. $\endgroup$ – Tuki Jun 13 '19 at 22:23
  • $\begingroup$ @Tuki Thanks! So yes, the rule of inferring a conjunct from a conjunction is called Simp. (also, in your system the rule to conjunct together any number of claims is called Conj, rather than Conjunction Introduction)) $\endgroup$ – Bram28 Jun 14 '19 at 11:45

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.