Deriving A implies B from Not A My logic textbook has the following example showing how to derive $A \to B$ from $\neg A$:
First we assume $A$ and use the conjunction introduction rule which results in a contradiction $[A] \land \neg A$. Now we can use the negation introduction rule to get $\neg \neg B$. With the negation elimination rule we get $B$ and after using the implication introduction rule we have $A \to B$.
However, I'm confused when it comes to using the negation introduction rule to get $\neg \neg B$ from $A \land \neg A$. While $A \land \neg A$ is clearly a contradiction resulting from our (temporary) assumption $A$, shouldn't this result the opposite of our assumption, that is $\neg A$, being true? Where does the $\neg \neg B$ come from? Quoting my textbook: "When we have derived a contradiction $B \land \neg B$ from the temporary assumption $A$, we consider $\neg A$ proved."
 A: Not having the proof in front of me, I can't really comment on the proof you are referring to, as a whole, as I can only conclude that you are perhaps mixing up proofs?
Your post begins by stating that you are concerned about a proof in your text about deducing $A\rightarrow B$ from the premise $\lnot A$. And you start by suggesting that the proof proceeds by making the assumption $A$.  With this assumption, together with the premise $\lnot A$, we have conjunction introduction to get $A \land \lnot A$.
But then you go on to discuss $\lnot \lnot B$, and in your second paragraph, refer to the result of having proved $\lnot A$. What I'm confused about is why set out to prove $A \implies B$, given $\lnot A$, and conclude, $\lnot A$ is therefore true?  
What I suspect your text is proving is something like the following:


*

*$\lnot A\quad \text{premise}$

*$\;\;\;*\;\;A\quad \text{assumption}$

*$\;\;\;*\;\;*\;\;\lnot B\quad\text{assumption}$

*$\;\;\;*\;\;*\;\;A \land \lnot A \quad\text{$1, 2$, conjunction introduction}$

*$\;\;\;*\;\;\lnot\lnot B \quad\text{$3, 4$, negation introduction}$

*$\;\;\;*\;\;B\quad\quad\text{$5$, negation elimination}$

*$A\rightarrow B \quad\text{$2-6$, conditional introduction}$


Note that following $(4)$, having derived a contradiction, namely $A \land \lnot A$, we can deny any assumption occuring prior to the contradiction. 

However, we can alternatively start with the given premise, $\lnot A$.  By disjunction introduction $\lnot A \lor B$ then follows. But $$\lnot A \lor B \equiv A\rightarrow B,$$ thus proving that from $\lnot A$ we can derive $A \rightarrow B$.
A: A negation introduction rule often means that from a contradiction we can infer the negation of the proposition that we've assumed.  So, I think your textbook aims at some proof like this (note the difference with amWhy's proof):
1 $\lnot$ A assumption
2 |  A assumption
3 || $\lnot$ B assumption
4 || (A $\land$ $\lnot$ A) 1, 2 conjunction introduction
5 | $\lnot$ $\lnot$ B 3-4 negation introduction
6 | B 5 negation elimination
7 (A $\implies$ B) 3-6 conditional introduction
The $\lnot$ $\lnot$ B comes from assuming $\lnot$ B, deriving a contradiction, and then using negation introduction.
A: Again (I did this for another (great!) answer by amWhy already) I am giving an alternative representation of amWhy's proof that makes all assumptions much more explicit. I did this here for myself anyway (to truly understand this proof), so I just tex'd it.
Format:
col 1 = assumptions,
col 2 = line number,
col 3 = derived formula,
col 4 = the numbers used are all line numbers, except for numbers in "[]", which are the assumption numbers that get discharged
We want to show: $\neg A \vdash A \rightarrow B$
\begin{align*}
1     & &(1) & &\neg A           & &A\\
2     & &(2) & &A                & &A\\
1,2   & &(3) & &\bot             & &\neg{}E\  1,2\\
1,2   & &(4) & &\neg \neg B      & &\neg{}I\  3[]\\
1,2   & &(5) & &B                & &\neg\neg{}E\ 4\\
1   & &(6) & &A\rightarrow B   & &\rightarrow{}I\ 5[2]
\end{align*}
In the above proof there are two things to note:
1. The negation elimination in line (4) discharges an assumption that was not explicitly made, thus the empty parentheses. Alternatively, we could have made an assumption 3 $\neg B$ and then discharged this assumption. Both variants are complelety equivlant, the one shown is just shorter.
2. Just like in all the orher proofs provides here, we cannot introduce B directly, but not B, as the only rule that allows us to infer something from a contradiction (i.e., $\bot$) is negation introdcution. Well, and not surprisingly, this rule has to introduce a negation... So we introduce a negation to negated B thus later leading to B.
