# How to prove (A v ¬ B), (¬ A v C), (¬ C → B) therefore (¬ D v C)

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.

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:

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

• "`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"

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:

**RULE NAME: IMPLICATION -- PARENT TO LEFT-CHILD **
`[¬ (α -> β)] therefore α`

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

IMPLICATION -- PARENT TO RIGHT-CHILD
INPUT "`α -> β`" is `false` OUTPUT: "`β`" is `false`

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

** DISJUNCTION -- PARENT TO LEFT-CHILD**
INPUT "`α v β`" is `false` OUTPUT: "`α`" is `false`

** DISJUNCTION -- PARENT TO RIGHT-CHILD**
INPUT "`α v β`" is `false` OUTPUT: "`β`" is `false`

Anyway, just keep going like that.

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.