The n-Category Café

Very nice. I was always having the “feeling” that a well-ordered set could be interpreted as a set where one always has a “preferred” option, but I never could make it precise. This is exactly the way to make it precise! Thank you for sharing!

Is there some way to think of the singleton embedding of X into P’(X) as the unit of an adjunction? (The set of non-empty finite subsets of X, equipped with the binary operation of union, is the free semilattice on the generating set X, and this looks temptingly similar to what you’ve got here)

Having a choice function rather than just being able to make a choice in each individual case is already a form of consistency (many local choices versus one global choice), let’s call it “very weak consistency”, since you already used “weak”. The axiom of choice is already bridging a gap between no consistency at all and some consistency.

Any constructivist light to be shone on the topic of this post?

From nLab: well-ordering theorem:

…in constructive mathematics, the well-ordering principle is (seemingly) actually weaker than the full axiom of choice, as it does not imply excluded middle by itself. It does, however, imply the full axiom of choice (and hence excluded middle) if by ‘well-order’ we mean a classical well-order, in the sense that every inhabited subset has a least element, rather than the constructively sensible notion of well-order that merely permits inductive proofs.

What is meant at the end there by the “constructively sensible notion”?

This sure is interesting! Never seen it before – it probably deserves to be published.

Picking up on the train of ideas started by Yemon and Kevin, it looks like there are chunks that are translatable into relational algebra of a kind reminiscent of Barr’s definition of topological space as relational $\beta$-module.

I’ll just make a few observations. As Kevin said, $P'$ carries a monad structure. If $u$ is the unit of the monad, then for a map $h:P'(X) \to X$ the condition

$$u h \leq 1_{P'(X)}$$

is synonymous with $h(A) \in A$ for all nonempty $A$.

Tom’s strong consistency condition says that for the covariant monad structure $(P', u: 1_{Set} \to P', m: P'P' \to P')$ as described by Kevin, the diagram

$$\array{ P'P'X & \stackrel{P'h}{\to} & P'X \\ \downarrow \mathrlap{m} & & \downarrow \mathrlap{h} \\ P'X & \underset{h}{\to} & X }$$

commutes.

Another fun fact about this monad is that the unit map is atomic in the sense that if $f \leq u: X \to P'X$, then also $u \leq f$. Now, by pre-composing $u h \leq 1$ with $u$, we get $u h u \leq u$, which by atomicity of $u$ gives $u \leq u h u$ so that $u = u h u$, and now $1 = h u$ by monicity of $u$. So the unit law is also satisfied, i.e., the type of structure Tom is describing is indeed a $P'$-algebra (with an extra condition: $u h \leq 1$).

As Kevin was saying, $P'$-algebras are posets which admit all sups except possibly the empty sup (which would be the bottom element). Ordinarily, the structure map $h: P'X \to X$ would be interpreted as sending a nonempty subset of $X$ to its sup $h(X)$. The only difference here is that Tom is following the usual convention that a well-order is defined to be a linear order in which every nonempty subset contains its inf; we could of course buck the trend and define a well-order to be a linear order in which every nonempty subset contains its sup, at the cost of reversing the conventional order and confusing the hell out of people, but the concept seems to be the same.

Anyway, this is a really cool idea. I’m wondering about this weird laxity $u h \leq 1$, i.e., where else it comes up in this sort of categorical relational algebra.

FWIW, this equivalent way of thinking about well-orders is used a lot in the model theory for conditional logics. (Specifically in Stalnaker’s selection function semantics, which is formalized in terms of consistent choice functions but typically glossed in terms of well-orders.) The consistency condition is usually stated slightly differently though: if $h(A) \in B$ and $h(B) \in A$ then $h(A)=h(B)$.

I’ve just discovered that the equivalence between well orderings and weakly consistent choice functions is given as Exercise 7.1 of Peter Johnstone’s 1987 book Notes on Logic and Set Theory. He called them “orderly” choice functions.