# Reverse contraposition

While it is trivial to prove contraposition

∀ A B: Prop, (A → B) → (~B → ~A)


using Coq, is it equally trivial to prove the reversed form:

∀ A B: Prop, (~A → ~B) → (B → A)


? In particular, is it doable without using any additional axioms, e.g. from classical logic?

## 1 Answer

It is not provable without additional axioms. In fact, it implies double negation elimination (take $B=\top$), which in turn is equivalent to the excluded middle.

• This was my feeling as well, but I do not know how to turn this feeling into a proof that this formula cannot be proved without an additional axiom, as well as to figure out which axiom will be a minimal addition that makes the proof possible. – Alexander Kogtenkov May 23 '14 at 17:57