I have the following premise:
$$(A\implies C) \vee (A\implies D)$$
And I have to prove this formula:
$$A\implies C \vee D$$
I don't know how to start. I really appreciate your time.
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It only takes a minute to sign up.Sign up to join this community
Notations : in my answer, $A, B, C...$ are formulas.
Visualize two parts in your mind : the context (premises) and the goal (conclusion). The rules are interactions between and within the context and the goal.
Think of $A \Rightarrow B$ as a function : given a proof of A it produces a proof of B.
The rules have two reading : from top to bottom, given the premises I can have the conclusion. From bottom to top, to prove the conclusion, I have to prove the premises (proof search).
[$\Rightarrow$-introduction] If $A \Rightarrow B$ is in the goal, introduce $A$ in the context and prove $B$ to show that given $A$ you can produce $B$.
[$\lor$-introduction] When $A \lor B$ is in the goal, you have to make a choice : prove $A$ or prove $B$.
[$\Rightarrow$-elimination] When $H: A \Rightarrow B$ is in the context, it can be seen as a function you can use, if you also have $A$ in your context, you can use it to produce a proof of $B$ by function application $H(A) = B$.
[$\lor$-elimination] When $A \lor B$ is in the context and you have a goal $G$, you don't know which one hold so you have to make a proof "by case". You have now two goal :
Either $A$ holds and then you prove $G$
Either $B$ holds and you prove $G$ as well (one path can be contradictory but a least one should succeed).
Notation : Context $\vdash$ Goal
Before writing your proof, try to understand how to connect every rules and "which path to take". You can try to draw a tree from bottom to top for instance then write your proof from top to bottom.
We start with $(A⟹C)∨(A⟹D) \vdash A⟹C∨D$
The obvious first thing to do is to introduce $A$ in the context ($\Rightarrow$-intro) : $A, (A⟹C)∨(A⟹D) \vdash C∨D$
You can : make the choice to prove either $C$ or $D$ but it's wrong since you have a disjunction $\lor$ in your context. You can tell that the disjunction is useful (by looking at its subformulas) and you don't know which side holds so if you make your choice too soon you won't have enough information. Split your proof in two goals ($\lor-elim$) :
In each goal apply the premises together ($\Rightarrow$-elim) then you can make your choice ($\lor$-intro).
Try to write what you've understood with the rules of Natural Deduction