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:

  1. $\lnot A\quad \text{premise}$
  2. $\;\;\;*\;\;A\quad \text{assumption}$
  3. $\;\;\;*\;\;*\;\;\lnot B\quad\text{assumption}$
  4. $\;\;\;*\;\;*\;\;A \land \lnot A \quad\text{$1, 2$, conjunction introduction}$
  5. $\;\;\;*\;\;\lnot\lnot B \quad\text{$3, 4$, negation introduction}$
  6. $\;\;\;*\;\;B\quad\quad\text{$5$, negation elimination}$
  7. $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$.