Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Since it came up in another thread, I’ve made reverse mathematics slightly less stubby. I included some notes on constructive reverse mathematics, but perhaps it should have its own page.
Thanks for this.
What I find curious is that the idea
to establish for many theorems … exactly which set existence principles they rely on
is a completely general wide-spread idea in mathematics. It is good practice to do this with every theorem one states, and it is the basis of all kinds of abstractions that one considers.
Ah wait, is “set existence principles” a typo for “set of existence principles”, or does it really mean “principles of set-existence” ?
Given who are the main proponents, Harvey Friedman and Stephen Simpson, and their attitude towards category theory, I should think it very unlikely that they’d appreciate ’reverse mathematics’ being taken over as suggested by the likes of us.
Sure, that’s exactly what I am highlighting. It’s curious that a strategy that is basic to all of abstract maths is both highjacked and rejected, at the same time, by a small circle. But at least “reverse mathematics” sounds more professional than “centipede mathematics”.
There’s always ’transcendental’ from transcendental argument, but maybe that’s already too loaded.
In fact, Simpson is quite interested in sheaves nowadays. For instance, this paper. It does not use any heavy machinery, but at least uses the language.
Re #3: principles of set-existence, as in asserting that certain subsets of exist, as in certain weak second-order systems of arithmetic. The Wikipedia page gives a pretty good idea: typically one takes an ordinary theorem in mathematics and asks which set-theoretic principles sufficient to prove the theorem are implicit or necessary, and those principles generally fall into one of five classes.
It’s understood to denote a pretty specific research program, as opposed to a general familiar research stratagem; I agree that we had better not appropriate the term “reverse mathematics” for our purposes.
If pressed, I would say something like “principle of abstraction”. There was a slogan during the heyday of abstraction in the 1940’s and 1950’s, “Be wise, generalize”, which also captured the essential spirit. (It was supposed to be a take-off on “Be wise, Simonize”, which was an advertising slogan for a certain method of dry-cleaning.)
So the idea is that just as “evil” now directs to “principle of equivalence”, we could have “centipede mathematics” redirect to “principle of abstraction” (or something similar). Most of the content currently at centipede mathematics would seem to fit such a page title, and whatever pejorative implications that adhere to centipede mathematics could still be discussed there.
Right, “principles of set-existence” in RM refers specifically to a particular kind of hypothesis-inspecting that is, I think, quite far from the interest of most mathematicians, who are happy to use all of ZFC. It’s not completely unrelated to the activity of interest to categorical logicians of expressing theories in fragments of logic like regular and coherent so that they can be interpreted internally to more categories, but its focus and tools are rather different. (Once during a conversation with Damir Dzafarov I half-convinced myself that classical “reverse mathematics”, or at least one of the subsystems of set theory it uses, was roughly analogous to working with the hyperdoctrine of complemented subobjects in a non-Boolean category; but I don’t remember any more why.)
I do feel like “centipede mathematics”, even stripped of its perjorative implications, is a bit different from what I would call the “principle of abstraction” in general. When I think of abstraction, what I think of immediately is finding an abstract context that describes a class of given examples. Often the focus is on the right level of generality for an entire theory, not on the maximal level of generality for a particular result, whereas I feel like centipede mathematics is more about the latter (or even more strongly, about what fragments of a result we can recover after going above its maximal level of generality).
Maybe I feel like we don’t need a page title that is an exact synonym for “centipede mathematics”. Centipede mathematics would just be one form that abstraction or generalization could take. So, we could have a section that talks about “right generality” versus “maximum generality”, with pros and cons for the latter. (I remember that Mac Lane in Cats Work also talks about right generality vs. maximal generality, in the context of discussing the history of the concept of adjoint functor: that Bourbaki had come close, but went too far in order to accommodate something in multilinear algebra that was dear to French traditions, and that Kan was the first to get it right. That might be an example.)
Re:10 Grothendieck’s notion of equivalence of categories in his Tohoku (before Kan) was in fact assuming the triangle identities, hence he defined not mere equivalence but right away the adjoint equivalence. Thus, Grothendieck was probably aware (in some form) of the concept of ajdointness before Kan but did not put it into his focus.
@Todd: Okay, fair enough.
I’m curious to know what Bourbaki were actually doing. I wonder whether they were anticipating multicategories?
Re #10-12, a few months ago I ran into a paper by David Ellerman that had some discussion of this from a “heteromorphic” perspective: Mac Lane, Bourbaki, and Adjoints: A Heteromorphic Retrospective.
Zoran: that’s interesting. The Tohoku paper was 1957, and Dan Kan’s big paper where adjoint functors are introduced was 1958. So they’re pretty close;something was in the air. Of course adjoint functors are considerably more general than adjoint equivalences, and the big step of isolating the former as an abstract concept is one of Kan’s tremendous innovations; glory be to him.
Mike: maybe! Lambek, who wrote an influential book on rings and modules, made a big point of the analogy between multicategories and multilinear algebra in not a few papers, and as you know he was also the first to do multicategory algebra-style proof theory, re-imagining cut elimination with applications to coherence theory. (I discern a lot of unity of thought in Lambek, and appreciation of what he did will continue to grow.)
Todd: Why not ask Phil Scott? He was a close friend and collaborator of Jim Lambek and will know of some ideas that Jim had discussed that were not made so evident in what was written.
At the risk of repeating what others have implied: classical reverse mathematics is about finding the axioms which are equivalent the a given theorem. Proving, for instance, that theorem X in classical real analysis implies such and such restricted induction given some weak base axioms is a bigger deal than just finding the appropriate generality in which it could be proved. To mind my, category theorists don’t really do this version of things, at least explicitly.
Tim, thanks for the suggestion. The discussion was about something Bourbaki proposed, but it triggered a little free association in my mind involving Lambek. I didn’t have anything in particular I wanted to ask about Lambek though.
I will say that Lambek, who sadly died not long ago, had a huge influence on me and especially on the development of my thesis. I’m not sure I read everything he wrote on the topic of categorical proof theory, but I read quite a lot of it, going all the way back to his first papers on the topic, which for me were very illuminating. (His student Szabo also wrote a book, Algebra of Proofs, which I had found very helpful; unfortunately that book had some technical errors and the book suffered some disrepute, somewhat exaggeratedly in my opinion.) In fact Lambek and I wound up corresponding a bit, and it was Lambek who put me on the trail of interpreting Girard’s cyclic trips and comparing them with a graphical calculus I was developing – which was the crucial step for my thesis. Also Lambek was on my PhD committee. So obviously, I am greatly indebted to him intellectually.
As to Bourbaki, would Pierre Cartier be worth consulting?
@Noam #13, the quote from MacLane given there suggests that what Bourbaki actually did was consider representable profunctors. Which is reasonable and important and all, but certainly not quite adjunctions.
Well, Pierre Cartier became part of Bourbaki much later than the 1948 issue at stake. Still, he might have some cue. As far as time frame of Kan’s paper 1958 and Tohoku 1957, the Kan’s paper has been written in 1957 and Tohoku mostly in 1955 when he was overseas (the content discussed with Serre in their letters, also the paper was long in redaction before acceptance, here ask Cartier) and Grothendieck did not see the Cartan-Eilenberg book when writing Tohoku (some of the things overlap) and write to Serre that he suspects that some of the things would presumably also be in Cartan-Eilenberg (I do not recall if he mentioned that he heard of manuscript or already of the book).
@Todd 17
His student Szabo also wrote a book, Algebra of Proofs, which I had found very helpful
Coincidentally, I have a copy of that book out from the library right now. However, I’m having a lot of trouble making it through his notation and terminology. I don’t suppose you could share a “guide to the highlights” or a “terminology cheatsheet” matching up his words with ones that I might be more familiar with?
I can try. Mostly I had found it helpful as a guide to presenting free categorical structures via Lambek equivalence on sequent derivations, and the cut-elimination procedure. (The stuff on putting derivations into normal form is where people have noted serious mistakes.)
I don’t have the book though. Maybe the closest university has a copy, but … would it be possible to send me a photocopy of a representative page or two where you’re having trouble?
@#21: Szabo has two papers related to the material in his book in NDJFL that probably parse more easily:
@parallel thread: concerning the errors you can check out the remarks (p.vi,27) in
I’ll see what I can do. Presenting free categorical structures with sequent calculus, and in particular exactly what kind of “commutative conversions” you have to impose on the derivations, is exactly what I want to understand better. I feel like I understand the analogous thing for “natural deduction” style theories much better, where the equations you have to impose are beta-eta sort of reductions.
I’m not sure what is quite the right thread, but not long ago there was some push-back against usage of the term “centipede mathematics”, such as expressed to some extent in #5.
Like the term “evil”, the connotations of this phrase could be easily misunderstood outside a small community which has adopted it.
While I think “reverse mathematics” is taken, I think maybe there could be an article “abstraction” which includes the specific connotations mentioned in the article centipede mathematics and some other ones as well. The word “abstraction” is at least unobjectionable and surely has some objective meaning, and so I’ve written up a little something and put it on my web for consideration for exportation to the nLab – it includes the current text for centipede mathematics. I envision the inclusion of more illustrative quotes.
This is really nice; thank you Todd! I would support putting this on the main nLab and redirecting centipede mathematics to it.
Yes, I agree with Mike about putting it on the main nLab.
Some things to think about:
Should we take ’abstraction’ and ’generalization’ as equivalent? There’s certainly a way to generalize via abstraction, but is that the only way? Can’t I just extend a treatment to a larger domain. Also, in Hegelian-Lawverian spirit, we’ve been looking at the combinations general/particular abstract/concrete at abstract general, concrete general and concrete particular.
There’s a connection between abstraction and how people around here have been trying to use ’synthetic’, as in ’synthetic homotopy theory’ or ’synthetic quantum field thoery’ and three Cafe posts by Mike. So do we try to make the connection?
There are also close entries such as concrete structure (subtitled ’concrete and abstract structure’) to link to.
Okay, centipede mathematics now redirects to abstraction (i.e., I renamed the former to the latter, and added the new text). Thanks for the feedback, guys.
Clearly there is more work to be done. I am certainly open to re-examining the (apparent or implicit) equation between abstraction and generalization. In fact all of David C.’s comments are worth considering.
In the centipede mathematics section, I inserted the word ’extant’ because I think that’s crucial. It’s not that we’re starting all over again, but experimenting with things already there.
Now that we have a newish article, I think it might be worthwhile rethinking the description of reverse mathematics as a branch of centipede mathematics. I am skeptical that’s accurate, and maybe “reverse mathematics” deserves its own section (it has its own article of course).
Oh, one more thing: how do people feel about that photo? :-)
The photo is not great.
David R., I think Zoran might feel similar distaste about the photo (and maybe for the term ’centipede mathematics’). It was probably originally included just for fun.
I’ve added to abstraction a few more illustrative quotes, with references, and also included some related entries suggested by David C. in #27.
With regard to ’synthetic’, maybe we could talk about that some more (with a view towards an nLab article, perhaps contrasting ’synthetic’ with ’analytic’ as these terms are used in philosophy and elsewhere). Usually, when thinking about this, my default example is synthetic vs. analytic geometry, where analytic geometry refers to a reduction of geometry to coordinate algebra, and synthetic geometry refers to axiom systems where ’point’, ’line’ etc. are primitive or undefined (so not defined via reductions to something else). Similarly, one could look upon manifolds as defined analytically (in terms of coordinate patches etc.), or instead give axioms for categories (of manifold-like objects) as is done in synthetic differential geometry.
Beyond this, I’m not sure how others understand these terms, or how this is supposed to relate to the traditional analytic-synthetic distinction in philosophy as described here.
Yeah, let’s get rid of that photo. Not only is it weird, but it doesn’t really fit the overall style of the lab.
I agree that abstraction is not the same as generalization. Going from Lebesgue integration on to Henstock integration is a “generalization” in the sense that it integrates strictly more functions, but I would say that Lebesgue integration is the more abstract, since it applies also to other measure spaces.
As to whether reverse mathematics is a branch of centipede mathematics, I would say it’s just a matter of how you define the latter. If it means narrowly “removing axioms from a definition”, then including reverse mathematics is a stretch. But it does feel similar in the sense of “pulling off pieces” from a theory.
Todd wrote
with a view towards an nLab article, perhaps contrasting ’synthetic’ with ’analytic’ as these terms are used in philosophy and elsewhere
We do have analytic versus synthetic. It’s amazing how many bits and pieces there are out there, but then hopefully as time goes on, a phase of reconciling entries occurs.
That entry is mostly about the mathematical senses. Even there debate is possible, and in fact was actual down at the conference in Bristol the other week. Andrei Rodin was reminding us of the earlier sense as used by the Greeks when presenting proofs. Descartes probably picked up something of that, but then ’analytic’ took on the sense of coordinate-based.
As for the philosophical sense, I have a student working on the shifting meanings of the distinction. Again, another very complicated story.
We also have synthetic mathematics and synthetic geometry!
“Reverse Mathematics” - Dzhafarov and Mummert, 500p., book ad, youtube. Might be good.
1 to 33 of 33