Proof of $A \lor B, \lnot A\models B$ with natural deduction 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.
 A: 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")):


*

*$A \lor B$ (Premise)

*$\neg A$ (Premise)

*$A$ (Assumption) (Open assumptions: $A$)

*$\bot$ (Non-Contradiction -- 2. and 3.) (Open assumptions: $A$)

*$B$ ($\bot$-Elimination) (Open assumptions: $A$)

*$B$ (Assumption) (Open assumptions: $B$)

*$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.
A: 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:


*

*$A \lor B\qquad\qquad\qquad\text{premise}$

*$\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$)}$



*$B \qquad\qquad\qquad\quad\;\text{(OR elimination 1, 4, 8)}$

A: 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


