Deriving A implies B from Not 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$.