# Is “all categorical reasoning formally contradictory”?

In the December 2009 issue of the newsletter of the European Mathematical Society there is a very interesting interview with Pierre Cartier. In page 33, to the question

What was the ontological status of categories for Grothendieck?

he responds

Nowadays, one of the most interesting points in mathematics is that, although all categorical reasonings are formally contradictory, we use them and we never make a mistake.

Could someone explain what this actually means? (Please feel free to retag.)

-
The interview goes on like that : "Grothendieck provided a partial solution in terms of universes but a revolution of the foundations similar to what Cauchy and Weierstrass did for analysis is still to arrive." –  user2330 May 5 '10 at 10:53
On the other hand, if one works naively, lots of the reasoning one makes is wrong. For instance, is Tor(-, -) a bifunctor from Mod to Mod, in the sense that the Tor of two modules is a module? Well, one can choose a resolution and get a module... but not canonically. The best one can get is an isomorphism class of modules with canonical isomorphisms. Does this still justify calling Tor(-, -) a bifunctor? I don't know. But (please correct me if this is wrong) if one is just a bit more careful, one comes up with the notion of anafunctor, and Tor makes sense again... –  darij grinberg May 5 '10 at 13:02
@darij: modules have canonical (="choice-free") free resolutions using generating set of all elements. And if one goes back to ways of making injectives, can say same for injective resolutions (ditto in various sheaf categories). These are things which everyone has to come to terms with in their own way; I have no idea what an "anafunctor" is, and don't see the need for anything extra. Anyway, in categorical stuff infinitely many things do get used all at once: derived categories, for example. Computers aren't a good test; they don't do anything related to "infinite" issues Cartier raises. –  BCnrd May 5 '10 at 13:59
@darij: look at the usual proof that there are enough injectives in a category of modules: the resolution that can be derived from that proof is completely functorial. –  Mariano Suárez-Alvarez May 5 '10 at 16:38
Does anyone know what Cartier is referring to at the end of the paragraph? "I have just proposed a possible program to give a solid basis to categories at a meeting in Oberwolfach." –  François G. Dorais May 5 '10 at 17:27

Note: I am not a historian. I'm just guessing as to what prompted the comments.

Here's my guess: if you do set theory naively, in the old-fashioned "anything is a set" way, then you run into Russell's paradox; the set consisting of all sets that aren't elements of themselves gives you trouble. So you then decide set theory needs formalising (I'm talking about 100 years ago here of course) and you write down some axioms, and the ones that "won" are ZFC, where only "small" collections of things are sets, and "big" things like "all groups" aren't sets. Of course there's nothing contradictory about considering all groups, or quantifying over groups (i.e. saying "every group has an identity element"), but you can't quantify over the set of all groups.

And now because it's the 50s or 60s and you want to do homological algebra and take derived functors and do spectral sequences and stuff in some abstract way, you are now feeling the pressure a bit, because you want to define "functions" from the category of all G-modules (G a group) to the category of abelian groups called "group cohomology", but "H^n(G,-)" isn't a function, because its domain and range aren't sets. So you call it a "functor", which is fine, and press on.

And as time goes on, and you start composing derived functors, you know in your heart that it's all OK.

And then Grothendieck comes along, and probably other people too, and raise the issue that one really should be a bit more careful, because we don't want another Frege (who wrote a huge treatise on set theory but allowed big sets and his axioms were contradictory because of Russell's paradox). So Grothendieck tried to tame these beasts and "go back to basics"---but in some sense he "failed"---or, more precisely, realised that there were fundamental problems if he really wanted to treat categories as sets. "Sod it all", thought Grothendieck, "this is not really the main point". So he said "let's just assume there's a universe, i.e. (basically) a set where all the axioms of set theory hold" (it was a bit more complicated than that but still). This assumption (a) fixed all his problems but was (b) unprovable from the axioms of ZFC (because of Goedel).

So there's a guess. Cartier is perhaps going over the top with "contradictory"---the statement "Russell's paradox is a paradox" is true but the statement "any mathematical manipulation with collections of objects that don't form a set is formally contradictory" is much stronger and surely false.

-
I quoted this post here once before: cs.nyu.edu/pipermail/fom/2007-December/012359.html It's Bill Messing pointing out that one has to be careful. –  Kevin Buzzard May 5 '10 at 10:56
Your "guess" is just wonderful! And Cartier is The Last of the Bourbaki... –  Wadim Zudilin May 5 '10 at 11:26
"'Sod it all', thought Grothendieck"? Blimey, I never realized he spoke to himself like that. –  Pete L. Clark May 5 '10 at 11:27
I should clarify. Firstly I was just joking when I said he said "oh sod it"---he of course never said that. Secondly the point I was trying to make is that I got the impression that rather than trying to formalise what he wanted to do in ZFC, he decided that in fact the fact that he was having trouble formalising what he wanted to do was a deficiency of ZFC, so he added a new axiom which fixed things because he didn't want to get bogged down here, he just wanted to get on with the alg geom. That was what I meant when I made the flippant remarks. –  Kevin Buzzard May 5 '10 at 22:15
@AndrewL: Grothendieck's universes axiom is a farily mild addition to ZFC; it's an easy consequence of most of the large cardinal axioms that set theorists happily throw around, and there's no particular reason to suspect them inconsistent. So he wasn't being irresponsible! The danger is that later mathematicians want to do without them, as they're both rather cumbersome and a bit hacky. Cartier's point is about this: we can't just ignore them; we either need to accept them, or think hard about what alternatives we're using. –  Peter LeFanu Lumsdaine May 6 '10 at 1:05

Here is Pierre Cartier's abstract from the Oberwolfach meeting Category Theory and Related Fields: History and Prospects (February 2009).

Living in a contradictory world: categories vs. sets?

In the present time, the ambition to offer global foundations for mathematics, free of ambiguities and contradictions, covering the whole spectrum of the mathematical activities, has been challenged by known flaws induced by the use and abuse of "big" categories. Unless we are ready to abandon a large part of fruitful trends in mathematical research, we have to face head on the reality (or nightmare) of contradictory mathematics. I’m suggesting a possible escape by using a theory of types to formalize the proofs of category theory.

In their pioneering paper on "Natural transformations", Eilenberg and Mac Lane stressed the importance of a new kind of constructions, now known as functors. So far the known constructions in geometry would associate two classes element by element, for instance a circle in a plane and its center. Examples coming from topology were of a different kind associating globally to a space another space (like the loop space) or algebraic invariants (like homotopy or homology groups). Also the question was raised of the naturalness of some transformations, like the identification of a finite dimensional vector space with its dual (not natural) or its bidual (natural). The insistence on transformations leads to a style of proof, which is "without points". Again, in his axiomatic description of the homology groups of a group (or Lie algebra) as given in the 1950 Cartan Seminar, Eilenberg considers a "construction" which to a group G associates the homology groups Hi(G;Z) for instance. But he is not explicit about how to express such a construction in the accepted paradigm of set theory. In Cartan-Eilenberg book, there is also a description “without points” of the direct sum of two modules. So, in the minds of the founding fathers of category theory, this theory was a kind of superstructure on the existing mathematics, more at the level of metamathematics.

In his epoch-making Tohoku paper, Grothendieck reversed this trend. Inspired by the work of Cartan and his collaborators on sheaves and their cohomology, Grothendieck introduced head on infinitary methods in category theory. His purpose was to use direct limits to define the stalks of sheaves in a categorical way, since one knew already many examples of sheaves in a category, like sheaves of groups, of rings, etc... Also one of the greatest discoveries of Grothendieck in this paper is the existence of injective objects in a reasonable category (satisfying axiom AB 5*). Going back from this abstract level, one can freely use injective sheaves, thereby greatly simplifying the general theory of sheaves.

In so doing, Grothendieck was combining two lines of thought: the rather metamathematical (hence finitary) methods of Eilenberg and Mac Lane, with the infinitary methods of Bourbaki Topology and Algebra focusing on infinite limits (direct or inverse) and universal problems. This mariage was extraordinarily fruitful for mathematics, but a price had to be paid. Categorical reasoning was “proofs without points” but the new methods required to consider the actual (not potential) totalities of all spaces, or all continuous transformations between spaces. Immediately, the old ghosts of the set-theoretic paradoxes resurfaced, like the Burali-Forti antinomy of the set of all sets, or the Richard antinomy bearing on definable objects. A natural development led to fundamental notions, like limit of a functor, representable functor and Yoneda lemma, adjoint pair of functors. But the logical disease remained, leading for instance to a questionable proof of the general existence of an adjoint functor.

If category theory can easily be formulated within a framework of first-order logic (and this led to Lawvere formulation of set theory in this spirit), and if set theory received a proper axiomatization as the Zermelo-Frenkel system, the combination of both proved explosive. Some cures were attempted, like the use of universes by Grothendieck and Gabriel-Demazure. But this is highly artificial, like all methods using a universal domain, and brings us to the difficult (and irrelevant) problems of large cardinals in set theory.

At the moment, the situation is not unlike the one prevailing in the 18th century in the infinitesimal calculus. Everyone knew that the existence of infinitesimal quantities was questionable and that its use leads easily to contradictions. Today, we know about the dangerous spots, where not to swim, and try to stay away while continuing our exploration.

A possible exorcizing of ghosts

I would like to suggest a possible way out of this impasse. It seems to me that the initial sin is the prevalent view about the underlying ontology of mathematics. From a technical point of view, the Hilbert proposal of encoding every mathematical object as a set has been extremely successful. After the successful arithmetization of analysis, representing (in various ways: Dedekind cuts,...) a real number as a collection (or set) of integers, or pairs of integers, ..., all kinds of mathematical constructions yielded to the set theoretic paradigm. But in the accepted way of thought, a set is defined only after all of its elements have been created and put under control. So, speaking of the set of cats (integers) means that you could call the roll of all the cats (integers). So when we speak of the category of groups, all imaginable groups should be present. This is the point of view of actual infinities in an extensional sense. The undecidability of continuum hypothesis represents for me an unescapable blemish of this “realistic” point of view about infinity.

The new approach should be based on a comprehension scheme. That is, a set is described by the characteristic property of its elements: the set of cats is defined by the property of being a cat, described as accurately as possible, without any claim about the totality of existing cats. This is a standard practice in typed languages in computer science. Typically, a programme begins by instructions like

x : real

n : integer

t : boolean

... ... ...

declaring variables of various types (or sorts). Such a language embodies rules to create new types out of old types, for instance the type

integer → real

is the type of sequences of real numbers. Usually, there is also available an abstraction principle, in the form of a λ-operation

λx.t

to describe a function associating to x the value t (described by a formula containing x). So the framework is a typed λ-calculus.

There have been recent advances in theoretical computer science, in the form of various proof assistants (HOL Light, Mizar, Coq, Isabelle,...). They are able to create completely formalized proofs of “real” mathematics, like the prime number theorem, and check and guarantee their correctness.

I’m raising the challenge to translate the usual proofs of category theory within such a system. What should be required is the existence of types like cat (= categories), func (= functors),... So a standard sentence like: “Let C be a category” should be encoded by a declaration like:

C : cat .

There is no need to think of the totality of all possible categories. Of course, a type like set would embody the category of sets.

Of course, the implicit strategy is the one of Russell when he invented type theory to cure the diseases of set theory, like the set of all sets. . . I would also like to mention that the inner logic of a topos looks very similar, so we could perhaps formalize large segments of category theory within a syntactically defined universal topos.

-
This is missing som emphasis from the original. Feel free to fix for accuracy. mfo.de/programme/schedule/2009/08a/OWR_2009_08.pdf –  François G. Dorais May 5 '10 at 19:31
Sorry I cannot resist: mathoverflow.net/questions/16095/… . Of course You may avoid to quantify over all categories, but even within large category like Set how do You know what are elements before You define it? General quantification may be defined as certain formula in set theory (1957 Andrzej Mostowski), but I wish to see definition in language of categories... I presume it has to use at least isomorphism between categories... –  kakaz May 6 '10 at 7:27

With regard to what Darij said, if Haskell is viewed as a formal system, it's quite easy to derive contradictions; they correspond to infinite loops:

loop :: forall a. a
loop = loop


However, when viewed in this light, the quote becomes something like:

Nowadays, one of the most interesting things in computer programming is that, although most languages allow one to write infinite loops, most programs that people write aren't infinite loops.

But this isn't surprising at all, because most people construct programs with some productive activity in mind, rather than just spinning in a vicious loop. And similarly, most mathematicians presumably choose theorems and proofs that they find to be similarly productive, rather than a masquerading paradox, even if the formal system would allow the latter. Just because the formal system allows paradox doesn't mean that there aren't non-paradoxical ways to prove things in the system, or that most proofs people write wouldn't be the latter.

Now, one might say, "people do write infinite loops." And this is true. But, the analogy with Haskell breaks down a bit at that point, because Haskell makes it easy to write infinite loops. It's just a given in the language, like mine above. With inconsistent formal systems, it's typically not as easy to get a proof of false. People did a lot of naive set theory without noticing that you could do it for instance. Russel's paradox is probably the easiest of the bunch, but it's quite easy to break it. For instance, you could have a naive set theory with more typing restrictions, such that propositions like x ∉ x aren't well-formed. It will still be inconsistent, but you'll have to do more work to construct a paradox. As another example, a type theory with Type : Type (that is, there's a type of all types) is inconsistent, but proving false is a lot of work.

So, to posit a reason for why people never make mistakes with their categorical proofs, despite it being a possibility given that people typically work in a naive system: it may well be much harder to construct circular proofs (in category theory) for most theorems that people are interested in than it is to write good proofs. For one, it might be hard to prove false. For two, proving false and then inferring whatever you want is obviously bad, so the paradoxical logic would have to be disguised as a legitimate argument. And that's unlikely to be the sort of reasoning a mathematician has in mind to prove things that aren't fairly related to paradoxes.

-

I'm not a logician at all, but since I'm using categories, I decided at some point to find out what is going on. A logician would probably give you a better answer, but in the mean time, here is my understanding.

Grothendieck's Universe axiom (every set is an element of a Grothendieck universe) is equivalent to saying that for every cardinal there is a larger strictly inaccessible cardinal.

(Recall that a cardinal $\lambda$ is weakly inaccessible, iff a. it is regular (i.e. a set of cardinality $\lambda$ can't be represented as a union of sets of cardinality $<\lambda$ indexed by a set of cardinality $<\lambda$) and b. for all cardinals $\mu<\lambda$ we have $\mu^+<\lambda$ where $\mu^+$ is the successor of $\mu$. Strongly inaccessible cardinals are defined in the same way, with $\mu^+$ replaced by $2^\mu$. Usually one also adds the condition that $\lambda$ should be uncountable.)

Assuming ZFC is consistent we can show that ZFC + " there are no weakly inaccessible cardinals" is consistent. The way I understand it, this is because if we have a model for ZFC, then all sets smaller than the smallest inaccessible cardinal would still give us a model for ZFC where no inaccessible cardinals exist. See e.g. Kanamori, "The Higher Infinite", p. 18.

So far the situation is pretty similar to e.g. the Continuum Hypothesis (CH): assuming ZFC is consistent, we can show that ZFC+not CH is consistent.

What makes the Universe Axiom different from CH is that we can not deduce the considtency of ZFC + IC from the consistency of ZFC (here IC stands for "there is an inaccessible cadrinal"). This is because we can deduce from ZFC + IC that ZFC is consistent: basically, again all sets smaller than the smallest inaccessible cardinal give a model for ZFC. So if we can deduce from the consistency of ZFC that ZFC + IC is consistent, then we can prove the consistency of ZFC + IC in ZFC + IC, which violates G\"odel's incompleteness theorem (see e.g. Kanamori, ibid, p. 19).

Notice that the impossibility to deduce the consistency of ZFC + IC from the consistency of ZFC is stronger that simply the impossibility to prove IC in ZFC.

So my guess would be that Cartier is referring to the fact that the consistency of ZFC implies the consistency of ZFC plus the negation of the Universe Axiom, but not ZFC plus the Universe Axiom itself.

-
Although it is true that universes have a large cardinal strength, as you say, this doesn't make their use contradictory. So I doubt that this is what Cartier meant when he said that catogorical reasoning is formally contradictory. After all, neither the category theorists nor the set theorists believe that the existence of large cardinals or universes is inconsistent. Rather, I believe that Cartier was referring to the fact that much of category-theoretic reasoning uses a version of naive set theory that skirts very close to or even allows the Russell contradiction. –  Joel David Hamkins May 5 '10 at 18:33
Joel -- I seriously doubt that Cartier was talking of an actual formal contradiction, since none have been discovered so far. So I think this statement should be taken as a figure of speech, which is why I mentioned something which may look like a contradiction without actually being one. Another option would be that the phrase "formal contradiction" is the interviewer's interpretation of something else or that it simply appeared in translation (if things can get lost in translation, presumably they can appear as well:). –  algori May 6 '10 at 2:30