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?
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
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.
See also Proof by cases.
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æ:
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).