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 1


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.

  • $\begingroup$ 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. $\endgroup$ May 23, 2014 at 17:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.