2
$\begingroup$

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)
    Q.E.D

Is my proof correct?

$\endgroup$
6
  • $\begingroup$ your statement is missing a closing parenthesis $\endgroup$
    – J. W. Tanner
    Jun 13, 2019 at 17:46
  • $\begingroup$ @J.W.Tanner What do you mean by this? $\endgroup$
    – Tuki
    Jun 13, 2019 at 17:47
  • $\begingroup$ The first $($ is extraneous $\endgroup$
    – Bram28
    Jun 13, 2019 at 17:48
  • 1
    $\begingroup$ Yes that would be typo, I'll fix that $\endgroup$
    – Tuki
    Jun 13, 2019 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, 2019 at 17:51

1 Answer 1

Reset to default
1
$\begingroup$

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!

$\endgroup$
4
  • $\begingroup$ Are you sure about that? $\endgroup$
    – Bertrand Wittgenstein's Ghost
    Jun 13, 2019 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, 2019 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, 2019 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, 2019 at 11:45

You must log in to answer this question.

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