# What is an efficient nesting of mathematical theorems?

Various mathematical areas of research evolved from a wide and diverse range of questions. Many are physical in nature or come from informatics/computer science, some are procedural or optimization problems and so on. Often patterns emerge and lead to studies of abstract structures and in this way extend our knowledge of what is considered pure mathematics. Often, the original context gets stripped off and eventually, in the process of generalization, formerly different frameworks can be seen under a new perspective. Under some circumstances notation might be introduced and new and sometimes more elegant proofs are discovered.

If I have abstractly proven a statement, say for example in category theory (like the Grothendieck–Hirzebruch–Riemann–Roch theorem), and I then choose one of several specific frameworks, which satisfies certain structural patterns, then I can draw conclusions from the more abstract theorem and state new ones as a lemma (like the classical Riemann-Roch theorem). There are many statements in diverse geometric theories (like Poisson, Symplectic, Riemann or Euclidean geometriy, Lie Group theory etc.), which can be viewed as really just the same theorem under different lights. If I prove Stokes theorem, I might avoid finding individual proofs for various kinds of integral theorems. The core of some statements in de Rham cohomology is already hidden in more abstract cohomology theories with less specific context. My question is ultimately concerned with such a nesting and is kind of an optimization problem.

From the point of view of organization, one might consider drawing top-down conclusions more efficient than finding several more specific proofs. Lets assume one is interested in the bulk of major mathematical research areas and also able to draw all drawable conclusions for certain given axioms. It then seems to me that the following order of analysis seems like an suitable one: Introducing the notion of an abstract set, introducting all the various logics in an intelligent order, introduce abstract algebra followed by the category theoretic framework and then various more specific sets with axioms which make up relevant structures (including topology, numbers, modules, vector spaces, geometries,...). All the time with some intelligent order in mind, i.e. jumping from special case to special case in a minimalist way, even if there might not be an optimal way to do so, of course. Encyclopedic web pages like Wikipedia, MathWorld or comprehensive treatises give a rough conception of how this may work. (Personally, there are a couple of ambiguities for me, especially regarding the points at which I just have to introduce set theory. For example, I don't know if you really have to introduce sentences as objects in propositional calculus or what other big areas are explicable in non-set theoretic terms, even if they usually are explained that way. I also have little insight in modern model theoretic perspective.) Having said that:

What would be an (or maybe the) efficient order to introduce the mathematical frameworks (of current knowledge, state of the art and relevance), and why? Here the term "efficient" is understood in the sense explained above.

I would not be surprised if there are different good ways to approach this. But in any case, there are obviously theorems which include others and since one can put many mathematical disciplines on their own feet, there is some unambitious pyramiding. A more synthesizing formulation of the above question, one stated in terms of the specific fields, would be to ask:

Which are major mathematical theorems, which are strongly including in this sense? Which are theorems which have an unnegligible power with regard to special cases or sub-theorems and would therefore be worth of being proven first? As another approach, a start might be to find out which axioms are really necessary, i.e. doing reverse mathematics.

-
Great question. Better minds than I will have actual answers for you; I just wanted to suggest that you cross-post this to mathoverflow as well. That site is geared toward research-level mathematics, and may have other answers for you. – Drew Christianson Dec 11 '11 at 21:51
@Drew: I don't know if this would be within the StackExchange policies. Although the argument "Each site is focussed at a specific topic area." doesn't really apply for MathSE vs. MathOverflow, I guess I'll leave it here for now. There might come good answers from MathOverflow, I agree, but I don't know what the common opinion on cross posting is. If the answers here seem not thorough, then I don't mind if the question gets shifted there. – NikolajK Dec 11 '11 at 23:59
Really good question; this is something I struggle with constantly when trying to organize the mathematics I am learning. – ItsNotObvious Dec 12 '11 at 3:14
I think the kind of consideration you express was at the basis of the Bourbaki project (although that was pre-category-theory of course). Notably, I think they tried to present every result in the "most general" setting in which it is valid (although one never can be sure about the existence of even more abstract and general results). Studying that case in detail will reveal both the forces and the weaknesses of the approach, and also many concrete instances of deduction from generality. – Marc van Leeuwen Dec 12 '11 at 7:51
@NikolajKunst, about Dieudonné, see mathoverflow.net/questions/52708/…. – lhf Dec 15 '11 at 11:12

The premise of this question, which seems to be that there a key general theorems in mathematics from which other results can be deduced, is a little dubious. (There are also some inaccuracies in the post: e.g. Grothendieck--Hirzebruch--Riemann--Roch is a theorem in algebraic geometry, not category theory.)

Let me discuss just one fundmental theorem: the prime number theorem. On the one hand, this fits into a whole family of related theorems, all of fundamental significance in number theory: the asymptotic form of Dirichlet's theorem on primes in arithmetic progression; Cebotarev's density theorem; or, more recently, the Sato--Tate conjecture. On the other hand, there is no general result from which these results all follow.

More precisely, all these results can be proved by showing that an appropriate $L$-function (or family of $L$-functions) has analytic continuation up to the line $\Re(s) \geq 1$, and has no zeroes in this region. Given this, the claimed result then follows from the Wiener--Ikehara Tauberian theorem; so this is a general result which is involved in their proof. And this result can be realized as a special case of the much more general result in the theory of $L^1$ of locally compact groups, due to Gelfand. So that very general Tauberian theorem could feature as one vertex on the proposed network.

But this leaves open the question of how to affect the analytic continuation on $\Re(s) \geq 1$ (and how to verify the zero-freeness there). There is no general theorem that implies this. There are very general conjectures, in particular those coming from the Langlands program(see also the various posts on the Langlands program linked to here for more information on this program). But these are conjectures, not general theorems (as of yet).

There has been enormous progress on this program: e.g. Taylor and Wiles's proof of Shimura--Taniyama, or Sato--Tate, or Ngo's Fields Medal-winning work on the fundamental lemma. But these result reach out from what is known into the unknown. They involve an enormous amount of mathematics, including many results that would appear on the vertices of the envisaged network (algebraic geometry and etale cohomology, perverse sheaves, class field theory, ...). But all evidence suggests that it will be a long time before the general statement that encompases them all (the general form of Langlands's functoriality and reciprocity conjectures) is proved.

The conclusion that I draw from this is that, to the extent that mathematics is a living subject, it reaches out into the unknown; and the underlying principles are always being reformulated, with new ones being discovered. (As just one example of a recently discovered fundamental framework that is related to the prime number theorm, but is not part of the Langlands program, see the use of nilsystems in the work of Green and Tao on linear equations in primes.) In short, the envisaged network doesn't exist, at least as a way to encompass mathematics as a continually evolving subject. (Incidentally, I would also object to such a framework from a pedagogical view-point, but that is a different topic.)

-
Thanks for the answer and the examples. I don't see a problem with unproven theorems. They of course don't have the same status, but that just means that their lower status propagates down the tree reaching every theorem, which can only be proven by using them. Equally they can be left out or viewed as an axiomatic stating point, I guess. – NikolajK Dec 22 '11 at 7:56

At the end of the day it sounds like you want a directed graph with a node for every provable assertion and directed arcs representing logical implication.

In order for such a graph to be most useful you would ideally need to find a "normal form" for each provable assertion (or node).

But I don't see how this is possible, even restricting attention to assertions written in an extremely limited "sublanguage" of mathematics - consider "classical" Euclidean geometry, for example, where even a single theorem can typically find expression in several different equally valid, abstract, elegant, etc. forms (completely visual "proofs" of the Pythagorean theorem come to mind).

I suspect the best you can do is add "less than perfectly general" arcs and nodes to your logical graph via explicit proofs (written and read by humans). You could then have an automaton traverse the graph to find "cycles" (which indicate a set of "logically equivalent" assertions), "sources" (which indicate powerful statements), and "sinks" (which indicate weak ones).

But the usefulness of such a graph (even if received in Complete Perfection by a Supreme Intelligence) is limited by our ability to find the node for a given logical assertion. Making the statements as abstract as possible reduces the number of nodes in the graph (which may help) but may make it harder to decide if a given node (e.g. a theorem in Category Theory) really is equivalent to (or stronger than) the particular assertion we're interested in (e.g. a theorem in algebraic topology).

But maybe we're in a better position today to make the "search" for relevant nodes easier (e.g. by decorating the abstract statement of a theorem with "links" to equivalent forms and specific applications) than were previous generations of logicians. And if you actually start to build the graph maybe you'll figure out a format for "nodes" and "edges" that is sufficiently general to make the project appealing to other people, and you can make some progress.

Good luck!

EDIT: The distinction between "nodes" and "edges" is of course artificial - after all, logical statements boil down to implication, e.g. "A and B together imply C", and "logical statement X is stronger than logical statement Y" is itself a logical statement. But since the question seems to be about exploring relationships between logical statements I think it makes sense to distinguish the statements themselves (nodes) and logical relationships between them (arcs).

-
Thanks for your answer too. Why do you see a problem with the language? At the top of such a graph, we'd find axioms and definitions, which should tell us what language to use. And I think the choice of what node is stronger hasn't necessarily to be made by a computer. – NikolajK Dec 22 '11 at 7:49
Indeed, I don't think the determination of node A implies node B can be made by computer, except in very special cases. And although having nodes for axioms and definitions is of course useful, a key challenge is finding a way to make the graph show the same "abstract" theorem working in different contexts (I'm thinking of functors mapping statements about group theory to statements about topology, for example). Maybe it would be useful to have multiple types of nodes ("objects/definitions" vs. "assertions/theorems") and edges ("generalizes" vs. "implies"). – wolfen Dec 22 '11 at 22:13

A classical theorem

On the frontiers of math I can not say anything. I think I share the pursuit of what I'll call "general theorems" or "fundamental theorems". But if you can let me give an example of a "general theorem" in classical analysis. This theorem gives conditions for the two repeated limits commute. This theorem is widely does not receive due attention.

This theorem can be found in books of Lang (Analysis vol. 2 for example). But I think the wording of Zorich (Mathematical Analysis II p. 381) more generally. I will state it as it is in Zorich that describes in detail all the above mentioned consequences of this theorem. It's a pity we can not visualize them in google.

Theorem. Let $\{ F_t ; t\in T\}$ be a family of functions $F_t : X \rightarrow \mathbb{C}$ depending on a parameter t; let $\mathcal{B}_X$ be a base $X$ and $\mathcal{B}_{T}$ a base in $T$. If the family converges uniformly on $X$ over the base $\mathcal{B}_{T}$ to a function $F : X \rightarrow \mathbb{C}$ and the limit $\lim_{\mathcal{B}_{T}} F_t(x)=A_t$ exists for each $t\in T$, the both repeated limits $\lim_{\mathcal{B}_{X}}(\lim_{\mathcal{B}_{T}}F_t(x))$ and $\lim_{\mathcal{B}_{T}}(\lim_{\mathcal{B}_{X}}F_t(x))$ exist and the equality

$$\lim_{\mathcal{B}_{X}}(\lim_{\mathcal{B}_{T}}F_t(x))=\lim_{\mathcal{B}_{T}}(\lim_{\mathcal{B}_{X}}F_t(x))$$ holds.

The uniform convergence required in the hypotheses of this theorem is obtained via compactness and monotonicity when possible way (for example if $X = \mathbb{R}$).

For a convenient definition of the set $T$ (usually $T = \mathbb{N},\mathbb{R}$) and of functions $F_t$ (whit $X=\mathbb{R},\mathbb{R}^n,\mathbb{N}$ for exemple) follows immediately the following theorems

1) classical Fubini's theorem

2) Leibniz's rule for differentiation under the integral sign

3) Schwarz's theorem

4) Fundamental Calculu´s theorem

5) Arzelà–Ascoli theorem ( local version )

6) differentiation on the limit of some parameter

7) integration on the limit of some parameter

(Note. I hope I have written in English language common names of these theorems above.)

I'm not sure about that but I would venture to put on the list above theorems for continuous and differentiable dependence to ode and also the classical theorem of Weierstrass approximation.

I hope I have contributed to this example.

-

Philosophy is the hierarchical organization of ideas, and what you are asking for is tantamount to a philosophy of mathematics. This will depend on what you consider meaningful, important, and interesting. Every age (in German, Zeitgeist) is going to have their own answer to this question, which defines that age. And every individual likewise has their own perspective, which stands in relation to that. If you read the preface of an outstanding math book, and if the author is able to express their experience, you will also gain much insight to lead you closer to your personal answer to this question.

-
Well yeah, I explicitly stated that I don't expect uniqueness, rather approaches. – NikolajK Dec 22 '11 at 21:52

May i start off by recommending http://www.amazon.com/Experience-Nature-John-Dewey/dp/0486204715

I think that an axiomatic, bottom up, approach to mathematics is completely unnatural. Almost all of the great mathematical discoveries were leaps, braving the unknown - leaps of faith. The rigor is usually filled in after the fact.

-

The Atiyah–Singer index theorem certainly includes several important theorems.

-