Infinite Ascent.

by CJ Quineson

Conjunction is adjoint to implication

posets, limits, adjoints

In this post I’m trying to digest some things I’ve been learning from Daniel Rosiak’s Sheaf Theory Through Examples, by building up to the statement “conjunction is adjoint to implication.”

Possible-worlds semantics

Tomorrow, it will either rain, or not rain. These are two possible tomorrows.

Or rather, they’re sets of possible tomorrows. There’s many possible tomorrows where it rains. In some of them, I will eat a bowl of ice cream. In others (most of them), I won’t eat any ice cream.

We can represent a proposition like “it rains” as the set of possible tomorrows aa where it holds. Similarly, we can represent a proposition like “I eat a bowl of ice cream” as a set bb. We’ll abuse notation and use aa and bb for both the propositions and the sets of possible tomorrows where they hold.

Consider the set of possible tomorrows where it both rains and I eat a bowl of ice cream. As sets, this is aba \cap b: it’s the intersection of the tomorrows where it rains, and the tomorrows where I eat a bowl of ice cream. Thus, the proposition aba \land b translates to aba \cap b. Note how the symbols \land and \cap look similar.

Similarly, what are the set of possible tomorrows where it rains or I eat a bowl of ice cream? As sets, this is aba \cup b; as propositions, this is aba \lor b.

We can also work backward, starting from a set of possible tomorrows, then thinking about which proposition it represents. Which proposition does the empty set, \varnothing, represent? It should be a proposition that holds in no possible tomorrows, so it’s false, which we will write as 00. And the opposite, the set consisting of all possible tomorrows, represents the proposition true, which we write as 11.

Interlude: semantics

In mathematical logic, semantics is about translating logical statements into mathematical objects. When I first studied logic, the semantics I was taught was truth-value semantics: a proposition is one of the Boolean values false or true, and \land and \lor are the boolean operations on those values. The boolean operations capture our intuitive sense of what it means for when aba \land b should be true, which is iff aa is true and bb is true.

What we’ve discussed, where we interpret propositions as the set of possible worlds in which it’s true, is called possible-worlds semantics (nLab, SEP). Here, \land and \lor are intersection and union, which again capture the intuitive sense for when a possible world is in aba \land b: iff it’s in aa and in bb.

Note that truth-value semantics is a special case of possible world semantics, where there’s only one possible world. In particular, if there’s only one possible world, then there’s two sets of possible worlds: the empty set (false, 00), and the set containing that possible world (true, 11).

Are there other possible semantics? In my type theory handout, I discuss another kind of semantics, called proof-theoretic semantics, which is about interpreting propositions as their proofs: aba \land b is an ordered pair of proofs of aa and bb, while \lor is either a proof of aa, or a proof of bb. (In that handout, I also use \perp instead of 00; the symbolic counterpart would be \top instead of 11. But I’m sticking with Rosiak’s notation for consistency.)

External and internal implication

We’ve talked about conjunction (\land) and disjunction (\lor). We’ll now discuss implication. In possible-world semantics, there’s actually two reasonable ways to think about ”aa implies bb”:

  • We can say that aa implies bb when: every time aa holds in a possible world, then bb also holds in that possible world.

  • Or, ”aa implies bb” can be a proposition in itself. It’s the set of possible worlds where, if aa holds, then bb also holds.

The former is external implication, and the latter is internal implication. The former is a fact that, by looking at all the possible worlds, can be either true or false. The latter is a set of possible worlds, and it will always exist, though sometimes it’s empty. nLab uses the terms entailment and conditional statement.

Concretely, consider some sets of possible tomorrows:

  • aa: It rains tomorrow.
  • bb: I eat a bowl of ice cream tomorrow.
  • cc: I have dessert tomorrow.

Then:

  • bb externally implies cc, because in every tomorrow where I eat a bowl of ice cream, I have dessert. As sets, this means bcb \subseteq c.

  • However, aa does not externally imply bb. There are some tomorrows where it rains, but I don’t eat a bowl of ice cream.

  • The set ”aa implies bb” is the set of possible tomorrows where: if it rains, then I eat a bowl of ice cream. It includes some of the tomorrows in aa: particularly, the ones which are also in bb. But note that it also includes all the tomorrows in which it doesn’t rain, because that’s how logical implication works.

To introduce some notation, we’ll say that:

  • aba \le b is the statement that aa externally implies bb, and

  • aba \limplies b is the set that represents the internal implication ”aa implies bb”.

The set aba \limplies b is also called the relative pseudocomplement of aa with respect to bb. It’s the set of all possible worlds except the ones where aa holds but bb doesn’t. So it’s like the opposite of aa under bb.

Let’s check our understanding:

  • What’s the relationship between the two sets aba \limplies b and aca \limplies c? A possible tomorrow is in aba \limplies b if, when it rains, I eat a bowl of ice cream. Because I eat ice cream, I have dessert. Thus, it’s also in aca \limplies c. So, every world in aba \limplies b is also in aca \limplies c. Thus, abaca \limplies b \le a \limplies c.

  • What’s the relationship between external implication and internal implication? Consider the fact that bcb \le c, or, that bb externally implies cc. Then what is the set bcb \limplies c? It consists of all possible worlds in which, if bb holds, then cc holds. But because every world where bb holds is also a world where cc holds (because bcb \le c, or bcb \subseteq c), this must be every world. So bcb \limplies c is the set of all possible worlds, or \top.

  • What’s the proposition a0a \limplies 0? It’s the set of all possible tomorrows in which, if it rains, then false. So it cannot have any possible tomorrows where it rains. But it has all the possible tomorrows where it doesn’t rain, in the same way that aba \limplies b has all the tomorrows where it doesn’t rain. Thus, a0a \limplies 0 represents the proposition that it doesn’t rain.

  • What’s the proposition a(ab)a \land (a \limplies b)? Recall that aba \limplies b consists of the worlds that are in both aa and bb, as well as all the worlds not in aa. We are intersecting this with the set of worlds that are in aa. So this is aba \land b.

  • What’s the proposition a(ab)a \lor (a \limplies b)? Note that every possible world is either in aa, or not in aa. But if it’s not in aa, it’s in aba \limplies b. So a(ab)a \lor (a \limplies b) has to be every possible world, or 11.

Posets, meets, and joins

The notation we’ve been using, with \le and \land and \lor, is meant to emphasize that we’re working in a poset. We use posets as a bridge to understanding categories because they’re a special case of categories. There’s an nLab page that says “if you’re having trouble understanding an item in [category theory], then first you should understand the item in [order theory].”

Recall that a poset (Wikipedia, nLab) is a set PP with a reflexive, transitive, and antisymmetric binary relation \le. The set of set of possible worlds forms a poset, with the \le we’ve been using above. Depending on your definition of possible worlds, this could be a special case of the fact that, for any set SS, its power set 2S2^S is a poset under \subseteq.

Through the rest of the post I’ll be implicitly referring to Hasse diagrams of posets. For concreteness, you can imagine this Hasse diagram of the poset of subgroups of the dihedral group with order eight. When I refer to relative directions, like “above” and “below”, or “highest” and “lowest”, I’m referring to an imaginary Hasse diagram that I’m not going to include in this post because I’m too lazy to make diagrams. It’s maybe helpful pedagogically to force you to recreate the diagrams I’m thinking of, I dunno. Anyway.

The poset thinking encourages us to think of sets of possible worlds via only \le, that is, without referring to individual worlds. So, using only \le, can we still define \land and \lor and \limplies?

One general trick we’ll use is the notion of taking “the largest” or “the smallest” of a specific kind of property. Indeed, aba \land b is “the largest” set that is a\le a and b\le b. We’ll now talk about this in lots of detail.

Consider, the following property of a set of possible worlds: “It rains in every possible tomorrow in the set.” There’s several sets that satisfy this property.

  • It’s true of aa, the set of every possible tomorrow where it rains.

  • It’s also vacuously true for 00, the empty set.

  • It’s also true of the set aba \land b, the set of possible tomorrows where it both rains and I eat a bowl of ice cream.

  • Consider the set ss of possible tomorrows where it rains, I eat a bowl of ice cream, and I go to work. It’s also true of this set.

Of all of possible sets that satisfy this property, there happens to be one of them which is the largest: aa itself. It’s “the largest” in the sense that, if aa' is any set that satisfies this property, then aaa' \le a. Indeed, 0a0 \le a, and abaa \land b \le a, and sas \le a, and even aaa \le a.

In the Hasse diagram, I imagine the sets that satisfy this property as a shaded region of the Hasse diagram. The largest one, aa, is on top, and everything in the shaded region has an arrow pointing to aa. Further, nothing outside of the shaded region has an arrow pointing to aa.

Now consider the property “In every possible tomorrow in the set, it rains, and I eat a bowl of ice cream.” Again, several sets satisfy this property, like 00, or ss. But the largest such set that satisfies this property is aba \land b. Conversely, every set that satisfies this property is ab\le a \land b. And every set that doesn’t satisfy this property isn’t ab\le a \land b.

Both of these properties can be restated in the same form:

  • “It rains in every possible tomorrow in the set” can be written as “the set is a\le a.”

  • “In every possible tomorrow in the set, it rains, and I eat a bowl of ice cream” can be written as “the set is a\le a and b\le b.”

In general, the pattern is: we have some set of elements in the poset ({a}\{a\} in the first one, {a,b}\{a, b\} in the second one), and we’re considering all elements that are \le each of them. In these cases, there happens to be a largest such element (aa in the first one, aba \land b in the second one). We call that element the meet (Wikipedia, nLab) of the set.

Note that the meet doesn’t need to exist. Consider the poset on four elements whose Hasse diagram looks like a \bowtie. The set of elements that’s \le the upper two elements is the lower two elements. But neither of them is larger than the other, so there’s no “largest” one. So the upper two elements in this poset don’t have a meet. But, when it does exist, it’s unique, so we can say the meet. (If there were two, each is \le the other, so by antisymmetry they’re equal.)

In the poset of sets of possible worlds, the meet always exists. We can then define aba \land b as the meet of the set {a,b}\{a, b\}. Similarly, we can define \lor using the dual notion, the join of a set, which is the smallest element that each of them are \le than.

As a special case, note that the meet of an empty set is 00, and the join of an empty set is 11.

Interlude: categories and limits

I’ve mentioned that a poset is a special case of a category. One way it’s special is antisymmetry: in a poset, if aba \le b and bab \le a then a=ba = b. If you drop this condition, you get a preorder (nLab, Wikipedia). The thing you lose in a preorder is uniqueness, but things are still unique up to isomorphism.

Generalizing from a preorder to a category is trickier, though. In a preorder, we say aba \le b, and we don’t have to worry about how aba \le b. In other words, if aba \le b, there’s only one way for aa to be b\le b. In a category, we generalize to allowing multiple ways for something to be \le than another. We then write aba \to b, and call these multiple ways morphisms.

In a poset, transitivity says that if aba \le b and bcb \le c, then aca \le c. The categorical version of this is composition, which says that if f ⁣:abf \from a \to b is a morphism, and g ⁣:bcg \from b \to c is another morphism, then you get another morphism gf ⁣:acg \circ f \from a \to c.

To go the other way around, we can start from the definition of a category, and define a thin category, where two morphisms with the same source and target are equal. Then we can define a skeletal category, where two isomorphic objects are equal. A poset is a thin skeletal category.

To me, what feels like the main difference when working with poset and categories is that, in a poset, all diagrams commute. Because there’s only one way to get from one point to another, everything commutes automatically. Thus, to generalize from posets to categories, you have to worry a bit more about making things commute.

As an example, consider how to generalize meets. In a poset, we take meets of sets of elements, and we don’t really care about the \les between them. In a category, if we take the meet of a set of elements, and ignoring any \tos between them, we generalize meets to products.

To be specific: we have a set of elements, we take all the elements that are \to to every element in that set, and we see if there’s a “largest” such element, one that everything else is \to to. This is the product (nLab, Wikipedia), so named because in the category of sets, this is the cartesian product.

Back to a poset. Suppose, instead of just thinking about sets of elements, we considered diagrams of elements, where we also care about the \les between them. Well, this kinda doesn’t matter when we’re taking their meet—whatever element we take, it’ll respect those \les. Like, suppose we had three elements {a,b,c}\{a, b, c\} satisfying aca \le c and bcb \le c. And suppose there’s some element mm that’s \le each of them. Then mam \le a, by definition, and because aca \le c, then by transitivity we have mcm \le c. And similarly, combining mbm \le b and bcb \le c we get mcm \le c. And by definition (of mm), we also have mcm \le c. Which, well, in the poset case, we ended up with mcm \le c thrice, and that’s fine.

But what about in a category? Consider the diagram with three elements {a,b,c}\{a, b, c\} with morphisms f ⁣:acf \from a \to c and g ⁣:bcg \from b \to c. Then suppose there’s some element mm, with morphisms \to each of them. There’s some morphism am ⁣:maa_m \from m \to a, by definition, and because f ⁣:acf \from a \to c exists, then by composition there’s fam ⁣:mcf \circ a_m \from m \to c. And similarly, combining bm ⁣:mbb_m \from m \to b and g ⁣:bcg \from b \to c we get gbm ⁣:mcg \circ b_m \from m \to c. And by definition (of mm), we also have some cm ⁣:mcc_m \from m \to c. And now, we have three morphisms that go from mm to cc, namely, famf \circ a_m, gbmg \circ b_m, and cmc_m. And these aren’t necessarily the same.

If we require them to be the same—that is, you require the whole diagram to commute—we get the notion of the limit (nLab, Wikipedia) of a diagram. In a poset, the limit of any diagram happens to be the same as the product of its elements; they’re both the meet. But because things don’t automatically commute in a category, then the limit of a diagram isn’t the same as the product of its elements.

Dually, the generalizations of joins are coproducts and colimits.

Lattices and adjoints

A lattice (Wikipedia, nLab) is a poset with all finite meets and joins. By taking the meets and joins of empty sets, we get that a lattice must have 00 and 11, which are smaller and larger than every element. Our poset of the sets of possible worlds is in fact a lattice.

Given a lattice, we now move to the task of defining \limplies. How do we characterize aba \limplies b in terms of what we have? We’ll end up doing something similar to what we did for meets and joins, where we take “the largest” of a particular kind of property.

Let’s recall our running example, where aa represents the proposition “it rains tomorrow” and bb represents the proposition “I eat a bowl of ice cream tomorrow.”

The property we’ll consider is: “In every possible tomorrow in the set, if it rains, then I eat a bowl of ice cream.” Let’s consider some sets that satisfy this property:

  • It’s vacuously true of 00, the empty set.

  • It’s also true of aba \land b, the possible tomorrows where it both rains and I eat a bowl of ice cream.

  • It’s also true of the set of possible tomorrows where it doesn’t rain, because that’s how logical implication works.

The key property here is its relationship with “what happens when it rains”, or when you do aa \land to it. In particular, these are all rewrites of each other:

  • “For each possible tomorrow in the set where it rains, I eat a bowl of ice cream.”

  • “The tomorrows in the set that are in aa are also in bb.”

  • “When you aa \land the set, the result is b\le b.”

We can then define aba \limplies b to be (provided it exists) the largest such set so that, when you aa \land it, the result is b\le b. This means that a set satisfies this property iff it’s ab\le a \limplies b. We can thus write

asbsab\frac{a \land s \le b}{s \le a \limplies b}

where the bar means “if and only if”. In general, lattices don’t always have an \limplies, but the power set lattice does, and so does the poset of possible worlds.

This general shape is called an adjunction. Given two functors (\le-preserving functions) ff and gg, both from the poset to itself, we say that ff is adjoint to gg if:

f(s)bsg(b)\frac{f(s) \le b}{s \le g(b)}

(Here, I’m using the category theory words functor and adjoint. In usual order theory, functors are called monotone maps (Wikipedia, nLab), and adjoint pairs are called a Galois connection (nLab, Wikipedia). If the word functor scares you, you can replace it with function and you’ll be fine.)

Note that adjoints are asymmetric: we call ff the left adjoint and gg the right adjoint. In this particular case, ff is the functor xaxx \mapsto a \land x and gg is the functor xaxx \mapsto a \limplies x. So conjunction by aa is adjoint to implication from aa. Or, in snappier phrasing, conjunction is adjoint to implication.

Provided that a right adjoint to ff exists, it must be unique. This is for similar reasons to the above: if we want to compute g(b)g(b), we take all ss such that f(s)bf(s) \le b, and then take the largest. (“…the largest such set so that, when you aa \land it, the result is b\le b.”) Similarly, left adjoints are unique.

We can think of adjoints as “the closest thing to inverses”. Consider that the functor aa \land takes a set bb and returns aba \land b. If an inverse functor existed, it would take a set aba \land b and return the original set bb. But, given just aa and aba \land b, we can’t tell what the original bb is. If we imagine the Hasse diagram, and I highlight aa and aba \land b, then there’s a region of possible bbs, ranging from aba \land b, and going up. We then take the largest of these, which is aba \limplies b.

Now let’s consider the dual case. If conjunction is adjoint to implication, then what is adjoint to disjunction? Using the “smallest” perspective, the left adjoint must be the smallest set that satisfies the property:

  • “When you b\lor b the set, then aa \le the result.”

  • “The possible tomorrows in aa are in bb, or the set.”

  • “For each possible tomorrow where it rains, then I eat a bowl of ice cream, or it’s in the set.”

Many sets satisfy this property. It’s trivially true of 11, the set of all possible worlds. It’s also true of aa, the set of tomorrows where it rains. But what’s the smallest set that satisfies this property? It’s aba \setminus b, or the set of possible tomorrows where it rains, but I don’t eat a bowl of ice cream. So subtracting bb is adjoint to disjunction by bb. In snappier words, subtraction is adjoint to disjunction:

absasb\frac{a \setminus b \le s}{a \le s \lor b}

Like the situation with \limplies, not every lattice has a \setminus, but the power set lattice does, and so does the poset of possible worlds.

Comments

Loading...