deducing $\lnot B \implies \lnot A$ from $A \implies B$ One way how to prove a statement of the form $A \implies B$ is to presume that $A$ is true and deduce $B$. Lets have $A \implies B$ and lets assume that $\text{not}~B$ is true. $A$ is true or it is false (duh). If it were true, $B$ would also be true. However, we know that $B$ is not true and therefore $A$ must not be true either. We conclude $\lnot B \implies \lnot A$.
The other direction follows similarly.


*

*Is my deduction sound?

*Is there a more formal way to see these two are equivalent?

 A: Yes, indeed, you've informally argued using a proof by contradiction.
(1) Given $A \rightarrow B$.


*

*(2) Assume $\lnot B$.

*

*(3) Assume $A$.

*(4) Then $B\;$ ((1) & (3), modus ponens)

*(5) Then $\lnot B \land B\;$ ((2) & (4) $\land$-Introduction)

*(6) $\perp\;$ Contradiction. (5)


*(7) Therefore $\lnot A\;$ ((3) - (6), $\lnot$-Introduction)


(8) Therefore $\lnot B \rightarrow \lnot A\;$ (2-7)
Similarly, we can deduce $A\rightarrow B$ if given that $\lnot B \rightarrow \lnot A$.
With both directions proven, we will have then proven (by natural deduction) the equivalence of an implication and its contrapositive: $$A \rightarrow B \iff \lnot B \rightarrow \lnot A$$
A: @amWhy gives the standard Natural Deduction proof. And note that it does not, repeat NOT, depend on the assumption that "A is true or false". That's significant. the inference from $A \to B$ to its contrapositive $\neg B \to \neg A$ is valid in intuitionistic logic where we don't have the law of excluded middle. So your informal argument wen't wrong by suggesting that the law of excluded middle was involved, even though you didn't actually depend on it.
A: Formally, negation can be defined (and often is defined) by saying that $\neg P$ means $P \to \bot$ where $\bot$ is a 0-ary logical connective denoting absurdity.
So if you have $A \to B$ and $\neg B$ then you have $A \to B$ and $B \to \bot$, and we can combine these implications to get $A \to \bot$, which by definition is $\neg A$.
Note that the assumption "$A$ is true or false" is not needed, nor is any other application of the law of excluded middle.
A: This is exactly the same solution as given by amWhy, but written in a format that makes the assumptions a bit more explicit (I prefer it for that reason).
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: $A \rightarrow B \vdash \neg B \rightarrow \neg A$
\begin{align*}
1     & &(1) & &A \rightarrow B  & &A\\
2     & &(2) & &\neg B           & &A\\
3     & &(3) & &A                & &A\\
1,3   & &(4) & &B                & &\rightarrow{}E\  1,3\\
1,2,3 & &(5) & &\bot             & &\neg{}E\  2,4\\
1,2   & &(6) & &\neg A           & &\neg{}I\  5[3]\\
1     & &(7) & &\neg B \rightarrow\neg A           & &\rightarrow{}I\  6[2]
\end{align*}
