Feferman Set Theory

November 30, 2009

Posted by Mike Shulman

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

There’s been a bunch of discussion online recently (e.g. SBS, MathOverflow 1, 2, 3, etc.) about set-theoretic foundations for category theory, the role of universes, and so on. So I thought I would take this opportunity to advertise a set theory which isn’t that well-known, but which I find particularly pleasing as a foundation for category theory. I’ll call it strong Feferman set theory, since it is a stronger variant of a theory proposed by Solomon Feferman in his paper “Set-theoretical foundations of category theory.” Feferman called his theory ZFC/S (“ZFC with smallness”), and thus strong Feferman set theory could reasonably be called “ZMC/S,” for reasons explained below. (Feferman called the strong variant “ZFC/S + RIn(S)”.)

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

I’m going to assume some familiarity with the set-theoretic issues besetting category theory, and also some exposure to the idea of (Grothendieck) universes. To summarize the application of the latter to category theory, the first idea we might come up with is that if we have a universe $U$ , we can treat the mathematical objects in $U$ as the “small” ones, so that then the category $Set=Set_U$ of all small sets is, itself, a set (just not a small one). Thus, we can manipulate “large” categories with impunity, since they are still just sets, rather than mysterious and ill-behaved “proper classes.” In particular, one can form functor categories $B^A$ when $A$ and $B$ are large, which most theories of classes don’t allow.

However, what if at some later date we decide there’s something not in $U$ that we want to treat as an ordinary “small” mathematical object? For instance, it might be a category $C$ that’s large relative to $U$ . We’d have to hope there’s another, bigger universe $U'$ that contains $C$ , so we could switch to working with $U'$ as our universe. To ensure that such switches are always possible, Grothendieck proposed the axiom that “every set is contained in some universe.”

Why might one be dissatisfied with universes? Well, one thing is that even the existence of one universe is unprovable in ZFC (assuming it is consistent), and Grothendieck’s axiom is noticeably stronger than that. However, it is also very weak compared to many large-cardinal axioms, so let’s lay aside that question. I think a more important philosophical objection, though perhaps rarely voiced, is that many mathematicians are accustomed to thinking of $Set$ (for instance) as the category of all sets, and it’s disconcerting to be told that actually, you’re only allowed to include small sets in it.

That philosophical unease actually also has a purely mathematical manifestation. Suppose I want to prove something about (say) all groups, and I do it by considering some arbitrary group as an object of the category $Grp$ . In the universe framework, I haven’t actually proven something about all groups; I’ve proven something about all $U$ -small groups. However, presumably my proof didn’t use any properties of $U$ other than that it was a universe, and so for any group $G$ whatsoever, I could choose (assuming Grothendieck’s axiom) a universe containing $G$ and repeat the proof using that universe as my $U$ . In other words, all of our theorems come with an implicit quantifier “for any universe $U$ ,…” stuck on the front.

But wait! It’s not just that the statement I’ve proven only applies to $U$ -small groups; any quantifiers in the statement that run over “all groups” are also restricted to $U$ -small groups. For instance, consider the universal property of the cartesian product of groups $G\times H$ , which says that for any group $K$ and any homomorphisms $\phi\colon K\to G$ and $\psi\colon K\to H$ , there exists a unique homomorphism $\chi\colon K\to G\times H$ such that $\pi_1\chi = \phi$ and $\pi_2\chi = \psi$ . Now suppose that, through clever category theory, I’ve managed to prove the statement that “ $G\times H$ is a product of $G$ and $H$ in the category $Grp$ ”. In the world of ordinary set theory, where $Grp$ is the category of all groups, I’m done! But in the world of universes, where $Grp$ is the category of $U$ -small groups, I’ve only shown that the universal property holds for $U$ -small groups $K$ .

Now, as before, I could presumably repeat my proof for any universe $U$ , thereby showing that the universal property actually holds for all groups $K$ (since, by Grothendieck’s axiom, any such $K$ is contained in some universe). However, in a more complicated situation, the construction of $G\times H$ (or some other object having a putative universal property) might, in theory at least, depend on $U$ . This isn’t as far-fetched as it might sound; maybe we have some object constructed by an appeal to the adjoint functor theorem, which depends on size considerations for the entire category $Grp$ , and thereby on the universe $U$ . So if I really want a universal property that is true for all groups $K$ , I have to do some careful analysis of my construction and make sure that it will be preserved by “passage to a higher universe.”

(Strong) Feferman set theory remedies this as follows. To ZFC (or your favorite set theory) we add a constant symbol $U$ together with the axiom “ $U$ is a universe,” and also an axiom schema stating that for any statement $\varphi$ , all of whose parameters are in $U$ but which does not mention $U$ explicitly, we have $\varphi^U \iff \varphi$ . Here $\varphi^U$ denotes $\varphi$ relativized to $U$ , meaning that all of its quantifiers are constrained to run only over elements of $U$ . (In other words, $U$ is an elementary substructure of the class of all sets.) This is called a reflection principle. Intuitively, you can think of it as saying “large objects act the same as small ones.”

Some examples should help clarify what this means and how it is used. We define a small set to be an element of $U$ , and likewise a small group and so on. Notice that $U$ is now fixed and doesn’t vary. We define $Set$ to be the category of all small sets, and likewise $Grp$ . And as in the ordinary setup of universes, these large categories are still sets, so there is no problem doing anything with them that we might like.

Now suppose we know that for some small groups $G$ and $H$ , some other small group $G\times H$ is a product in the category $Grp$ . That means that the following statement is true:

for all small groups $K$ , for any homomorphisms $\phi\colon K\to G$ and $\psi\colon K\to H$ , there exists a unique homomorphism $\chi\colon K\to G\times H$ such that $\pi_1\chi = \phi$ and $\pi_2\chi = \psi$ .

Now we observe that this statement is the relativization to $U$ of the following statement:

for all groups $K$ , for any homomorphisms $\phi\colon K\to G$ and $\psi\colon K\to H$ , there exists a unique homomorphism $\chi\colon K\to G\times H$ such that $\pi_1\chi = \phi$ and $\pi_2\chi = \psi$ .

That is, to get from the second to the first we replaced the quantifier “for all groups” with a quantifier ranging over small things: “for all small groups.” (Strictly speaking, we should have replaced the quantifiers over homomorphisms as well—that is, we should have written in the first statement “for any small homomorphisms” and “there exists a unique small homomorphism.” However, properties of a universe ensure that any function between small sets is always small, so this is unnecessary.) Moreover, all the parameters of the second statement ( $G$ , $H$ , and $G\times H$ —everything that’s not quantified over) are in $U$ , but the statement doesn’t mention $U$ explicitly. Thus, the reflection schema applies, and tells us that the second statement follows from the first. In other words, after proving a universal property in the category $Grp$ of small groups, we can automatically conclude that the same universal property holds—for the same product $G\times H$ —relative to all groups.

Okay, well, what about cartesian products of large groups? We can apply the reflection schema again. Assuming our construction of products in $Grp$ was sufficiently general, we’ve actually proven that

for all small groups $G$ and $H$ , there exists a small group $G\times H$ and homomorphisms $\pi_1\colon G\times H\to G$ , $\pi_2\colon G\times H \to H$ , such that for all small groups $K$ , for any homomorphisms $\phi\colon K\to G$ and $\psi\colon K\to H$ , there exists a unique homomorphism $\chi\colon K\to G\times H$ such that $\pi_1\chi = \phi$ and $\pi_2\chi = \psi$ .

But this is the relativization of the statement

for all groups $G$ and $H$ , there exists a group $G\times H$ and homomorphisms $\pi_1\colon G\times H\to G$ , $\pi_2\colon G\times H \to H$ , such that for all groups $K$ , for any homomorphisms $\phi\colon K\to G$ and $\psi\colon K\to H$ , there exists a unique homomorphism $\chi\colon K\to G\times H$ such that $\pi_1\chi = \phi$ and $\pi_2\chi = \psi$ .

and therefore the latter is also true. In this way, we can constrain ourselves to work with small things whenever necessary, so that our large categories are (sets and hence) well-behaved, but then turn around and apply the reflection schema to expand all of our conclusions to arbitrary objects, not just small ones. Or, in other words, we can use large categories with impunity to prove things about the category $Set$ of small sets, but then when we are done, anything we’ve proven about $Set$ (of a suitable logical form) will also be true about the category $SET$ of all sets (which is a “classical” large category, i.e. a proper class). This deals nicely with the philosophical objection to universes: though we may care about the category of all sets, we can restrict ourselves to a category of “small” sets without changing the content of our theorems, because of the reflection schema.

Let me end with some remarks on the strength of strong Feferman set theory. First notice that it can prove Grothendieck’s axiom of universes. For suppose that $x$ is a small set. Then since $U$ is a universe, the statement “there exists a universe containing $x$ ” is true. By reflection, it is also true that “there exists a small universe containing $x$ .” But since $x$ was an arbitrary small set, we have shown that “for all small sets $x$ , there exists a small universe containing $x$ .” Now by reflection again in the other direction, it must also be true that “for all sets $x$ , there exists a universe containing $x$ .” In particular, $U$ itself is contained in a universe, which is contained in another universe, and so on. But since every small set is also contained in a small universe, there are plenty of universes below $U$ as well. So we have a plethora of universes—but of all of them, only $U$ is distinguished by the reflection schema.

In fact, strong Feferman set theory is equiconsistent with ZMC, which means ZFC together with the assumption that $Ord$ , the class of ordinals, behaves like a Mahlo cardinal. This is notably stronger than Grothendieck’s axiom, but still not very strong as large-cardinal principles go, and I think most set theorists would agree that it is almost as sure to be consistent as ZFC itself.

Feferman’s original proposal was actually no stronger than ZFC, because it didn’t assert that $U$ is a Grothendieck universe, only that it satisfies the ZFC axioms. (The difference is in whether the replacement axiom is first-order or second-order.) This is good enough for many purposes, so anyone who wants a universe-like theory but is philosophically unsettled by anything stronger that ZFC should consider Feferman’s original set theory ZFC/S. However, the weaker version also leads to some unexpected technical difficulties in category theory, which are detailed here for anyone who is interested. So while Feferman’s original goal was (I believe) to show that universes are unnecessary to category theory, I think the stronger version of his theory that does involve a universe is actually a more comfortable place to work.

Posted at November 30, 2009 5:49 AM UTC

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

74 Comments & 0 Trackbacks

Re: Feferman Set Theory

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

Thanks for your efforts, Mike.

It would be nice if we could express this in a structural context such as ETCS by introducing to that an axiom along the lines: there is a category $Set_U$ internal to $SET$ such that suitable statements about $Set_U$ hold also for $SET$ .

Posted by: Urs Schreiber on November 30, 2009 9:00 AM | Permalink | Reply to this

Re: Feferman Set Theory

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

It would be nice if we could express this in a structural context

Yes, that’s easy to do. I didn’t mention it because I wanted to make this post accessible to dyed-in-the-wool materialists as well. (-:

There do seem to be a few problems with making it intuitionistic (and hence topos-meaningful), though. In ZF, the replacement schema implies a certain finitary reflection schema, which is what proves the relative consistency of ZFC/S. However, in intuitionistic logic, it appears that even the strong collection schema is insufficient to imply a similar reflection schema, so “IZF/S” may not be conservative over IZF. (I haven’t seen an actual proof of independence of reflection over IZF, but I don’t know the literature of IZF all that well.)

On the other hand, Zermelo set theory plus the finitary reflection schema implies the replacement schema and hence is equivalent to full ZF, and I believe that that is still true intuitionistically. So perhaps the finitary reflection schema is really a better thing to assume in the axioms of IZF. I’ve been feeling the lack of that reflection schema in other places as well.

Posted by: Mike Shulman on November 30, 2009 4:56 PM | Permalink | PGP Sig | Reply to this

Re: Feferman Set Theory

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

Fascinating stuff!

But I still think it’s depressing that we might need to resort to an axiom schema to prove that the product of two small groups in the category of small groups is also their product in the category of all groups. It’s sort of like admitting that we’re hopelessly befuddled by this size issue and need a deus ex machina to save us.

But… how often does this actually occur? Surely we can prove that $\mathbb{Z}/6$ is the product of $\mathbb{Z}/2$ and $\mathbb{Z}/3$ without resorting to this axiom schema. What’s the simplest, or practical, situation where this schema is needed?

I guess I should read your paper. Hmm, it’s surprisingly readable and fun! But maybe you can mention a place where the ‘working mathematician’ might need Feferman’s schema.

Posted by: John Baez on November 30, 2009 5:12 PM | Permalink | Reply to this

Re: Feferman Set Theory

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

I’ll write more later, but what have you got against axiom schemas? (-:

Posted by: Mike Shulman on November 30, 2009 5:21 PM | Permalink | PGP Sig | Reply to this

Re: Feferman Set Theory

I don’t have anything against axiom schemas, but this particular one really smells like what programmers would call a ‘patch’ or ‘bug fix’.

Posted by: John Baez on November 30, 2009 7:22 PM | Permalink | Reply to this

Re: Feferman Set Theory

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

this particular one really smells like what programmers would call a ‘patch’ or ‘bug fix’.

I’d call that a ‘hack’. Patches (or bug fixes) are good—they correct mistakes you made, like fixing a hole in a proof. It’s embarrassing to have to admit you made the mistake, but good to fix it. Hacks are approaches that do the job, but without any regard for elegance, consistency with the style elsewhere, or the likelihood that people will want to extend the basic idea to other cases in the future. Also, hacks are likely to stop working if any of the background assumptions change, but often the technical nature of the hack means it won’t be obvious that this is going to happen until it does (which I don’t think applies to this case.)

Posted by: Tim Silverman on November 30, 2009 8:01 PM | Permalink | Reply to this

Re: Feferman Set Theory

Thanks for the clarification — though as Mike pointed out, ‘kludge’ might be even more accurate.

I have a Windows Vista laptop, and every week Microsoft sends me megabytes of ‘patches’, and I can’t help but feel there’s something annoying about this. So I guess I was sloppily blurring the distinction between a suboptimal initial setup, and the desperate ‘patches’ with which one might try to save this setup without tossing it and starting all over. I think ‘universes’ fit into the former category, while ‘strong Feferman set theory’ fits into the latter.

Posted by: John Baez on December 2, 2009 3:41 AM | Permalink | Reply to this

Re: Feferman Set Theory

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

John said:

I have a Windows Vista laptop

I think the “hack” vs “kludge” thing might be a difference between British and American English. “Kludge” sounds very American to me, and, living in Britain, I’ve never heard anyone use “hack” in an approving way. (Some hacks are clever in a certain sense, but it’s more the ingenuity of a Heath-Robinson (American: Rube Goldberg) device than something you’d want to emulate).

One consequence of hacking something is that it tends to go wrong whenever anything else changes, resulting in the need for frequent patches! And the patches may themselves be hacks, meaning you end up needing to patch the patches. Much better to do it properly the first time.

There seems to me to be a close similarity between, on the one hand, the process of getting an “elegant” software solution where the software structures and processes closely match the conceptual organisation of the real-world domain that they’re supposed to be supporting and, on the other hand, the aim of getting “natural” definitions in a new area of mathematics, where the formalisation accurately captures the intuitions or phenomena it’s supposed to be formalising. (Maybe this comment should be in the “emotions” thread.)

Posted by: Tim Silverman on December 2, 2009 12:50 PM | Permalink | Reply to this

Re: Feferman Set Theory

“Hacking” in an approving sense has all but faded out, but I guess it comes from the original self-described hackers going back to the fifties and early sixties. The first definition of “hacker” given in the Dictionary of Computer Terms by Downing and Covington is “an exceptionally skilled computer programmer”, with connotations of elegant wizardry. Here is Jeremy Bernstein in his review of Steven Levy’s book The Hackers: Heroes of the Computer Revolution (from Bernstein’s Cranks, Quarks, and the Cosmos):

The use of the terms hack, hacking and hacker in the sense of Levy’s book seems to have developed at MIT in the 10950s. It is difficult to give an entirely precise definition of what a hack is. It is more than a “trick.” It is a very elegant way of doing something – solving something – that a priori might seem undoable or unsolvable or even uncreatable. The German word witz conveys the same idea, if one happens to know German. A person who is able to hack consistently comes to be regarded as a hacker. I see it as a designation with broad applications. Glenn Gould and Duke Ellington were hackers, as was Mozart. Beethoven wasn’t. Nabokov and Thomas Pynchon were and are hackers. Socrates was and Aristotle wasn’t. Kant certainly wasn’t. As my friend Marvin Minsky, who was regarded by a whole generation of MIT students as the king of the computer hackers, once noted, “If you do enough hacking you often get something profound.” This was certainly true of Mozart.

Bill Gosper, also a self-described hacker, opines that the later connotation of “hacker” as a malicious person who breaks into computer systems and damages them may be due to certain self-styled security experts who were around when non-malicious persons breached a computer system, simply to demonstrate that the system wasn’t secure, and would cry, “Look, hackers!” to create a sensation and employment for themselves.

Posted by: Todd Trimble on December 2, 2009 2:53 PM | Permalink | Reply to this

Re: Feferman Set Theory

If you work on a big software system like Windows you have to anticipate that your code will have a lifespan somewhere between 5 and 30 years, so it is absolutly essential that other people can understand it and add features (or bugfixes).
In this context a “hack” could be a quick and dirty solution, as has been explained already, or a “hack” could be an extremly ingenious solution that drives the successors if it’s inventor nuts because no one can understand it.
I’ve witnessed that a collegue deleted code worthy months of work, of another programmer who had left the company, and started from scratch, because he was able to convince the managemenent that it was impossible to understand that code and therefore impossible to add any features to it.
So “(s)he is a hacker” could be meant as a warning, like “(s)he is extremly brilliant but does not care if anyone understands what (s)he does, so you better make sure that you do understand it - pin her resp. him down and make her resp. him explain it to you if you must - before (s)he leaves!”.

Sorry if this is off topic, but somehow I got the impression that the phrase “(s)he is a hacker!” with this connotation could be of use to you in your everyday life.

Posted by: Tim vB on December 2, 2009 3:37 PM | Permalink | Reply to this

Re: Feferman Set Theory

a “hack” could be an extremly ingenious solution that drives the successors [of] [its] inventor nuts because no one can understand it.

A choice example in this latter vein for a math group is John Carmack’s inverse square root function, including the “magic number” 0x5F3759DF.

Posted by: John Armstrong on December 2, 2009 4:27 PM | Permalink | Reply to this

Re: Feferman Set Theory

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

Dixit John Armstrong, in reply to Tim vB:

a “hack” could be an extremly ingenious solution that drives the successors [of] [its] inventor nuts because no one can understand it.

A choice example in this latter vein for a math group is John Carmack’s inverse square root function, including the “magic number” 0x5F3759DF.

Ah yes, I forgot to mention that one place hacks can be justified is in optimisation (e.g. for speed) where you need to be tied to the technical details of the calculation more than to its conceptual framework. To some extent, this mirrors the tension in mathematics between definitions that are easy to understand, and definitions that are easy to use for calculating things with.

Posted by: Tim Silverman on December 2, 2009 4:59 PM | Permalink | Reply to this

Re: Feferman Set Theory

Well if we’re going into definitions, I think the appropriate reference for once is not the OED, but ESR’s Jargon File.

Hack (in relevant part):

1. n. Originally, a quick job that produces what is needed, but not well.
2. n. An incredibly good, and perhaps very time-consuming, piece of work that produces exactly what is needed.

Hacker:

1. A person who enjoys exploring the details of programmable systems and how to stretch their capabilities, as opposed to most users, who prefer to learn only the minimum necessary. RFC1392, the Internet Users’ Glossary, usefully amplifies this as: A person who delights in having an intimate understanding of the internal workings of a system, computers and computer networks in particular.
2. One who programs enthusiastically (even obsessively) or who enjoys programming rather than just theorizing about programming.
3. A person capable of appreciating hack value.
4. A person who is good at programming quickly.
5. An expert at a particular program, or one who frequently does work using it or on it; as in ‘a Unix hacker’. (Definitions 1 through 5 are correlated, and people who fit them congregate.)
6. An expert or enthusiast of any kind. One might be an astronomy hacker, for example.
7. One who enjoys the intellectual challenge of creatively overcoming or circumventing limitations.
8. [deprecated] A malicious meddler who tries to discover sensitive information by poking around. Hence password hacker, network hacker. The correct term for this sense is cracker.
The term ‘hacker’ also tends to connote membership in the global community defined by the net (see the network. For discussion of some of the basics of this culture, see the How To Become A Hacker FAQ. It also implies that the person described is seen to subscribe to some version of the hacker ethic (see hacker ethic).
It is better to be described as a hacker by others than to describe oneself that way. Hackers consider themselves something of an elite (a meritocracy based on ability), though one to which new members are gladly welcome. There is thus a certain ego satisfaction to be had in identifying yourself as a hacker (but if you claim to be one and are not, you’ll quickly be labeled bogus). See also geek, wannabee.
This term seems to have been first adopted as a badge in the 1960s by the hacker culture surrounding TMRC and the MIT AI Lab. We have a report that it was used in a sense close to this entry’s by teenage radio hams and electronics tinkerers in the mid-1950s.

Posted by: John Armstrong on December 2, 2009 4:22 PM | Permalink | Reply to this

Re: Feferman Set Theory

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

this particular one really smells like what programmers would call a ‘patch’ or ‘bug fix’.

I’m surprised to hear you say that. Are there other people reading who feel the same way?

To me, it feels very convenient and natural. What I would like most is to have a set of all sets, so that the category of all sets would be small and we wouldn’t ever have to worry about size. Unfortunately, that’s impossible, but Feferman set theory gives us the next best thing: a set that might as well be the set of all sets, in terms of what you can prove about it.

Posted by: Mike Shulman on November 30, 2009 8:18 PM | Permalink | PGP Sig | Reply to this

Re: Feferman Set Theory

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

but Feferman set theory gives us the next best thing

Maybe what might make it feel unsatisfactory is that the way Feferman theory “gives” this thing is by effectively postulating it.

That’s one reason I was thinking of the structural version. The reformulation: “The category $SET$ is such that it admits an internal category $Set_U$ inside $SET$ that looks effectively like all of $SET$ .” makes the same postulate sound maybe like a more natural desireatum.

Posted by: Urs Schreiber on November 30, 2009 9:14 PM | Permalink | Reply to this

Re: Feferman Set Theory

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

If “The category $SET$ is such that it admits an internal category $Set_U$ inside $SET$ that looks effectively like all of $SET$ ” seems more natural to you than “The class $V$ of all sets is such that it admits a set of sets $U$ inside $V$ that looks effectively like all of $V$ ,” then that’s great. To me they say basically the same thing, although of course I prefer structural axioms for other reasons.

Maybe what might make it feel unsatisfactory is that the way Feferman theory “gives” this thing is by effectively postulating it.

As opposed to all the other axioms of set theory (including Grothendieck’s axiom of universes), which give us things that we want by… postulating them? (-: Sorry if that sounds glib, but I don’t understand the difference.

Posted by: Mike Shulman on November 30, 2009 9:38 PM | Permalink | PGP Sig | Reply to this

Re: Feferman Set Theory

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

If “The category $SET$ is such that it admits an internal category $Set_U$ inside $SET$ that looks effectively like all of $SET$ seems more natural to you than “The class $V$ of all sets is such that it admits a set of sets $U$ inside $V$ that looks effectively like all of $V$ ,” then that’s great.

Yes, it does. I take comfort in the idea (the way I learned it originally from Todd) of how $SET$ is something primordial to mathematics that we all understand by grace, due to its relational nature, with all formal mathematics taking place inside it.

This doesn’t work with “the class of all sets” as well for me, as that seems to always beg the question of what the context is that this lives in.

But I agree that I am being very subjective here.

As opposed to all the other axioms of set theory (including Grothendieck’s axiom of universes), which give us things that we want by… postulating them?

Well, sure. I guess the point is to emphasize here the difference between solving a problem and realizing that a given problem was a wrong wall to bang one’s head against.

Posted by: Urs Schreiber on November 30, 2009 10:27 PM | Permalink | Reply to this

Re: Feferman Set Theory

Sorry if that sounds glib, but I don’t understand the difference.

The problem, to me, is that there isn’t much of a difference. You’ve gone from one form of postulation to another, and they both look like hacks. It doesn’t feel worse, but it doesn’t feel particularly better, either.

Posted by: John Armstrong on November 30, 2009 11:26 PM | Permalink | Reply to this

Re: Feferman Set Theory

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

Urs wrote:

Maybe what might make it feel unsatisfactory is that the way Feferman theory “gives” this thing is by effectively postulating it.

Mike wrote:

As opposed to all the other axioms of set theory (including Grothendieck’s axiom of universes), which give us things that we want by… postulating them? (-: Sorry if that sounds glib, but I don’t understand the difference.

There’s a difference between an axiom you throw in because it formalizes an insight, and one you throw in because you get stuck and you don’t know what else to do. It’s like the difference between swimming because you know how and enjoy it, and thrashing around because you’ve fallen into the pool and you’ll drown if you don’t do something.

All the attempts to deal with Russell’s paradox that I’ve seen feel like thrashing around to keep from drowning. This includes the axiom of universes as well as Feferman set theory.

But perhaps because of the way you motivated it, Feferman set theory seems particularly desperate. “Okay, I’ve got all these universes… but darn it, if I prove something in one universe I still don’t know if it’s true in a larger universe. Hmm. I know! I’ll throw in an axiom schema that says it is!”

I don’t know any good way to deal with Russell’s paradox, but I believe there is one. I believe someday we’ll find it. But I don’t think we’ll find it by trying to ‘weasel out’ of the problem. Somehow we need to think a new way — a clearer way, that makes the paradox just disappear.

Posted by: John Baez on December 1, 2009 3:15 AM | Permalink | Reply to this

Re: Feferman Set Theory

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

At an informal level, I feel that I have Russell’s paradox licked. Doubtless someone will now patiently tell me why I haven’t really got it licked, causing that pleasant feeling to disappear. Oh well; let’s try it.

I’ve pretty much entirely moved over to a point of view in which it doesn’t make sense to ask of any two sets $A$ and $B$ the question ‘is $A \in B$ ?’ For example, I don’t think it makes sense to ask whether $\emptyset \in \mathbb{Q}$ . And once you’ve adopted this point of view, the ‘paradox’ dissolves.

Now, some people will agree with this point of view and some will disagree, but let’s put that discussion to one side for the moment. The point I want to make is that this is a systematic, coherent viewpoint. It’s got historical roots in Cantor’s original work. It’s got mathematical roots in Lawvere’s categorical set theory. And, in my opinion, it more accurately reflects ‘sets’ as used by most mathematicans than the kind of set theory where you can always ask ‘is $A \in B$ ?’

It’s emphatically not ‘thrashing around’, and has absolutely no need to be motivated as a reaction to Russell’s paradox. It’s swimming because you want to, and know how to do it well.

Posted by: Tom Leinster on December 1, 2009 4:07 AM | Permalink | Reply to this

Re: Feferman Set Theory

Russell’s paradox is for this reason something of a red herring, or perhaps the expression is merely a rubric for something else. To me the structural point is more along the lines of Cantor’s theorem, that a set cannot map onto its power set. This has all sorts of consequences, such as Freyd’s theorem that a complete category (where ‘complete’ is unqualified by a smallness condition of some sort) is a poset, or that there is no initial algebra for the covariant power set functor.

Of course you know all this. I’m just sayin’.

Posted by: Todd Trimble on December 1, 2009 12:30 PM | Permalink | Reply to this

Re: Feferman Set Theory

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

I’ve pretty much entirely moved over to a point of view in which it doesn’t make sense to ask of any two sets $A$ and $B$ the question “is $A \in B$ ?”

That is, by the way, the structural set theory viewpoint that Mike and I talk about above.

One pleasant aspect of this is that the category of all sets – and thus with its collection of objects the collection of all sets – happily lives as the ETCS $SET$ .

But that doesn’t mean that considerations of universe objects inside $SET$ and considerations along the lines here becomes superfluous.

Posted by: Urs Schreiber on December 1, 2009 7:49 AM | Permalink | Reply to this

Re: Feferman Set Theory

I don’t know any good way to deal with Russell’s paradox, but I believe there is one. I believe someday we’ll find it. But I don’t think we’ll find it by trying to ‘weasel out’ of the problem. Somehow we need to think a new way — a clearer way, that makes the paradox just disappear.

Just trying to use an appropriate smiley swim

Posted by: J-L Delatre on December 1, 2009 3:00 PM | Permalink | Reply to this

Re: Feferman Set Theory

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

Tom wrote:

At an informal level, I feel that I have Russell’s paradox licked. Doubtless someone will now patiently tell me why I haven’t really got it licked, causing that pleasant feeling to disappear. Oh well; let’s try it.

Okay…

I’ve pretty much entirely moved over to a point of view in which it doesn’t make sense to ask of any two sets $A$ and $B$ the question ‘is $A \in B$ ?’ For example, I don’t think it makes sense to ask whether $\emptyset \in \mathbb{Q}$ .

I agree with that wholeheartedly. A bit more precisely, I think it’s better to work in a setup where it’s impossible to ask this question.

And once you’ve adopted this point of view, the ‘paradox’ dissolves.

Well, Russell’s paradox in its original form dissolves, but I’m not sure the underlying problem is gone. Let’s talk about this!

Todd wrote:

Russell’s paradox is for this reason something of a red herring, or perhaps the expression is merely a rubric for something else.

Yeah, I was being sloppy. But the term ‘rubric’ sounds more dignified, so thanks.

I’ll say some stuff you know… and then I’ll ask you some questions.

I think of Russell’s paradox as an early manifestation of the fact that you can get in real trouble trying to talk about ‘the thing of all things’ — to treat the totality of mathematical entities as a mathematical entity in itself.

Maybe this is a naive understanding of what the real problem is! But there’s a lump in the carpet somewhere around here, and I get the feeling that people have been pushing the lump around removing it. Presumably removing it requires lifting up the sofa, which is a lot of work.

It’s often fun to look at early naive attempts to solve deep problems, because you can really see people openly thrashing around — while later more sophisticated attempts occasionally resemble someone pretending to be swimming while actually struggling to keep from drowning.

So, it’s fun to look at Russell and Whitehead’s theory of ramified types. I don’t know much about it! Most people just say it was a fiasco and leave it at that. But there’s a nice sketch on PlanetMath. And they describe how Russell and Whitehead developed this hierarchy where “predicates of degree 1 apply only to objects, predicates of degree 2 apply to predicates of degree 1, and so forth.” And then predicates got stratified by ‘levels’ where “At the first level of degree $n+1$ one has predicates that apply to elements of degree $n$ and which can be defined with reference only to predicates of degree $n$ . At second level there appear all the predicates that can be defined with reference to predicates of degree $n$ and to predicates of degree $n+1$ of level 1, and so forth.”

But then they got stuck in difficulties and imposed the ‘axiom of reducibility’, which states that if a predicate of degree $n$ occurs at some level $k$ , it occurs already on the first level.”

I’m not saying it’s technically the same, but it smells like Feferman set theory, where — according to Mike “To ZFC (or your favorite set theory) we add a constant symbol $U$ together with the axiom ‘ $U$ is a universe,’ and also an axiom schema stating that for any statement $\phi$ , all of whose parameters are in $U$ but which does not mention $U$ explicitly, we have $\phi^U \iff \phi$ .” First we build up a big hierarchy and then we get fed up with it and add an axiom that says we don’t need to worry about it.

Anyway, let’s flash forwards and say we work in some structural approach to set theory like ETCS.

(I don’t know anything about about ETCS, by the way! I’m opinionated about foundations, but largely ignorant. I think this is okay though, since my opinion is mainly that people should try all sorts of foundations and see what happens. I certainly don’t have some favorite approach that I think is ‘right’.)

This approach incorporates Tom’s insight that we shouldn’t be allowed to just grab two sets off the rack and ask if one is a member of another.

But apparently the difficulties with the ‘thing of all things’ aren’t gone. Right?

Can I talk about the category of all categories? If I prove a theorem about categories, does it apply to the category of all categories? Or do I have to play universe games to deal with these issues?

Todd writes:

To me the structural point is more along the lines of Cantor’s theorem, that a set cannot map onto its power set. This has all sorts of consequences, such as Freyd’s theorem that a complete category (where ‘complete’ is unqualified by a smallness condition of some sort) is a poset, or that there is no initial algebra for the covariant power set functor.

That’s an interesting way of putting it, because I don’t tend to think of Cantor’s theorem as a ‘problem’… while I tend to think of needing nested universes as a ‘problem’, reflecting some defect in our understanding. Maybe my attitude is wrong.

And maybe I’ve never thought about any of this stuff hard enough. Instead, like most mathematicians, I shy away from it! I guess the only place where these size issues ever affects me personally is when I want to talk about the ‘space of all spaces’, i.e. the geometric realization of the nerve of the topological groupoid of all spaces. It’s a very useful space — in certain conceptual ways — and I find it a blemish on the beauty of this idea to talk about the ‘large space of all small spaces’. But I can live with it.

Posted by: John Baez on December 1, 2009 6:43 PM | Permalink | Reply to this

Re: Feferman Set Theory

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

But apparently the difficulties with the ‘thing of all things’ aren’t gone. Right?

Yes, that’s right. ETCS requires universe games just as much as ZFC.

There are three paradoxes of naive set theory:

Russell’s paradox: the set $\{x | x\notin x\}$ is contradictory.
Cantor’s paradox: for any set $A$ , its power set $P A$ is not a subquotient of $A$ ; but if $A$ were a set of all sets, then $P A \subseteq A$ .
Burali-Forti’s paradox: no well-ordered set can be isomorphic to an initial segment of itself; but if $\Omega$ were the set of all well-orders, then it would itself be well-ordered, hence isomorphic to an element of itself, and hence isomorphic to an initial segment of itself.

The first is an artifact of material set theory where the global membership predicate $\in$ applies to all sets. The second and third, however, are just as problematic in structural set theory. You just have to interpret “the set of all sets” as “a family of sets such that every set is isomorphic to one in this family” and likewise for “the set of all well-orders.”

Posted by: Mike Shulman on December 1, 2009 6:55 PM | Permalink | PGP Sig | Reply to this

Re: Feferman Set Theory

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

As another data point, type theories are more on the structural side of things, but having $Type : Type$ allows you to encode Girard’s paradox, which, if I recall correctly, is a related to the Burali-Forti paradox. Russel’s paradox, however, typically can’t be encoded very directly.

The trend in type theories as far as computer science goes seems to be along the lines of the ramified hierarchy. Instead of $Type : Type$ one has $Type_i : Type_{i + 1}$ , possibly with some additional fanciness. Of course, this leads to a problem related (I think) to the math above: datatype/function/etc. definitions may make sense at any point in the hierarchy, but each definition is restricted to particular universes. For instance (in Agda):

data List (A : Set) : Set where [] : List A _::_ : A -> List A -> List A

data List1 (A : Set1) : Set1 where [] : List1 A _::_ : A -> List1 A -> List1 A

The above are clearly identical except for the Sets replaced with Set1s. One way out of this is to try to add universe polymorphism to the language, where definitions can be parameterized by a universe level. Then we might be able to write:

data List {n} (A : Set n) : Set n where [] : List A _::_ : A -> List A -> List A

And instantiate the definition at whatever level we need. Perhaps this solution doesn’t have similar appeal on the mathematical end, though (and I don’t think I’d call it a settled issue on the programming-with-theorem-proving language design end, either).

As an unrelated aside, one unique solution to Russel’s paradox I’ve seen is to restrict certain segements of set theory to use linear logic without the modalities that let you encode classical statements. One can then work with an unrestricted comprehension schema, which will let one define Russel’s paradoxical set, but, it doesn’t explode, because the proof of a contradiction from the set requires using it as a premise twice, which is not allowed in the particular fragment of linear logic. I’m not sure if such a restriction prevents other paradoxes, and such a restricted logic may be too… restrictive for it to be useful. But I think it’s an interesting result (I suppose paraconsistent logics in general are a potential “solution” to set theoretic paradoxes). A paper that explains it better than I could can be found here.

Posted by: Dan Doel on December 1, 2009 9:19 PM | Permalink | Reply to this

Re: Feferman Set Theory

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

There’s a difference between an axiom you throw in because it formalizes an insight, and one you throw in because you get stuck and you don’t know what else to do.

I emphatically see Feferman set theory as formalizing an insight, namely that large collections behave just like small ones (but there is a difference between the two). I guess I should have emphasized this more. The audience I had in mind when writing this post was people who like universes and don’t know why they should consider anything else. I didn’t realize there was all this antipathy towards universes around here! I agree that universes feel like a hack, but Feferman set theory does not feel like a hack to me, because of that essential insight.

I also don’t think it’s fair to criticize Feferman set theory on the grounds that it isn’t an evil-free world. It’s a set theory, so you should instead be comparing it to other set theories, like ZFC, NBG, and Grothendieck universes. I don’t think the above insight depends on the fact that it’s a theory of sets rather than a theory of categories or $\infty$ -categories; in the latter it would just be formulated as “large ( $\infty$ -)categories behave just like small ones.” In fact, it seems to me possible, and even likely, that reflection principles will still turn out to be useful and important in higher-categorical foundations.

In particular, it’s by no means clear to me that higher-categorical foundations, all by themselves, will be helpful in resolving Cantor’s paradox. (I agree with Todd that Russell’s paradox is an artifact of material set theory; the real problems with a set of all sets are Cantor’s paradox and Burali-Forti’s paradox.) My experience playing with the idea of a category of all sets leads me to believe that the “ $\infty$ -category of all $\infty$ -categories” will have just as many problems as the set of all sets.

Posted by: Mike Shulman on December 1, 2009 6:44 PM | Permalink | PGP Sig | Reply to this

Re: Feferman Set Theory

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

Mike wrote:

I emphatically see Feferman set theory as formalizing an insight, namely that large collections behave just like small ones (but there is a difference between the two).

Okay. To me this feels more like a hack than an insight. We got in trouble, and to escape it we made up this distinction between large and small collections. But we’re not really interested in this distinction except insofar as it keeps us out of trouble! So we add a footnote saying “don’t worry about this distinction: if you can prove something for small collections, it’ll still hold for large ones — unless there’s some obvious reason why it shouldn’t.”

It reminds me of one of the White Knight’s inventions:

But I was thinking of a plan
To dye one’s whiskers green,
And always use so large a fan
That they could not be seen.

But since I don’t have a better proposal, all I can do is whinge from the sidelines, and urge people to keep trying lots of ideas!

I also don’t think it’s fair to criticize Feferman set theory on the grounds that it isn’t an evil-free world.

I agree. If you look carefully, you’ll see I’m not doing that. For example, your link above points to a comment where I was trying to help Urs guess what Beilinson meant by saying “Arguably, the common language of category theory may be inadequate for describing the homotopy world.” This has nothing to do with Feferman set theory!

My experience playing with the idea of a category of all sets leads me to believe that the “ $infty$ -category of all $\infty$ -categories” will have just as many problems as the set of all sets.

Perhaps! Do you know if Makkai confronts this issue? He’s the only one I know who has seriously tried a foundation of math based on $\infty$ -categories.

I’m fond of this idea, but I have no idea if it helps:

You should not be allowed to talk about the set of all sets — only the category of all sets. You should not be allowed to talk about the category of all categories — only the 2-category of all categories. And so on.

If we stop here — right after ‘and so on’ — do we succeed in avoiding problems akin to those of the set of all sets? That would be cool.

Unfortunately, nobody (not even me) seems satisfied to stop here: they all want to go straight to $\omega$ -categories, and the $\omega$ -category of all $\omega$ -categories. And then we’re right back to talking about the ‘thing of all things’.

Is there some interesting meaning to the ‘ $(\omega + 1)$ -category of all $\omega$ -categories’?

Posted by: John Baez on December 1, 2009 7:10 PM | Permalink | Reply to this

Re: Feferman Set Theory

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

To me this feels more like a hack than an insight. We got in trouble, and to escape it we made up this distinction between large and small collections.

It sounds like what you really mean is that the whole notion of a distinction between small and large is a hack. (I observe in passing that hack can also mean the opposite of what you intend; perhaps an even better word would be kludge.) I’m not sure where I stand on that question. What I’m saying is rather that if we assume that a distinction between small and large has to be made, then Feferman set theory is an elegant way of dealing with (some might say “minimizing” or “allowing us to ignore”) that distinction.

your link above points to a comment where I was trying to help Urs guess what Beilinson meant by saying “Arguably, the common language of category theory may be inadequate for describing the homotopy world.” This has nothing to do with Feferman set theory!

That comment also included the statement “I think that for real improvements in the foundations of mathematics — as opposed to hacks — we need to try really radical new ideas.” I interpreted that as a reference to Feferman set theory since that’s what you’d previously been calling a hack, but maybe that was unjustified.

You should not be allowed to talk about the set of all sets — only the category of all sets. You should not be allowed to talk about the category of all categories — only the 2-category of all categories. And so on.

If we stop here — right after ‘and so on’ — do we succeed in avoiding problems akin to those of the set of all sets? That would be cool.

It depends on whether you insist that every discrete category is a set. If not, then what you’ve got is basically a non-evil-ified version of an infinite sequence of universes $U_1\in U_2\in \dots$ , and this certainly avoids the problems.

However, if you insist that “set” means the same thing as “discrete category,” then the question is somewhat murkier. I played around with it a bit here. It turns out that if you additionally assume that functor categories exist, and that either (i) power sets exist, or (ii) opposite categories exist, or (iii) every category has a core, or (iv) the law of excluded middle holds, then you can reproduce Cantor’s paradox. I don’t know whether there are problems if you don’t have functor categories, but it’s worth pointing out that even a set of all sets is possible if you don’t have function sets: the pretopos of finite-or-countable sets contains a universal family.

Posted by: Mike Shulman on December 1, 2009 8:12 PM | Permalink | PGP Sig | Reply to this

Re: Feferman Set Theory

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

Mike wrote:

It sounds like what you really mean is that the whole notion of a distinction between small and large is a hack.

Well, it feels like a hack to me. I could be wrong. But I think that moving beyond the usual ideas on this distinction — in some good way, some way that makes perfect sense in retrospect — might have the potential to really change our outlook on foundations. So, I want to encourage discontent with the current approaches to this issue, in hopes that some smart person will have a good idea.

What I’m saying is rather that if we assume that a distinction between small and large has to be made, then Feferman set theory is an elegant way of dealing with (some might say “minimizing” or “allowing us to ignore”) that distinction.

I agree with that!

But — in math, at least — I have a certain distaste for ‘elegant tricks that minimize the damage caused by previous bad design decisions’. You could argue that they’re better than inelegant tricks. But in some ways they’re even worse: they do a better job of lulling us into complacency and keeping us from inventing radical new improvements.

Anyway, I think I’ve made my point. I don’t want to overdo it. I’m very glad you explained this idea of Feferman! I’d never heard of it. And it’s great that we’re getting more blog entries on foundational issues, now that you’re on the team.

(I bet a lot of people around here would like to hear more about ‘structural foundations’ and/or topos theory, especially if it’s explained in a way that non-logicians can easily follow.)

Posted by: John Baez on December 2, 2009 5:55 AM | Permalink | Reply to this

Re: Feferman Set Theory

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

[The distinction between small and large] feels like a hack to me. I could be wrong.

As I said, I’m not sure where I stand on this. I’m fine with encouraging discontent in hopes that someone will come up with something better, but I also think that until and unless that someone arrives, we should use the best approach we currently have. For one thing, there might not be anything better out there to be found.

I have a certain distaste for ‘elegant tricks that minimize the damage caused by previous bad design decisions’.

I won’t disagree with that in general. But I don’t think it’s quite fair to call a design decision “bad” until you have something better to propose! If a bad-looking design decision is, in fact, unavoidable, then we shouldn’t let our distaste for it prevent us from using elegant tricks to minimize the damage it does.

(I bet a lot of people around here would like to hear more about ‘structural foundations’ and/or topos theory, especially if it’s explained in a way that non-logicians can easily follow.)

Yeah, the post “Syntax, Semantics, and Structuralism II” is sitting half-written on my hard drive. I’ll get around to it soon; I just keep finding other things that I want to post about more urgently. (-:

Posted by: Mike Shulman on December 2, 2009 6:46 AM | Permalink | PGP Sig | Reply to this

Re: Feferman Set Theory

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

I apologize if this was mentioned already. I just wanted to point out the Reflection Principle for ZF http://en.wikipedia.org/wiki/Reflection_principle. From this point of view, already in ZF you find that whatever you want to prove you only have to prove in some “small” universe. Also, ZF can be axiomatized using Reflection,

\Delta_0

-specification, Foundation and Extension. I think this is why Reflection Axioms are considered natural (cf. the references on wikipedia, especially Marshall’s article).

Posted by: Peter Krautzberger on December 8, 2009 10:27 AM | Permalink | Reply to this

Re: Feferman Set Theory

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

I did mention the reflection principle of ZF up here, along with the fact that it can serve as an alternate axiomatization of ZF. (But you can certainly be forgiven for not finding that in these meandering comments!) Of course, the reflection principle of ZF is how one proves that Feferman set theory is conservative over ZF. ZF-theorists are generally quite comfortable to use the reflection principle of ZF whenever necessary, and category theorists could certainly do the same thing. I think Feferman’s idea was that by introducing it as a schema with a fixed universe $U$ (rather than having to choose a new $U$ for every proof) would make the axiom system feel more comfortable.

On the other hand, I would initially regard the fact that the proof doesn’t seem to work intuitionistically (does it?) as evidence against the “naturality” of reflection principles. Unless, of course, we have an intrinsic justification for reflection principles, which I think is quite reasonable. Then the failure of the proof is just telling us that we chose the wrong axiomatization of ZF when making it intuitionistic; we should have chosen a reflection principle instead.

Posted by: Mike Shulman on December 8, 2009 4:02 PM | Permalink | PGP Sig | Reply to this

Re: Feferman Set Theory

Thank you for the link. The discussion is very interesting to read even for a dilettante like myself.

Posted by: Peter Krautzberger on December 8, 2009 9:17 PM | Permalink | Reply to this

Re: Feferman Set Theory

People working on intuitionistic type theory don't seem to mind using reflection principles, at least if they're not trying to keep the theory weak. At any rate, I see people talking about them when discussing Coq.

Posted by: Toby Bartels on December 9, 2009 3:24 AM | Permalink | Reply to this

Re: Feferman Set Theory

A comment by David Ben-Zvi in MO made me read in this article by Beilinson, which contains the puzzling remark “Arguably, the common language of category theory may be inadequate for describing the homotopy world.”(p.4). What do you think about that?

Posted by: Thomas on December 1, 2009 1:21 AM | Permalink | Reply to this

Re: Feferman Set Theory

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

I haven’t read the article, but there’s a clear sense in which categories are not sufficient for homotopy theory: we need $\infty$ -categories, or at the very least, $(\infty,1)$ -categories.

For example, homotopy theorists have known for a long time that pullbacks aren’t good enough for what they want to do. They need homotopy pullbacks. And so on. Until recently, this has been the major force driving the development of $\infty$ -categories.

Of course, we can use category theory as an infrastructure for $\infty$ -category theory… so there’s another sense in which category theory is enough to do homotopy theory. But this is a bit like saying that a stone hand-axe is enough to build a space ship. It lets you build the tools that let you build the tools that… let you build a space ship.

Posted by: John Baez on December 1, 2009 2:54 AM | Permalink | Reply to this

Re: Feferman Set Theory

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

Beilinson is quoted as writing:

Arguably, the common language of category theory may be inadequate for describing the homotopy world.

John replied:

I haven’t read the article, but there’s a clear sense in which categories are not sufficient for homotopy theory: we need ∞-categories, or at the very least, (∞,1)-categories.

Beilinson seems to mean to include higher category theory in his comment. The full quote from p. 4 is

Intuitively, a homotopy world is a kind of $\infty$ -category (see Remark below). Lopping off higher homotopies (i.e. replacing the clever localization by a stupid one), one gets a plain category - the homotopy category of the model category. This is a desolate place, where no interesting construcitons can be performed. The homotopy world is a (yet unnamed) animation of the homotopy category that hovers inbetween the latter and higher non-canonical model categories.

Remark In [Gr] Grothendieck suggested to perceive homotopy types as $\infty$ -groupoids ${}^6$ . Unfortunately, a simple intrinsic definition of the concept is not available. Arguably, the common language of category theory may be inadequate for describing the homotopy world. ${}^7$ .

That footnote 7, by the way, brings us back on topic here, it says:

A shade of this inadequacy presents already in plain category theory: while its force lies in the fact that one need not distinguish equivalent categories, it ostensibly asserts that for a (small) category its set of objects is a meaningful notion.

These statements leave me a bit puzzled, I have to say. Since a small category is defined to be one that, as opposed to a large category, has a set of objects, I don’t see which point the footnote means to make. And I am not sure I know what would count as “intrinsic” as far as definitions of $n$ -groupoids go.

Conversely, lately we witness everything is pointing in the direction that the vague “homotopy world” finds its precise natural home in higher category theory.

Posted by: Urs Schreiber on December 1, 2009 8:11 AM | Permalink | Reply to this

Re: Feferman Set Theory

Perhaps when he says “it ostensibly asserts that for a (small) category its set of objects is a meaningful notion”, Beilinson just means that “plain category theory” talks about the set of objects of a category in the extensional sense. This would allow us to ask bad questions, such as how many objects are isomorphic to a given one.

Posted by: David Corfield on December 1, 2009 8:44 AM | Permalink | Reply to this

Re: Feferman Set Theory

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

Oh, I see, he is pointing to the fact that the set of objects of a category is not a notion invariant up to equivalence.

Hm, but this is entirely analogous to saying that the set of points of a small topological space is not a notion invariant up to homotopy equivalence.

Posted by: Urs Schreiber on December 1, 2009 8:53 AM | Permalink | Reply to this

Re: Feferman Set Theory

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

Beilinson wrote:

… Grothendieck suggested to perceive homotopy types as ∞-groupoids Unfortunately, a simple intrinsic definition of the concept is not available.

I’m not sure what he means by a ‘simple intrinsic definition’. I find that Kan complexes provide a simple definition of ∞-groupoid. But is it intrinsic? Maybe he’s complaining that this definition is founded on set theory rather than developed ‘from scratch’. That might seem like an odd thing to complain about — after all, lots of math is founded on set theory! But he suggests why it might be bad in this case:

A shade of this inadequacy presents already in plain category theory: while its force lies in the fact that one need not distinguish equivalent categories, it ostensibly asserts that for a (small) category its set of objects is a meaningful notion.

I think I understand the dissatisfaction he’s expressing here. In the usual approach founded on set theory, a (small) category has a set of objects. This allows us to ask if two categories $C$ and $D$ are isomorphic: namely, if there are functors $F: C \to D$ , $G : D \to C$ that are bijections on objects and morphisms.

From the viewpoint of category theory, it’s evil to ask if categories are isomorphic! We should instead ask if they’re equivalent. A really ‘intrinsic’ approach to category theory, not founded on set theory, might prevent us from asking whether categories are isomorphic, by making the concept meaningless.

For this to work, a category would no longer have a set of objects, at least not in the usual sense.

I am fond of Makkai’s foundations of mathematics precisely because he tries to tackle this problem! It’s founded on the ∞-category of ∞-categories, and there is no concept of equality, just ‘equivalence’. All meaningful properties are invariant under equivalence.

This is very radical, so it will take a long time to catch on — if it ever does! Perhaps centuries.

However, I think that for real improvements in the foundations of mathematics — as opposed to hacks — we need to try really radical new ideas. And to me it makes sense that ultimately mathematics will be founded on ∞-categories, with sets appearing as a simple special case.

Posted by: John Baez on December 1, 2009 5:16 PM | Permalink | Reply to this

Re: Feferman Set Theory

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

I like Makkai’s general idea too. I am also intrigued by another, similar, possibility: using a form of intensional type theory (with “identity types”) as a model for $\infty$ -groupoids. Garner-van den Berg and Lumsdaine have independently shown that every object of intensional type theory naturally has the structure of a globular $\infty$ -groupoid. I believe that they and others are thinking right now about how to show that intensional type theory has a semantics valued in $(\infty,1)$ -categories. If this all works out well, then it may turn out that the very old notion of intensional type theory, invented by Martin-Löf and others for completely different purposes, turns out to be a good foundation for higher-categorical/homotopical mathematics without sets and without evil.

Posted by: Mike Shulman on December 1, 2009 6:39 PM | Permalink | PGP Sig | Reply to this

Re: Feferman Set Theory

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

There seem to be two different directions one can explore here, I think.

Firstly, there’s the direction you’re mentioning here that’s explored in the Makkai paper, and that seems to connect to intensional type theory.

Here we say “Hey! These things that we thought were sets — actually, they had identity types which we’d previously been ignoring, so they’re really groupoids! Hang on, no — they’re 2-groupoids! Oh — no, actually…” and so on ad infinitum. We never assume equality as a primitive, so the higher-categorical structure extends up arbitrarily far. So: our primitive “set-like” things are the objects of a (weak) $\omega$ -category. (In fact, we possibly want to make it $(\infinity,1)$ , but let’s leave that for now.) One way to look at this is as the natural upshot of really taking the Curry-Howard viewpoint seriously.

On the other hand, the way we usually look at universes seems to be digging down rather than building up. Or perhaps a better metaphor is that we’re zooming out, as opposed to zooming in. We say “OK, these sets are living as the 0-cells in a category of sets. No! — they’re 1-cells in the 2-category Cat! No! — they’re 2-cells in the 3-category 2-Cat…” So from where we started, we’re digging deeper and deeper down: this picture is something like an $\omega^\mathrm{op}$ -category, where there’s a highest level, but no bottom level. Everything lives inside some universe, but that universe is one level deeper in categorical dimension. Making this a weak $\omega^\mathrm{op}$ -category seems to then describe the “universes without evil” picture quite nicely. In many ways this is a less radical foundational idea than the first one — we still have good ol’ sets and simple equality of elements with equality at the highest “home” level — but I think it’s the one which more closely describes the way we tend to think of universes.

Of course, we could combine these two ideas and wonder about something like a $\Z$ -category with cells weakly invertible above dimension 0…

Posted by: Peter LeFanu Lumsdaine on December 6, 2009 4:46 AM | Permalink | Reply to this

Re: Feferman Set Theory

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

I don’t regard the first foundational idea as radical or as supplanting sets in any way. Rather than saying “these things we thought were sets are actually $\infty$ -groupoids,” I view it as saying “these things we’ve been calling sets are actually a very special type of $\infty$ -groupoid.” I don’t want to make sets any less set-like or get rid of their equality; what I would hope for is a theory of $\infty$ -groupoids that’s as easy to use as ordinary set theory is, and which would reduce to ordinary set theory when we restrict attention to the $\infty$ -groupoids in which all hom-spaces are empty or contractible.

I realize that’s not what the intensional type theorists are after, but I think one of the exciting things about that direction of research is that it could end up satisfying us both.

Now let me see if I understand your second proposal. We’re imagining a $\omega^{op}$ -category that has (say) 0-cells, $(-1)$ -cells, $(-2)$ -cells, and so on down, with each $k$ -cell having a $(k-1)$ -cell as its source and target as usual, and composition operations etc., whatever that means. We also have a particular chosen $k$ -cell for each negative integer $k$ ; call it $T_k$ and think of it as the point incarnated at that level. We assume that the source of $T_k$ is $T_{k-1}$ , and we give the target of $T_k$ the name $(k+1)Cat$ . Of course, since $(k+1)Cat$ must be parallel to $T_{k-1}$ , its source must be $T_{k-2}$ and its target must be $k Cat$ .

Now sets are defined to be $(-1)$ -cells from $T_{-2}$ to $Set = 0 Cat$ . The terminal set is $T_{-1}$ . An element of a set $X\colon T_{-2}\to Set$ is a 0-cell from $T_{-1}$ to $X$ . Since the only 1-cells are identities, we have a notion of equality for elements of a set. More generally, a function between sets is a 0-cell between them; again we have a notion of equality for these.

Likewise, categories are defined to be $(-2)$ -cells from $T_{-3}$ to $Cat = 1Cat$ . The terminal category is $T_{-2}$ . A functor between categories is a $(-1)$ -cell between them, and a transformation between those is a 0-cell between them. In particular, an object of a category $C$ is a $(-1)$ -cell from $T_{-2}$ to $C$ , and a morphism of $C$ is a 0-cell between objects. Note that $Set$ is a category, by definition, and that sets and functions, as defined above, are precisely the objects and morphisms of $Set$ .

More generally, $n$ -categories are defined to be $(-n-1)$ -cells from $T_{-n-2}$ to $n Cat$ , and the objects of an $n$ -category $C$ are the $(-n)$ -cells to it from $T_{-n-1}$ (the terminal $n$ -category). By definition, $(n+1)Cat$ is an $n$ -category, and its objects are, by definition, the $(n+1)$ -categories.

I think I like this, although all the negative-dimensional cells are kind of annoying. Maybe we should “re-grade everything cohomologically” so that $(-n)$ -morphisms are the same as $n$ -comorphisms.

Has anyone done serious work on the notions of $\omega^{op}$ -category and $\mathbb{Z}$ -category?

Posted by: Mike Shulman on December 6, 2009 5:34 AM | Permalink | PGP Sig | Reply to this

Re: Feferman Set Theory

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

(I’ll reply about the two different ideas separately.)

Rather than saying “these things we thought were sets are actually ∞-groupoids,” I view it as saying “these things we’ve been calling sets are actually a very special type of ∞-groupoid.” I don’t want to make sets any less set-like or get rid of their equality; what I would hope for is a theory of ∞-groupoids that’s as easy to use as ordinary set theory is, and which would reduce to ordinary set theory when we restrict attention to the ∞-groupoids in which all hom-spaces are empty or contractible.

I realize that’s not what the intensional type theorists are after, but I think one of the exciting things about that direction of research is that it could end up satisfying us both.

Hmmmm… Yes, I guess I was thinking of it differently from how you were. If I understand right, you’re describing sets as a class of special ∞-groupoids — so for you, Sets would be a subcategory of ∞-Gpds, as (the weakly essential image of?) the “discrete” inclusion. In the way you generally work with them in ITT, you take them as something like ∞-groupoids with all higher cells “considered as identities” — in other words, Sets is a quotient of ∞-Gpds, along the “connected components” functor. (You may also want to pass to “setoids”, i.e. take an exact completion of some sort, depending on your base type theory.)

Classically, these two viewpoints are of course perfectly compatible: these functors (and others too) exhibit Set as a retract of ∞-Gpds. My gut feeling is that the latter approach should adapt better to an ∞-categorical foundation — for instance, asking a hom-set to be contractible involves arbitrary high dimensions, and I’m not sure what kind of language you could work in that would let you talk about that internally (though of course you might not want do be able to do that anyway). But this seems like an interesting question, without an obvious right or wrong answer!

Posted by: Peter LeFanu Lumsdaine on December 6, 2009 6:18 AM | Permalink | Reply to this

Re: Feferman Set Theory

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

Classically, these two viewpoints are of course perfectly compatible: these functors (and others too) exhibit Set as a retract of ∞-Gpds.

Indeed – and not just a retract but a reflective subcategory. I think I’d be unsatisfied with an $\infty$ -categorical foundation that didn’t let me talk about both of those functors, although of course I might be compensated in other ways.

asking a hom-set to be contractible involves arbitrary high dimensions, and I’m not sure what kind of language you could work in that would let you talk about that internally

That is indeed a problem. But unless I’m mistaken, that sort of thing is going to come up all over the place if we want to actually work in an $\infty$ -categorical foundation. How do we express $\infty$ -categorical limits, adjunctions, coherent monoidal structures, etc. without some language that can talk about “all dimensions at once”?

Posted by: Mike Shulman on December 6, 2009 8:22 AM | Permalink | PGP Sig | Reply to this

Re: Feferman Set Theory

Good question! In the ITT framework you can only talk about finitely many dimensions at once, so in a sense, while a type may have infinitely high non-trivial structure, internally you can only work with it via its finite-dimensional approximations.

Having some basic properties defined by coinduction, as you suggest, seems like a nice way to talk about a restricted class of infinite-dimensional properties in a finite language.

Posted by: Peter LeFanu Lumsdaine on December 6, 2009 4:45 PM | Permalink | Reply to this

Re: Feferman Set Theory

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

One way that comes to mind to talk about contractibility is by coinduction. If $X$ is a contractible $\infty$ -groupoid, then (1) $X$ is inhabited, and (2) for any $x,y\in X$ , $hom_X(x,y)$ is contractible. Moreover, contractibility is maximal with this property in the following sense. Suppose $P$ is any property of $\infty$ -groupoids such that if $X$ has property $P$ , then (1) $X$ is inhabited and (2) for any $x,y\in X$ , $hom_X(x,y)$ has property $P$ . Then in fact $P\Rightarrow$ contractible. These finitary statements uniquely characterize the notion of contractibility, so I could imagine an $\infty$ -categorical foundation that takes them as axioms. Perhaps the second statement would be a schema with $P$ replaced by any first-order logical formula.

In case anyone listening in finds the idea of a coinductive axiom schema odd, note that inductive axiom schemas are not unknown in set theory. In Intuitionistic ZF, the “foundation” axiom is phrased as “set-induction”: given any property $P$ , if for any set $x$ , to conclude that $P(x)$ it suffices to show that $P(y)$ for all $y\in x$ , then in fact $P(x)$ holds for all sets $x$ .

Posted by: Mike Shulman on December 6, 2009 9:13 AM | Permalink | PGP Sig | Reply to this

Re: Feferman Set Theory

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

One way that comes to mind to talk about contractibility is by coinduction.

Ah, nice — yes, that seems very natural. And I guess you might well also want to talk about weak equivalence/invertibility defined coinductively, as discribed in eg Cheng An $\omega$ -category with all duals is an $\omega$ -groupoid.

Posted by: Peter LeFanu Lumsdaine on December 6, 2009 4:37 PM | Permalink | Reply to this

Re: Feferman Set Theory

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

And I guess you might well also want to talk about weak equivalence/invertibility defined coinductively

Indeed. Although one of the nice things about $\infty$ -groupoids is that a map is an equivalence iff each of its fibers is contractible. And of course an $\infty$ -groupoid is contractible iff its map to the terminal object is an equivalence, so at a foundational level I think you really only need one of the two notions.

Posted by: Mike Shulman on December 7, 2009 1:23 AM | Permalink | PGP Sig | Reply to this

Re: Feferman Set Theory

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

Mike wrote:

Has anyone done serious work on the notions of $\omega^{op}$ -category and $\mathbb{Z}$ -category?

I guess you know Jim Dolan and I pointed out that spectra are examples of $\mathbb{Z}$ -groupoids. So in particular a positively graded cochain complex is an example of a strict $\omega^{op}$ -groupoid.

But this is not what I’d call ‘serious work’ — just a hint that such work would be worthwhile.

Posted by: John Baez on December 6, 2009 6:46 AM | Permalink | Reply to this

Re: Feferman Set Theory

Ah, thanks! In the time it took me to write the long screed below and wrangle with Markdown over the subscripts, you answered the first question I was asking in it. :-)

Posted by: Peter LeFanu Lumsdaine on December 6, 2009 7:34 AM | Permalink | Reply to this

Re: Feferman Set Theory

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

I guess you know Jim Dolan and I pointed out that spectra are examples of $\mathbb{Z}$ -groupoids

Yes, I did know that. I think I even remember you telling me about it over lunch in Minneapolis 5 years ago. (-: But I guess no one has gone any further down that road since then.

I wonder how much of, say, the Batanin/Leinster globular-operad approach to weak higher categories would go through starting with strict $\mathbb{Z}$ -categories instead of strict $\omega$ -categories.

Posted by: Mike Shulman on December 6, 2009 8:18 AM | Permalink | PGP Sig | Reply to this

Re: Feferman Set Theory

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

For $\omega^\mathrm{op}$ -categories, at least the main definitions of the Leinster approach go through: you have a finitary cartesian monad on $\omega^\mathrm{op}$ -Gph, you have a clear notion of contraction, and the category and monad are just as nice as the usual case (a presheaf category, a finitary familially representable monad) so everything works fine. And afaics it should work pretty much the same for $\mathbb{Z}$ -categories, though I haven’t thought about that carefully.

The “pasting diagrams” you get are still pretty familiar: they’re just normal finite-dimensional pasting diagrams, suspended infinitely many times. In the Batanin tree picture, they’re infinitely tall palm trees: they can branch normally near the top, but below some finite top part, they’re just a single stem. (If I’m not mistaken this description works both for $\mathbb{Z}$ and $\omega^\mathrm{op}$ .)

The “initial operad-with-contraction” looks like the colimit of using the usual Leinster ones on every upper segment, if that makes sense. (Again, I’m confident this works for $\omega^\mathrm{op}$ , and I think it should work similarly for $\mathbb{Z}$ .) So $\omega^\mathrm{op}$ - (or $\mathbb{Z}$ -) categories do have exactly “hom-weak- $n$ -categories” (or - $\omega$ -) in the Leinster sense at depth $n+1$ , as you’d hope.

Posted by: Peter LeFanu Lumsdaine on December 6, 2009 5:07 PM | Permalink | Reply to this

Re: Feferman Set Theory

This is about as far as I’ve really thought any of this through, by the way — it’s also the first time I’ve taken any of it beyond my own head or notepaper, so apologies if it’s a little disjointed.

Posted by: Peter LeFanu Lumsdaine on December 6, 2009 5:16 PM | Permalink | Reply to this

Re: Feferman Set Theory

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

That’s very encouraging. Have you any plans to write this up? I can think of a couple of pages that someone ought to create.

Posted by: Mike Shulman on December 7, 2009 1:34 AM | Permalink | PGP Sig | Reply to this

Re: Feferman Set Theory

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

Has anyone done serious work on the notions of $\omega^\mathrm{op}$ -category and $\mathbb{Z}$ -category?

I was hoping you (or someone else) would tell me ;-) I vaguely remember seeing $\mathbb{Z}$ -categories bandied about here or on the nLab a few years ago, in a way that suggested they’d been studied (though not in a foundational context), but now I can’t find where, and I don’t know where thy’ve been studied, if so. But once you start playing around with about them, a lot of things fall out fairly clearly; as evinced by:

Now let me see if I understand your second proposal

Yes — what you describe is pretty much exactly what I was thinking of, up to notation.

I think I like this, although all the negative-dimensional cells are kind of annoying. Maybe we should “re-grade everything cohomologically” so that (−n)-morphisms are the same as n-comorphisms.

I’m glad you like it too: I find it a nice picture, and I think the strict version is a fairly accurate description of how (in classical foundations) the hierarchy of universes tends to get used.

The negative indices are a bit cumbersome, yes… But comorphisms seems a bit dreadful too! I’m not at all sure what the nicest way to deal what indexing is. In playing with it, I’ve used “depth $k$ ” to mean “dimension $-k$ ”, which is where the $k$ -categories live, and more generally the $n-k$ -cells of $n$ -categories; but I haven’t found anything that really works well.

For formal definitions, the way I’ve been working with it: consider the chain

Set $\rightarrow$ Cat $\rightarrow$ 2-Cat $\rightarrow \ldots$

where each functor is “cut off the lowest dimension”, aka “take the disjoint union of all hom-categories”. Then $\omega^\op$ -Cat is the colimit of this chain: small strict $\omega^\op$ categories).

Also, define a “spined n-category” to be an n-category with a chosen pair of parallel cells $T^i, U^i: T^{i+1} \to U^{i+1}$ in each dimension $n-i$ : a “spine”, looking like how “terminal objects/points” and “universes” are behaving in the foundational example. Now we have another chain

sp-Set $\rightarrow$ sp-Cat $\rightarrow$ sp-2-Cat $\rightarrow \ldots$

where the functors are “take the hom-category of the lowest elements of the spine” (with left adjoints “unreduced suspension”; the previous chain also had left adjoints, but not quite such nice ones). Now take sp- $\omega^\mathrm{op}$ -Cat to be the colimit of this chain: small strict spined $\omega^\mathrm{op}$ -categories.

Now it’s immediate from these (if I’m not mistaken) that:

1) Any strict spined $\omega^\mathrm{op}$ -category gives a strict (unspined) $\omega^\mathrm{op}$ -category.

2) If we have $\omega+1$ -many Grothendieck universes $G^0, G^1,\ldots ,G^\omega$ , then we get a $G^\omega$ -small strict spined $\omega^\mathrm{op}$ -category, where $T^n$ “is” the terminal $n$ -category, and $U^n$ “is” the $G^n$ -small $n$ -category of $G^{n-1}$ -small $n-1$ -categories.

Whew… all those indexes! But yes… that’s how I’ve been making this all precise; and I don’t think any of it will surprise you, or anyone else who fights their way through all the indices :-)

I’ve played a bit further with weakening this and trying to write down a type theory for it. Unsurprisingly, things get rather less clear-cut at this point, in interesting ways! But this comment is long already, so I should stop here for now…

(Eech — sorry for a lot of the should-be-subscripts being broken, but I forgot that Markdown chokes on underscores in math, and I’m a bit too tired to either figure out how to unbreak them or rewrite everything in a different encoding.)

Posted by: Peter LeFanu Lumsdaine on December 6, 2009 7:27 AM | Permalink | Reply to this

Re: Feferman Set Theory

D’oh, I shouldn’t try to write this late! Errata: in the chains above for defining $\omega^\mathrm{op}$-categories, of course the arrows were supposed to point _left_ and I meant to ask for the _limit_ of the chains. But I think I at least described the right functors in the prose…

Posted by: Peter LeFanu Lumsdaine on December 6, 2009 7:39 AM | Permalink | Reply to this

Re: Feferman Set Theory

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

“Comorphisms” was mostly a joke. But “depth” isn’t too bad of a terminology for the moment.

Posted by: Mike Shulman on December 6, 2009 8:30 AM | Permalink | PGP Sig | Reply to this

Re: Feferman Set Theory

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

Mike, I have a question. You wrote:

the category […] of all small sets is, itself, a set

and

“large” categories […] are still just sets

and enough other similar things that these can’t be typos.

What do you mean by saying that such-and-such a category “is” a set?

My question has nothing to do with smallness, universes etc. It’s a matter of grammar or type-checking.

Posted by: Tom Leinster on December 1, 2009 2:02 AM | Permalink | Reply to this

Re: Feferman Set Theory

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

What [does Mike] mean by saying that such-and-such a category “is” a set?

Has a set of objects.

Posted by: Urs Schreiber on December 1, 2009 7:56 AM | Permalink | Reply to this

Re: Feferman Set Theory

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

Are you sure? Now that I think about it a bit more, I guess Mike means that the arrows form a set. After all, this would be fairly similar to the usage of ‘finite category’ to mean ‘category whose collection of arrows is finite’.

Well, I’ll wait and see what Mike says.

Posted by: Tom Leinster on December 1, 2009 2:56 PM | Permalink | Reply to this

Re: Feferman Set Theory

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

What do you mean by saying that such-and-such a category “is” a set?

That was a bit sloppy for a structuralist; I should have said instead that its collections of objects and arrows are both sets. (Of course, this follows from knowing that its collection of arrows is a set.)

However, in material pure-set theory such as ZFC (the context I was writing in), categories can be sets, since one often formally defines structures such as groups, rings, spaces, and categories to be ordered tuples, which in turn are sets (according to the Kuratowski definition of ordered pairs). So in ZFC, it does make sense to say that a category $C$ is a set, namely the 6-tuple $(C_0, C_1, s, t, c, i)$ , and this is equivalent to saying that $C_0$ and $C_1$ are sets.

Posted by: Mike Shulman on December 1, 2009 5:54 PM | Permalink | PGP Sig | Reply to this

Re: Feferman Set Theory

Got it. Thanks.

Posted by: Tom Leinster on December 1, 2009 10:27 PM | Permalink | Reply to this

Re: Feferman Set Theory

In fact there is a very simple solution to these quandaries, and, as Baez predicts, it involves thinking in a clearer manner to make the paradoxes disappear. Unfortunately, it is not palatable to a lot of mathematicians.

The solution is to STOP PRETENDING THAT MATHEMATICAL OBJECTS EXIST BEFORE YOU THINK ABOUT THEM.

No one would be surprised at finding contradictions in my reasoning about “everything I am ever going to say”, especially if allow myself to talk about “all the things I will never talk about”. The “space of all spaces” is a non-concept, why the heck are you surprised that it doesn’t work out?

To get rid of the paradoxes, it would take a lot of work: we would have to build foundations for mathematics as a science of patterns that we create, of rule-following. This would involve fascinating mathematics, but philosophically it would be straightforward. Moreover, the mathematics would have clear challenges and goals, and at the end we would be able to say, “here is something of value: mathematics reflecting a more accurate view of what reality is like”.

As it stands, all the thrashing comes from trying to pretend that mathematics is something other than it is. And if anyone ever succeeds at this impossible task, they will only be able to say, “well, we managed to keep up the pretense”.

Posted by: El Duderino on September 5, 2010 10:52 AM | Permalink | Reply to this

More truth values known; Re: Feferman Set Theory

El Duderino, with all due respect, I think you err in assuming that Platonic Realism is either true or false. The Metaphysics of Mathematics has well over a dozen well-defined schools of thought. Many of us on this blog are familiar with many of them. It’s nice that you are enthusiastic, but I politely advise you to read a whole lot more by experts such as host or guest-host these blog threads.

Posted by: Jonathan Vos Post on September 5, 2010 6:07 PM | Permalink | Reply to this

Re: Feferman Set Theory

I have a similar position but what do I know, eh?
Do not bother to disturb the mathematicians in their addiction to (mostly) useless silly mind games.

Posted by: J-L Delatre on September 6, 2010 7:33 AM | Permalink | Reply to this

fundamental importance of discourse; Re: Feferman Set Theory

I think that I understand your position that “As I hinted the only purpose of objects is to serve as carriers of properties in our discourse.”

Making this discussion focus on Discourse shifts the emphasis to Pragmatics (from Syntax and Semantics) and Social Construction.

As I’ve said elsewhere, Scientists and Mathematicians each fall into many sometimes distinct metaphysical camps. The use of any terminology or representation is a minefield of possible confusions from foundational and linguistic differences in assumptions.

See, for example:

The fundamental importance of discourse in theoretical physics
Authors: Philip V. Fellman, Jonathan Vos Post, Christine M. Carmichael.
The purpose of the following paper is to demonstrate that the “limits of physics” are in a very important way determined by the conceptual framework and language of discourse that we use to describe physical reality. In this paper we examine three areas where the structure of discourse has been particularly difficult. In this regard we examine three problems, the problem of time (which is discussed in two sections of the paper), the problem of non-locality in quantum mechanics and some related general difficulties of interpretation specific to the Copenhagen school, and the concept of maximality as it is employed with respect to cosmic inflation in general relativity and quantum cosmology.

Posted by: Jonathan Vos Post on September 6, 2010 5:03 PM | Permalink | Reply to this

Re: fundamental importance of discourse; Re: Feferman Set Theory

Making this discussion focus on Discourse shifts the emphasis to Pragmatics (from Syntax and Semantics) and Social Construction.

No, no, no, not at all, I mean this is not what I find significant in changing the focus toward the discourse instead of the purported models (platonic or otherwise) of mathematics or physics.
Because Pragmatics, Syntax, Semantics and Social Construction are already yet another attempt at formalizing the subject matter, only at another “level” (the discourse), premature formalization is, I think, what gets in the way of a better understanding.
Lets just keep the vagueness of everyday language for a while until we have plausible reasons to be confident in the formalizations we can envision.
Do you use Pragmatics, Syntax and Semantics talking to your buddies at the bar?
I guess not, but if you look closer you will find that you do not use them either in colloquial mathematical discourse as it happens on this blog.
Yet this discourse does makes sense (mathematically), does it not?
Because even vague statements can convey a precise meaning between speakers sharing a common understanding and can usually be made more precise if needed by more explanations and exchange.
We see this process as we perform it but unfortunately it seems we cannot analyze it in order to formalize what happens.
There is some opacity, a twilight zone around our thinking, we can think but cannot think about how we think, we don’t have (yet?) the capacity to establish a good formalization of this elucidation process.
Mathematics are even the most blatant case of this discrepancy between the “shapes” of the subject matter, the discourse and the mental models which bridge the gap between the discourse and what is “talked about”.
The paper On proof and progress in mathematics by William Thurston makes this abundantly clear: mathematics are not really about formal models.

I am not myself interested in mathematics except as a good test case for this strange role of language as a bridge between the informal and the formal.
I am looking forward to the possibility to turn the informal sketch of a mathematical proof (good enough for a skilled mathematician knowledgeable in the field) into a fully formalized proof.

Posted by: J-L Delatre on September 6, 2010 7:49 PM | Permalink | Reply to this

Re: Feferman Set Theory

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

I’m not quite sure what El Duderino is talking about here specifically.

The fact is, Russell discovered an inconsistency in Frege’s Grundgesetze der Arithmetik, and this fact about a formal system doesn’t just go away by changing one’s philosophic position. Ever since then, mathematicians of all philosophic stripes have had to exercise care in how set theory and neighboring theories are axiomatized, and I don’t know of any evidence that anti-platonists know how to do it better than anyone else. (Note: I speak as someone with decidedly formalist, anti-platonist tendencies.)

Posted by: Todd Trimble on September 6, 2010 2:26 PM | Permalink | Reply to this

Re: Feferman Set Theory

Thanks to Jonathan and Todd for polite and thoughtful replies.

I realize that as an “anonymous Dude on the internet” I come off as an interested amateur. I have read up on a reasonable amount of the philosophy of mathematics, though, and I am aware of the several schools of thought, to the point where I am ready to murder anyone who mentions the canonical quartet of “Logicism, Intuitionism, Formalism and Platonism” in a 21st-century talk.

I’m not sure I understand Jonathan’s remark about Platonism being neither true nor false. It seems to me that, as a claim about reality, it must be one or the other. Moreover, it appears obviously false to me. Like so many other metaphysical claims, I think it survives out of a combination of tradition, simplicity and pride. (I am a working mathematician, and at first it was hard to let go of the romantic view and come to grips with the fact that I am studying entirely imaginary things, beautiful and useful though they may be occasionally.)

Todd, of course you are right that the inconsistency in Frege’s system is an entirely objective fact. You can write down the proof of contradiction and grasp it fully. You see that it follows from the *rules* set up by the system.

My claim is that this paradox is not so surprising as it is made out to be. It is directly derived from the system’s ability to manipulate non-concepts such as “the extension of a concept” and “the set of all sets s.t. …”. Both are predicated on the previous existence of “all sets” or “everything to which a concept applies”, which is tantamount to the existence of “all possible speech” or “all future developments”. These things only exist as we make them, not by themselves beforehand. Russell’s paradox is a point strongly favorable to my view.

Posted by: El Duderino on September 7, 2010 3:50 AM | Permalink | Reply to this

Re: Feferman Set Theory

El Duderino, I’m all for demystifying Russell’s paradox. If you don’t know it already, you might be interested in Lawvere’s paper Diagonal arguments and cartesian closed categories which provides a common setting for closely related matters such as Russell’s paradox, Cantor’s theorem, Gödek incompleteness, Tarski-Knaster fixed point theorem, and others, and seeks to demystify them. A very gentle readable exposition of Lawvere’s ideas here has been given in a paper by Noson Yanofsky.

I’m glad to hear you’re a professional mathematician, but I still don’t know what “quandaries” you are referring to in your initial post, and what simple solutions to them you have in mind precisely. It is widely understood that phrases like “set of all sets” etc. are question-begging to say the least, and by now largely out of use (not counting New Foundations), so tell me again what is it that you think we are surprised about, exactly?

(I hope you don’t mind my saying that your initial post really did sound like a rant, and didn’t sound like it came from a working professional who has anything precise to say.)

Posted by: Todd Trimble on September 7, 2010 5:12 AM | Permalink | Reply to this

Re: Feferman Set Theory

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

It sounds to me as though you are advocating some form of predicativism. Predicativism has a respectable philosophical/mathematical pedigree, and I find it intriguing, but I also find it difficult to accept as a working philosophy of mathematics from a purely pragmatic standpoint.

In particular, regarding the topic at hand, category theory has a very real need for large categories. Many things we do with large categories could be rephrased in terms of “a sufficiently-large small category” instead, but would thereby become extremely cumbersome. (E.g. for any small category $C$ there exists a small category of sets $set$ and a Yoneda embedding $C \hookrightarrow set^{C^{op}}$ , which is a free cocompletion relative to colimits whose size is no bigger than the sets in $set$ , etc.) Feferman’s axiom can be regarded as a way of encoding all of this cumbersome rephrasing into a language which enables us to talk as if we really did have a category $Set$ of all sets.

Posted by: Mike Shulman on September 7, 2010 6:54 AM | Permalink | Reply to this

Re: Feferman Set Theory

Btw, people’s bad reaction to “Feferman’s axiom” may be unaware that it is a recurrent phenomenon in set theory (e.g. provable in ZF) that there is a “large” (closed unbounded) class of levels of the cumulative hierarchy s.t. the level behaves exactly like the entire universe with respect to a given finite set of formulas. The key terms are “absoluteness” and “reflection principle”. This derives from the poverty of the language, which is, after all, only countable.

Feferman’s axiom is extremely natural if you understand a reasonable amount of set theory.

Posted by: El Duderino on September 7, 2010 3:55 AM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

November 30, 2009