Logical implication is a comparison operator (opens in new tab)

(btdmaster.bearblog.dev)

40 pointsbtdmaster8mo ago23 comments

23 comments

This perspective is the inspiration for much of lattice theory. When you consider implication as an ordering, then "x and y" becomes max(x, y), "x or y" becomes min(x, y). True becomes the top term, False becomes the bottom. One of the neat implications is that much of what we think of as being propositions in boolean algebra also work in the wider setting of Heyting algebras i.e., any lattice that also has implication.

practal8mo ago

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

That allows you to define B ⇒ C as the supremum of all A such that A ∧ B ≼ C, in every complete lattice. If the join-infinite distributive law [1] holds, above condition will hold with this definition, and you get a complete Heyting algebra this way.

This is exactly how I turn abstraction algebra into abstraction logic [2].

[1] https://proofwiki.org/wiki/Axiom:Infinite_Join_Distributive_...

[2] http://abstractionlogic.com

AbstractPlay8mo ago

On your website, you seem to claim in bold letters that you've talked to Graham Priest about your work:

> A Conversation with Graham Priest About Abstraction Logic

but admit afterward that you talked to Claude prompted to sound like Graham Priest:

> A conversation about abstraction logic with Claude representing Graham Priest.

You also wrote an update stating:

> Update: The real Graham Priest says that it doesn't really sound like his voice. So enjoy with caution .

Don't you find it unethical to claim that you had "a conversation with Graham Priest about Abstraction Logic"? You didn't have a conversation with Priest. You had an interaction with Claude in Priest clothing. It doesn't even sound like Priest agrees with what you prompted Claude to say. Do you think it's permissible to let LLMs speak on behalf of people without their consent? Do you think that what an LLM says when prompted to speak as though it were some person should be accepted as what the person would actually say and believe?

Why should we find it interesting what any LLM has to say about your work, regardless of whose voice you dress it up as?

practal8mo ago

All the information you need to know about that article is right at the top of it [1]. I am very clear that this is a conversation with a Claude impersonation of Graham Priest, not Graham Priest himself.

I don't see what is unethical about that.

> Why should we find it interesting what any LLM has to say about your work, regardless of whose voice you dress it up as?

Who is "we"? I don't even know who you are, AbstractPlay. The article exists because I personally find it interesting, and I actually learnt something through it. If somebody else finds it interesting, great. If you don't, too bad. Thanks for letting me know either way.

[1] https://practal.com/press/cwgpaal/1

1 more reply

gettingoverit8mo ago

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

spyrja8mo ago

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);
  }

Kind of silly, I know, but it does work.

gettingoverit8mo ago

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

Nicolas898mo ago

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

btdmasterOP8mo ago

Great catch, thanks!

ufo8mo ago

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

gettingoverit8mo ago

F is a left adjoint of G, and tautology below is a tensor-hom adjunction :)

spyrja8mo ago

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)?

atoav8mo ago

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

ygritte8mo ago

By the way, `if a implies b and b implies c then a implies c` is the Barbara syllogism.

https://en.wikipedia.org/wiki/Syllogism

fjfaase8mo ago

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.

IshKebab8mo ago

I think it's best not to refer to Visual Basic when considering logic...

fjfaase8mo ago

So, in Visual Basic one can use '>=' for imply.

practal8mo ago

Good one! (Q)Basic was my first language. Well, my second really, after .bat files.

qihqi8mo ago

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.

rawling8mo ago

> 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 >=?

ayaros8mo ago

This confused me too.

j / k navigate · click thread line to collapse

23 comments

siddboots8mo ago

practal8mo ago

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.

    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_...

[2] http://abstractionlogic.com

AbstractPlay8mo ago

On your website, you seem to claim in bold letters that you've talked to Graham Priest about your work:

> A Conversation with Graham Priest About Abstraction Logic

but admit afterward that you talked to Claude prompted to sound like Graham Priest:

> A conversation about abstraction logic with Claude representing Graham Priest.

You also wrote an update stating:

> Update: The real Graham Priest says that it doesn't really sound like his voice. So enjoy with caution .

Why should we find it interesting what any LLM has to say about your work, regardless of whose voice you dress it up as?

practal8mo ago

I don't see what is unethical about that.

> Why should we find it interesting what any LLM has to say about your work, regardless of whose voice you dress it up as?

[1] https://practal.com/press/cwgpaal/1

1 more reply

gettingoverit8mo ago

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

spyrja8mo ago

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);
  }

Kind of silly, I know, but it does work.

gettingoverit8mo ago

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

Nicolas898mo ago

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

btdmasterOP8mo ago

Great catch, thanks!

ufo8mo ago

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

gettingoverit8mo ago

F is a left adjoint of G, and tautology below is a tensor-hom adjunction :)

spyrja8mo ago

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)?

atoav8mo ago

Given that it can be cloudy and not rain, but (for the sake of the example) not rain without clouds¹ I would agree.

ygritte8mo ago

By the way, `if a implies b and b implies c then a implies c` is the Barbara syllogism.

https://en.wikipedia.org/wiki/Syllogism

fjfaase8mo ago

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.

IshKebab8mo ago

I think it's best not to refer to Visual Basic when considering logic...

fjfaase8mo ago

So, in Visual Basic one can use '>=' for imply.

practal8mo ago

Good one! (Q)Basic was my first language. Well, my second really, after .bat files.

qihqi8mo ago

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.

rawling8mo ago

> 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 >=?

ayaros8mo ago

This confused me too.

j / k navigate · click thread line to collapse