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

Obviously since A → C and B → D then if A v B one of C or D must be true.

My only idea is v must be introduced, but how would I use subproofs to show one of A /\ C or B /\ D is never false if A v B?

Here is part of the question:

My only idea is v must be introduced, but how would I use subproofs to show one of A/\C or B/\D is never false if A v B?

It might be best to think of using disjunction elimination initially although disjunction introduction may be needed later.

The OP notes the following:

Obviously since A → C and B → D then if A v B one of C or D must be true.

Even though this is obvious, the challenge is to provide a proof using inference rules or to use a truth table to show the result. Here are both kinds of solutions.

To provide a proof one could use a natural deduction Fitch-style proof checker: Note how both cases of the disjunction in line 1 are handled separately. The A case is handled in lines 4-6 first using conditional elimination or modus ponens and then disjunction introduction. The B case is handled in lines 7-9 similarly. Finally disjunction elimination is used on the last line to derive the result.

To show this using a truth table first conjoin the premises and then use an implication to connect those conjoined premises with the goal. Place that final proposition in a truth table generator.: Notice that the top-level connective shown in red is true for all valuations of the proposition variables. That means the proposition is a tautology and one can validly derive the goal from the premises.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

Michael Rieppel. Truth Table Generator. https://mrieppel.net/prog/truthtable.html

You can use proof by contradiction:

p1: A v B

p2: A -> C

p3: B -> D

1. assume ~(C v D)
2. ~C & ~D (from 1, De Morgan's law)
3. ~C (from 2, conjunction elimination)
4. ~D (from 2, conjunction elimination)
5. ~A (from 3, p2, modus tollens)
6. B (from 5, p1, disjunctive syllogism)
7. D (from 6, p3, modus ponens)
8. D & ~D (4, 7)

Since D & ~D is a contradiction, our assumption must be false. Therefore C v D.

Hint

You have to apply OR-elimination to first premise and used 2nd and 3rd premises to derive "C OR D" under both cases.

Then the conclusion follows.

It helps to rewrite each implication as a disjunction, viz. Obviously since A → C and B → D then if A v B one of C or D must be true.

That is basically the natural deduction proof right there.

More formally:

• Under the assumption of A we can derive C (by → elimination with premise A → C) and thus C v D (by v-introduction)

• Under the assumption of B we can derive D (by → elimination with premise B → D) and thus C v D (by v-introduction)

• Therefore C v D may be derived using v-elimination and the premises A v B, A → C, B → D.

It can be proved by resolution. The following proof was generated by the resolution prover of Fōrmulæ: • I downloaded Formulae and have it running, but I don't see how you entered this. Is there documentation showing how the logic packages work? Oct 1 '19 at 1:37
• Hi Frank. The logic inference package is disabled by default. Go to Settings -> Packages and enable it. In order to create a predicate, in the tree at left, choose Logic -> Predicate (or press the 'p' key). Editing is very natural but it is tricky at first, I recommend you to read this tutorial wiki.formulae.org/Editing_F%C5%8Drmul%C3%A6_expressions. Oct 1 '19 at 1:44
• Thank you! I realized I needed to include the inference package, but the tutorial I haven't seen yet. That should be all I need. Oct 1 '19 at 2:16

You can also reduce it.

Base Premises: AvB A->C B->D

Break it up:

Part 1: Using Premise A->C, assume A, therefore C by premise

Part 2: Using Premise B->D, assume B, therefore D by premise

The first ignores B and D, the truth of B is irrelevant to Part 1,

The second ignores A and C, the truth of A is irrelevant to Part 2, now the third case,

Part 3: Assume A^B (A and B), therefore C^D by Parts 1 and 2.

Part 4a: Using Premise A->C, assume !A (not A)...the truth of C can be anything and is irrelevant - by definition of implication

Part 4b: Using Premise B->D, assume !B (not B)...the truth of D can be anything and is irrelevant - by definition of implication

Part 5: Assume !A^!B, truths of (CvD) are irrelevant

Asum | P1 | P2 | P3 | Cn

_ | A | A | B | C

_ | v | > | > | v

_ | B | C | D | D

A | T | T | T | T

B | T | T | T | T

AB | T | T | T | T

!A!B | F | T | T | T

Proof in Agda (an interactive theorem prover):

``````data _or_ (A : Set) (B : Set) : Set where
inl : A → A or B
inr : B → A or B

dilemma : {A B C D : Set} (f : A → C) (g : B → D) (t : A or B) → (C or D)
dilemma f g (inl a) = inl (f a)
dilemma f g (inr b) = inr (g b)
``````

We can show that the truth of "C or D" can be derived from the premises using algebra.

For this, it is convenient to use a different notation for logic from the one you are using. Conjunction is denoted by juxtaposition, like algebraic multiplication. XY means "X and Y". Disjunction is denoted using +, so that X + Y means "X or Y". Negation is indicated using ', so that X'Y means "not X and Y". Truth is written as 1, and falsehoold as 0. We will retain the arrow notation for the conditional.

Given:

(A ∨ B) ∧ (A → C) ∧ (B → D)

we can rewrite that is:

(A + B)(A → C)(B → D)

These are our premises, which we are asserting to be true; we can represent that as a nequation:

(A + B)(A → C)(B → D) = 1

We apply the identity (A → C) = A'+C:

(A + B)(A' + C)(B' + D) = 1

Now an algebraic trick: we can multiply out the (A + B) factor to distribute its terms over the other factors:

A(A' + C)(B' + D) + B(A' + C)(B' + D) = 1

Let's rearrange the products in the second term:

A(A' + C)(B' + D) + B(B' + D)(A' + C) = 1

Then we multiply (so to speak) these A and B in:

(AA' + AC)(B' + D) + (BB' + BD)(A' + C) = 1

Note that AA' is a falsehood: "A and not A", and similarly so is BB'. We remove these, and our premises have been reduced to this form:

AC(B' + D) + BD(A' + C) = 1

Our left hand side basically has the form CX + DY where X = A(B' + D) and Y = B(A' + C). We have a "sum of products" representation in which every term has either C or D as a factor:

CX + DY = 1

From this form we know that C and D both cannot be zero/false. Hence, we have established the truth of (C + D).

Simply input inference, and view truth table https://logic-proof.io/87 