Probably à typing mistake in "Denying the consequent" section, which should rather state "if P => Q then not-Q => not-P"?

One quite useful application of this is that implication can play the role of the partial-order operator in a Galois Connection. A Gallois connection is an iff-and-only-if formula of the form

    F(x) ≤ y  iff x ≤ G(y)

One form of this is the tautology when F(x) = (x and a), G(y) = (a => y), and pick logical implication as the "≤".

    ((x and a) => y) iff (x => (a => y))

https://en.wikipedia.org/wiki/Galois_connection#Power_set;_i...

That's because you can consider categories of preorders and formulas where these operators will be morphisms.

(b >= c) && (a >= b) -> (a >= c) is a composition.

The more interesting consequence is that function types and implications are different names for the same thing. This is a Curry-Howard-Lambek correspondence.

This means that in order to prove

(b -> c) -> (a -> b) -> (a -> c)

it's enough to implement a function

f g h x = g (h x)

Another consequence is that exponentiation a^b can be considered the same thing as b -> a.

a^(bc) = (a^b)^c

(b && c) -> a = c -> b -> a

prepositions p(a) -> q(a) can be thought as super set relationships. Let P = {a | p(a) holds} and Q = {a | q(a) holds) then p(a) -> q(a) and the statement P is subset of Q is the same.

Such a satisfying result! However the example is confusing. "Because it is cloudy it will rain." Shouldn't that be the other way around (ie. rain implies the presence of clouds)?

This assumes that the value of true is larger than false. In Visual Basic true is equal to -1, the signed two-complement value were all bits are set.