>>11511254(A => B) => ((not B) => (not A))
is constructively true. In fact it's a special case of
(A => B) => ((B => C) => (A => C))
The Brouwer–Heyting–Kolmogorov style functional proof p of this is very easy:
p(f) := g \mapsto ( a \mapsto g(f(a)) )
where f:A->B, g:B->C, a:A.
In words
>given a reason f to believe that A implies B, then given a reason g that B implies C, then the following is the case: given a reason that A holds, you can conclude that B holds (via f) and, in turn, that C holds (via g).Replace =>C with =>False to get the claim about negation.
The other direction can't constructively be true. No matter how many reasons to believe about some negations and implications between negations being true, you can't ever find a reason to believe =>B (unless you take double negation as an axiom)
