In her paper The unification of Mathematics via Topos Theory, Olivia Caramello says "one can generate a huge number of new results in any mathematical field without any creative effort". Is this an exaggeration, and if not is this a new idea or has it always been thought that topos theory could enable automatic generation of theorems ?
$\begingroup$
$\endgroup$
8
asked Jun 23, 2010 at 13:03
-
41$\begingroup$ I'd love to see the first theorem on the Navier-Stokes equations proved by means of the topos theory... $\endgroup$– Andrey RekaloCommented Jun 23, 2010 at 13:37
-
55$\begingroup$ Being able to create a huge number of new dishes doesn't make one a chef. $\endgroup$– Charles MatthewsCommented Jun 23, 2010 at 13:58
-
28$\begingroup$ To those voting to close: honestly, people! Whether or not the question sounds polemical to you, there are already some interesting answers below and perhaps more are coming. That's what matters. $\endgroup$– algoriCommented Jun 25, 2010 at 23:27
-
35$\begingroup$ One doesn't need to know anything about topos theory to know that the claim "One can generate a huge number of new results in any mathematical field without any creative effort" is trivially true if the new results are not required to be of interest to anyone and trivially false otherwise: almost by definition "creative effort" is that which produces interesting, new theorems. I found the paper (including its title) to be rather over the top. Probably others here feel similarly. But it shouldn't reflect negatively on the OP -- he just asked for our opinion on this curious statement. $\endgroup$– Pete L. ClarkCommented Jun 26, 2010 at 6:02
-
39$\begingroup$ Why are there suddenly so many straw men being thrown around? Yes, this statement is trivially true if taken to cover any new theorems, and almost certainly false if very specific well-known theorems are asked for. But the original intent is clearly somewhere between: how many interesting non-trivial theorems are there (none? some? or many, as Caramello claims?) that can be read straight off via topos-theoretic dictionaries from theorems in other areas? And this is surely an interesting and reasonably precise question! $\endgroup$– Peter LeFanu LumsdaineCommented Jun 27, 2010 at 19:46
|
Show 3 more comments
5 Answers
$\begingroup$
$\endgroup$
0
Topos theory provides a dictionary between (certain areas of) logic and (certain areas of) geometry. As such, it provides all the benefits that mathematical dictionaries do: It lets you translate between two languages whose natural evolutions proceeded independently. An insight that is obvious in one domain may not be so obvious when translated to the other domain.
Dictionaries cannot perform magic. In particular, it is usually too optimistic to think that a dictionary will allow you to prove significant new theorems with no effort. True, sometimes we do get lucky in this way. When Richard Stanley first discovered the dictionary between toric varieties and convex polytopes, he almost immediately reaped the reward of proving an important combinatorial conjecture with very little effort, because geometers had already put in a lot of work to solve exactly the problem he needed. But more commonly, the payoff of a dictionary is that it allows you to formulate good questions with very little effort. That is, you now have a new way to think about old problems, so you may be able to find your way more easily to a solution by borrowing concepts from both domains. You will still need to do hard work to solve hard problems, but your toolbox is now bigger.
answered Jun 25, 2010 at 22:45
$\begingroup$
$\endgroup$
1
I can't really answer the question, but I attended Olivia's talk today at CT2010 in Genova where she was presenting this paper, and I asked her some questions afterwards. Any errors or misrepresentations in my following comments are entirely mine.
When the informal statement is made technical, there appear to be some qualifications. First, it applies only to mathematical theories that can be formalized in geometric logic. This is a kind of logic with a restriction on how quantifiers can be used in axioms. According to Olivia, this is not much of a restriction, because it includes for example finitary logic, and more.
Second, to be able to transport results from one theory to another, the theories must be Morita equivalent. Apparently this is more common than one might think, and once one has Morita equivalence, one can transport all kinds of results back and forth. So perhaps it would be fair to say that "some creative effort" goes into finding appropriate Morita equivalences in the first place.
Olivia refered to her Ph.D. thesis for a number of examples where this had been done. I have not really seen the examples. The areas of mathematics that she specifically mentioned in her talk were algebra, topology, two different branches of logic (proof theory and model theory), and a 5th one which I forgot. Definitely not PDE's or Riemannian geometry.
Two more remarks: a topos is a kind of set theory, so it is indeed plausible that all kinds of areas of mathematics can be formalized within a topos. Sometimes this is done by "real" mathematicians (i.e., non-logicians). For example, Tom Hales's ongoing formalization of the proof of the Kepler conjecture is done in HOL Light, which uses a topos logic as far as I remember. (The proof is not constructive, as excluded middle and the axiom of choice have been added as additional axioms). Tom has already given a complete machine-checkable proof of the Jordan curve theorem. The point of doing this in HOL Light, at this point, is not so much the topos aspect, but the fact that the proofs can be verified by machine, eliminating the referee's residual uncertainty. This is impractical with "ordinary" set theory.
Last, when one claims to be able to generate "new theorems", this does not necessarily mean "interesting new theorems". I guess that in some cases, they can be interesting, but perhaps more so to logicians than to other mathematicians. Then again, it's happened before that disjoint areas of mathematics were related, and when this happens, it is always useful. Seems nice to have another avenue.
-
$\begingroup$ Welcome to MathOverflow, and thanks for the comment! $\endgroup$ Commented Jun 25, 2010 at 16:32
$\begingroup$
$\endgroup$
7
This statement is true, but there's substantially less than meets the eye to it.
Topoi are gadgets which are both models of both a fairly large fragment of logic (typed higher-order logic), and are generalizations of sheaves on a topological space. (The reason this connection is possible is morally that the open sets of a topological space form a Heyting algebra, which is a model of propositional intuitionistic logic.) As a result of their high logical strength, you can take many practical constructions and encode them in the internal logic of a topos. Then you can take an external view and hit these constructions with topologist technical wizardry.
Since topologists and logicians talk to each other rather less frequently than we ought to, this method is a very fertile source of theorems. "Without creative effort" is just a rhetorical flourish intended to encourage people to learn about topoi -- there's no way (presently) that a computer could generate theorems via topos theory. But it is an effective tool for human mathematicians to port ideas from one area to another, which has always been a productive endeavor.
The book to read on this subject is MacLane and Mordeijk's Sheaves in Geometry and Logic, which, as you can guess from the title, emphasizes the moral that taking a synthesizing perspective on mathematics is often valuable.
answered Jun 23, 2010 at 13:23
-
16$\begingroup$ Please give an example of an interesting theorem generated via the procedure of the second paragraph. $\endgroup$– BoyarskyCommented Jun 23, 2010 at 15:54
-
14$\begingroup$ Fiore and Simpson's "Lambda-Definability with Sums via Grothendieck Logical Relations" showed how to adapt the idea of a cover algebra or Grothendieck topology to the setting of structural proof theory, which Balat et al subsequently used to give a normalization algorithm for the lambda calculus with disjoint sum types. The insight was that the case-distinction in the disjunction elimination rule could be split apart and the pieces could be taken as a kind of "open cover" of the whole proof. $\endgroup$ Commented Jun 23, 2010 at 16:34
-
12$\begingroup$ Dear Neel: Unfortunately I don't understand what your example is saying (even the insight which you say hadn't been noticed before). I should have said "interesting theorem in a field of mathematics different from logic", since logicians appear to already be sold on topoi. Since you say the quote in the question is true, in the spirit of "any mathematical field" let's be specific and take 3 big fields: PDE, Riemannian geometry, and representation theory. $\endgroup$– BoyarskyCommented Jun 23, 2010 at 17:23
-
3$\begingroup$ Dear Neel: Good luck with the representation theory; it's a beautiful subject. (It boggles my mind how it could have any applications of the sort you suggest, but perhaps that is due to my own ignorance of logic.) $\endgroup$– BoyarskyCommented Jun 24, 2010 at 12:54
-
8$\begingroup$ I'm a fan of category theory in general and think toposes are just nifty (for geometry at least), but this answer made me cringe. $\endgroup$ Commented Jun 25, 2010 at 23:17
$\begingroup$
$\endgroup$
2
It would be presumptuous on my part to attempt to answer this question, but I want to share with other MOers this recent paper
http://www.ihes.fr/~lafforgue/math/TheorieCaramello.pdf
of Laurent Lafforgue and this video
https://sites.google.com/site/logiquecategorique/Contenus/20130227_Lafforgue
of one of his recent lectures, [dont] le but [] est de poser cette question (inspirée par la théorie de Caramello) : l'indépendance de $l$ de la cohomologie $l$-adique et la correspondance de Langlands sont-elles des équivalences de Morita entre topos classifiants ?
Here is a quote from the paper : La théorie de Caramello... offre déjà un très grand nombre d'exemples d'équivalences de Morita et de leurs applications. Ces exemples sont étonnament divers et ils apparaissent presque toujours comme surprenants. Beaucoup d'énoncés auraient été très difficiles à démontrer, et plus encore à imaginer, sans les topos et sans les méthodes de calcul que la théorie des topos classifiants et des équivalences de Morita rend possibles et naturelles. Quand on songe que la correspondance de Langlands ressemble beaucoup à une equivalence de Morita et qu'elle en est peut-être une, on se dit que le champ ouvert à cette théorie est immense.
answered Mar 18, 2013 at 14:42
-
11$\begingroup$ Thanks a lot for sharing this. So fields medalist Lafforgue seems to be convinced of the power and the future impact of Caramello's theory. $\endgroup$ Commented Mar 18, 2013 at 17:07
-
6$\begingroup$ and he's not isolated at the IHES with his opinion... ;) $\endgroup$– user5831Commented Mar 18, 2013 at 18:48
$\begingroup$
$\endgroup$
19
When a phrase is taken from a context, it is easy to misread it. If one looks at the paper, "one can generate a huge number of new results in any mathematical field without any creative effort" makes sense and is justified.
The idea is that most Mathematics can be formalized as a geometric theory, i.e, a logical theory with infinitary disjunction and finitary conjunction with the natural rules of inference. This is true since most Mathematics can be formalized in first-order logic which can be translated in geometric logic, and the translation preserves set-theoretic models. The model theory of geometric logic is naturally categorical; in fact, it is sound and complete (in a strong sense) when one considers the categorical models living inside Grothendieck toposes. The completeness theorem is proved by constructing a universal model which lives in a special topos, the classifying topos.
Olivia's result shows that very different theories share the same classifying topos (or better, they have different but equivalent classifying toposes). When this fact happens, and it is not uncommon - Olivia provides very general techniques to achieve this result - the classifying topos allows to move results from one theory to another. Examples have shown that very simple results in one theory translate into very deep results in other theories. But the translation technique is not-dictionary oriented but rather "modulo an abstract invariant" which allows for an extremly high degree of freedom.
The interesting thing in this machinery, which is not automatic, is exactly that a huge number of new mathematical results in any field of Mathematics can be generated without any significant creative effort. Of course, not every result can be generated in this way, as far as we know now, and not every generated result is significant. The mathematical intuition of an educated mathematician is needed to choose the right theories and the correct invariant to achieve a significant result. Olivia's examples show that very simple invariants applied to very classical theories provide explanations to deep results and a couple of new interpretation of classical results have been obtained.
As far as I'm able to understand Olivia's results, I believe her conclusions because her articles prove them. Of course, my understanding is not perfect and the explanation above are approximations of the real results. And yes, she is doing a big claim - but I became convinced that it is a true one.
-
20$\begingroup$ @Marco: It will help to clarify matters if you can provide one example of a deep result in some part of mathematics apart from logic or set theory which is deduced from a simple result in another theory by means of topoi. (Note: results which are routine applications of Zorn's Lemma and/or easily equivalent to the Axiom of Choice do not count as deep.) $\endgroup$– BCnrdCommented Jun 29, 2010 at 3:40
-
4$\begingroup$ @BCnrd: a partial answer to your question can be find in arxiv.org/abs/0808.1972 which shows a non-trivial result obtained in Algebra, specifically in the theory of fields. On the other side, one should consider that Olivia's theory has been conceived in 2008. It has reached its full expression at the end of 2009, and in the last months it has been refined and extended, as one can check in the Math Archive. It is not strange that there is a limited number of examples outside logic: If one has to develop a new theory, s/he would first focus on the field where it naturally lives. $\endgroup$ Commented Jun 29, 2010 at 14:31
-
21$\begingroup$ Dear Marco: what is interesting (let alone deep) from the viewpoint of the theory of fields in the link you give? (I don't think I have ever encountered a situation where the DeMorgan issue is relevant, and I know the theory of fields extremely well and have used it in many many ways.) In particular I still don't see what justifies the claim that her works allows one to translate something simple in one part of math into something deep in another. As far as I can tell, the grand sweep of what Olivia claims is not appropriate at the present time. $\endgroup$– BCnrdCommented Jun 30, 2010 at 4:34
-
34$\begingroup$ @Marco: Thanks very much for the follow-up! Now that I see the definitions of terms I didn't know, the assertion with finite fields is very well-known, easy to prove directly (not deep), and has been used for a long time. If someone told you it's hard to see with standard methods, they're wrong. It supports my original "concern": after unraveling the logic terminology, the "transferred" result in the other area of math will be obvious if no creative effort was required. It's up to Olivia to justify her claim of interesting/deep applications to other areas of math; I'll leave it to her. $\endgroup$– BCnrdCommented Jul 12, 2010 at 12:36
-
8$\begingroup$ Dear BCnrd, I have to say that I'm quite surprised by your answer. I see now that the example we discussed is "easy" in the theory of fields, but the point I wanted to make is that, once you have a description of the classifying topos, this result as well as many others (e.g., the ones I previously reported) flow naturally and immediately from it (and I really mean by a one-line yet entirely rigorous proof) - note that to prove this result by standard methods, a basic knowledge of the theory of field extensions is needed, while the topos-theoretic proof follwos a completely different path. $\endgroup$ Commented Jul 16, 2010 at 21:40