Logical implication is a comparison operator
18 comments
·July 17, 2025null
practal
In Terence Tao's book "Compactness and Contradiction", at the very start on page 1, he introduces material implication "If A Then B" (or "A implies B") as "B is at least as true as A", and then lists the various easy conclusions one can draw from this.
Very interesting, I think, that "A implies B" is the same as "A ≼ B", is apparently mathematical main stream, and not just popular in formal logic.
If you continue along these lines, you also not just need to ask, what is implication, but what are A and B? Well, they are things you can compare for their truth content, so let's call them truth values. Surely, "≼" should form a partial order, and if you want arbitrary conjunction and disjunction to exist, truth values with "≼" should form a complete lattice T. This means that "∧" and "∨" are now operations T×T → T. If you want implication ALSO to be such an operation "⇒", instead of just the comparison relation "≼", you can use the following condition (somebody already mentioned it in another comment here, via Galois connections), which just means that "A and B imply C" is the same as "A implies that (B implies C)", interpreting implication simultaneously as "⇒" and "≼":
A ∧ B ≼ C iff A ≼ B ⇒ C
This is exactly how I turn abstraction algebra into abstraction logic [2].
[1] https://proofwiki.org/wiki/Axiom:Infinite_Join_Distributive_...
gettingoverit
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
spyrja
Another consequence is that exponentiation a^b can be considered the same thing as b -> a.
In the case where a and b are not strictly boolean (supposing they are instead probabilities for example) you could even generalize it somewhat in terms of "pure" mathematical operations.
double implies(double a, double b) {
double dif = a - b;
double abx = sqrt(dif * dif);
return 1 + pow(0, abx - dif) - pow(1, abx + dif);
}
gettingoverit
Nice to know!
I thought about it in terms of cardinalities of types. If A and B are types with |A| and |B| values correspondingly, there are |B|^|A| possible functions A -> B.
Another funny thing is that if you consider
forall a. (a -> a) -> (a -> a)
the type of natural numbers (weird, I know, but basically we encode numbers in unary with number of times we compose (a -> a) to itself), then exponentiation on such numbers will be
a ^ b = b a
spyrja
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)?
atoav
Given that it can be cloudy and not rain, but (for the sake of the example) not rain without clouds¹ I would agree.
¹: in reality weather can be extremely weird sometimes. I had it rain without visible clouds before on the open field. I am pretty sure it was just very light and uniform fog I was inside of, that would count as a cloud technically, but one could argue..
Nicolas89
Probably à typing mistake in "Denying the consequent" section, which should rather state "if P => Q then not-Q => not-P"?
btdmaster
Great catch, thanks!
ygritte
By the way, `if a implies b and b implies c then a implies c` is the Barbara syllogism.
ufo
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)
((x and a) => y) iff (x => (a => y))
gettingoverit
F is a left adjoint of G, and tautology below is a tensor-hom adjunction :)
fjfaase
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.
fjfaase
So, in Visual Basic one can use '>=' for imply.
practal
Good one! (Q)Basic was my first language. Well, my second really, after .bat files.
IshKebab
I think it's best not to refer to Visual Basic when considering logic...
rawling
> Ever notice that the notation for a ⇒ b looks awfully similar to a >= b, just with the symbols switched around? Well, they're the same thing.
...
> This means that only if x>y, then the statement is false. A simpler way to write this is that x ≤ y, which reveals the connection.
So it's the same as <= not >=?
qihqi
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.