My idea is to use disjunction elimination on (¬ A v C)to obtain C, and then use disjunction introduction to obtain (¬ D v C), but I'm having a hard time obtaining C.

2 Answers 2


Yes, that's the way to go.

You have two disjunctions in the premise. Eliminate both of them. Eliminate the conditional premise too.

  • When you assume A, you can derive C from ¬ A v C via disjunctive syllogism (or sub-prof)
  • When you assume ¬ B, you derive C from ¬ C → B via modus tollens (or sub-prof).
    • Whenever you can derive C you may derive ¬ D v C by disjunction introduction.
  • Therefore deriving ¬ D v C from A v ¬ B by disjunction elimination.

  |  A v ¬ B          Premise
  |  ¬ A v C          Premise
  |_ ¬ C → B          Premise
  |  A v ¬ B          Reiteration (first premise)
  |  |_ A             Assumption
  |  |  ¬ A v C       Reiteration (second premise)
  |  |  |_ ¬ A        Assumption
  |  |  |  :          :
  |  |  |  ¬ D v C    Somehow
  |  |  + 
  |  |  |_ C          Assumptuon
  |  |  |  ¬ D v C    v-Introduction
  |  |  ¬ D v C       v-Elimination
  |  +
  |  |_ ¬ B           Assumption
  |  |  ¬ C → B       Reiteration (third premise)
  |  |  :             :
  |  |  ¬ D v C       Somehow
  |  ¬ D v C          v-Elimination

First, draw a tree diagram of the formula:

tree diagram with whole formula written inside of each node

When you draw trees by hand, it is faster (and equally correct) to only write down the root operator for each node.
A "node" is one of the circles/boxes in the tree

tree diagram root operators only

  • "therefore" is the same as .
  • comma , has the same meaning as and

I can feel the hate coming, so I will warn you you that some philosophers have a bee in their bonnet about "meta" vs "non-meta" operators:

  • "therefore" is technically meta-level logical implication
  • is the non-meta implication operator ("implication" is if...then)
  • comma , is meta-level conjunction (and operator)
  • some symbol, like ^, represents non-meta conjunction (and operator)

"meta" versus "non-meta" only matters if you do things like define meta-implication differently from non-meta implication.

In your case, your meta-level operators and the non-meta operators are defined the same way. So, there is no difference. For all intents and purposes meta-level and (the comma ,) is the same thing as non-meta and.

Basically, you are trying to prove:

For all A, B, C, and D in the set {true, false}
[(A or [not B]) and ([not A] or C) and ([not C] → B)] → ([not D] or C)

Given that your teacher used separate "therefore" and , I am a little bit worried for you. The same people often also say you cannot prove new rules of inference using the letters ABC...Z.
Instead you must use Greek letters for proving new rules of inference. That is just wrong; factually incorrect.
If you have a bad professor, do what you need to do to pass the class, but take everything they say with a grain of salt.

Anyway... end of digression. Let us get back to proving things!

Do a proof by contradiction.
Begin by assuming that the theorem is false.
Finish by finding a contradiction (X and [not X] for some statement X).

Mark the root node as "false"

enter image description here

There is a rule of inference which says that if an implication node is false, then its left child is true.

For any x, y in {true, false}, [not (x -> y)] -> x

Using your teacher's notation, it probably looks something like this:

[¬ (α -> β)] therefore α

There is a different rule which says that if a -> node is false, then its right child must also be false.

INPUT "α -> β" is false OUTPUT: "β" is false

enter image description here

There is a rule of inference which says that if an or node is false, then both of its children are false.

INPUT "α v β" is false OUTPUT: "α" is false

INPUT "α v β" is false OUTPUT: "β" is false

enter image description here

Anyway, just keep going like that.

enter image description here

Our proof looks like this:

| LINE NO |                         STATEMENT                          | SOURCE LINES |          JUSTIFICATION           |
|       1 | NOT [[(A v ¬ B) and (¬ A v C) and (¬ C → B)] -> (¬ D v C)] | n/a          | assumption                       |
|       2 | [A v (¬ B)] and [(¬ A) v C] and [ (¬C) → B]                | 1            | [¬ (α -> β)] therefore α         |
|       3 | ¬(¬ D v C)                                                 | 1            | [¬ (α -> β)] therefore ¬β        |
|       4 |    D                                                       | 3            | ¬(α v β) therefore ¬α            |
|       5 | ¬C                                                         | 3            | ¬(α v β) therefore ¬β            |
|       6 | (¬C) → B                                                   | 2            | AND(x1, x2, ... xn) therefore xn |
|       7 | B                                                          | 5, 6         | α and (α -> β) therefore β       |
|       8 | A v (¬B)                                                   | 2            | AND(x1, x2, ... xn) therefore xn |
|       9 | A                                                          | 7,8          | (not β) and (α v β) therefore α  |
|      10 | (¬ A) v C                                                  | 2            | AND(x1, x2, ... xn) therefore xn |
|      11 | C                                                          | 9, 10        | (not α) and (α v β) therefore β  |
|      12 | C and (not C)                                              | 5, 11        | conjunction                      |
|      13 | [(A v ¬ B) and (¬ A v C) and (¬ C → B)] -> (¬ D v C)       | 1, 12        | proof by contradiction           |

Your professor might not allow the rules of inference that I used.
If that is the case, just prove each of my rules from your professor's rules.
Then the proof is complete.
All of my rules are very easy to prove.
(not α) and (α v β) therefore β comes straight from the truth-table definition of the v operator.
Mathematicians would just say, "by the definition of the or operator"

Sometimes with the tree-approach, we can get stuck. Sometimes, we cannot propagate a value from parent to child or a child to parent.
Next time, if you ever get stuck using the "tree" diagram method, proceed by cases.
Choose a node to make true in one case and false in the other case.
Write truth values in two different color pens. For example, the node (A v ¬ B) might say true in red ink, and false in blue ink.

You must log in to answer this question.

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