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-

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;_implication_and_conjunction https://en.wikipedia.org/wiki/Galois_connection#Power_set;_i...