Prove that: $A \lor B, \lnot A\models B$

Looks easy but im stuck, and i dont know if to start with an OR elimination or with NOT introduction.

Also, different books/texts/etc about Natural Deduction uses different notations (Fitch scheme or tree-like inferences) and "diferent" rules... for example, the RAA (reduction to absurd) rule looks like the same thing that the NOT introduction, i can work with the NOT introduction and never care about RAA, so i dont know wath is it for, maybe they are just the same.

Any help about this topic would be appreciated.

Now i have this:

    • $A \lor B$
    • $\lnot A$
    • assume B
      • B by "Iteration with 3"?, i dont know if this is the way to write it...
    • assume A
      • assume $\lnot B$
        • A by AND elimination with 1
        • $\lnot A$ by "Iteration with 2"?
        • $\bot$ falsum introduction with 7,8.
      • B by NOT introduction with 6,9
    • B by OR elimination 1,4,10

Also the " falsum introduction with 7,8. " is more like an AND introduction that generates the contradiction, dont know wich is the correct way to handle it.

  • $\begingroup$ What's your rule for negation elimination? $\endgroup$ Jun 10, 2013 at 16:53
  • $\begingroup$ @DougSpoonwood Mi rule for NOT elimination is: "A, $\lnot A$ then $\bot$ ". Wich i dont understand, i mean... i can use it but i think that something like: $\lnot \lnot A$ then A, makes more sense for this rule. $\endgroup$
    – Wyvern666
    Jun 10, 2013 at 17:39
  • $\begingroup$ You sure that's your rule? In some natural deduction system you have the rule ""A, ⊥, then [meaning infer] ¬A " in other natural deduction systems you have "¬¬A then A". It looks like your system has the first rule. $\endgroup$ Jun 10, 2013 at 23:28

3 Answers 3


Given the inference rules you are using, you're on the right track, but I've suggested some omissions.

For example, you cannot invoke "AND" elimination on $(1)$, since $(1)$ is a disjunction and is already an operative assumption $(5)$! Nor do you need to reiterate $A$, because that is an operative assumption. Further, there's no need to reiterate $\lnot A$, since the scope of the premise includes the "assumptive subproof", and so is valid to appeal to/use from within the subproof.

Invoking "NOT Introduction", as you use it, seems contrary to your previously posted definition of RAA:

And this is the RAA (reduction to absurd) rule:

Suppose $\lnot A$. Derive $\bot$. Then (discharging the assumption) $A$.

So I will use RAA:

  1. $A \lor B\qquad\qquad\qquad\text{premise}$
  2. $\lnot A \qquad\qquad\qquad\quad\text{premise}$
    • $B\qquad\qquad\qquad\;\text{ (assumption)}$
      • $B\qquad\qquad\quad\text{(iteration of $(3)$)}$
    • $A \qquad\qquad\qquad\text{(assumption)}$
      • $\lnot B\qquad\qquad\text{(assumption)}$
      • $\bot \qquad\quad\text{falsum introduction with (5, 2))}$
    • $B \qquad\qquad\quad\text{(RAA with 6,7), (discharge of assumption $\lnot B$)}$
  3. $B \qquad\qquad\qquad\quad\;\text{(OR elimination 1, 4, 8)}$
  • $\begingroup$ When do you think is necessary the "iteration of n" thing when working with this demostration scheme?. Because in a top-down tree model i never need it. $\endgroup$
    – Wyvern666
    Jun 10, 2013 at 20:27
  • 1
    $\begingroup$ I used it, e.g., immediately following the assumption $B$, to have a "conclusion" to that subproof. "Assuming B, then B". It never hurts to include it, but isn't usually necessary when it exists within a statement's scope. So you weren't wrong in iterating when you did. Does this make sense? $\endgroup$
    – amWhy
    Jun 10, 2013 at 20:31
  • $\begingroup$ Newly introduced assumptions don't have the same scope as premises. Also, falsum introduction doesn't change scope like the introduction of a new assumption. In step 8, you didn't introduce a negation symbol, you eliminated it. $\endgroup$ Jun 11, 2013 at 0:09
  • $\begingroup$ @Doug I didn't claim it had the scope, but if it is an open assumption previously made, it does not need reiteration. It WAS needed for $B$. Please, stop harassing me. $\endgroup$
    – amWhy
    Jun 11, 2013 at 0:13
  • 1
    $\begingroup$ @Wyvern666 You're doing good work! Keep it up! I'll keep my eye out on your newest post, to see if you get any more clarification on the answer given! $\endgroup$
    – amWhy
    Jun 12, 2013 at 4:50

amWhy's answer provides one possible interpretation of $\lor$-elimination. Another form of it is:

Given proofs of $A \to C$ and $B \to C$, we may infer $A \lor B \to C$.

which obviously calls for a slightly different approach. We will need $\bot$-elimination:

Given a proof of $\bot$, we may infer any statement $A$.

Using the above rules, we form the following proof (a line consists of "statement" ("rule used") ("open assumptions")):

  1. $A \lor B$ (Premise)
  2. $\neg A$ (Premise)
  3. $A$ (Assumption) (Open assumptions: $A$)
  4. $\bot$ (Non-Contradiction -- 2. and 3.) (Open assumptions: $A$)
  5. $B$ ($\bot$-Elimination) (Open assumptions: $A$)
  6. $B$ (Assumption) (Open assumptions: $B$)
  7. $B$ ($\lor$-Elimination)

It is sad that so many different forms of natural deduction exist due to authors' wildly varying preferences; this makes it significantly harder to help teaching the material to new apprentices in the subject. Usually, the approaches are equivalent, and all of them have their merits and drawbacks.

There is really no way around getting one's hands dirty to grasp the matter for the first time. Once you do, it is advisable to look at different systems and discover why, and how, they are equivalent. This will greatly enhance your understanding of the subject -- at least, it did for me.

  • 1
    $\begingroup$ The proof given uses the rule: Given $A \lor B$, and a proof from $A$ to $C$, and a proof from $B$ to $C$, infer $C$. Which is indeed the canonical statement of or-elimination in a ND setting. $\endgroup$ Jun 10, 2013 at 17:43
  • $\begingroup$ @Lord_Farin Please see mi edit, i used the OR elimination. I think is a longer solution than yours but maybe is correct. $\endgroup$
    – Wyvern666
    Jun 10, 2013 at 17:44
  • 1
    $\begingroup$ I do not know what you mean by "AND elimination with 1", and it is not necessary to assume $\neg B$; we already have $A$ as a standing assumption in 5., so 9. can actually be 6. (but now applied to 2. and 5.). And if you then look at the resulting proof, you see it's the same as the one in my answer. Cheers! $\endgroup$
    – Lord_Farin
    Jun 10, 2013 at 17:55
  • $\begingroup$ Thanks. Hehe, the "AND elimination with 1" was a fail, i already had "A" in 5 as you said. $\endgroup$
    – Wyvern666
    Jun 10, 2013 at 20:29
  • $\begingroup$ I don't see how your rule for $\lor$ consists of an elimination rule. I also don't see how you used it here. Did you get a proof of "A→B" and "B→B"? If you did, your rule would give you ((B$\lor$B)→B), which isn't what you want to prove here. $\endgroup$ Jun 11, 2013 at 0:18

You're looking for a formal proof or derivation, not a semantical argument (in which case you could use a truth table... and that seems shorter here than a formal proof). So, you want to show A∨B, ¬A |- B.

Anytime you include a new assumption, you need to keep track of the scope of that assumption. One way to do this consists of always using one more raise dot (or lines... or boxes) when introducing a new assumption. If you use dots to keep track of the scope of the assumption, you only introduce dots when you make a new assumption. You also only end up with fewer dots when the assumption has gotten discharged.

    • A assumption

By itself the above consists of a proof which starts with A and ends with A. You could also write:

    • A assumption
    • A 1 repetition, or reiteration, or repeat

If for some reason your rule doesn't quite seem to allow either of those, then you could do the following proof:

    • A assumption
    • (A$\lor$A) 1 OR Introduction
    • (A$\land$(A $\lor$ A)) 2, 1 AND introduction
    • A 3, AND elimination

You can prove the same theorems in a natural deductive system which doesn't have falsum introduction, as one which has falsum introduction. The negation introduction rule then can go something like "from a derivation which starts with p, and ends with (q $\land$ $\lnot$ q), infer $\lnot$p" and the negation elimination rule can go something like "from a derivation which starts with $\lnot$p, and ends with (q $\land$ $\lnot$ q), infer p." I'll use that negation elimination below.

Additionally, before I write out a proof here, I'll use a slightly different (though basically equivalent) OR elimination rule than you might have seen, because I think it makes it easier to keep track of scope here. The rule says "From (p$\lor$q), (p$\implies$r), (q$\implies$r), you may infer r."

    • (A∨B) premise
    • ¬A premise
      • B assumption
    • (B$\implies$B) 3-3 conditional introduction (so 3. has gotten discharged and can't get used again)
      • A assumption
        • $\lnot$ B assumption
        • (A$\land$¬A) 5, 2 AND introduction
      • B 6-7 negation elimination
    • (A$\implies$B) 5-8 conditional introduction
    • B 1, 4, 9 OR elimination
  • $\begingroup$ If you prefer to use the negation elimination rule "from $\lnot$$\lnot$p, infer p", then you could use negation introduction at step 8 giving you $\lnot$$\lnot$B, and then use negation elimination to get B. $\endgroup$ Jun 11, 2013 at 0:13
  • 1
    $\begingroup$ Doug, there are different systems, with different rules. To adamantly insist upon a superior, one-and-only valid system, or method, as being correct is pretentious, at best. $\endgroup$
    – amWhy
    Jun 11, 2013 at 0:21
  • $\begingroup$ @amWhy I'm not insisting on any system as superior overall. What are you objecting to with your comment? $\endgroup$ Jun 11, 2013 at 0:23

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .