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.)
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.
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.
The ghost of contradiction
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.
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.
