[Math] Proof of $A \lor B, \lnot A\models B$ with natural deduction

logicpropositional-calculus

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.

Best Answer

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$)}$
  9. $B \qquad\qquad\qquad\quad\;\text{(OR elimination 1, 4, 8)}$
Related Question