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?

10 Answers 10


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:

enter image description here

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.:

enter image description here

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.



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.

See also Proof by cases.


It helps to rewrite each implication as a disjunction, viz. enter image description here


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æ:

enter image description here

  • 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? – Frank Hubeny 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. – Laurence R. Ugalde 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. – Frank Hubeny 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.


(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

enter image description here

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.