The Curious Dependence of Set Theory on Order Theory

October 13, 2012

The Curious Dependence of Set Theory on Order Theory

Posted by Tom Leinster

$MathML-enabled post (click for more details).$

(Note: the Café went down for a few days in early November 2012, and when Jacques got it back up again, some of the comments had been lost. I’ve tried to recreate them manually from my records, but I might have got some of the threading wrong.)

This is the first of a series of posts on set theory, order theory, and how they are intertwined.

I won’t assume you know any more set theory than the average pure mathematician: in other words, no axiomatic set theory, just the ordinary “naive” principles that mathematicians use every day. (And I’ll steer clear of the debate about which system of axioms is “best”. Important as that is, it tends to suck the oxygen out of a room.) As far as order theory is concerned, I’ll assume just the very basic definitions, such as “partially ordered set”.

In this first installment, I’ll ask: why is it that some of the fundamental theorems of set theory do not mention order in their statements, but apparently need substantial order theory in their proofs?

$MathML-enabled post (click for more details).$

Although I’m steering clear of axiomatics, I should probably clarify one assumption: the “sets” I’ll talk about are taken to satisfy the axiom of choice. Any of the standard elementary formulations will do: every surjection has a right inverse, or every equivalence relation has a system of representatives, or the product of any family of nonempty sets is nonempty.

Here are three of the most basic nontrivial theorems about sets. For sets $X$ and $Y$ , I’ll write $X \cong Y$ to mean that there exists a bijection between $X$ and $Y$ .

(Cantor–Bernstein theorem) Let $X$ and $Y$ be sets. If there exist injections $X \to Y$ and $Y \to X$ then $X \cong Y$ .
(Cardinal comparability) Let $X$ and $Y$ be sets. Then either there exists an injection $X \to Y$ or there exists an injection $Y \to X$ .
(Squares of infinite sets) Let $X$ be an infinite set. Then $X \times X \cong X$ .

The Cantor–Bernstein theorem is often called the Schröder–Bernstein theorem, but people who know the history seem to prefer the first name. Here’s a passage from R. M. Dudley’s book Real Analysis and Probability (page 22):

The equivalence theorem came up as an open problem in Cantor’s seminar in 1897. It was solved by Felix Bernstein, then a 19-year-old student. Bernstein’s proof was given in the book of Borel (1898). Meanwhile, E. Schröder published another proof. The equivalence theorem has often been called the Schröder–Bernstein theorem. Korselt (1911), however, pointed out an error in Schröder’s argument. In a letter quoted in Korselt’s paper, Schröder gives full credit for the theorem to Bernstein. […] Bernstein also worked in statistics […] and in genetics; he showed that human blood groups A, B, and O are inherited through three alleles at one locus.

I couldn’t resist including the Cantor–Bernstein theorem in this list, since it really is one of the basic nontrivial results about sets. But in a way it doesn’t belong, because it doesn’t require any order theory to prove it.

I know two proofs. The first (which I’m guessing was Bernstein’s) is dynamical. It takes injections $f\colon X \to Y$ and $g\colon Y \to X$ , and traces each element of $X$ or $Y$ along its backwards trajectory for as long as possible. The second is order-theoretic. It uses the result in order theory known as Tarski’s fixed point theorem or the Knaster–Tarski fixed point theorem. (Incidentally, the two proofs construct the same bijection between $X$ and $Y$ , starting from an initial choice of injections $f\colon X \to Y$ and $g\colon Y \to X$ .)

So while the Cantor–Bernstein theorem can be proved using order theory, it doesn’t have to be.

However, I don’t know a proof of cardinal comparability that doesn’t use substantial order theory. Here’s one classic proof. It uses a certain class of partially ordered sets called the well-ordered sets. A well-ordered set is a set equipped with a well-order, which is an order relation satisfying certain further conditions that don’t matter for the present purposes. We’ll need two facts:

every set can be equipped with a well-order
if $X$ and $Y$ are well-ordered sets then either $X$ is isomorphic (as an ordered set) to a subset of $Y$ or $Y$ is isomorphic to a subset of $X$ .

Cardinal comparability follows immediately.

I’m claiming that cardinal comparability is a general theorem about sets whose statement doesn’t mention order, but whose proof uses order in an essential way. You might object that it’s not a very good example. Sure, the statement doesn’t mention order explicitly, but it’s there all right, in thin disguise. After all, there’s a (pre)order $\leq$ on the class of all sets defined by

$X \leq Y \iff \text{there exists an injection }  X \to Y,$

and cardinal comparability simply states that it’s a total order.

I concede: it’s not a great example. But what about the third theorem, on squares of infinite sets? The statement here really isn’t order-theoretic at all. (Well, not except in a trival sense: any theorem asserting that two sets have the same cardinality could be called order-theoretic, since by Cantor–Bernstein, $A \cong B$ if and only if $A \leq B \leq A$ .) So here’s a question for you all:

Does anyone know a proof that $X \times X \cong X$ for infinite sets $X$ that neither uses substantial order theory nor involves elaborate convolutions to avoid doing so?

I should make clear that I have no objection to order theory. In fact, I probably like it more than most people (and, for example, I find the order-theoretic proof of the Cantor–Bernstein theorem more appealing than the dynamical proof). But I’d like to understand better why it is that basic results about sets seem to depend so heavily on the concept of order.

I’ll finish by posing and attempting to answer a question:

Is it strange that results about sets should depend on results about order?

On the one hand, yes.

Think again of the proof of cardinal comparability sketched above. We took two abstract sets $X$ and $Y$ , and we equipped them with well-orders in a quite arbitrary way. (Even if you don’t know what a well-order is, it should be clear that the choice is arbitrary: given one well-order on $X$ , you can transport it along any bijection $X \to X$ to obtain another.) Then we used some order theory to show that either $X$ is order-isomorphic to a subset of $Y$ or vice versa, then we threw away the orders, to conclude that either $X$ is set-theoretically isomorphic to a subset of $Y$ or vice versa.

If you’re already familiar with that kind of argument, maybe it doesn’t seem so strange. In that case, consider the following. It’s a fact that every nonempty set can be equipped with a group structure. (For finite sets, use the cyclic groups; then observe that taking the free group on an infinite set doesn’t change its cardinality.) Wouldn’t it be strange if we proved a result about abstract sets by (1) equipping them arbitrarily with group structures, (2) using some result from group theory, then (3) forgetting the group structures to draw some conclusion about the sets themselves?

Or — leaving set theory behind — consider the fact that every finite abelian group can be given a multiplicative structure making it into a ring. (Proof: every finite abelian group is a product of cyclic groups, and every cyclic group can be given a ring structure.) There’s no canonical way to do this: for example, in the group of order three, there’s no canonical choice for the multiplicative identity. Wouldn’t it be strange to prove a theorem about finite abelian groups by (1) equipping the groups arbitrarily with multiplicative structures, (2) using some theorem about rings, then (3) forgetting the multiplicative structures?

On the other hand, no, it’s not strange.

Consider elementary enumerative arguments about finite sets. For example, suppose someone asks you: why are there exactly $n!$ permutations of an $n$ -element set? You’d probably reply with something like: there are $n$ places for the first element to go, then $(n - 1)$ places for the second element, and so on. Almost without thinking, you’ve chosen an ordering on the set concerned. Indeed, it’s hardly surprising that choosing an ordering is involved: for a set $X$ to have $n$ elements means that there exists a bijection between $X$ and $\{1, \ldots, n\}$ , so to exploit the fact that $X$ has $n$ elements, we’re probably going to have to choose such a bijection.

Still, perhaps it’s a surprise that when we progress from finite to infinite sets, the question of ordering moves to centre stage. In the world of finite sets, putting an order on the set is something we do almost without noticing — it feels like a trivial part of the argument. But in the world of infinite sets, the order theory becomes really substantial. Indeed, for the three theorems above, it makes up the weightiest part of the proofs.

I’d like to understand better what’s going on here, and I hope your comments will help me to do so. It seems that set theory, which is about maximally unstructured objects, depends on order theory, which is about more structured objects. Is that really true? If so, what are some comparable situations elsewhere in mathematics? (I’m thinking of maybe geometric structures on topological manifolds, but I’m not sure how similar that really is.) And can someone paint a philosophical picture that makes this seem natural?

Posted at October 13, 2012 4:22 PM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2568

71 Comments & 0 Trackbacks

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Since the axiom of choice is equivalent to the well-ordering principle, one might say that when doing “set theory” with the axiom of choice, one is assuming explicitly that one’s “maximally unstructured” objects are simultaneously “maximally structurable”. I think it’s not surprising, then, that results which depend on that assumption will proceed by choosing such a structure. Suppose you wanted to prove some theorem about “all sets which admit a group structure” — it wouldn’t be at all strange to begin your theorem by putting a group structure on your set, since you expect to have to use your hypothesis! So I would say that any uncomfortableness one feels with the idea that “results about sets depend on results about order” should actually be regarded as an uncomfortableness with the axiom of choice. (-:

Posted by: Mike Shulman on October 13, 2012 6:08 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

I see your point, but I’m not sure I buy it. Suppose there were results about sets whose only known proofs involved extensive detours through linear algebra, and used the fact that every vector space has a basis. One could say “we’re assuming the axiom of choice, which is in some sense equivalent to the statement that every vector space has a basis, so it’s hardly surprising that linear algebra is involved.” But I’d still find it pretty curious; wouldn’t you?

Posted by: Tom Leinster on October 13, 2012 6:26 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

I’d still find it pretty curious; wouldn’t you?

Well, it depends on what you mean by “curious”. Interesting, certainly. But as you mentioned, there are other places in mathematics where the best, or only, known way to prove something is by introducing some new structure that wasn’t obviously inherent in the statement to be proved. For instance, Fermat’s Last Theorem: are modular forms really inherent in the statement “ $a^n + b^n \neq c^n$ ”? The difference with a well-ordering is that the new structure we introduce is just asserted to exist, rather than constructed in any natural way, and I think that’s what makes it feel odd.

By the way, I just noticed that your comment about finite sets also supports my point:

In the world of finite sets, putting an order on the set is something we do almost without noticing — it feels like a trivial part of the argument.

As you said, because the definition of “finite” is “admits a bijection to a set of the form $\{0,1,2,\dots,n\}$ ”, it’s not surprising that when we want to prove something about finite sets, we begin by choosing such a bijection, and then making use of additional structure on $\{0,1,2,\dots,n\}$ (such as its ordering). Similarly, when we want to prove something about sets which are bijective to some ordinal, we begin by fixing such a bijection and using additional structure on the ordinal. And for some reason, some people think that all sets are bijective to some ordinal. (-:

Posted by: Mike Shulman on October 13, 2012 9:05 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

Issues of choice and finiteness are actually the source of much hassle in computer programming. In a computer program, it’s frequently the case that we can construct a decidable equality function at a given type, but we can’t cook up a decidable ordering.

This means that when we go to define a type of “finite” sets, we face an awkward decision: do we require that elements of a finite set support only an equality, or do we require them to support ordering, as well? If you do not require that elements of a finite set be ordered, then you cannot support a deterministic choice operation. That is, you can’t write a cursor function that takes a nonempty set, and then gives you an element plus the set of remaining elements. Such functions are “iterators” or “enumerators” in CS jargon. OTOH, if you do make this a requirement, you cannot support sets of elements which don’t have decidable order. (For example, pointer types in garbage-collected languages.)

Another way of putting it is that the distinction between finiteness and being finitely indexed (aka Kuratowski-finite) is rather more pervasive than you’d expect, and having the indexing function to hand is rather less common than you’d want.

Posted by: Neel Krishnaswami on October 15, 2012 4:29 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

That’s funny; I would have thought that in practice you would just use a finite list instead of a finite set if you expected to have to take elements out of it in some order. Presumably the elements were put into the set in some order, so if you’re going to need to take them out in some order, why not just keep that order around?

Posted by: Mike Shulman on October 15, 2012 5:57 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

Lists only provide a collection which allows enumerating the elements in some arbitrary unknown/unknowable order. Lists don’t support non-arbitrary enumeration orders, faster than linear (FTL) element insertion while maintaining the no-duplicates invariant, FTL element removal, FTL membership testing, FTL unions, FTL intersections, FTL cardinality,…

It is precisely the ability to give some type a fixed known order (whether arbitrary or meaningful) which enables the various data structures that support some or all of the above operations. The only exception is the FTL cardinality which can be supported by lists annotated with their lengths (whereas for certain tree structures this information is necessary for other operations and so is “free”).

Posted by: wren ng thornton on October 16, 2012 1:10 AM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

I feel as though one should also make a distinction between arguments which use structure already naturally available on certain sets, and those that involve somewhat arbitrary structures on sets that can be imposed by using a choice principle.

For example, it’s hard for me to shut my eyes to the fact that power sets are partially ordered from the get-go. The fact that the Cantor-Schroeder-Bernstein theorem can be proved by taking advantage of a complete semilattice structure naturally available on power sets doesn’t sound any philosophical alarms to me, not in the same way that appealing to the well-ordering theorem would.

Put slightly differently, one might see the dynamical or backtracking proof of CSB as implicitly referring to certain subset inclusions anyway, e.g., the closure of a singleton subset of $A \sqcup B$ under the inverse operations $f^{-1}$ , $g^{-1}$ is the smallest subset such that…

Posted by: Todd Trimble on October 13, 2012 7:13 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Yes, I agree with everything you say: there are two different kinds of ordering going on here, the canonical and the arbitrary. That was something that I thought about a bit as this post was brewing in my mind, though I didn’t actually mention it.

I think my parenthetical observation that the two proofs of CSB actually lead to the same bijection must be closely related to your last paragraph.

Posted by: Tom Leinster on October 13, 2012 9:36 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

I was surprised that you didn’t bring up the process of proving basis-independent statements in linear algebra by first picking a basis.

Posted by: Mark Meckes on October 13, 2012 7:46 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Good point. I didn’t think of that.

Posted by: Tom Leinster on October 13, 2012 9:38 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

In the world of finite sets, putting an order on the set is something we do almost without noticing — it feels like a trivial part of the argument.

But for finite sets it is a trivial part of the argument. Finite Choice isn’t problematic in any of the ways stronger versions of Choice are.

But, as Mike Shulman says, you’re assuming Choice in your definition of sets, which is equivalent to assuming the well-ordering principle; so it doesn’t strike me as odd that you then go on to use that well-ordering. But even if you don’t buy that argument, there’s something special about well-ordering structure that doesn’t hold for other structures. Namely, well-ordering corresponds to an inductive principle, so by assuming well-ordering you’re assuming you can perform certain sorts of induction. Given the role of induction in forming proofs, the “specialness” of this order-theory isn’t especially strange, ne?

If there were any examples of the sorts you allude to (adding ring structure to groups; adding group structure to sets;…), I would find those far stranger since those structures do not obviously correspond to logical principles of proof formation. Or, if there were other order-theoretic proofs of set-theoretic theorems which demand the full power of order-theory rather than just simple/naive parts thereof, that would also be intriguing.

Posted by: wren ng thornton on October 13, 2012 9:47 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Given the role of induction in forming proofs, the “specialness” of this order-theory isn’t especially strange, ne?

I think this is close to the heart of the matter. I still think it’s noteworthy, though, that it’s this particular extra structure on sets that we appear to need in order to prove basic statements. And it’s noteworthy that — like in linear algebra proofs involving bases — the orders are chosen at random, used, then discarded.

But, as Mike Shulman says, you’re assuming Choice in your definition of sets, which is equivalent to assuming the well-ordering principle; so it doesn’t strike me as odd that you then go on to use that well-ordering.

Much as I said to Mike, I don’t think this explanation comes close to getting to the bottom of things. Let me say why in a bit more detail.

First, let’s be careful about unspoken assumptions. You and Mike have both said that Choice is “equivalent” to the statement that every set can be well-ordered. I’m guessing that what you both mean is that in the presence of the ZF axioms, the two statements are logically equivalent. But that’s not really pertinent here. I haven’t mentioned ZF, nor have I specified any set of axioms at all, and I’m not even saying that one of the axioms is the axiom of choice. All I’m assuming is that we have some fairly commonplace set of axioms for sets, and that they imply Choice (perhaps as a consequence of half a dozen other axioms, perhaps as an axiom in itself; it doesn’t matter).

Anyway, it’s agreed that the well-ordering principle —

every set admits at least one well-ordering

— is a consequence of whatever the background assumptions are. But so too is the statement:

every nonempty set admits at least one group structure.

(For all I know, that’s even “equivalent”, in your sense, to the axiom of choice. If it’s not, there are surely structures other than groups or well-orderings for which it is equivalent.)

Now, you and Mike have said that since my assumptions about sets imply that every set can be well-ordered, it’s not surprising that proofs about sets often involve choosing a well-ordering on them. But by the same argument, since my assumptions about sets imply that every (nonempty) set can be given a group structure, it wouldn’t be surprising if proofs about sets often involved choosing a group structure on them.

And I think it would be surprising! I think if you were to produce even one proof of a theorem about sets that involved equipping the sets with arbitrary group structures, people would be amused and impressed. (And that’s not even as extreme a situation as for order theory, where almost all serious theorems about sets use this move.) In other words, I agree with your sentence here:

If there were any examples of the sorts you allude to (adding ring structure to groups; adding group structure to sets;…), I would find those far stranger

That’s why I find this explanation of yours and Mike’s incomplete. We’re all very used to well-orders as a piece of extra structure that traditionally comes up in set theory, but this explanation doesn’t account for why it’s this structure, not something else, that seems to be essential.

Posted by: Tom Leinster on October 13, 2012 10:40 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

I didn’t have ZF axioms in mind particularly. The equivalence of the axiom of choice to the well-ordering principle is a theorem of mathematics, which could be formalized in any adequate ambient context, including ZF, a suitable topos, or what-have-you.

Anyway, your point is well-taken; I concede. I guess I was reacting mainly to the second part of what you’re saying here:

Given the role of induction in forming proofs, the “specialness” of this order-theory isn’t especially strange, ne?

I think this is close to the heart of the matter. I still think it’s noteworthy, though, that it’s this particular extra structure on sets that we appear to need in order to prove basic statements. And it’s noteworthy that — like in linear algebra proofs involving bases — the orders are chosen at random, used, then discarded.

The axiom of choice is the reason we can choose (well-)orders at random and then discard them. Otherwise, if we wanted them, we would have to keep them around, as Bob suggests. But you’ve made a good point that there is, indeed, something special about well-orderings which makes them the particular structures that we want to have around.

I had also been thinking about the importance of inductive principles, so I’m glad wren pointed that out too. Here’s an argument for why well-ordering is the particular extra structure that we need. As we all know, proofs are programs, and like a program, a proof is only any good if it terminates. And to say that a program terminates is to say that if we order its possible “states” by setting $s_2 \lt s_1$ if some amount of computation from $s_1$ can lead to $s_2$ , then this order contains no infinite decreasing chains $\cdots \lt s_3 \lt s_2 \lt s_1 \lt s_0$ . In other words, it must be well-founded. So well-foundedness is precisely about the concept of termination of programs, i.e. validity of proofs.

Posted by: Mike Shulman on October 13, 2012 11:32 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

I didn’t have ZF axioms in mind particularly. The equivalence of the axiom of choice to the well-ordering principle is a theorem of mathematics, which could be formalized in any adequate ambient context, including ZF, a suitable topos, or what-have-you.

Thanks for replying to this bit. I’d been puzzled by what you had in mind when you said that the axiom of choice and the well-ordering principle were “equivalent”, because I didn’t think that you of all people would unthinkingly assume ZF as a background.

But what do you mean by a “theorem of mathematics”? If we want to deduce the axiom of choice from the well-ordering principle, or vice versa, surely we have to assume something about sets?

Posted by: Tom Leinster on October 14, 2012 4:38 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

surely we have to assume something about sets?

Yes, hence my use of the word “adequate”. (-:

In doing everyday mathematics, we don’t usually make all our assumptions explicit, nor all steps in our derivations. That is, we don’t work explicitly in any particular formal or axiomatic system. I think it’s valuable to view the process of “formalization” as something which starts from the sort of thing that most mathematicians call a “proof” and turns it into something else. In particular, the same input “proof” can be formalized in various different ways into various foundational systems. Of course a given formal system will not necessarily be adequate to formalize all unformalized proofs — a case in point is that if the unformalized proof uses the axiom of choice, then the formal system had better be able to deal with that.

But surely, one might ask, the “axiom of choice”, by the very nature of being called an “axiom”, is something that belongs to formal mathematics? I think the best way to answer that is to realize that the interaction between informal and formal mathematics is not unidirectional. Sometimes it’s useful to view informal mathematics as a “target” which a formal system can attempt to provide an encoding for. Other times, foundational developments can influence the way informal mathematics is done.

Personally, I tend to think of there being a sort of “core” of informal set-based mathematics which any foundational system had better be able to formalize to be worthy of the name. I’ll probably try to avoid having to pin down precisely what that core consists of, but it’s probably roughly what you have in an elementary topos. (I should maybe point out that I don’t think this “core” is determined only by Platonic mathematical considerations, but also by social conventions and common practice among human mathematicians. In particular, there’s no reason to suppose that what constitutes this “core” would remain constant over time. Probably some mathematicians would consider the axiom of choice as belonging to it by now. Others would prefer to exclude anything impredicative like a subobject classifier.)

Then there’s other stuff that we can consider adding, which is where things become more fluid. On the one hand, foundational developments can bring to light new axioms (such as the axiom of choice or large cardinals) or more radical novelty (such as homotopy type theory), which mathematicians then incorporate into everyday informal practice. On the other hand, informal mathematics may change or develop in such a way that formal systems have to then try to keep up with. There’s a feedback loop, of course: the axiom of choice originated in foundational concerns, but then became widely used informally, and now has to be at least taken into account (if not necessarily blanketly assumed) by any foundational system. On the other hand, one might argue that the need/desire of informal category theory for things like “the category of all sets” is driving new foundational development (with interesting results, if none that are yet entirely satisfactory). And the growing importance of homotopy theory and higher category theory in mathematics is certainly one motivation for the increasing study of homotopical and higher-categorical foundations.

So to sum up this long-winded answer to your question, by a “theorem of mathematics” I mean a theorem of informal mathematics, which could probably be formalized in any foundational system implementing the “core”. (In particular, it’s true in any topos — see D4.5.13 in Sketches of an Elephant.)

Posted by: Mike Shulman on October 14, 2012 6:12 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

Nice answer! :-) - especially the ‘I’m not being snarky’ chapter and verse reference to the topos-theoretic proof in the Elephant.

Posted by: David Roberts on October 15, 2012 7:40 AM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

That is indeed a really nice theorem in the Elephant. It couldn’t be cleaner. For those who don’t have a copy lying open beside them (shame on you!), it says:

In any topos, the choice objects are exactly the well-orderable objects.

I can’t say I knew what a “choice object” was, but the definition is a wrinkle-free topos-theoretic generalization of the standard set-theoretic idea.

Posted by: Tom Leinster on October 24, 2012 12:33 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

So well-foundedness is precisely about the concept of termination of programs, i.e. validity of proofs.

I like this point of view; I think it clarifies things.

The following is very likely a digression, but: is it really true that a program is only any good if it terminates? For example, the software that runs the Café sits there and does what it does, responding to inputs and producing outputs in the way we know and love. And we wouldn’t want it to terminate: if it did, we’d write to Jacques saying “help! the software’s stopped working!”

I suppose this is to do with the difference between programs in the classical Turing-esque sense of computability theory, and the more general and flexible notion of program that we’re used to in day-to-day life. Doubtless this difference has been very well raked over and understood by computer scientists, but it hasn’t entirely been understood by me.

Posted by: Tom Leinster on October 14, 2012 4:46 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

I suppose this is to do with the difference between programs in the classical Turing-esque sense of computability theory, and the more general and flexible notion of program that we’re used to in day-to-day life.

I think that’s one perfectly good explanation. One could say that a program in the Turing sense is designed to compute a result, whereas a program like a web server is designed to continue an interaction. And when we say that proofs are programs, we mean the first kind of program.

On the other hand, with an expressive enough type system, one can often regard “interaction” programs as “result” programs. For instance, in Haskell there is a “monad” called IO, such that a program whose type involves IO is one which interacts with “the world” along the way to producing a result. That is, a program of type IO int can read input from the user, request a web page, take a photograph and save it to disk, before returning its integer result. The main function in a Haskell program, which controls the overall execution, is generally of type IO (), meaning that it performs interaction and returns nothing interesting (the type () is Haskell’s “unit type”).

However, Haskell is a bad example if we want to talk about termination vs nontermination, because all programs in Haskell are potentially nonterminating. But there are languages with yet more expressive type systems (such as Coq) in which nontermination itself can be encoded, often using “coinductive types”.

An inductive type, like the natural numbers or the type of finite lists, is by definition well-founded. In particular, we can define functions over an inductive type by recursion, and such programs will be guaranteed to terminate on any input. On the other hand, a coinductive type is by definition ill-founded, like the type of infinite lists. Dual to how we can define functions out of an inductive type by recursion, we can define functions into a coinductive type by corecursion, and the guarantee that we get is not one of termination but rather of productivity: continuing to produce more and more data as it is evaluated (rather than “getting stuck” or “spinning forever”).

I think you’re familiar with corecursion, Tom, but I’ll explain a little more anyway for the benefit of bystanders. To illustrate the difference, here are two functions, one defined by recursion and one by corecursion. nat denotes the natural numbers, list nat the type of finite lists of natural numbers (an inductive type), stream nat the type of infinite lists of natural numbers (a coinductive type), a :: l the list (finite or infinite) obtained from the list l by sticking the number a in front, and nil the (finite) empty list.

countdown : nat -> list nat
countdown 0     = nil
countdown (n+1) = n :: (countdown n)

countup : nat -> stream nat
countup n = n :: (countup (n+1))

The function countdown is defined by recursion over nat, and is guaranteed to terminate because its natural number argument decreases by one with every call, and the natural numbers are well-founded. While the function countup is defined by corecursion into stream nat, and is not guaranteed to terminate (and in fact, never terminates), but is guaranteed to be productive in that every time you evaluate it further, it produces more elements of the (potentially) infinite list that is intended to be its “value”.

In this language, a program like a web server which is designed to “run forever” and “interact with its environment” could be regarded as producing a coinductive infinite stream of “interactions”. By introducing coinductive types, we can accomodate such potentially-infinite-running programs without sacrificing our ability to know that other programs (those without coinductive types) do always terminate — and therefore without sacrificing our ability to identify such programs with proofs. If we allowed arbitrary not-necessarily-terminating programs of any type, as is done in most “real-world” programming languages nowadays, then we would have plenty of “programs” which oughtn’t to correspond to a “proof” in any way, like

oops : false
oops = oops

the infinite loop, which can be declared to have any type (even a proof of false), since it never has to actually return any values. But it is neither terminating (of course) nor productive, so it is not valid either recursively or corecursively.

A nice explanation of essentially the same dichotomy from a slightly different point of view is this blog post from Bob Harper.

So I guess the short version of that answer is: there’s a more nuanced perspective according to which we don’t require that all programs terminate, only the recursive ones. In particular, we don’t always need our proofs to terminate either; if we write a coinductive proof (which is usually about a corecursive function), then it doesn’t terminate either—but it still must be productive, which is what makes it valid. However, recursive/terminating proofs are still so important, that I think they still explain the central role of well-foundedness.

Posted by: Mike Shulman on October 14, 2012 6:49 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

As Tom probably knows, what Mike describes is part of the coalgebraic approach to computer science, as adopted by CMCS and CALCO.

Ah, I see Bart Jacobs has just made available a version 2 of Introduction to Coalgebra: Towards Mathematics of States and Observations. Version 1 was very helpful to me writing my coalgebra paper.

Posted by: David Corfield on October 15, 2012 9:22 AM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

I almost feel as though a ‘Leinsterian’ sort of question to ask here is “what makes well-orderings an especially natural or ‘inevitable’ proof-technique when considering consequences of the axiom of choice?” (Of course, this is very close to questions Tom is asking in some of his comments! but I’m emphasizing the word ‘inevitable’ because it harks back to his recent series of posts on ultrafilters.)

And I also sense that the explanations by Mike and wren ng thornton are especially pertinent in trying to answer this question. It’s especially noteworthy that Mike has brought up corecursion and coinduction, because the notions of well-foundedness and well-ordering are indeed thoroughly coalgebraic in nature.

This topic is treated beautifully in Paul Taylor’s Practical Foundations of Mathematics. But it seems difficult to talk about this without discussing some order theory as well (which prompts me to voice a discomfort with Tom’s question, “Does anyone know a proof that $X \times X \cong X$ for infinite sets $X$ that neither uses substantial order theory nor involves elaborate convolutions to avoid doing so?” – my basic reaction to that is “how much order theory is too much?”). Thus, I’d prefer to nudge the question more toward the Leinsterian query posed at the top of this comment.

Here are a few remarks:

A binary relation $\prec$ on a set $X$ is the same thing as a $P$ -coalgebra structure $\theta: X \to P X$ , where $P$ is the covariant power-set functor. The connection is that $x \prec y$ iff $x \in \theta(y)$ . In many applications, $\prec$ will be transitive.
Under this translation, given a coalgebra $(X, \theta)$ , we say a subset $i: S \hookrightarrow X$ is inductive if, in the pullback
$\array{ H & \stackrel{j}{\to} & X \\ \downarrow & & \downarrow^\mathrlap{\theta} \\ P U & \underset{P i}{\to} & P X }$

the map $j: H \to X$ factors through $i: S \to X$ . We say $(X, \theta)$ is well-founded if the only inductive subset of $X$ is $X$ itself. (More discussion here.)
A coalgebra $(X, \theta)$ or binary relation $\prec$ is extensional if $\theta$ is monic. In other words, if $\{x: x \prec y\} = \{x: x \prec z\}$ implies $y = z$ .
By definition, a well-ordering is a transitive, well-founded, extensional relation. (Discussion here, including a proof that under excluded middle, we get from this definition the usual formulation of well-ordering, in particular the fact that the ordering must be linear.)

As a testing ground for some of these coalgebraic reformulations, it would be nice to consider the proof of Zorn’s lemma from the axiom of choice. Some time ago I had written an argument out for the nLab here, pretty much paraphrasing the line of argument presented in Lang’s Algebra. Looking back on this now, it looks a bit like pulling a rabbit out of a hat (it’s an argument not likely to impress Tom with any sense of its ‘inevitability’) – the well-orderings with which the argument begins seem to come out of the sky. But it seems to me that it should be possible to look at the structure of this argument anew through a coalgebraic lens, and write out an argument in which the magical well-orderings come out of the wash, and appear more naturally in a coalgebraic way.

Roughly what I have in mind is this. There is this absolute gem of constructive reasoning called Pataraia’s theorem. Look it over, and put a pin through that! Then, looking at the hypotheses of Zorn’s lemma, suppose we have a nonempty preordered set $X$ in which every chain of elements has an upper bound. Choose, for every nonempty set $S \subseteq X$ , a strict upper bound $\phi(S)$ for $S$ , and let $f(S) = S \cup \{\phi(S)\}$ ( $f(S) = S$ if $S$ has no strict upper bound). Following the ideas in Pataraia’s theorem, consider the smallest subset $A \subseteq P X$ that contains $\emptyset$ , is closed under $f$ , and is closed under taking unions of chains of inclusions.

I feel it should be possible to mimic some of the ideas in Pataraia’s proof to show directly that $A$ with its inclusion order is well-founded, transitive, and extensional, hence well-ordered (moreover that each element $T \in A$ is well-ordered by the relation it inherits as a subset of $S$ , and given $T, T' \in A$ , one is an initial segment of the other). This would lead to a proof of Zorn’s lemma in which well-orderings appear somehow more inevitably.

Posted by: Todd Trimble on October 14, 2012 9:30 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Sorry to have left this unanswered for so long. Partly it was life getting in the way, and partly I was embarrassed that you’d adjectivized me. “Leinsterian” is surely the right form if “Wagnerian” is. As for “Trimble”, I’d go for “Trimbolic”, along the lines of shambles/shambolic.

Anyway, I like your reformulation of my question. I’m also interested by the thought — expressed by both you and Mike — that well-orderings are coalgebraic in nature. Here’s a question: with the point of view on well-orderings that you have, what would you say is the most natural notion of “map” between well-ordered sets?

I agree, Pataraia’s fixed point theorem is a beaut. I remember Peter Johnstone getting tremendously excited about it in about 1999: if memory serves, it was announced at a PSSL (in Brno?), and Peter came back from there full of the joys of Pataraia’s theorem. Maybe you were even in Cambridge at the time, Todd.

I feel it should be possible to mimic some of the ideas in Pataraia’s proof […] [t]his would lead to a proof of Zorn’s lemma in which well-orderings appear somehow more inevitably.

That would be superb! It’s also close to what I’ve been planning to write about in the next post, though what you’re suggesting is much nicer than what I’ve been able to do.

Posted by: Tom Leinster on October 24, 2012 12:59 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

How about ‘Trimblean’? It was used here in a letter from Urs to Todd. I think I’ve also used that. But perhaps the club of classically-minded category theorists may wish to join in and tell us how to properly conjugate Todd’s nomen.

Posted by: David Roberts on October 25, 2012 12:23 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

The following is very likely a digression, but: is it really true that a program is only any good if it terminates?

It surely is a digression, but I think that question is one that has deeper importance than it may appear on the surface.

On the surface, the focus on terminating programs is, as you say, due to the focus on Turing-computable functions and the like, just as mathematics is traditionally concerned with finite/terminating proofs. As Mike says, this all comes from the idea that the targets of interest are objects— are things that are produced as the end result. Dually, there’s been a good deal of work on codata, which expresses programs that do not terminate (in a good way). From this perspective, the target of interest is not a thing, but rather is the process by which a thing is produced/consumed.

Personally, I see this divide as something like the divide I see between set theory and category theory. In set theory we focus on things —on sets and their elements— and take those to be the primitive notions from which everything else is derived. Whereas in category theory we focus on morphisms —on the processes of transformation between mostly-unspecified-things— and from these transformations derive all the rest (including any specifications on those mostly unspecified things).

But the above distinction between data and codata is part of the received wisdom, and I’m not sure that it really gets to the core of the question. I have the feeling that coming to a proper understanding of whether a “program” is only any good if “it terminates” is something we can only address once we have a better understanding of what programs really are and what termination (or productivity) really is. Surely the co/data story is a part of this deeper understanding, but it feels like it’s only scratching the surface. For instance, the syntactic guardedness condition on corecursion is an obvious hack: it’s blatantly sufficient for productivity, but just as blatantly not a necessary condition for productivity.

There are ways to get around that (e.g., induct on some counter which bounds how long you can go without providing output), so here’s a trickier one. In the social world we are perfectly well aware of the fact that nonresponse can, in itself, be a legitimate form of response. Indeed, refusing to answer a question is often sufficient to make clear what the answer to that question must be. But if we take this seriously, how can the co/data story account for the fact that nonresponse (or nonproductivity) can be a form of response (and therefore be productive)? Moreover, because time marches on, we must always either respond or nonrespond, and therefore must always leak a certain amount of information to our interlocutor. Thus, the progress of time during computation suggests that information-theoretic concerns will surely be tied up in the answer. And from there, issues of entropy and quantum-reversability aren’t too far behind. So it sounds at first like a question that has only to do with computer science (and hence logic and mathematics); but in the end it wades into the deeper waters of how entangled the physical and platonic worlds really are.

Posted by: wren ng thornton on October 14, 2012 11:02 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

“In the social world we are perfectly well aware of the fact that nonresponse can, in itself, be a legitimate form of response.”

This reminds me of a remark Ben Schumacher made to illustrate the same point. Paraphrasing: “When I was in college I had an arrangement with my parents. If I didn’t phone home at the weekend, this sent them the message that I didn’t even have a coin for the payphone, and so they should send money urgently.”

Posted by: Stuart on October 15, 2012 11:07 AM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

I see this divide as something like the divide I see between set theory and category theory

Hmm, I’m not sure I agree. Inductive and coinductive definitions both have natural (and dual) expressions inside category theory. I would say rather that data is something for which we focus on how it is used (hence giving a universal property for mapping out) while codata is something for which we focus on how it is produced (hence giving a universal property for mapping in).

For instance, the syntactic guardedness condition on corecursion is an obvious hack: it’s blatantly sufficient for productivity, but just as blatantly not a necessary condition for productivity.

While it’s true that it’s not necessary for productivity, it’s not an arbitrary hack either: it’s equivalent to definability using the terminal coalgebra characterization of a coinductive definition.

how can the co/data story account for the fact that nonresponse (or nonproductivity) can be a form of response (and therefore be productive)?

Easily: with a delay monad.

CoInductive partial (A:Type) : Type :=
| halt : A -> partial A
| delay : partial A -> partial A.

A computation of type partial A is either a terminated value of type A, or a delayed further computation. When handed a term of type partial A, you can choose to wait for it for any finite amount of time. If all it does is delay, then you have your responsive nonresponse.

By contrast, a truly nonterminating, nonproductive definition like my oops above does not give the caller the option of choosing how long to wait.

Posted by: Mike Shulman on October 15, 2012 4:00 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

Vaughan Pratt has argued for the duality of time and information in computer systems, writing, for example, in 1992 that:

“The states of a computing system bear information and change time, while its events bear time and change information.”

The interesting cases are those where the mere passage of time also transmits information, as in the muddy children problem and similar public announcement paradoxes.

Posted by: peter mcburney on October 28, 2012 12:03 AM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

If there were any examples of the sorts you allude to (adding ring structure to groups; adding group structure to sets;…), I would find those far stranger since those structures do not obviously correspond to logical principles of proof formation.

That’s an interesting example and it made me realize that the phenomenon we are discussing is common in homotopy theory. Namely, we often choose a model structure on a relative category and use it to prove some statement which is homotopy invariant, i.e. depends only on weak equivalences and not on the full model structure.

Perhaps one could even claim that such a move is in some sense unavoidable. Even if we can present a particular homotopy theory by something other than a model category, say a quasi-category or a complete Segal space, then the details of such presentation will use some model category type methods.

In fact (at least for cofibrantly generated model structures) this could count as a stucture corresponding to some logical principle which could be called “cellular induction”. By this I mean verifying a homotopy invariant statement about morphisms of a model category by first checking it for generating cofibrations and then that it is preserved by all operations we use to generate all cofibrations from them. That’s of course not the only way to use model categories, but I think it bears some similarity to the situation with sets and their well-orderings.

Posted by: Karol Szumiło on October 16, 2012 11:21 AM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Nice! I very much like the idea of model categories as a context in which to do “cellular induction”. In particular, it leads directly to higher inductive types! Ordinary inductive types are essentially a constructive way to build well-founded set-level structures, which we can then do induction over. Higher inductive types are a constructive way to build well-founded cell complexes, which we can then do “cellular induction” over.

In particular, I think that that point of view is illuminating as to the role of the axiom of choice in abstract homotopy theory: just as it allows us to put a well-founded ordering on an arbitrary set, it allows us to put a well-founded cell structure on an arbitrary homotopical object.

Coincidentally, I was discussing something closely related with Thierry Coquand yesterday: the classical proof that Kan complexes are an exponential ideal in simplicial sets (i.e. if $B$ is a Kan complex, then so is $B^A$ ) is apparently not valid constructively, because it depends on choosing a presentation of $A$ as a cell complex. Of course in a general model category, we only expect $B^A$ to be well-behaved when $B$ is fibrant and $A$ is cofibrant; but classically, every simplicial set is cofibrant, since we can well-order its simplices and use that order to build it up inductively as a simplicial cell complex. So constructively, it’s only natural to expect that we’ll need to assume $A$ to be cofibrant.

Posted by: Mike Shulman on October 16, 2012 3:33 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

In particular, I think that that point of view is illuminating as to the role of the axiom of choice in abstract homotopy theory: just as it allows us to put a well-founded ordering on an arbitrary set, it allows us to put a well-founded cell structure on an arbitrary homotopical object.

Right, this point seems especially similar to the one raised in the original post. I can vaguely see an analogy along the following lines. Homotopy theory of topological spaces up to (genuine) homotopy equivalence would correspond to set theory without a choice principle. Restricting attention to cell-complexes (equivalently, replacing homotopy equivalences with weak homotopy equivalences) would correspond to restricting attention to well-orderable sets. The fact that every space is weakly equivalent to a cell complex (I suspect this requires some form of choice) would correspond to some choice principle saying roughly “there are enough well-orderable sets” whatever “enough” should exactly mean.

Perhaps one could even state such a choice principle by postulating existence of a model structure on the category of sets satisfying some properties, one of which could be that cofibrant sets are well-orderable. Then “enough” would mean that every set admits a weak equivalence from a well-orderable set. We would also have a “Whitehead theorem” that every weak equivalence between well-orderable sets is a bijection. This still doesn’t help me in guessing what weak equivalences should be.

Posted by: Karol Szumiło on October 17, 2012 10:37 AM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Perhaps one could even state such a choice principle by postulating existence of a model structure on the category of sets satisfying some properties

An intriguing idea! But I’m not sure how to carry it out, since model category theory seems to use choice implicitly in so many ways. Also, there’s something funny going on somewhere, because cofibrant objects are usually the projective ones (good for mapping out of), while the well-orderable sets are the choice ones, which are good for mapping into.

Posted by: Mike Shulman on October 17, 2012 10:04 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

Also, there’s something funny going on somewhere, because cofibrant objects are usually the projective ones (good for mapping out of), while the well-orderable sets are the choice ones, which are good for mapping into.

Well, I would say that well-orderable sets are good for mapping out of since you can define maps out of them by transfinite induction. This fits with my analogy because cell complexes are good for mapping out of for the same reason.

Posted by: Karol Szumiło on October 18, 2012 7:21 AM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Yes, I realized that was what you meant, but there’s also a sense in which well-ordered sets are good for mapping into, because they come with a choice function. E.g. any entire relation with well ordered target contains a function.

Posted by: Mike Shulman on October 18, 2012 12:11 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

A similar phenomenon arises in computer science. People often speak loosely of data structures such as a “finite set”, but in reality you cannot work computationally with just a finite set. You need at least a decidable equivalence relation on elements, and, to be at all realistic, a decidable pre-order, in order to work with them. With only an equivalence (and no other assumptions) you tend to get linear-time algorithms for lookup; the pre-order is needed to get a logarithmic time lookup operation.

Sometimes people assume more structure, such as given enumeration of the elements of a finite set. This is often used in conjunction with the (entirely fictional) idea that you can access the elements of an array in constant time, which is to say that there is a constant time mapping [0..n] -> elts(A). This is only sort-of true for small enough n, but it is definitely not true for all n — underneath the assumption is a virtual memory system that uses a splay tree or similar data structure to do address translation.

I’m not sure if any of this has much bearing on your point, but I can definitely say that in CS the concept of an ordered set is far more important and useful than the concept of a “bare” set (common misleading terminology notwithstanding).

Posted by: Robert Harper on October 13, 2012 9:50 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

Hi Bob,

I had somehow overlooked your post when I wrote mine, which substantially overlaps with your comments. I’ll take this as an excuse to spell out some details of an interesting fact about “finite sets” in programming languages: namely, if all you have is a decidable equality relation on the elements, then there seems to be no function which can implement choice. That is, you can’t write a function choose : set -> (elt * set) option.

Concretely, suppose we represent sets as lists of nonrepeated elements. Then, we can write an operation choose : set -> (elt * set) option, which just returns a pair of the head and the tail if the list is nonempty, and returns NONE if it is empty.

However, this operation does not respect equality on sets. Note that any permutation of a list representing a given set also represents that same set, but the choose operation returns different answers for different permutations. As a result, this operation is not a function, since it does not behave extensionally on finite sets!

I feel there should be an argument involving parametricity which makes this work for arbitrary datatype representations, since all we rely on is the fact that equality can’t distinguish permutations. But I haven’t found it yet.

Posted by: Neel Krishnaswami on October 15, 2012 5:56 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

The difference between 1 and 2,3 is that 2,3 are each equivalent to Choice, whereas 1 isn’t.

Which I guess is an answer to your question “Does anyone know a proof”. I don’t any more, but I did 23 years ago when I took set theory from Peter Komjath, and I wager he still does.

Posted by: Allen K. on October 14, 2012 1:40 AM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

The difference between 1 and 2,3 is that 2,3 are each equivalent to Choice, whereas 1 isn’t.

It’s true: 1 is the odd one out, for a couple of different reasons (another one of which I mentioned in my post).

Which I guess is an answer to your question “Does anyone know a proof” [that $X \times X \cong X$ for infinite sets $X$ without using substantial order theory or involving elaborate convolutions to avoid doing so].

How so?

Posted by: Tom Leinster on October 14, 2012 4:28 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

I can’t help but bring up what I explain to students about the difference between linear orders and bijections of a finite set. Each is a nice example of a species, and the number of linear orders on a finite set is the same as the number of bijections: the factorial of the cardinality.

However, the number of structure types is not the same for bijections as it is for linear orders! Every linear order on a set is isomorphic to any other, but a bijection is only isomorphic to another which has the same size and number of cycles.

I don’t know if this sheds any light, since I’m not sure I understand the real question–or maybe it has been settled. Isn’t it true though, that linear orders are the unique species such that the ordinary (type) generating series and the exponential generating series are the same?

Posted by: stefan on October 14, 2012 7:25 AM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Yes, that’s my favourite example of two functors $F, G \colon A \to B$ such that $F(a) \cong G(a)$ for all $a \in A$ but $F$ is not naturally isomorphic to $G$ . I hadn’t thought of explaining it in terms of structure types, though. Thanks for that!

Posted by: Tom Leinster on October 24, 2012 1:04 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

In a material set theory where all sets are subsets of a universal set and you have equality of elements in different sets, does one need order theory for these examples. Never mind that such a theory doesn’t work for tricky large cases, much set theory has been done within this framework.

Posted by: RodMcGuire on October 14, 2012 7:30 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

So, a few thoughts, as everything smart has already been said.

There are four very commonly used forms of choice:

Surjections have a section
Every set has a well order
Zorn’s Lemma
Every vector space has a base

Two of them have to do with getting extra structure for free, two have to do with orders (intersection being obviously non-empty). The odd one out is the section thing. Is there any theorem that uses it in an essential way, yet doesn’t involve order or bases? Is it more or less useful than the well-ordering/existence-of-base ones? I’m pretty sure most mathematician would use the section lemma more casually (not even knowing it’s equivalent to choice).

On the well-ordering/base forms: using them almost necessarily means adding a structure that doesn’t appear in the statement. So the question is, probably, why these particular structures are useful rather than why we are adding structure out of thin air. I believe that that it allows the proof to be presented as a process nails it. (on a totally unrelated note, one thing I love about English is the ability to write “that that” in a grammatically correct sentence, I don’t know if it’s ever the right way to phrase it, though)

A last question could be: are there pure set-theoretic theorems out there that crucially depend on some order theories, but not on well-orders? Nor on fixed points?

All this is very naive, I’m afraid. Here is more naivety: from a higher category point of view, sets can be seen as something like 0-groupoids. Preoders are, then, 0-categories. So order theoretic stuff is, somehow, more primitive than pure set theoretic ones (in that sets are seen as preorder with extra-structures not the otherway around). From that point of view it wouldn’t be surprising that order-theoretic proofs of set-theoretic facts appear. However, it apparently has nothing to do with Tom’s questions.

PS: I believe we should agree to talk about “choice” or “principle of choice” rather than “axiom of choice” which is an unfortunate heritage of a particular avatar of it.

Posted by: Arnaud Spiwack on October 15, 2012 10:34 AM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Is there any theorem that uses it [the existence of sections of surjections] in an essential way, yet doesn’t involve order or bases?

Well, yeah. Zorn’s lemma, for one. (Zorn’s lemma as an axiom wouldn’t be very satisfying to most mathematicians, because it is hard to have a clear intuitive picture of what it means. Thus we prove it as a consequence of AC, for which we have developed intuitive pictures, and which many people believe is “true”.)

Some other examples that come to mind:

The Banach-Tarski paradox.
Vitali’s simple construction of a non-measurable set.

Posted by: Todd Trimble on October 16, 2012 1:16 AM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

I think I have an explanation. You mentioned arguments which prove things about sets by giving them an arbitrary well-ordering. You compared this with giving an arbitrary enumeration to a finite set to prove properties about it. Another example of something like this, which was mentioned by an earlier commenter, is using an arbitrary basis to a vector space. All of these examples have something in common: they take a mathematical object with lots of symmetries and give it a structure which removes these symmetries. In sets, this symmetry-removing structure is less obvious, but it still is serves the same purpose.

Now, I also have proofs for theorem 2 which doesn’t rely on this trick: Consider the bijections between an $A \subseteq X$ and a $B \subseteq Y$ . These form a partially ordered set if we say that $f \geq g$ iff $f$ is an extension of $g$ . In addition, every chain has an upper bound. By Zorn’s lemma, there is a maximal element $f : A \rightarrow B$ . This is only possible if $A = X$ or $B = Y$ .

I think a similar proof for theorem 3 is possible, although it’s definitely harder.

Posted by: Itai Bar-Natan on October 15, 2012 1:46 PM | Permalink | PGP Sig | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Thanks. The proof of theorem 2 (cardinal comparability) that you outline uses Zorn’s lemma, which I would certainly count as a significant chunk of order theory. So we’re still depending on order theory to prove basic results about sets. That, for me, is the noteworthy point.

Now it’s true, as you say, that this argument avoids uttering a phrase such as “now choose a well-ordering”. But one also has to prove Zorn’s lemma. A popular way to do that does involve an arbitrary choice of well-ordering. (Of course, we know that it will have to involve an arbitrary choice of something.)

Posted by: Tom Leinster on October 24, 2012 1:18 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

What sort of orders do you consider order theory, Tom?

For instance, D4.1.11 in the Elephant proves Cantor-Bernstein in a Boolean topos by considering the composite $PA\stackrel{\exists f}{\to}PB \stackrel{\neg}{\to}PB \stackrel{\exists g}{\to}PA \stackrel{\neg}{\to} PA$ where $f:A\to B$ and and $g:B\to A$ are injections. One might say this is a completely order-theoretic proof, but nothing to do with well-orders, just (Boolean) lattices, which is sort of to be expected with proofs by considering power objects.

Posted by: David Roberts on October 25, 2012 11:58 AM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

David wrote:

What sort of orders do you consider order theory, Tom?

This seems like a strange question. What sort of groups do you consider group theory? I’m not sure either question even makes sense.

Tautologically, I consider any part of the theory of orders to be a part of order theory. But I can’t imagine that helps you.

Johnstone’s proof of Cantor-Bernstein in a Boolean topos is a direct generalization of the order-theoretic proof I mentioned in my post, via Tarski’s fixed point theorem. I agree that when power objects are involved, it’s only natural to expect order theory to enter. But note that the statement of Cantor-Bernstein does not mention power objects.

Posted by: Tom Leinster on October 25, 2012 12:26 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

I meant it in the sense that a preordered set, or a partially ordered set, is quite a weak notion on its own. Lattices, well-ordered sets and so on are obviously much more structured and so one can say much more.

The fact that every set $X$ has a canonically - even functorially - associated distributive lattice $PX$ raises some flags for me, but I couldn’t say in technical terms why. And that is just objects of a topos, rather than looking at sets using full classical logic.

In the case of foundations when we don’t have power sets, then all sorts of interesting things break. If one could find a Boolean ‘predicative topos’ where, say Cantor-Bernstein failed, then we would be able to lay the blame squarely (or near enough) at the door of power sets, i.e. the assignment of a canonical lattice to each set. Benno van den Berg has worked on predicative toposes, he might be a good person to ask if this is possible.

Posted by: David Roberts on October 25, 2012 2:01 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

This, of course, won’t be as deeply insightful as the preceding remarks; as for Proposition 3, without mentioning cardinal ordinals (even a simple well-ordering on $X$ doesn’t seem enough help for me) the most I can make of $X$ being infinite is — actually I don’t know how this sort of infinity compares with others, but admitting enough Choice it shouldn’t matter — that $X$ has an injective map $f : X \to X$ which isn’t a surjection, and so has a natural partition into orbits of $f$ , which are of two principal sorts: $\mathbb{Z}/(r)$ s and $\mathbb{N}$ s — and at least one of the latter! How many parts there may be then depends on whether $X$ is countable, but in that case we already know that $X\times X$ is isomorphic to $X$ . If $X$ is not countable, then… I think I could argue that there are $|X|$ parts, but it seems awfully tedious. Don’t ask me to do more under such austerity!

All of that being prelude to remarking that admitting a well-order is nice, but admitting a cardinal well-order is even better, and there’s exactly one such type of well-order. In a similar way, working in an algebraically closed field is nice, but working in an algebraic closure of YOUR field is even better, when you can get away with it — and in both cases there may be many ways to get there, but it really doesn’t matter once that’s done.

The Thing about well-orders seems to me hinted at by the remarks preceding about $n$ and $(n)!$ ; and it then seemed a strange thing to me; for me there’s no objection at all in describing $(n)!$ in terms of orders because I don’t know how to say “ $n$ ” without describing implicitly some set that already has a canonical ordering on it. It’s very well to puzzle I’ve a set $X$ and every injection on it is automatically a bijection, so what can one say about $\mathfrak{S}_X$ ? but to talk about $n$ and $n!$ and ask one to ignore the natural ordering on the natural numbers is a rather perverse obscurity. To suppose that every set can be given a well-ordering is effectively to ask that the full subcategory on the ordinal tower should be skeletal in $Set$ ; which ordinals are equivalent to any given set is then much more like a Galois-theory question than a foundational question — it’s just the interval $[ |X| , |X|^+ )$ — or rather, those intervals are exactly the bijection classes in the ordinal tower.

But particularly, giving two cardinal orderings to a set is the same as giving a cardinal ordering and a bijection on the set. If I admit infinite sets, then I admit some really weird well-orderings (and that’s a good thing, too); but the type of the cardinal well-ordering is something like a normal form. There isn’t much else that the bijection class can remember about its members.

Posted by: Jesse C. McKeown on October 16, 2012 4:08 AM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Even if we only deal with naive set theory, it seems to me that, while proving theorems about sets, we are dealing with two kinds of sets: the sets we want to talk about and the sets we use to express ourselves. More generally, even if I want to speak about (the objects of) a category $C$ , I will use sets (talking of the set of maps from an object to the other, or saying that such object $X$ admits a presentation by a family (that is a set) of data which consists of maps of $C$ (i.e. a diagram) whose colimit is $X$ , for instance). If $C$ is the category of sets, sets of data as above don’t really have the same status as sets seen as objects of $C$ : after all $C$ might be any category which is a model of set theory (a boolean topos with axiom of choice, for instance), and I could prove theorems in $C$ using “ordinary naive sets” of data to present objects of $C$ . When I put some well ordering on a set $X$ , I simply see $X$ as the colimit of a (nice enough) functor $F:I\to C$ where $I$ is a small category with specific properties (a well ordered partially ordered set…); in other words, I then use an an external set (or category) theoretic language to speak of a specific object of the category of sets. Similar situations occur if you want to prove something about general modules over a ring, and use in your proof that you can prove something nice for projective module of finite type, and then use the fact that any module is a colimit of such things (or if you use the existence of an atlas while proving something about a manifold of some kind). This kind of things is still different in nature than endowing a set with a group structure: it is simply about generation of your category by privileged colimits, and, for sure, using such arguments might lead you to prove and use some specific things about the kind of indexing categories you use in your diagrams (like being a well ordered partially ordered set, a filtered category, a finite category, etc). In conclusion, it seems to me that the reason that some order theory arises in proofs of set theory is that we sometimes feel more comfortable to prove things using an external language (for instance to express the fact that an object may be constructed from a certain kind of data), rather than force ourselves to do everything internally.

Posted by: Denis-Charles Cisinski on October 17, 2012 10:46 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Well, that’s interesting.

In conclusion, it seems to me that the reason that some order theory arises in proofs of set theory is that we sometimes feel more comfortable to prove things using an external language (for instance to express the fact that an object may be constructed from a certain kind of data), rather than force ourselves to do everything internally.

Doesn’t this lead us back to the previous question: can we find a proof that $X \times X \cong X$ for infinite sets $X$ that doesn’t use order theory?

I had wondered whether the ordering was simply a matter of comfort or mental habit, as you suggest. By way of comparison, in elementary counting arguments about finite sets, sometimes we put the sets in order just out of habit; but perhaps we don’t actually need to. Similarly, if we’re struggling to prove something about vector spaces, we might choose a basis in order to put ourselves into a comfortable mental space, even if we don’t strictly need to (and work out a basis-free proof later).

Posted by: Tom Leinster on October 25, 2012 3:09 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Just a trivial observation regarding your question on the Hessenberg theorem, putting it into the context of your café, and trying to understand what you find strange. As you say, Hessenberg is usually proved by describing injections both ways, $X \rightarrow X \times X$ (trivially) and $X \times X \rightarrow X$ (using ordinal induction), and then invoking Cantor-Schröder-Bernstein. So to prove an isomorphism, the method resorts to maps that are not necessarily isomorphisms.

But this isn’t surprising at all. How often have you proved an isomorphism of groups, modules or some such, without resorting to non-iso homomorphisms? Or how often do people actually construct an inverse morphism in those categories if they just want to show that some two objects are isomorphic? I mean, it is surely very natural for everyone here to study the overall structure of a category even if we are mainly interested in its isomorphisms; so it strikes me as a little odd that you wouldn’t find it as natural for the category of sets.

Or perhaps your point is that the ordering of subobjects is so fundamental in the study of the category of sets with choice, where it is such a well-behaved thing. I don’t know; the same could be said about, say, the ideals of a module, which are only nice to work with as soon as you have a maximal ideal. Well, as soon as you have things that you can split into parts, you get a partial ordering which might be interesting. To me that’s as natural as it gets.

Posted by: maltem on October 20, 2012 2:24 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

I didn’t know it was called the Hessenberg theorem — thanks. But I think we might be talking at cross purposes. I certainly don’t find anything unnatural about using non-bijective functions between sets, or about using the inclusion order on subsets of a set. As you say, these are both very natural.

There are two things I find noteworthy:

For some basic theorems about sets, the statements do not mention order but the standard proofs do. Indeed, for some such theorems (such as Hessenberg’s), it seems that all known proofs use order theory. (E.g. the one you sketch uses ordinal induction.)
Moreover, the orders involved are not only the canonical inclusion orders that one has on a power set. A typical technique is to choose an arbitrary well-ordering on a set.

I’d like to know what pioneers such as Cantor and Dedekind thought of the apparent necessity of order theory in set theory. When they first started developing set theory, was it intuitively clear to them that significant amounts of order theory would have to be set up in order to prove results about sets? Or if not, were they surprised when this became apparent? And were they held back in their set-theoretic investigations by not knowing enough order theory (perhaps because it hadn’t been developed yet)?

Posted by: Tom Leinster on October 26, 2012 11:23 AM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

This comment is at best tangential to the main discussion here, but the following may shed some light on how Cantor viewed the relationship between sets and orderings. As you probably know, his notation for the cardinality of a set was not the currently popular “absolute value” notation but a double bar over the name of the set. The intention (and intension) behind the double bar was that the bars signify a mental operation of abstraction. One bar indicates abstraction from the particular elements of the set (regarding them all as essentially equivalent atoms of some sort); the second bar represents abstraction from the order in which the elements are given. Thus, from this point of view, sets come with an ordering a priori. If one wants to consider sets as we now understand them, completely abstract without an ordering, then one must perform the mental task of abstracting from the order.

(Originally posted at 18:41:39 on 5 Nov 2012)

Posted by: Andreas Blass on November 11, 2012 11:32 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

That’s fascinating — thanks very much. As it happens, I recently bought the little Dover book, Contributions to the founding of the theory of transfinite numbers, containing translations of two of Cantor’s seminal papers. I didn’t know about the notation you describe, which must mean that I hadn’t started reading it, because it’s introduced on the second page.

It’s worth quoting some of the first paper. Some of the phrases that follow seem familiar to me; I guess they’re famous. The paper begins:

By an “aggregate” (Menge) we are to understand any collection into a whole (Zusammenfassung zu einem Ganzen) $M$ of definite and separate objects $m$ of our intuition or our thought. These objects are called the “elements” of $M$ .

Half a page later:

Every aggregate $M$ has a definite “power”, which we will also call its “cardinal number”.

We will call by the name “power” or “cardinal number” of $M$ the general concept which, by means of our active faculty of thought, arises from the aggregate $M$ when we make abstraction of the nature of its various elements $m$ and of the order in which they are given.

I find the last few words of that, “order in which they are given”, quite strange, because the characterization of “aggregates” in the first quotation doesn’t refer to order at all.

He goes on:

We denote the result of this double act of abstraction, the cardinal number or power of $M$ , by $\overline{\overline{M}}.$

He then defines two aggregates $M$ and $N$ to be “equivalent” if (in modern language) there is a bijection between them. He writes $M \sim N$ to mean that $M$ and $N$ are equivalent. And a little later, he says something else I find strange:

Of fundamental importance is the theorem that two aggregates $M$ and $N$ have the same cardinal number if, and only if, they are equivalent

(or in his notation: $M \sim N$ if and only if $\overline{\overline{M}} = \overline{\overline{N}}$ ). What surprises me is that he calls this a theorem. The description of $\overline{\overline{M}}$ , with all the stuff about “active faculty of thought”, hardly seems precise enough to have a theorem proved about it. Perhaps the meaning of “theorem” has shifted over time, or perhaps translation is a factor here. Nevertheless, he does give a justifying argument for the theorem shortly afterwards. It reads to me like an explanation for why equivalence (as defined via existence of a bijection) is a good formalization of the idea of “have the same number of elements”.

(None of that is supposed to be critical of Cantor, who was of course performing amazing intellectual feats. It’s just impossible, at least for me, not to read an 1895 text through anything other than 2012 eyes.)

(Originally posted at 22:37:05 on 5 Nov 2012)

Posted by: Tom Leinster on November 11, 2012 11:33 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

What surprises me is that he calls this a theorem.

Yes, Cantor’s living in very different times. Look at Dedekind’s proof of the existence of infinite sets

My own realm of thoughts, i.e., the totality $S$ of all things, which can be objects of my thought, is infinite. For if $s$ signifies an element of $S$ , then is the thought $s'$ , that $s$ can be object of my thought, itself an element of $S$ . If we regard this as transform $\phi(s)$ of the element $s$ then has the transformation $\phi$ of $S$ , thus determined, the property that the transform $S'$ is part of $S$ ; and $S'$ is certainly proper part of $S$ , because there are elements in $S$ (e.g., my own ego) which are different from such thought $s'$ and therefore are not contained in $S'$ . Finally it is clear that if $a, b$ are different elements of $S$ , their transforms $a'$ , $b'$ are also different, that therefore the transformation is a distinct (similar) transformation [26]. Hence $S$ is infinite, which was to be proved.

And remember inner sense and time have been closely associated since at least Kant, whose influence on nineteenth century German thinking was immense. So it doesn’t surprise me that Cantor viewed the elements of a Menge as ordered.

Should we lament the loss of this more overtly philosophical mathematics?

(Originally posted at 08:52:06 on 6 Nov 2012)

Posted by: David Corfield on November 11, 2012 11:38 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Blimey!

It’s fun to go through this and discern the outlines of the notion of Dedekind finiteness (every injective endomorphism is invertible). I confess, I’d innocently imagined that Dedekind must at some stage have written something along the lines of: “we may regard a set $X$ as finite if every injective function from $X$ to $X$ is surjective.” Obviously he wouldn’t have used words like “injective” (or the German equivalent), but equally, I hadn’t imagined that he’d invoke his own ego.

It’s interesting what you say about time. Not knowing anything about nineteenth-century German philosophy, that’s news to me.

(Originally posted at 12:55:15 on 6 Nov 2012)

Posted by: Tom Leinster on November 11, 2012 11:39 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Should we lament the loss of this more overtly philosophical mathematics?

I sure don’t. (-: Although I’d be interested to hear arguments in favor of it…

(Originally posted at 15:19:09 on 6 Nov 2012)

Posted by: Mike Shulman on November 11, 2012 11:41 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Well, might we say you wouldn’t be in Princeton now had Martin-Löf not thought long and hard about Brentano, Frege and Husserl?

I’ve also been reading about how Weyl sees himself as conducting a Husserlian Wesenanalyse on the notion of space by understand its infinitesimal structure group-theoretically.

Then there’s Lawvere.

(Originally posted at 21:48:07 on 6 Nov 2012)

Posted by: David Corfield on November 11, 2012 11:47 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

It seems to me that there’s a difference between thinking about philosophy and then doing some mathematics motivated or inspired by the philosophy, versus thinking that philosophy is mathematics. I don’t really understand it when Martin-Lof or Lawvere descend into philosophy, but then they come back up with interesting mathematics. However, to me those passages from Cantor and Dedekind are philosophy — or, at least, they are not mathematics — and so I thought your question was whether we should lament the passing of their practice of calling it “mathematics”. (-:

(Originally posted at 14:51:22 on 9 Nov 2012)

Posted by: Mike Shulman on November 11, 2012 11:48 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Well I’m sure Lawvere has a more integrated view of the relationship than you, e.g.,

It is my belief that in the next decade and in the next century the technical advances forged by category theorists will be of value to dialectical philosophy, lending precise form with disputable mathematical models to ancient philosophical distinctions such as general vs. particular, objective vs. subjective, being vs. becoming, space vs. quantity, equality vs. difference, quantitative vs. qualitative etc. In turn the explicit attention by mathematicians to such philosophical questions is necessary to achieve the goal of making mathematics (and hence other sciences) more widely learnable and useable. Of course this will require that philosophers learn mathematics and that mathematicians learn philosophy. (Categories of Space and of Quantity, p. 16)

But you’re right, of course, that there’s been a change since the nineteenth century, with in most people’s minds a clearer separability of philosophical motivation and mathematics.

I’ve been looking at Weyl of late. There’s a very clear philosophical motivation for some of his work in the early 20s, e.g., when he shows that of the Finsler metrics which may be placed on a manifold, only those which are ‘Pythagorean’ have a certain property (admits just one affine connection) which must be the case for the space we inhabit. Maybe one could see this as foundations of physics, but he himself saw it as a Wesenanalyse of space in the sense of Husserl, and others see the strong hand of Fichte. (For all this, articles by Erhard Scholz are very useful.)

In 1925,

he started intense reading work for his contribution to Philosophie der Mathematik und Naturwissenschaften in Handbuch der Philosophie. He took this task very seriously; it occupied him well into the year 1926. In his letter to Born of Sep. 27, 1925, he characterized himself as “fettered to the deep swamp of philosophy (gefesselt an das tiefe Moor der Philosophie)”. This did not hinder him, on the other hand, to follow very closely what was going on inside the Göttingen group of theoretical physics during 1925, with its great step towards a new kind of mathematized quantum mechanics. (Scholz, Weyl entering the ‘new’ quantum mechanics discourse)

With this he seems to move away from mathematics being able to characterise the place of the knowing subject in the world. And generally that tie between philosophy and geometry seems to weaken. With logic the bond remains much stronger.

(Originally posted at 16:52:18 on 9 Nov 2012)

Posted by: David Corfield on November 11, 2012 11:50 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Returning here after having thought about something completely different, I think I got the point of your post now.

Observation: When working with abstract sets, there’s a need to endow them with some additional structure in order to define useful maps between them. Without at least their arithmetic structure, the real numbers, say, are just a huge point cloud, with nothing to get hold on. So when we want to convince ourselves that they have the same cardinality as some other set, we will use some of their structure, even if we’re just proving something about them as an abstract set. In a sense, abstract sets are “too abstract to work with”.

So when confronted with the task to construct an injection $X \times X \rightarrow X$ , there doesn’t seem to be another way out than to endow those sets with some structure (or better: find representants of those sets in a category over Sets where objects have more structure), then use that structure to define the injection.

Now your question is why an ordering should be the best way out. (Sorry, I was a little slow to arrive here.)

My bet is that it’s where naive reasoning gets you the fastest. Being confronted with two huge point clouds, $Y = X \times X$ and $X$ , with the task to construct an injection between them, how would I start about it? «Let’s see, for starters let us pick an element $y_0 \in Y$ , pick an element $x_0 \in X$ , and map $y_0$ to $x_0$ . Then pick the next element $y_1$ , choose some $x_1 \neq x_0$ to map it to, “and so on”. Of course this doesn’t work out until we invent a way to continue this and-so-on in a really clever way. And at each step we’ll also have to prove that there’s a suitable element of $X$ left. If only we had something like ordinal induction…»

This possibly doesn’t explain very much, so the next thing to do would be a psychological analysis of that line of naive reasoning… But one thing stands out at least: A well-order is a very handy tool if you want to construct an injection. If you’d hand me some arbitrarily chosen group structure on $Y$ , I still wouldn’t know how to start about it. With a well-order, on the other hand, I get at least an idea how to start; and then I’ll spell some magic incantations so as to be able to continue, and arrive.

(Originally posted at 14:41:06 on 3 Nov 2012.)

Posted by: maltem on November 11, 2012 11:30 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

“Can we prove $X \times X \simeq X$ without order theory?” Tom keeps asking. Having thought a little more about it, I still don’t know, but I’ve some different noises to make than last time. I will try to describe a semantics that incidentally makes order theory unhelpful, and show that under the same semantics the Hessenberg Theorem doesn’t seem to hold — or at least, the nonstandard semantics separates propositions that in Choicy Set Theory are equivalent to Hessenberg.

I’m told there’s some interest to be had from attempting a homotopical semantics for equality in first-order Set Theory propositions; so consider the map $2 : \mathbb{S}^1 \to \mathbb{S}^1$ of degree 2. This also has hfibers equivalent to Inductive S0 := Nh | Sh, which definitely is_inhab, but good luck getting a section. However, I think we should agree this map is not an injection, because it isn’t $\pi_1$ -surjective. So, $\mathbb{S}^1$ supports something-like-a-surjecion that also isn’t a-particular-sort-of-injection. If you will, $\mathbb{S}^1$ is not finite. At the same time, $\mathbb{S}^1 \times \mathbb{S}^1$ definitely is not equivalent to $\mathbb{S}^1$ — one needs two winding numbers to name a loop in $\mathbb{S}^1\times \mathbb{S}^1$ .

Now, by looking at this weird semantics, I haven’t exactly forbidden order theory, but certainly there isn’t any useful and continuous order one could put on $\mathbb{S}^1$ ; but whether you will look on this coincidence of unorderability and nonHessenbergsatz as accidental, or as evidence that one leads to the other, I don’t know.

(Originally posted at 01:51:17 on 6 Nov 2012)

Posted by: Jesse C. McKeown on November 11, 2012 11:36 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Cute. All sorts of choicy things do tend to fail when you involve types of h-level $\gt 2$ . I wonder whether there even is a meaningful notion of “finiteness” for such types.

Let’s see, according to the nLab page on finite sets we have

A set is finite if it admits a bijection with $[n]$ for some natural number $n$ . Clearly only h-sets can have that property!
A set is subfinite if it admits an injection into some finite set $[n]$ . If by “injection” we mean monomorphism, then only h-sets can have that property too.
A set is finitely indexed (or Kuratowski-finite) if it admits a surjection from some finite set [n]. If by “surjection” we mean an effective epimorphism (which is logical since these are the things that fit into a factorization system with the monomorphisms), then $S^1$ is finitely indexed, since $1\to S^1$ is an effective epi. But this doesn’t seem a particularly good notion of finiteness, since any connected type (with arbitrarily large higher homotopy) would be “finitely indexed”.
A set is subfinitely indexed if it admits a surjection from a subfinite set, or equivalently admits an injection to a finitely indexed set. Since that’s even more general than being finitely indexed, probably also not a good definition.
A set $X$ is Dedekind-finite if it satisfies one of the following:
- any injection $X\hookrightarrow X$ must be a bijection (i.e. an equivalence).
- for any function $f:\mathbb{N}\to X$ from the natural numbers, there exist $n,m$ with $n\neq m$ such that $f(n)=f(m)$ .

Your example shows that $S^1$ is not Dedekind-finite in the first sense. But if we interpret “there exists” in the h-prop logic, then it is Dedekind-finite in the second sense—as would be any connected type. So maybe that is not a good definition either.

Are there types of h-level $\gt 2$ that are Dedekind-finite in the first sense? Perhaps a type of finite h-level whose homotopy groups are all finite? And what happens if we interpret the second definition of Dedekind-finite in the propositions-as-types logic?

Of course there is also the categorical definition of finiteness: $Hom(X,-)$ preserves filtered colimits. For h-sets I think this is equivalent to Kuratowski-finiteness (is that right?), while classically for higher types it allows “compact” or “finitely presented” ones.

(Just out of curiosity, does anyone know what Kuratowski wrote that inspired people to name the notion of “finitely indexed” after him?)

(Originally posted at 15:48:26 on 6 Nov 2012)

Posted by: Mike Shulman on November 11, 2012 11:45 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

“Does anyone know a proof that X×X≅X for infinite sets X that neither uses substantial order theory nor involves elaborate convolutions to avoid doing so?”

Maybe I’m missing the point of the discussion here, but the assertion that “X×X≅X for all infinite sets X” is an easy equivalent of WO.

[For the -> direction: Let h(X)= { α ∈ On : there is an injection of α into X }. h(X) is an aleph and there is no injection of h(X) into X - ie we have ¬ (| h(X) | ≤ |X|).

Consider the disjoint union X + h(X). By hypothesis, (X + h(X)) × (X + h(X)) ≅ (X + h(X)), so | X × h(X) | = |X| × | h(X) | ≤ |X| or |h(X)|. By the `ie’ in the previous paragraph, we must have the latter: |X| × |h(X)| ≤ |h(X)|. Hence |X| ≤ |h(X)|. Hence |X| is an aleph. ]

Posted by: Charles Morgan on February 25, 2013 6:16 AM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Thanks for the comment, Charles.

I didn’t know the proof you gave. It seems to use about the same amount of order theory as the other proofs I know, which I’d call a “substantial” amount. Of course, “substantial” is a subjective judgement, but that was the sense in which I meant the word in my post.

The point is that when showing that

(your favourite axioms of set theory) + (axiom of choice) imply ( $X \times X \cong X$ for infinite sets $X$ ),

one seems to have to make a nontrivial detour via order theory. In the case of your proof, that involves well-orderings, ordinals, and alephs. None of those concepts is apparent in the statement of the result.

Posted by: Tom Leinster on February 25, 2013 10:09 AM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

“The point is that when showing that (your favourite axioms of set theory) + (axiom of choice) imply (X×X≅X for infinite sets X), one seems to have to make a nontrivial detour via order theory. In the case of your proof, that involves well-orderings, ordinals, and alephs. None of those concepts is apparent in the statement of the result.”

The little proof in my previous comment (due to Hartogs) shows that “X×X≅X for allinfinite sets X” implies that “every set can be well ordered.” Thus order concepts do appear in the statement of the result; and it’s understandable that order concepts are going to appear in the proof since the obvious general strategy - however one actually does the proof - is to start with an arbitrary set and show it can be well ordered. The reason for including the proof was to show how short it it - that is, that the hypothesis is only an extremely lightly disguised order-theoretic one.

More generally you asked:

“I’d like to know what pioneers such as Cantor and Dedekind thought of the apparent necessity of order theory in set theory. When they first started developing set theory, was it intuitively clear to them that significant amounts of order theory would have to be set up in order to prove results about sets?”

Without going into a blow-by-blow history of set theory, the answer to your question (at least for Cantor) is surely a resounding `yes.’ The discovery/invention of the ordinals (and transfinite recursion) is the big thing that Cantor did and he was very aware of that.

Posted by: Charles Morgan on February 25, 2013 6:26 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

I think either I’m not understanding you, or you’re missing the point of the post.

The idea is not to assume any of the paraphernalia of set theory, but to think about sets in as fresh a way as possible, without preconceptions. For example, it’s against the spirit of things to say:

the obvious general strategy - however one actually does the proof - is to start with an arbitrary set and show it can be well ordered.

It’s obvious to appropriately-trained people now, but that’s off the point.

Similarly, calling the proof you gave a “little proof” is against the spirit of things, because what we’re trying to do is to be very sensitive to all the concepts involved. When you look at that little proof carefully, you see that it contains a lot of concepts (including several order-theoretic ones). When you evoke the notion of an aleph, for instance, you’re calling on a substantial order-theoretic development.

Again, when you say “order concepts do appear in the statement of the result” (that $X \times X \cong X$ for infinite sets $X$ ), it only looks that way to you because you’re very familiar with the relationship between this result and order-theoretic results.

This might be beginning to sound as if I have something against order-theoretic methods. I don’t! I like order theory. But what I’m trying to do is listen to the mathematics, including all the tiny sounds.

More generally you asked:

“I’d like to know what pioneers such as Cantor and Dedekind thought of the apparent necessity of order theory in set theory. When they first started developing set theory, was it intuitively clear to them that significant amounts of order theory would have to be set up in order to prove results about sets?”

Without going into a blow-by-blow history of set theory, the answer to your question (at least for Cantor) is surely a resounding ‘yes.’ The discovery/invention of the ordinals (and transfinite recursion) is the big thing that Cantor did and he was very aware of that.

Do you know whether Cantor realized the necessity of order theory for set theory from the beginning? That was really my question.

Posted by: Tom Leinster on February 25, 2013 11:36 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

My impression is that Cantor invented set theory to prove the Cantor-Bendixson theorem by transfinite induction on ordinals. So yes, ordinals were always central his work on set theory.

Posted by: Walt on February 27, 2013 6:06 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Maybe it’s a little clearer to a bystander where a miscommunication has occurred here.

Tom says that the result

$X \times X \cong X$ for all infinite sets $X$ .

does not involve order-theoretic concepts in its statement. Charles says that the result

If ( $X \times X \cong X$ for all infinite sets $X$ ), then every set $X$ can be well-ordered.

does involve order-theoretic concepts in its statement. Tom and Charles have each used the phrase “the result” but were referring in different places to each of those results.

Posted by: Mark Meckes on February 26, 2013 3:01 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

Oh, I see. That does clarify things. Thanks.

Nevertheless, I would still say that this:

The reason for including the proof was to show how short it it - that is, that the hypothesis is only an extremely lightly disguised order-theoretic one

is not in the spirit of the post. Contemplating the passage between statements that do and don’t overtly involve order-theoretic concepts is the entire point. To describe this as an “extremely light disguise” is to gloss over the actual point of interest.

Posted by: Tom Leinster on February 26, 2013 4:21 PM | Permalink | Reply to this

Re: The Curious Dependence of Set Theory on Order Theory

$MathML-enabled post (click for more details).$

”.. or you’re missing the point of the post.”

“The idea is .. to think .. without preconceptions”

“what we’re trying to do is to be very sensitive”

“When you look at that little proof carefully”

“what I’m trying to do is listen to the mathematics, including all the tiny sounds”

oh the ironing

Posted by: Charles Morgan on March 1, 2013 4:21 PM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

October 13, 2012