<p>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.</p>

CC BY-SA 3.0
2014-05-23T17:57:45.667Z
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
CC BY-SA 3.0
2014-05-23T16:08:48.030Z
2014-05-23T16:08:48.030Z
cody
<p>While it is trivial to prove contraposition</p>

<pre><code>∀ A B: Prop, (A → B) → (~B → ~A)
</code></pre>

<p>using Coq, is it equally trivial to prove the reversed form:</p>

<pre><code>∀ A B: Prop, (~A → ~B) → (B → A)
</code></pre>

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

<coq>
Reverse contraposition
Alexander Kogtenkov
# Reverse contraposition

(Asked by: username_0 on 2014-05-23)

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?

**Tags:** coq


---

## 1 answers

### Answer by username_1 on 2014-05-23. Score: 3 | Accepted 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.

> **Comments:**
> **username_0**: 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.  

---

