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.

  • 1
    $\begingroup$ Assume $A$ and then apply $\lor$-elim to the premise deriving $C \lor D$ in both cases. $\endgroup$ – Mauro ALLEGRANZA Mar 13 '17 at 20:26
  • $\begingroup$ Thanks @Mauro. V-elim or ⟹-elim? $\endgroup$ – user425260 Mar 13 '17 at 20:59
  • $\begingroup$ Start with learning the rules of natural deduction, making sure you know what they mean. $\endgroup$ – DanielV Mar 13 '17 at 21:06
  • $\begingroup$ What does ⟹ mean in your context ? I think I misunderstood something. I thought it was the implication symbol. $\endgroup$ – Boris Mar 18 '17 at 17:54

How to start


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

Understanding of the rules

  1. [$\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$.

  2. [$\lor$-introduction] When $A \lor B$ is in the goal, you have to make a choice : prove $A$ or prove $B$.

  3. [$\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$.

  4. [$\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).

How to prove

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.

  1. We start with $(A⟹C)∨(A⟹D) \vdash A⟹C∨D$

  2. The obvious first thing to do is to introduce $A$ in the context ($\Rightarrow$-intro) : $A, (A⟹C)∨(A⟹D) \vdash C∨D$

  3. 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$) :

    • $A, (A⟹C) \vdash C∨D$
    • $A, (A⟹D) \vdash C∨D$
  4. In each goal apply the premises together ($\Rightarrow$-elim) then you can make your choice ($\lor$-intro).

  5. Try to write what you've understood with the rules of Natural Deduction

| cite | improve this answer | |
  • $\begingroup$ Nice guide to doing formal proofs!! $\endgroup$ – Bram28 Mar 13 '17 at 21:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy