You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
(=_=) (Mar 31 2020 at 12:43):Bobby T said:
let's say I'm comfortable talking about group theory, but know nearly nothing about topology as such. If I'm being taught about limits and the first example is from group theory, but the second is about topological spaces, I might just not catch the pattern, and then it becomes harder to follow everything. If that happens enough, you might just throw your hands up and say "it's abstract nonsense!"
There are plenty of detractors of CT I've met who work in group theory, which is funny because they do use homological algebra. I think it's because many workers in that area work on very specific concrete problems that may not need the level of abstraction that CT offers.
Morgan Rogers (he/him) (Mar 31 2020 at 14:30):Personally, resistance to CT has always felt like the an echo within mathematics of the inertia that exists at all levels of society against new ways of understanding things that are already familiar. People don't realise when what they're doing is "secretly" category theory because category theory feels foreign to them.
My own solution to this issue as a researcher is twofold. First, to work long and hard enough that one catches a big fish: a result which has eluded algebraists or geometers or number theorists working classically, but whose obstacles are circumvented by the abstraction of category theory. Rehashing known results or categorifying classical methods and proofs is (usually) straightforward but necessary and time-consuming work even once the "right" abstract context has been identified. It's only after that has been done that one can leverage the advantages of the more abstract framework, which is why until the net gets pulled in, mathematicians in the target fields are difficult to sway.
The second aspect is to teach and share the joy of category theory with any keen young mathematician, computer scientist, or student in another discipline. Categories abound, but it is only by introducing them to students and budding researchers that the necessary work mentioned above can be completed, in order for them to emerge (and ultimately be taught) as the modern foundation of mathematics that many of us in this community believe they should be.
Bobby T (Mar 31 2020 at 15:57):The second aspect is to teach and share the joy of category theory with any keen young mathematician, computer scientist, or student in another discipline.
As a keen young student from another discipline, I'm all in favor :grinning_face_with_smiling_eyes:
John Baez (Mar 31 2020 at 16:28):Jules wrote:
Reasoning with points is definitely partly cultural, but I have a strong feeling that it's also partly innate as well - reasoning without points and only with morphisms feels like an "unnatural" thing that needs to be learned and practiced, to me.
If your mental image of a morphism is a function of some sort between sets with some structure, then it's indeed unnatural to reason without using points - at least if you imagine a set as made of points, as most of us do. But if you think of a morphism as an action like "pour water in the pot", "put the carrots in the pot", etc., then we naturally reason using composition and tensoring of morphisms without points. So, it's good to teach people examples of categories where the morphisms aren't functions!
John Baez (Mar 31 2020 at 16:28):Applied category theory is actually very good for this.
John Baez (Mar 31 2020 at 16:33):Bobby wrote:
As someone who's come into this field with a pretty limited maths background, I think that there are probably two main reasons why category theory can get a bad rap:
I agree with those.
I think the psychological reason many people dislike category theory is that it makes them feel dumb. This is also the reason many people dislike mathematics. In this way category theory is a kind of "metamathematics": it's a kind of mathematics that even makes mathematicians feel dumb.
John Baez (Mar 31 2020 at 16:34):One reason people feel dumb when learning category theory is that it forces you to think in new ways. You have to literally rewire your neurons, and this creates a kind of ache in the mind.
John Baez (Mar 31 2020 at 16:35):I tell people that this ache is good, not bad.
John Baez (Mar 31 2020 at 16:35):Of course you have to stop after a while and relax and let it soak in while you're doing something else.
John Baez (Mar 31 2020 at 16:36):Another reason category theory makes people feel dumb is that (like most math) it's often poorly explained.
sarahzrf (Mar 31 2020 at 16:38):one of these days i need to commit my yoneda lecture to paper
sarahzrf (Mar 31 2020 at 16:38):it seems to work quite well
John Baez (Mar 31 2020 at 16:39):Another reason is that category theorists use phrases like "just", as in "the Eilenberg-Moore category of a monad is just a lax equalizer". This sort of phrase always means: "once you understand things this new way, it will allow you to see what you knew in as a special case of something that's simple in its own way." But it makes you feel dumb at first.
sarahzrf (Mar 31 2020 at 16:40):i do think there's an extent to which "just" has a technical meaning when used by category theorists, but i also think that it's just a bad choice of word for that a lot of the time too, and like...
sarahzrf (Mar 31 2020 at 16:41):i think there's also some fluidity between "expressing a useful alternate point of view" and "being dismissive"
sarahzrf (Mar 31 2020 at 16:42):and the fact that "just" is a word of choice exacerbates that fluidity
sarahzrf (Mar 31 2020 at 16:43):personally, i often like to say "precisely" or "exactly" instead of "just" if i wanna point out that things are the same, and try to reserve "just" for if i really am trying to communicate that i expect the listener to feel some kind of relief or "oh hey that's simpler!"
John Baez (Mar 31 2020 at 16:48):Often people use "just" when they are feeling relief or "oh hey that's simpler!" But their listener often doesn't feel this relief. At least, not for a few days.
sarahzrf (Mar 31 2020 at 16:51):this is true
sarahzrf (Mar 31 2020 at 16:52):ive for sure said shit before, or occasionally, when exercisign good judgment, caught myself before saying shit, like "X is just Y!" when a connection clicks when i know for a fact that more people understand X than Y
Vinay Madhusudanan (Mar 31 2020 at 17:13):sarahzrf said:
one of these days i need to commit my yoneda lecture to paper
it seems to work quite well
Is this available online somewhere? I'm studying the Yoneda lemma right now so that'd be super helpful.
sarahzrf (Mar 31 2020 at 17:14):it's not sorry
sarahzrf (Mar 31 2020 at 17:14):just a schtick i've delivered to people a few times
Vinay Madhusudanan (Mar 31 2020 at 17:14):Oh, okay. Then I do hope you write it up soon!
sarahzrf (Mar 31 2020 at 17:14)::)
Michael Zargham (Mar 31 2020 at 17:20):John Baez said:
If your mental image of a morphism is a function of some sort between sets with some structure, then it's indeed unnatural to reason without using points - at least if you imagine a set as made of points, as most of us do. But if you think of a morphism as an action like "pour water in the pot", "put the carrots in the pot", etc., then we naturally reason using composition and tensoring of morphisms without points. So, it's good to teach people examples of categories where the morphisms aren't functions!
As someone coming to this area with more of controls and signal processing background, a lot of my intuition already comes from composition. The wiring diagrams look a lot like formal generalizations of block diagrams which represent compositions. Is there anyone else from such a background and do they have commentary on the experience, as it compares to someone starting from reasoning about categories in terms of maps in point set topology?
John Baez (Mar 31 2020 at 17:24):A very good introduction to the Yoneda Lemma for beginners is the 3-part blog post starting here:
Make sure to also read parts 2 and 3, "The Yoneda embedding" and "The Yoneda Lemma".
Bobby T (Mar 31 2020 at 17:26):I completely second that! Everything by Tai-Danae Bradley has been super helpful to me!
Michael Zargham (Mar 31 2020 at 17:28):John Baez said:
A very good introduction to the Yoneda Lemma for beginners is the 3-part blog post starting here:
- Tai-Danae Bradley, The Yoneda perspective.
Make sure to also read parts 2 and 3, "The Yoneda embedding" and "The Yoneda Lemma".
"mathematical objects are completely determined by their relationships to other objects."
This statement is wonderful but also interesting in that complex systems science takes this as an assumption about the world without necessarily having formal support for the claim, and in particular model based systems engineering practice also requires this assumption (again irrespective of its formal support).
It is compelling that this is a basic result of CT.
David Egolf (Mar 31 2020 at 18:25):John Baez said:
I think the psychological reason many people dislike category theory is that it makes them feel dumb. This is also the reason many people dislike mathematics. In this way category theory is a kind of "metamathematics": it's a kind of mathematics that even makes mathematicians feel dumb.
This makes sense. However, I find that category theory interests me at least partially because it makes me feel dumb. I prefer to think of it as providing a sense of wonder: there is so much more to math than I thought, and it's all so much more connected than I guessed.
ishi crew (Mar 31 2020 at 21:09):I have a very low understanding of CT but had read discussions in old books and papers by N Rashevsky and R Rosen in theoreticl biology, and P Kainen and Ehresmann in neuroscience, and looked up a few things by S MacLane and had a paper given to me by an ex-grad student of Lawvere. I am mostly interested in applications to ecological, chemical reaction, economic, and social networks, but i am more familiar with the approach to these using graph theory and statistical physics. The 'dialect' of CT is quite different --it may be like learning how to build a rocket when all you need is a bicycle.
John Baez (Mar 31 2020 at 21:19):If you're doing just fine without category theory, carry on!
Jules Hedges (Mar 31 2020 at 21:51):A colleague of mine used a very similar phrase for exactly the same thing, "using a space shuttle to get to the second floor", I think it's great
Jules Hedges (Mar 31 2020 at 21:54):That being said, I always recommend 7 Sketches in Compositionality by Brendan Fong and David Spivak (a book, but also free on arXiv) for getting started from an applied motivation
Michael Zargham (Mar 31 2020 at 21:58):it's all about marginal costs... i could take a space shuttle to the moon, but if I can have a worm hole generator, i'd probably test it by going to the moon before I used it to go to alpha centauri. (here CT is the worm hole generator)
Speaking of which, @John Baez again provided the answers i sought above by providing more mappings of CT to concepts dynamical systems and control engineers know well with this: https://arxiv.org/pdf/1504.05625.pdf and I am cutting my teeth on analogue circuits because they already have wiring diagrams and I already know how to make filters and controllers by composing primitive processes.
Circuits and signal processing are great entry points for engineers (as opposed to mathematicians and computer scientists) to CT. I am firmly of the opinion (now) that we need CT in Cyberphysical Systems precisely because of the challenge of composing higher and higher order systems with less and less control of the associated subsystems. At that point the only thing you can hope to model (or design) is structure.
Today's big realization (conjecture, actually) is that Lyapunov stability can be thought of as the property that the system's structure is isomorphic to a passive system with the Lyapunov function as its notion of energy.
(=_=) (Apr 01 2020 at 00:59):@Morgan Rogers said:
Personally, resistance to CT has always felt like the an echo within mathematics of the inertia that exists at all levels of society against new ways of understanding things that are already familiar.
As William Gibson once put it, "The future is already here — it's just not very evenly distributed". You can see it in the reactions to the current pandemic as well.
People don't realise when what they're doing is "secretly" category theory because category theory feels foreign to them.
The best thing is when algebraic geometers are resistant to category theory: like, your entire discipline is full of category theory for goodness sake!
I think what people feel foreign about is CT for CT's sake. Homological algebra is part of CT, but most people don't think that, because it feels like a concrete calculating tool.
And this isn't restricted to CT either. Set theory has the same problem: you literally use set-theoretic notation every day, and yet most people don't care for set theory itself.
John Baez (Apr 01 2020 at 01:03):In the case of set theory, a lot of what set theorists study involve ways in which ZFC doesn't determine all the properties of "the" universe of sets, which is precisely what most mathematicians would rather not hear about.
(=_=) (Apr 01 2020 at 01:06):John Baez said:
In the case of set theory, a lot of the stuff that set theorists study are ways in which ZFC doesn't determine all the properties of "the" universe of sets, which is precisely what most mathematicians would rather not hear about.
You can phrase it as avoidance. The alternative view is this: that set theorists haven't produced any striking examples that are commonplace enough that most mathematicians' work would be adversely and unavoidably affected.
(=_=) (Apr 01 2020 at 01:07):The same goes for CT. If I'm an analyst -- hypothetically, of course, I couldn't produce an estimate if my life depended on it -- does CT give me tools for my specific research problems that I couldn't have obtained otherwise from a deeper study of analysis? We both know someone for whom the answer is: No.
(=_=) (Apr 01 2020 at 01:09):To continue in this vein, here's a question: In another thread, you mentioned your work on entropy that involves some good old-fashioned analysis. Could that analysis have been replaced with CT? If so, how? If not, why not?
(=_=) (Apr 01 2020 at 01:16):@John Baez said:
I think the psychological reason many people dislike category theory is that it makes them feel dumb. This is also the reason many people dislike mathematics. In this way category theory is a kind of "metamathematics": it's a kind of mathematics that even makes mathematicians feel dumb.
This is why I feel that I really need to challenge this view. Detractors of CT feel dumb on a regular basis: that's literally part and parcel of doing maths. So why does this instance of feeling "dumb" put them off?
John Baez (Apr 01 2020 at 01:20):Rongmin wrote:
"The alternative view is this: that set theorists haven't produced any striking examples that are commonplace enough that most mathematicians' work would be adversely affected."
That's probably how it feels to lots of mathematicians. Here's a question: suppose an abelian group has the property that every short exact sequence of abelian groups
splits. Is necessarily free?
The answer to this question is independent of ZFC. So, a certain line of research in algebra is blocked until we choose axioms extending ZFC that settle this question, and hopefully others, one way or the other.
But it seems not many algebraists are motivated to dig in this direction. For one thing, it would require a lot of work!
John Baez (Apr 01 2020 at 01:22):"In another thread, you mentioned your work on entropy that involves some good old-fashioned analysis. Could that analysis have been replaced with CT? If so, how? If not, why not?"
I have no idea! This result involved a blend of category theory and analysis. It was so hard to prove that when we were done we were just happy we succeeded. We didn't try to find another proof.
(=_=) (Apr 01 2020 at 01:25):John Baez said:
The answer to this question is independent of ZFC. So, a certain line of research in algebra is blocked until we choose axioms extending ZFC that settle this question, and hopefully others, one way or the other.
But it seems not many algebraists are motivated to dig in this direction. For one thing, it would require a lot of work!
Yup, and unless that work is rewarded, it won't be done, or you'll get workarounds.
In real life, if a certain line of research is blocked, people will route around it and ignore it. At least the career-minded ones would.
(=_=) (Apr 01 2020 at 01:28):John Baez said:
This result involved a blend of category theory and analysis. It was so hard to prove that when we were done we were just happy we succeeded. We didn't try to find another proof.
Let me rephrase my question so that it's clearer: is there a way for you to translate the analysis you've done into CT terms? Not another strategy or another approach, but just rewriting all the analysis you've actually done in the language of CT.
John Baez (Apr 01 2020 at 01:38):It sounds hard. I never considered doing it.
John Baez (Apr 01 2020 at 01:44):Tom Leinster has a nice categorical approach to Lebesgue integration, so it's possible one could take large chunks of real analysis and make them more categorical.
Eduardo Ochs (Apr 01 2020 at 01:47):Vinay Madhusudanan said:
sarahzrf said:
one of these days i need to commit my yoneda lecture to paper
it seems to work quite wellIs this available online somewhere? I'm studying the Yoneda lemma right now so that'd be super helpful.
Hi Vinay, take a look at this too...
http://angg.twu.net/math-b.html#notes-yoneda
It's about the gory details .
Gabriel Goren Roig (Apr 01 2020 at 02:23):Vinay Madhusudanan said:
Hi Gabo! What sort of undergraduate degree is seven years long… on the average? And if it has an inflexible curriculum, which aspect makes the time vary about the average?
(This is not very on-topic now that the conversation has been moved from "Introduce Youerself!" to "learning CT", but I'm answering here because I don't know where else I would and also I find it fun to share how different our degree system is. Ignore this if you don't care about university in Argentina!)
Hi! It's as @Rongmin Lu points out (I feel understood!). Our system is similar to the pre-Bologna European one, or so they say. It might sound weird: for engeneering, for example, the degree is literally "Engineer". For most disciplines, the standard degree is the Licentiate degree, but its length also varies from one discipline to the other. In my case, the Physics Licentiate degree is 6 years in paper, though the usual is 7.
There are many reasons why the time varies, but as a clarification, what I meant by "inflexible curriculum" is that you have almost no choice about what classes you must take, and not that you are required to complete the degree in a fixed amount of time (which you aren't). I would say the main reason for the variability is that most classes have very hard final exams, which you are not required to take at the end of the semester. Instead, you can take them any time as soon as you pass the rest of the class. It's almost universal for people to accumulate some of those, because you need a lot of time to prepare well for them and there's a balance to be kept between how much "final debt" you have and how good you want your grades to be. Keep in mind that for all these classes I'm referring to, the final exam determines 100% of your grade.
There are other things too, such as the fact that there's no tuition of any sort for undergraduate degrees (at least for public universities, which are the only ones you'll care about anyway if you're interested in Physics or Mathematics). All in all it's a different world around here :slight_smile:
Gabriel Goren Roig (Apr 01 2020 at 02:30):@Rongmin Lu and @Bobby T : Thanks for the kind words! I actually feel like I will understand stuff if I put serious time on it, especially given the nice resources that are available now such as Paolo Perrone's notes and Seven Sketches---it's more like feeling frustrated because of never finding time for it, or having my energy consumed by other things that I'd rather not be studying. I think I just need more time working through stuff on my own. Having a nice community here might make it more enjoyable though!
Gabriel Goren Roig (Apr 01 2020 at 02:47):Bobby T said:
Also, I also got interested in category theory partly from an interest in complex systems! We should set up a stream if there isn't one already!
Cool! About setting up a complex systems stream, my current understanding is that a lot of the work currently going under the name of Applied Category Theory would fit pretty well the name "complex systems from a CT viewpoint". So I'm not sure what could be the purpose of a separate stream. Perhaps I could see a need for translating questions and ideas back and forth between some established "complex systems" vocabulary and ACT, but I'm not sure. In any case @Jules Hedges 's question at #applied category theory -> "measuring non-compositionality" seems crucial to developing that relationship
sarahzrf (Apr 01 2020 at 02:50):Vinay Madhusudanan said:
Oh, okay. Then I do hope you write it up soon!
okay i actually did go and start working on writing it up a while after you suggested
sarahzrf (Apr 01 2020 at 02:50):although i wouldn't hold your breath, i lose focus on things suuuper easily :sob:
sarahzrf (Apr 01 2020 at 02:52):Screenshot_2020-03-31_22-35-20.png
heres the imagery ive ended up liking for presheaves after a few times around explaining yoneda :-)
sarahzrf (Apr 01 2020 at 02:52):well, that particular diagram is maybe not the best possible illustration of it, but
Robert Smart (Apr 01 2020 at 03:35):Wow. When I was looking for a proof of the Yoneda Lemma that was clear enough for me to implement, the best I found was by the Unapologetic Mathematician (https://unapologetic.wordpress.com/2007/06/06/yonedas-lemma/). This doesn't include the naturality conditions that are not always regarded as being part of the lemma proper. It ends with the claim that the two procedures it constructs are "clearly" inverses. I hope that means that I can assert that and the compiler will auto verify it. That should be the definition of "clearly" for some definition of "compiler".
sarahzrf (Apr 01 2020 at 03:48):main.pdf
here's what i've written up so far—mostly an explanation of the idea of what a presheaf is, not so much touching on yoneda at all yet
id guess this is probably like a third of the way into my usual schtick
sarahzrf (Apr 01 2020 at 04:02):all else aside, i am not going to fucking rest until it is standard pedagogical practice to use this kind of description for explaining what a presheaf is
sarahzrf (Apr 01 2020 at 04:03):hahahaaaaa i just opened the nlab page on "presheaf" to double check that this isn't how they explain it for some reason, saw that this explanation actually does exist over on "space and quantity" and remembered that id seen that before, and oops of course the citation is lawvere
sarahzrf (Apr 01 2020 at 04:04):how have i barely read any of his actual work
(=_=) (Apr 01 2020 at 04:24):John Baez said:
It sounds hard. I never considered doing it.
Exactly. That's probably how the thought process of many analysts who've encountered CT ended. They may play around it for a while, but once they got around to considering what I've just asked you to consider, they'd inevitably come to the same conclusion you just did: it sounds hard.
And that's why people avoid CT. Not because it's hard, but because it doesn't offer any clear advantage over the tools they currently have in their field. Yet.
(=_=) (Apr 01 2020 at 04:25):John Baez said:
Tom Leinster has a nice categorical approach to Lebesgue integration, so it's possible one could take large chunks of real analysis and make them more categorical.
That's a nice start, but that's only the chunk related to Lebesgue integration. Most analysts would probably only be convinced once you can do the - argument in CT, and probably only if it's sleeker than the old style.
(=_=) (Apr 01 2020 at 04:39):Gabriel Goren said:
This is not very on-topic now that the conversation has been moved from "Introduce Yourself!" to "learning CT"
Funny how that happened.
It's as Rongmin Lu points out (I feel understood!). Our system is similar to the pre-Bologna European one, or so they say.
De nada. :sweat_smile:
Your system follows the pre-Bologna Spanish system, which is similar to the other systems in continental Europe. In particular:
There are other things too, such as the fact that there's no tuition of any sort for undergraduate degrees
I'm not sure which sense of tuition you meant here -- fees, or classes outside of lectures -- but that's true in Germany AFAIK. The final exam determining 100% of your grade was also true in the old continental system, and perhaps even of the Oxbridge universities.
(=_=) (Apr 01 2020 at 05:04):@Gabriel Goren said:
Perhaps I could see a need for translating questions and ideas back and forth between some established "complex systems" vocabulary and ACT, but I'm not sure. In any case Jules Hedges 's question at #applied category theory > measuring non-compositionality seems crucial to developing that relationship
I think that's a nice topic to set up: a dictionary between current complex systems terminology and ACT. I don't know much about the study of complex systems and would like to learn more.
John Baez (Apr 01 2020 at 05:43):Most analysts would probably only be convinced once you can do the ϵ-δ argument in CT, and probably only if it's sleeker than the old style.
Probabily true. Just to be clear: I wasn't mentioning Tom's idea as something that would convince anyone to change how they do anything. I just think it's a cool result.
(=_=) (Apr 01 2020 at 07:46):John Baez said:
I wasn't mentioning Tom's idea as something that would convince anyone to change how they do anything. I just think it's a cool result.
Agreed, but it'd be nicer if more people worked on this neglected aspect of CT. Either to develop the capability, or to hit a brick wall so that we can reasonably say, "Well, that's something CT can't do".
Matteo Capucci (he/him) (Apr 01 2020 at 09:50):I believe it's misleading to think CT can be useful to (say) analysts only if we are able to prove estimates using categorical tools. That's actually the most useless way CT could enter a field, because it doesn't add anything new and it recasts everything in a language most people there don't understand, let alone master. Eventually, people will 'meh' it and go back to their usual methods.
What CT is great at is unraveling patterns. This enables cross-pollination between subjects, and that's where we should go looking for new results. If I can show the analyst I can open new fronts to attack a problem, using ideas from analogous but not-yet-related parts of math, this might at least sound like honest, working mathematics, and not just general abstract nonsense.
Joachim Kock (Apr 01 2020 at 10:33):Rongmin Lu said:
Most analysts would probably only be convinced once you can do the - argument in CT, and probably only if it's sleeker than the old style.
Here is an - argument in category theory. I don't think it will impress analysts, though!
Let be the category of finite sets. It plays the role of the ground field for objective linear algebra. For any set (possibly infinite), the slice category plays the role of the free vector space spanned by $S$, and the presheaf category plays the role of the profinite-dimensional vector space of functions on . The profinite structure comes from the fact that since is the inductive limit of its finite subsets , the function space is the projective limit of the finite function spaces . Continuity with respect to the profinite topology means to preserve these projective limits. Use Greek letters to denote finite sets.
PROPOSITION. A linear functor is continuous if and only if for every there exists such that factors through via the projections and .
This is from the paper [Gálvez-Kock-Tonks, Homotopy linear algebra]. (The 'homotopy' in the title refers to the fact that all this works the same for -groupoids instead of sets.) 'Linear functor' means sum-preserving. These are representable by spans, in the same way as in ordinary linear algebra linear maps can be expressed as matrices.
Nathaniel Virgo (Apr 01 2020 at 10:43):sarahzrf said:
main.pdf
here's what i've written up so far—mostly an explanation of the idea of what a presheaf is, not so much touching on yoneda at all yet
id guess this is probably like a third of the way into my usual schtick
Cool. So a presheaf can be seen as a profunctor to (or is it from?) the terminal category. I'm looking forward to the rest of these notes.
Vinay Madhusudanan (Apr 01 2020 at 12:17):@sarahzrf @Eduardo Ochs Thank you, thank you! Really helpful.
@sarahzrf The presheaf idea is new to me (I've seen the word before and seen some definition whose import I couldn't understand at the time, but that's it). Waiting for more!
Vinay Madhusudanan (Apr 01 2020 at 12:22):@Gabriel Goren Even my bachelor's offered no choices in the curriculum, but it was only three years. The examination pattern (especially the 100% weighted final) also sounds strange indeed. Can't help wondering what the implications are in terms of how effective it is — I suppose only really interested students take up these courses? (Which is not the case here)
(=_=) (Apr 01 2020 at 13:22):Matteo Capucci said:
I believe it's misleading to think CT can be useful to (say) analysts only if we are able to prove estimates using categorical tools. That's actually the most useless way CT could enter a field, because it doesn't add anything new and it recasts everything in a language most people there don't understand, let alone master. Eventually, people will 'meh' it and go back to their usual methods.
What CT is great at is unraveling patterns. This enables cross-pollination between subjects, and that's where we should go looking for new results. If I can show the analyst I can open new fronts to attack a problem, using ideas from analogous but not-yet-related parts of math, this might at least sound like honest, working mathematics, and not just general abstract nonsense.
You need both, and Grothendieck is the historical example. CT probably enabled him to transfer the thinking in functional analysis, which he acquired while working under Schwartz and Dieudonne, into algebraic geometry.
(A brief timeline:
This cross-pollination changed the face of algebraic geometry, but it also recast the tools of algebraic geometry in a language that many people there today still don't fully understand. On top of that, it improved those tools and corrected errors that were generated by the previous techniques.
Algebraic geometers could have said "meh" and carried on with their old intuitive techniques, but they didn't, because their old tools had been replaced with better ones. That's why they couldn't have said "meh".
I don't see the prospect of CT doing that for analysis yet, because the current tools are pretty rigorous and powerful, and what CT can do now seems to pale in comparison.
(=_=) (Apr 01 2020 at 13:27):What some analysts (and some group theorists, and other detractors) who are engaged in research into concrete problems don't really appreciate about CT is that they don't really feel that the capabilities of the tools in their domain have been exhausted yet to justify bringing in the big machinery of CT. They don't see the need for "cross-pollination between subjects", because many of them don't work between subjects.
As John Baez said upstream:
If you're doing just fine without category theory, carry on!
I agree.
But I'd argue it's still a big gap in our knowledge if we can't (or don't know if we can) simulate analysis using CT. I'm probably woefully under-informed, since Joachim Kock just contributed a reference upstream, but then perhaps if we can somehow already do analysis using CT, it's not really common knowledge and perhaps we should make that knowledge more common.
(=_=) (Apr 01 2020 at 14:08):@Joachim Kock said:
Here is an - argument in category theory. I don't think it will impress analysts, though!
I would clarify that I meant the reformulation of the standard - argument in category-theoretic terms, but I think what you have in that paper is pretty impressive -- to me, anyway. That makes me hopeful.
John Baez (Apr 01 2020 at 15:15):Category theory can be good in figuring out patterns and straightening out concepts in analysis. One very simple and fundamental example: instead of metric spaces, it's often better to use Lawvere metric space.
Morgan Rogers (he/him) (Apr 01 2020 at 15:24):Rongmin Lu said:
And that's why people avoid CT. Not because it's hard, but because it doesn't offer any clear advantage over the tools they currently have in their field. Yet.
cf my "big fish" comment earlier. Rehashing the basics of (in this example) analysis is time-consuming work that yields few initial rewards in terms of new results until it's complete. Like how one can't put on a performance at a theatre until it's built.
(=_=) (Apr 01 2020 at 17:15):Morgan Rogers said:
cf my "big fish" comment earlier. Rehashing the basics of (in this example) analysis is time-consuming work that yields few initial rewards in terms of new results until it's complete. Like how one can't put on a performance at a theatre until it's built.
I think I rehashed that here. :sweat_smile: I'm also reminded of Kevin Buzzard's exhortation to others to chip in to formalise known mathematical results in Lean or other automated theorem provers, so that there's a base on top of which more automated systems reasoning about mathematics can be built.
(=_=) (Apr 01 2020 at 19:30):I think I'd derailed this thread from its purported topic of "learning CT". I might shift the discussion to another topic.
John Baez (Apr 01 2020 at 19:32):You can shift the discussion starting at any comment...
(=_=) (Apr 01 2020 at 19:33):And I did. It's now "Resistance to CT".
sarahzrf (Apr 01 2020 at 19:45):bwahaha
John Baez (Apr 01 2020 at 19:45):Oh, good. Yes, everyone: you can retroactively decide a discussion has drifted from its original topic, and go back and change the topic starting where the digression began!
Jules Hedges (Apr 01 2020 at 19:45):I'll make the obvious "resistance is futile" joke before anyone else
John Baez (Apr 01 2020 at 19:45):You beat me by 3 seconds. :angry_devil:
sarahzrf (Apr 01 2020 at 19:45):resistance to CT is inversely proportional to current of CT
Stelios Tsampas (Apr 01 2020 at 19:47):Hah, that sounds about right!
Stelios Tsampas (Apr 01 2020 at 19:47):Also, the word "inertia" as used by @Morgan Rogers is accurate.
Fabrizio Genovese (Apr 01 2020 at 19:53):sarahzrf said:
resistance to CT is inversely proportional to current of CT
I lol'd.
(=_=) (Apr 02 2020 at 02:19):sarahzrf said:
resistance to CT is inversely proportional to current of CT
But unless CT is a superconductor, there will always be resistance.
So, how do you categorify a conductor and impose a -grading?
Mike Shulman (Apr 02 2020 at 03:14):A while ago, John Baez said:
suppose an abelian group has the property that every short exact sequence of abelian groups
splits. Is necessarily free?
The answer to this question is independent of ZFC. So, a certain line of research in algebra is blocked until we choose axioms extending ZFC that settle this question.
That's not how I would describe the situation. By analogy, let be a group and ; is it necessarily the case that ? The answer to this question is independent of the axioms of a group. But would you say that a certain line of research in group theory is blocked until we choose axioms extending the definition of a group that settle this question? Of course not; any particular person just has to choose whether they want to study abelian groups or nonabelian groups. That's the only thing it can possibly mean to "settle this question".
Similarly, the answer to the Whitehead problem is yes in some toposes and no in in others. That settles the question; now anyone can choose for themselves whether they want to work in Whitehead-toposes or non-Whitehead-toposes.
(=_=) (Apr 02 2020 at 03:32):That's a nice way to look at it, @Mike Shulman, thanks!
That's what I was referring to when I say people will look for workarounds.
The classical example is the insolubility of the quintic. Sure, now we have group theory and we can study groups and talk about every time we talk to the press.
However, there's another school that says, hang on, is this really a no-go theorem, the be-all and end-all on quintics, or can there be other ways of solving certain classes of quintics? It turns out the answer is yes.
When many people resist CT, they tend to think of the first approach: look at all the symmetries, isn't maths beautiful, blablabla. CT can do the second, of course, and many detractors take the second approach: more concrete and constrained problems. But these kinds of problems are not usually arenas where CT, right now, seems to perform as well as the existing domain-specific techniques.
The point I want to make is, why, and can we do better?
Mike Shulman (Apr 02 2020 at 03:39):Well, I wouldn't describe the situation as any kind of "workaround". To me the fact that there are both Whitehead toposes and non-Whitehead toposes is a beautiful discovery to be celebrated.
John Baez (Apr 02 2020 at 05:36):Mike wrote:
The answer to this question is independent of the axioms of a group. But would you say that a certain line of research in group theory is blocked until we choose axioms extending the definition of a group that settle this question? Of course not; any particular person just has to choose whether they want to study abelian groups or nonabelian groups.
But choosing that is exactly choosing axioms that extend the definition of group! You're either adding the axiom or its negation.
John Baez (Apr 02 2020 at 05:38):And in the case of groups we feel perfectly comfy with doing this. But when it comes to Whitehead's problem I fear most mathematicians would tend to say "oh, it's undecidable in ZFC, I won't mess with this issue any further". That's the way in which research gets blocked.
John Baez (Apr 02 2020 at 05:41):If my fear is misguided - if plenty of mathematicians are willing to extend ZFC with extra axioms to settle Whitehead's conjecture one way or another, or choose a topos in which the conjecture either holds or doesn't... well, then I'm happy to hear that!
John Baez (Apr 02 2020 at 05:44):In short, I don't see that we really disagree here.
(=_=) (Apr 02 2020 at 05:51):Mike Shulman said:
Well, I wouldn't describe the situation as any kind of "workaround". To me the fact that there are both Whitehead toposes and non-Whitehead toposes is a beautiful discovery to be celebrated.
Implying that workarounds can't be beautiful. Workarounds are frequently creative, because you need to think outside the box in order to bypass the roadblock.
(=_=) (Apr 02 2020 at 05:57):In fact, Grothendieck's metaphor of the rising sea is an accurate description of how a good workaround behaves, as well as the many workarounds in mathematics that have littered its history.
Mike Shulman (Apr 02 2020 at 14:06):@Rongmin Lu If you actually understand something at a deeper level, as in the rising sea, I would not describe the resulting solution as a "workaround".
Mike Shulman (Apr 02 2020 at 14:08):@John Baez I certainly agree that in practice mathematicians have trouble with this for ZFC. But I think it's important to emphasize that the problem is with their psychology, not with the mathematics, and not to imply that there's a "solution" out there that will tell us which of the two possibilities is "true".
Mike Shulman (Apr 02 2020 at 14:42):Maybe the latter isn't what you meant, but I think it would be easy to read "choose axioms extending ZFC that settle this question" that way.
John Baez (Apr 02 2020 at 16:06):Yes, this thread was about psychological resistance to category theory... and someone (Rongmin?) compared it to the psychological resistance that mathematicians have learning set theory beyond the basics. I feel the two cases are quite different, but still worth comparing. I raised Whitehead's Conjecture as an example of a question that could push algebraists into learning some serious set theory, but as far I can tell, for the most part hasn't.
For example, I don't see books on homological algebra saying "In this chapter we'll assume the axiom of constructiblity, so that implies is free and also..."
I'm sure someone must be doing research like this, but I feel it's not in the mainstream. My feeling is that for most algebraists, the perceived pain of learning serious set theory outweighs the perceived advantages of being able to march ahead exploring algebra in multiple axiom systems extending ZFC.
Nikolaj Kuntner (Apr 02 2020 at 16:58):I think the difference is that in general mathematics, axioms of group theory are understood to be chosen to fix a framework with many models/examples, while the axioms of set theory are understood to be chosen to do the opposite: Capture and thus pin down one example/model. Logical categoricity is in contrast to abstraction, and thus an abstract algebraist works in a different framework than a set theorist that fine-tunes his theory to his aesthetic.
The "real world" was pinned down by the logicans 100 years ago, promoted as providing the monic substance for other theories. This relation makes it so that their axioms of group theory or manifolds, etc. are not understood as expressions capturing mathematical objects out of the aether, but are seemingly just conditions that select from among the objects in the "real world." In other words, for the so called practical mathematician, to specify groups and other axioms at the beginning of a mathematical text is not conceiving mathematical objects in a broad sense, but instead the act of stating the axioms is merely the act of declaring the focus of the investigation at hand. In that mindset, to choose axioms which are known to concern the people who provided rules of set theory may seems as breaking away from the "real world," the actual mathematical truth.
Mike Shulman (Apr 02 2020 at 17:07):@Nikolaj Kuntner Yes. The problem is that that mindset is wrong. (-:
John Baez (Apr 02 2020 at 17:14):But I think it's important to emphasize that the problem is with their psychology, not with the mathematics, and not to imply that there's a "solution" out there that will tell us which of the two possibilities is "true".
Okay, fine. But I'm sick of emphasizing this, because it's so obvious to me and I've spent so much time trying to tell people this. I don't want to become a boring old fart who keeps saying the same thing over and over.
I mainly talk about the case of Peano arithmetic, where it's even harder to get people to accept that this has many different models just like the axioms for a group - and not one "true" model and a bunch of "nonstandard" ones, like the true king and a bunch of pretenders to the throne.
Johan Commelin (Apr 02 2020 at 17:18):Wait... and here I've always been thinking that is the one true group, and all others are pretenders...
John Baez (Apr 02 2020 at 17:25):Right! It's fun to imagine people thinking that the axioms of a group have one true model. Why do they do it for the axioms of set theory? Something about the foundations of mathematics drives people crazy - maybe it's the word "foundations". I prefer the word "entrances". A building can have many entrances.
Nikolaj Kuntner (Apr 02 2020 at 17:28):Well the people that go crazy at least must have had enough exposure to come to different conclusions. When it comes to foundational theories, I think the issue is not just that non-logic minded mathematicans think there is "one true" theory among others, but that people don't even think the others are notions that can be made concrete. E.g., that studying "set that can contain themselves" were similar to studying that one algorithm that solves the Halting problem.
Nikolaj Kuntner (Apr 02 2020 at 17:30):They don't want to Turing jump out of their own department.
Ryan Wisnesky (Apr 02 2020 at 19:55):@John Baez But people don't usually think about non-standard models of natural numbers, even though those also exist, at least in first-order logic. In second order logic, you can uniquely define the natural numbers as well as various set theories. In fact this happens all the time doing math in Coq, which is higher order.
Mike Shulman (Apr 02 2020 at 20:01):Personally, I think different models of Peano arithmetic inside a given topos are also less interesting than different toposes. The latter arise naturally in other areas of mathematics, whereas I don't know any such applications of the form.
Ryan Wisnesky (Apr 02 2020 at 20:12):That's a good illustration of how axiomatization is done to taste: sometimes I want to axiomatize a class of things, sometimes I want to axiomatize one thing uniquely. And whether I can get what I want depends not only on the 'things' in an intuitive sense, but on the logic and meta-logic I'm working in. FWIW, I think the resistance to CT from programmers stems not so much from the fact that the CT axioms are somehow harder to understand than say group theory, but that programmers would resist group theory as well, and since category theory is more applicable to functional programming that most other axiomatic algebraic theories, it is category theorists stuck bearing the burden of proof in that domain.
Paul Blain Levy (Apr 03 2020 at 00:42):John Baez said:
I mainly talk about the case of Peano arithmetic, where it's even harder to get people to accept that this has many different models just like the axioms for a group - and not one "true" model and a bunch of "nonstandard" ones, like the true king and a bunch of pretenders to the throne.
So despite not believing in the "true" model of PA, you do believe that PA is consistent. [Since you assert that it has "many different models".] That's a curious combination of scepticism and belief. I wonder what convinces you of Con(PA). Gentzen's proof by epsilon_0 induction, or the double negation proof that PA is consistent relative to Heyting arithmetic?
[This is off topic admittedly.]
(=_=) (Apr 03 2020 at 00:57):Paul Blain Levy said:
[This is off topic admittedly.]
Shhhhh... don't tip off the moderator. :sweat_smile:
(=_=) (Apr 03 2020 at 00:57):I think it's on-topic because apparently this thread is all about psychology, so it's a great place to talk about "scepticism and belief".
(=_=) (Apr 03 2020 at 01:04):That being said...
@John Baez said:
Yes, this thread was about psychological resistance to category theory... and someone (Rongmin?) compared it to the psychological resistance that mathematicians have learning set theory beyond the basics.
I want to push back on the notion that the resistance is psychological because:
(=_=) (Apr 03 2020 at 01:08):I think there's a productive conversation to be had about identifying the pragmatic reasons for resistance to CT, because it'd lead us to think about what CT can and can't do currently, so that we can identify areas for future work. I don't think it's productive to engage in armchair psychology.
Paul Blain Levy (Apr 03 2020 at 01:14):Some people are put off category theory by the size issues. And I can hardly blame them. The issues are more serious than many category theorists are willing to admit.
(=_=) (Apr 03 2020 at 01:15):Ryan Wisnesky said:
FWIW, I think the resistance to CT from programmers stems not so much from the fact that the CT axioms are somehow harder to understand than say group theory, but that programmers would resist group theory as well, and since category theory is more applicable to functional programming that most other axiomatic algebraic theories, it is category theorists stuck bearing the burden of proof in that domain.
Anecdotally, many programmers I know hate mathematics. For some reason, the way of thinking that we take for granted is very alien and uncomfortable to them, whereas the way of thinking that pays off in programming comes more naturally for them.
(=_=) (Apr 03 2020 at 01:16):Paul Blain Levy said:
Some people are put off category theory by the size issues. And I can hardly blame them. The issues are more serious than many category theorists are willing to admit.
I hear you. I recently gave a talk about Lawvere's fixed point theorem and some ultrafinitist in the crowd started peppering me with questions about size issues. Fun times. Admittedly, what was I thinking in giving that talk?!
Mike Shulman (Apr 03 2020 at 01:47):Paul Blain Levy said:
So despite not believing in the "true" model of PA, you do believe that PA is consistent. [Since you assert that it has "many different models".] That's a curious combination of scepticism and belief.
Why is it curious to believe that there are many of something but that no single one of them is particularly special?
I wonder what convinces you of Con(PA).
Perhaps the fact that it has many models? (-:O
(=_=) (Apr 03 2020 at 01:52):Mike Shulman said:
Rongmin Lu If you actually understand something at a deeper level, as in the rising sea, I would not describe the resulting solution as a "workaround".
A "workaround", as I understand it, is a bypass, or a routing, around an obstruction. We may eventually understand something deeper, the obstruction may eventually shrivel from a mountain to a pebble, but there is no denying the obstruction still remains in the examples that have come up. That's the rising sea.
Let's agree to disagree.
Mike Shulman (Apr 03 2020 at 01:56):Sure. Let me give one parting shot: a workaround is defined as "a method for overcoming a problem or limitation in a program or system." But when you deeply understand what is going on, it frequently happens that the situation is no longer viewed as a "problem" or a "limitation", but rather an opportunity to discover new realms of beautiful mathematics.
sarahzrf (Apr 03 2020 at 03:15):Rongmin Lu said:
Ryan Wisnesky said:
FWIW, I think the resistance to CT from programmers stems not so much from the fact that the CT axioms are somehow harder to understand than say group theory, but that programmers would resist group theory as well, and since category theory is more applicable to functional programming that most other axiomatic algebraic theories, it is category theorists stuck bearing the burden of proof in that domain.
Anecdotally, many programmers I know hate mathematics. For some reason, the way of thinking that we take for granted is very alien and uncomfortable to them, whereas the way of thinking that pays off in programming comes more naturally for them.
as a programmer, can second this anecdote, there's a lot to unpack
David Michael Roberts (Apr 03 2020 at 03:19):Rongmin Lu said:
I hear you. I recently gave a talk about Lawvere's fixed point theorem and some ultrafinitist in the crowd started peppering me with questions about size issues. Fun times. Admittedly, what was I thinking in giving that talk?!
ooh, cool. Can you give me more info privately? (I don't want to derail this conversation more than it has been ;-)
John Baez (Apr 03 2020 at 03:26):Ryan Wisnesky said:
John Baez But people don't usually think about non-standard models of natural numbers, even though those also exist, at least in first-order logic. In second order logic, you can uniquely define the natural numbers as well as various set theories. In fact this happens all the time doing math in Coq, which is higher order.
I think the notion that you can uniquely define the natural numbers in set theory is a kind of illusion. There's indeed a theorem saying that in ZFC there's a unique-up-to-isomorphism 'standard' model of the natural numbers - I'm not denying that. But there are many different models of ZFC, and if we look at the 'standard' model of the natural numbers in these different models we find that different sentences in the language of arithmetic hold. In short, the ambiguity has just been pushed back one notch.
A similar thing is true for second-order logic.
For much more on this:
John Baez (Apr 03 2020 at 03:39):Paul Blain Levy said:
So despite not believing in the "true" model of PA, you do believe that PA is consistent. [Since you assert that it has "many different models".] That's a curious combination of scepticism and belief. I wonder what convinces you of Con(PA). Gentzen's proof by epsilon_0 induction, or the double negation proof that PA is consistent relative to Heyting arithmetic?
There are several reasons to believe Peano arithmetic is consistent; you mentioned two, and a third more important one is that we haven't found an inconsistency yet. This is like why I believe that I can't fly by flapping my arms: I haven't succeeded yet.
But more importantly, I don't really need to believe in the consistency of PA: I just act like I do when I'm studying models of PA, so I don't have to keep saying "if PA is consistent, so that models exist..."
sarahzrf (Apr 03 2020 at 03:41):sometimes i wish nelson's inconsistency proof had gone through
sarahzrf (Apr 03 2020 at 03:41):just to shake things up
sarahzrf (Apr 03 2020 at 03:43):plus it would've been extra hilarious that he'd developed internal set theory and given these incredibly infinitary ultrapower-based models for it and then went on and broken something waaaay further down in the foundations
Paul Blain Levy (Apr 03 2020 at 05:02):Mike Shulman said:
Paul Blain Levy said:
So despite not believing in the "true" model of PA, you do believe that PA is consistent. [Since you assert that it has "many different models".] That's a curious combination of scepticism and belief.
Why is it curious to believe that there are many of something but that no single one of them is particularly special?
I don't find it curious in the case of groups, because I can see specific nonisomorphic examples of groups, such as S_4 and S_7. By contrast, I'm not aware of any examples of PA models other than those that are derived from my a priori belief (based on intuition) in the true model. This leaves me unable to understand why someone would believe in the existence of PA models without believing in the true model, unless they derive that belief from a prior belief in Con(PA), which prompted my question of where that belief would come from.
Paul Blain Levy (Apr 03 2020 at 05:46):John Baez said:
Paul Blain Levy said:
So despite not believing in the "true" model of PA, you do believe that PA is consistent. [Since you assert that it has "many different models".] That's a curious combination of scepticism and belief. I wonder what convinces you of Con(PA). Gentzen's proof by epsilon_0 induction, or the double negation proof that PA is consistent relative to Heyting arithmetic?
There are several reasons to believe Peano arithmetic is consistent; you mentioned two,
I did, but each of them would be seen as problematic by at least some finitists, those who accept only Primitive Recursive Arithmetic. By asking this question I was trying to probe your position. Since you find these proofs acceptable, I reckon that you accept PRA + epsilon-induction as valid, and also System T (i.e. PRA + higher-order functions). Right?
and a third more important one is that we haven't found an inconsistency yet
By this argument we should believe that the Goldbach conjecture is true but independent of PA, since we haven't found an inconsistency in PA + Goldbach, nor in PA + not-Goldbach.
Mike Shulman (Apr 03 2020 at 05:47):Since from one PA model you can construct many others, as soon as you believe in one PA model you must believe in lots of them. But once you realize that, it's natural to come to suspect that whatever PA model you started from might have been constructed from some other one, so there's no reason to expect it to be the "true" on either. (I believe this is a PA version of Hamkin's argument for the "Wellfoundedness Mirage" axiom of the set-theoretic multiverse.)
Compare to the theory of relativity. In Galilean physics we may imagine we are in the global rest frame and other frames of reference are moving with respect to us. But in Einsteinian physics we realize that the moving reference frames (at least the inertial ones) appear, to those inside them, identical to our global rest frame. Then it's hard to avoid taking the step of realizing that in fact there is no such thing as a "global rest frame", since from the perspective of other frames it is moving.
Mike Shulman (Apr 03 2020 at 05:50):Paul Blain Levy said:
By this argument we should believe that the Goldbach conjecture is true but independent of PA, since we haven't found an inconsistency in PA + Goldbach, nor in PA + not-Goldbach.
Note that to those of us who don't believe in one "true" model of PA, it doesn't even make sense to say that the Goldbach conjecture is "true" distinct from its provability.
sarahzrf (Apr 03 2020 at 06:08):(pedantic complaint: the lack of a rest frame works perfectly well in galilean relativity too)
sarahzrf (Apr 03 2020 at 06:09):(...or is that a point about galileo's conceptual framework? i don't know what he thought about absolute motion)
Mike Shulman (Apr 03 2020 at 06:15):@sarahzrf Doesn't that break when you introduce electromagnetism? Since all speeds in a moving Galilean frame are additive in the direction of motion, I thought that you could distinguish the global rest frame as the one in which the speed of light is the same in all directions. (Of course, I'm sure that various other things about electromagnetism also break in Galilean physics.)
sarahzrf (Apr 03 2020 at 06:16):oh, yeah it does
sarahzrf (Apr 03 2020 at 06:16):i was only thinking about mechanics
Paul Blain Levy (Apr 03 2020 at 06:21):Mike Shulman said:
Since from one PA model you can construct many others,
Yes. For example, ones that prove not-Con(PA).
as soon as you believe in one PA model you must believe in lots of them.
Yes. And where does that initial belief come from? From my intuition of the actual totality of natural numbers. I can just about imagine doubting that intuition. But then I would have no model, rather than many models, and Con(PA) would be thrown into doubt.
But once you realize that, it's natural to come to suspect that whatever PA model you started from might have been constructed from some other one,
I cannot understand this. Your sentence seems to assume that I did actually start with a PA model, i.e. I was not mistaken in thinking that I did. That your phrase "whatever PA model you started with" denotes. So let's call it the "true model". Or the "starting model" if it makes you happier.
so there's no reason to expect it to be the "true" on either.
Let me take this further. Does your multiverse of equally legitimate models include ones that validate not-Con(PA), even though you believe Con(PA)? Or does it include only models that validate the same sentences as the starting model, such as Con(PA)? (Your relativistic analogy appears to suggest the latter.) Or neither?
Paul Blain Levy (Apr 03 2020 at 06:26):Mike Shulman said:
Paul Blain Levy said:
By this argument we should believe that the Goldbach conjecture is true but independent of PA, since we haven't found an inconsistency in PA + Goldbach, nor in PA + not-Goldbach.
Note that to those of us who don't believe in one "true" model of PA, it doesn't even make sense to say that the Goldbach conjecture is "true" distinct from its provability.
Surely a finitist will say that a sentence that cannot be refuted in PRA is true.
John Baez (Apr 03 2020 at 06:54):@Paul Blain Levy wrote:
I did, but each of them would be seen as problematic by at least some finitists, those who accept only Primitive Recursive Arithmetic. By asking this question I was trying to probe your position. Since you find these proofs acceptable, I reckon that you accept PRA + epsilon-induction as valid, and also System T (i.e. PRA + higher-order functions). Right?
No, I never really rendered a judgement on whether these proofs are "acceptable". I don't know what it would mean for me to "accept PRA + epsilon-induction as valid". What does "acceptance" involve, exactly? Is this some sort of psychological state, or maybe a willingness to bet a lot of money on something? How would such a bet be settled? It's all too complicated for me. Luckily I don't feel I need to sort out these issues: they don't impact how I do math.
When I said this:
I mainly talk about the case of Peano arithmetic, where it's even harder to get people to accept that this has many different models just like the axioms for a group - and not one "true" model and a bunch of "nonstandard" ones, like the true king and a bunch of pretenders to the throne.
I wasn't trying to say I accepted something or not, or believed in some mathematical entity or not. I was all-too-briefly alluding to a project I have cooking on the back burner with Michael Weiss, here:
and here:
I haven't gotten far enough to give a really clear explanation yet.
sarahzrf (Apr 03 2020 at 07:03):tbh i personally find that mulling over that kind of issue produces super interesting math, which is certainly an impact c:
(=_=) (Apr 03 2020 at 07:44):@David Michael Roberts said:
Rongmin Lu said:
I hear you. I recently gave a talk about Lawvere's fixed point theorem and some ultrafinitist in the crowd started peppering me with questions about size issues. Fun times. Admittedly, what was I thinking in giving that talk?!
ooh, cool. Can you give me more info privately? (I don't want to derail this conversation more than it has been ;-)
Let's do it here. This conversation has already completely derailed into a discussion about finitism and other set-theoretic issues anyway. Also, I'd like the others to chip in with their comments.
So, ask away! Details will be a bit hazy because of the lag, but I did a second talk and size issues cropped up again.
(=_=) (Apr 03 2020 at 07:52):Mike Shulman said:
Sure. Let me give one parting shot: a workaround is defined as "a method for overcoming a problem or limitation in a program or system." But when you deeply understand what is going on, it frequently happens that the situation is no longer viewed as a "problem" or a "limitation", but rather an opportunity to discover new realms of beautiful mathematics.
That's semantics. Much of the history of mathematics is a history of creative workarounds that overcame the limitations of the prior understanding and opened up new vistas of beautiful mathematics. The other half isn't really exciting for the people here, and is what Nikolaj Kuntner has described above, namely fixing a set of assumptions and working out the mathematical consequences.
(=_=) (Apr 03 2020 at 07:54):@sarahzrf said:
Rongmin Lu said:
Anecdotally, many programmers I know hate mathematics. For some reason, the way of thinking that we take for granted is very alien and uncomfortable to them, whereas the way of thinking that pays off in programming comes more naturally for them.
as a programmer, can second this anecdote, there's a lot to unpack
Please unpack, the floor is yours.
sarahzrf (Apr 03 2020 at 07:55):aaa maybe later it's 4am i need to go to sleep soon
sarahzrf (Apr 03 2020 at 07:55):🥱
(=_=) (Apr 03 2020 at 07:57):Good night!
(=_=) (Apr 03 2020 at 08:06):John Baez said:
Something about the foundations of mathematics drives people crazy - maybe it's the word "foundations". I prefer the word "entrances". A building can have many entrances.
It drives people crazy because they're not interested in becoming architects.
Unless I'm an architect, I'm not going to walk into a building and gawk at the entrances. Unless I'm a structural engineer, I'm not going to be terribly interested in a building's foundations. What I want from a building is to do things in it, not to study how it's built.
The same goes for maths to the general public, or PL theory to programmers. Yes, they are "woven into the fabric of our existence": this is precisely why people ignore them!
(=_=) (Apr 03 2020 at 08:08):And it's probably no coincidence that CT in CS finds the most use in architectural issues in software development. This is probably ACT's greatest strength, and well may it capitalise on that to spread the knowledge developed in CS to other disciplines. But there are other areas in which CT isn't as strong, and perhaps some people may like to look at that and build CT up in those areas.
(=_=) (Apr 03 2020 at 08:15):@Paul Blain Levy said:
Some people are put off category theory by the size issues. And I can hardly blame them. The issues are more serious than many category theorists are willing to admit.
Can you give some examples of the size issues that you're concerned about? That might perhaps also refresh my memory of what the size issues were that cropped up in my talks.
Mike Shulman (Apr 03 2020 at 08:17):@Rongmin Lu Yes, arguing about whether a particular word is appropriate is more or less the definition of "semantics". (-:
Mike Shulman (Apr 03 2020 at 08:26):@Paul Blain Levy Personally, I don't believe that any models of PA "exist" in a Platonic sense, since I don't believe that any mathematical objects exist in a Platonic sense. Mathematical existence only makes sense within a framework, like first-order logic or dependent type theory, in which there is a quantifier called "there exists" that can be proven to hold. But I can sort of imagine what it might be like to believe that mathematical objects exist Platonically, and I was trying to argue from that perspective.
Clearly you believe that models of PA exist because of your intuition for "the" totality of natural numbers. But what I'm saying is that another person might believe in lots of models of PA for different reasons. They might have an intuition for "a" totality of natural numbers admitting more than one possible model, that compels belief as strongly as your intuition for a unique totality of natural numbers does for you.
Morgan Rogers (he/him) (Apr 03 2020 at 09:04):I enjoy the theological parallels that could be drawn from that last comment. Personally I think this is why foundations drive people crazy: it's because once you dig down into them it's impossible to ignore the old bones of philosophy that are revealed, and at that point there are no fundamentally right answers. The best you can do is to build a framework that seems(!) robust enough to carry the maths you want to do on top of it. But that's okay because on a finer scale it's how maths works at all levels!
(=_=) (Apr 03 2020 at 09:16):Morgan Rogers said:
I enjoy the theological parallels that could be drawn from that last comment. Personally I think this is why foundations drive people crazy: it's because once you dig down into them it's impossible to ignore the old bones of philosophy that are revealed, and at that point there are no fundamentally right answers. The best you can do is to build a framework that seems(!) robust enough to carry the maths you want to do on top of it. But that's okay because on a finer scale it's how maths works at all levels!
Yes, most people want to just do the maths on top of that framework, not worry about whether or not the planet would suddenly vanish beneath their feet! That's kind of what Nikolaj Kuntner was pointing out here: many mathematicians fix a set of axioms and proceed from there using tools that were built within that framework.
Another thing that I've found that puts people off CT: some proponents don't understand that many working mathematicians aren't trying to organise stuff, they just want to calculate stuff. And CT at the moment isn't very suited to perform the kinds of calculations that they need.
It's like, I want to know that 1+1=2, and you show me several hundred pages of Principia Mathematica. That's not very appealing, to put it mildly.
David Michael Roberts (Apr 03 2020 at 10:26):@Rongmin Lu The proof of the diagonal argument (yes, not Lawvere's FPT) holds in any pointed magmoidal category with diagonals. The proof requires only equational logic, no power sets needed, no proper classes; technically, not even infinite sets (though then it's less surprising a result, maybe). I really can't imagine how size issues would come up. What were the main objections?
David Michael Roberts (Apr 03 2020 at 10:49):@Rongmin Lu hmm, you gave a number of talks in that group! Would have been interesting, for sure.
(=_=) (Apr 03 2020 at 11:52):@David Michael Roberts said:
Rongmin Lu The proof of the diagonal argument (yes, not Lawvere's FPT) holds in any pointed magmoidal category with diagonals. The proof requires only equational logic, no power sets needed, no proper classes; technically, not even infinite sets (though then it's less surprising a result, maybe). I really can't imagine how size issues would come up. What were the main objections?
I wish I knew all this going in. Yes, I did point out that no infinite sets were involved. That was the size issue. I know, it's pretty trivial, most of the audience was pretty annoyed too. :shrug:
(=_=) (Apr 03 2020 at 11:58):David Michael Roberts said:
Rongmin Lu hmm, you gave a number of talks in that group! Would have been interesting, for sure.
Oh yeah. It can get tedious, because programmers are very detail-oriented, but I learned a lot (of patience).
I gave another talk about profunctor optics, based on a recent paper that's part of the thesis of @Mario Román. This time the size issue was less trivial, because coends were involved.
Paul Blain Levy (Apr 03 2020 at 15:40):Mike Shulman said:
Paul Blain Levy Personally, I don't believe that any models of PA "exist" in a Platonic sense, since I don't believe that any mathematical objects exist in a Platonic sense.
Let me check that I understand you correctly. You don't think that (for example) associativity of natural number addition is a "true" statement. For you it's merely a theorem of certain formal systems (e.g. PRA). So you wouldn't be surprised to find a counterexample. Right?
Clearly you believe that models of PA exist because of your intuition for "the" totality of natural numbers. But what I'm saying is that another person might believe in lots of models of PA for different reasons. They might have an intuition for "a" totality of natural numbers admitting more than one possible model, that compels belief as strongly as your intuition for a unique totality of natural numbers does for you.
Including models that validate not-Con(PA)?
Mike Shulman (Apr 03 2020 at 15:46):@Paul Blain Levy What do you mean by "counterexample"? Do you mean some collections of actual objects in the world that gave different answers when grouped in different ways? I would be very surprised by that, because the formal system of the natural numbers, although it is only an idea rather than a Platonic entity that exists in the same sense as apples do, has been designed to be a good model of the real world, so that we expect its conclusions to be applicable to the real world.
As for your second question -- sure, why not? The thing about intuition and belief is that something that's intuitive for one person can be highly non-intuitive for another one.
Paul Blain Levy (Apr 03 2020 at 15:47):John Baez said:
When I said this:
I mainly talk about the case of Peano arithmetic, where it's even harder to get people to accept that this has many different models just like the axioms for a group - and not one "true" model and a bunch of "nonstandard" ones, like the true king and a bunch of pretenders to the throne.
I wasn't trying to say I accepted something or not, or believed in some mathematical entity or not.
Then I misunderstood you - sorry.
I was all-too-briefly alluding to a project I have cooking on the back burner with Michael Weiss, here:
and here:
I haven't gotten far enough to give a really clear explanation yet.
Thanks for the links!
Dan Doel (Apr 03 2020 at 16:31):There's a paper by Sergei Artemov (The Provability of Consistency, I think) that argues that the Gödel statement of consistency is actually not appropriate for capturing what we mean. I.E. by quantifying over the natural numbers, it must hold uniformly in all models of arithmetic, including the non-standard ones.
So, possibly one way to think about not-Con(PA) models is that they also contain non-standard notions of proof that you would not really agree are real proofs, but you've tricked yourself into equating them with the normal proofs you think about. This angle is also kind of similar to some work on formal systems for ultrafinitism. They include 'inconsistent' axioms, but the proofs you'd have to construct to demonstrate the inconsistency are too large to actually perform, so the ultrafinitist doesn't agree that they actually exist.
Dan Doel (Apr 03 2020 at 16:37):But, to flip things around on the ultrafinitists (to illustrate Mike's point), there's a question on mathoverflow (I think) about how if we count things twice, do we get the same answer? The question asserts that we only believe this because formal systems assume it, but I think that's backwards.
We use formal systems where counting is reliable because we have learned it is a reliable tool. If you counted something earlier, and you count it now and get a different number, you don't just say, "oh, well, that's how things work." Instead, you start trying to figure out why your two counts didn't match.
Dan Doel (Apr 03 2020 at 16:38):That doesn't mean a system where counting is unreliable wouldn't be useful, necessarily, but there's a reason why we usually take it to be reliable.
Reid Barton (Apr 03 2020 at 19:22):Paul Blain Levy said:
Some people are put off category theory by the size issues. And I can hardly blame them. The issues are more serious than many category theorists are willing to admit.
Since we ended up talking about some size issues anyways I'm curious to hear about what kind of issues you have in mind here. I've heard the same sort of thing before but my impression is that for the most part category theorists are pretty careful about size issues. But I will grant that quite a lot of this happens below the level at which we communicate so you might not see the issues addressed explicitly.
Joachim Kock (Apr 03 2020 at 23:43):Dan Doel said:
If you counted something earlier, and you count it now and get a different number, you don't just say, "oh, well, that's how things work." Instead, you start trying to figure out why your two counts didn't match.
Joachim Kock (Apr 03 2020 at 23:44):Hi, my favourite model for PA is the Toy Model, where 2+2=4 and all cardinals bigger than 20 are large :-)
Joachim Kock (Apr 03 2020 at 23:45):(This is not to make fun of the ongoing discussion. It is mostly to make fun of myself. I wish I could follow the discussion.)
Daniel Geisler (Apr 04 2020 at 02:17):I just read that there's an issue with declaring the category of categories, just as there is an issue with declaring the set of sets. Could someone explain the issues with declaring the category of categories? Does this act to make higher category theory more difficult?
John Baez (Apr 04 2020 at 02:28):The category of all small categories is itself a large category - the links will explain those concepts. If one wishes to get serious about working with large categories, it's good to assume the axiom of universes, which states that every set is contained in a Grothendieck universe.
None of this makes higher category theory more difficult.
Dan Doel (Apr 04 2020 at 02:31):It's already so difficult that this doesn't matter. :mischievous:
(=_=) (Apr 04 2020 at 07:17):In other related news, this just happened, and I'm sure I'll unleash a firestorm here if someone notices this. This long-running controversy is exactly the kind of scenario that Voevodsky feared would become more common in the future. In fact, it started barely after HoTT became a thing.
Morgan Rogers (he/him) (Apr 04 2020 at 10:38):Rongmin Lu said:
In other related news, this just happened, and I'm sure I'll unleash a firestorm here if someone notices this. This long-running controversy is exactly the kind of scenario that Voevodsky feared would become more common in the future. In fact, it started barely after HoTT became a thing.
"Acceptance of the work in Publications of the Research Institute for Mathematical Sciences (RIMS) — a journal of which Mochizuki is chief editor, published by the institute where he works at Kyoto University — is the latest development in a long and acrimonious controversy over the mathematicians' proof."... If no one else believes you, just use your own platform I guess :face_palm:
(=_=) (Apr 04 2020 at 15:13):Morgan Rogers said:
"Acceptance of the work in Publications of the Research Institute for Mathematical Sciences (RIMS) — a journal of which Mochizuki is chief editor, published by the institute where he works at Kyoto University — is the latest development in a long and acrimonious controversy over the mathematicians' proof."... If no one else believes you, just use your own platform I guess :face_palm:
You've conveniently omitted this paragraph, which shows that this is a common occurrence:
Mathematicians often publish papers in journals where they are editors. As long as the authors recuse themselves from the peer-review process “such a case is not a violation of any rule, and is common”, says Hiraku Nakajima, a mathematician at the Kavli Institute for the Physics and Mathematics of the Universe in Tokyo formerly part of Publications of RIMS’s editorial board. Mehrmann confirms that this would not violate EMS guidelines.
James Wood (Apr 04 2020 at 16:04):It's kinda orthogonal but interesting to note that in HoTT, univalent categories only form a univalent 2-category, and there is no map from there to univalent 1-categories without truncating stuff. So in a sense, when you take higher categories seriously, there may well not be a 1-category of all (small) 1-categories.
Morgan Rogers (he/him) (Apr 04 2020 at 17:06):Rongmin Lu said:
Morgan Rogers said:
"Acceptance of the work in Publications of the Research Institute for Mathematical Sciences (RIMS) — a journal of which Mochizuki is chief editor, published by the institute where he works at Kyoto University — is the latest development in a long and acrimonious controversy over the mathematicians' proof."... If no one else believes you, just use your own platform I guess :face_palm:
You've conveniently omitted this paragraph, which shows that this is a common occurrence:
Mathematicians often publish papers in journals where they are editors. As long as the authors recuse themselves from the peer-review process “such a case is not a violation of any rule, and is common”, says Hiraku Nakajima, a mathematician at the Kavli Institute for the Physics and Mathematics of the Universe in Tokyo formerly part of Publications of RIMS’s editorial board. Mehrmann confirms that this would not violate EMS guidelines.
"Since others won't accept my proof, I'll just publish it in the journal I'm in charge of," says Mochizuki.
"This is okay," says member of staff on same journal.
"This is technically allowed, but if they go ahead with this it will reflect badly on them," says president of European society responsible for distributing said publication.
Anyway, it's not the fact that he's publishing it this way that's the problem, it's the fact that he's refusing to acknowledge the community's problems with his work.
Paul Blain Levy (Apr 05 2020 at 07:43):Dan Doel said:
So, possibly one way to think about not-Con(PA) models is that they also contain non-standard notions of proof
As long as you accept that there's a distinction between standard and nonstandard, I don't think we disagree. (And a nonstandard model certainly gives rise to a nonstandard notion of proof. Nothing controversial about that.) The hypothetical person that Mike is trying to get me to understand, who directly intuits many nonisomorphic models, does not accept this distinction.
(=_=) (Apr 05 2020 at 08:01):Morgan Rogers said:
Anyway, it's not the fact that he's publishing it this way that's the problem, it's the fact that he's refusing to acknowledge the community's problems with his work.
The "community" is not a monolith: there's a pro-M faction, an anti-M faction, some people are running for cover, and some of us would like the warring factions to calm down and focus on clarifying the mathematics.
I won't rehearse the history too much, but suffice it to say that he had addressed promptly some (minor?) problems with his work soon after it was released. It was only after a workshop was held in the UK that things broke down terminally, and then Scholze-Stix stepped in.
(=_=) (Apr 05 2020 at 08:02):The point of mentioning M's work is this: If M had released his work 2 decades after HoTT was released, we may not have had this debacle, because we may have built the tools that could have made the checking of his work a lot less laborious. Unfortunately, M released his work in Aug 2012 and the HoTT book came out in 2013.
Paul Blain Levy (Apr 05 2020 at 08:24):Mike Shulman said:
As for your second question -- sure, why not?
Because this hypothetical person believes that PA is actually consistent. Thinking about this makes your hypothetical person's views even less comprehensible to me; they intuit these "models of PA" but this notion relies on a notion of natural number.
The thing about intuition and belief is that something that's intuitive for one person can be highly non-intuitive for another one.
For me, the existence of PA models that validate not-Con(PA) is just as intuitive as the compositeness of 1147. Each of these was easy for me to believe after I saw a proof, but the proofs were needed because I don't intuit the statements directly. I find the idea that another person could intuit them directly, and therefore have no need of proof, to be far-fetched.
Paul Blain Levy (Apr 05 2020 at 08:53):Mike Shulman said:
Paul Blain Levy What do you mean by "counterexample"? Do you mean some collections of actual objects in the world that gave different answers when grouped in different ways?
Yes, but maybe my associativity example was too trivial. Take more advanced theorems of PA (or PRA if you prefer).
I would be very surprised by that, because the formal system of the natural numbers, although it is only an idea rather than a Platonic entity that exists in the same sense as apples.
Natural numbers certainly don't exist in the same sense that apples do. I don't think anyone ever claimed this.
The ontological status of apples is much shakier than that of natural numbers.
has been designed to be a good model of the real world, so that we expect its conclusions to be applicable to the real world.
I admit this PA includes small natural numbers such as you might encounter in the "real world". But also large natural numbers such as googolplex that apparently are not realizable in the "real world". So I don't see why one would think that it correctly predicts the properties of the former, unless one believes in the totality of natural numbers.
Paul Blain Levy (Apr 05 2020 at 09:15):Reid Barton said:
Paul Blain Levy said:
Some people are put off category theory by the size issues. And I can hardly blame them. The issues are more serious than many category theorists are willing to admit.
Since we ended up talking about some size issues anyways I'm curious to hear about what kind of issues you have in mind here.
The basic problem is that the most important category of all, viz. the category of sets, doesn't exist. None of the proposed workarounds is entirely satisfactory. (I learnt a lot on this subject from Mike Shulman's paper "Set theory for category theory.")
I've heard the same sort of thing before but my impression is that for the most part category theorists are pretty careful about size issues. But I will grant that quite a lot of this happens below the level at which we communicate so you might not see the issues addressed explicitly.
I suppose you mean that some people say one thing, which doesn't really make sense, but secretly think another, which does. Not saying what one means is hardly an ideal situation.
David Michael Roberts (Apr 05 2020 at 09:49):Paul Blain Levy said:
The basic problem is that the most important category of all, viz. the category of sets, doesn't exist. None of the proposed workarounds is entirely satisfactory. (I learnt a lot on this subject from Mike Shulman's paper "Set theory for category theory.")
Interested to hear why you say this.
ZFC people say "classes don't exist", but one can write down the syntactic category of definable classes in ZFC, and get a perfectly good infinitary pretopos, and indeed a model of Algebraic Set Theory. I would assume a similar syntactic category could exist for sets (isSet(x) is something you can say about a class x, no?), but I'm no expert. Unless working with such formal objects doesn't count as 'existence'?
Fabrizio Genovese (Apr 05 2020 at 10:52):I think the reason why many people are "at ease" with maths not being super strict about proof verification is that it is extraordinarily resilient. It's very difficult to explain this properly but basically "correct arguments tend to stay so also when the proofs are incorrect". Giancarlo Rota provides an example of what I mean here:
"When the Germans were planning to publish Hilbert’s collected papers and to present him with a set on the occasion of one of his later birthdays, they realized that they could not publish the papers in their original versions because they were full of errors, some of them quite serious. Thereupon they hired a young unemployed mathematician, Olga Taussky-Todd, to go over Hilbert’s papers and correct all the mistakes. Olga labored for three years; it turned out that all the mistakes could be corrected without any major changes in the statement of the theorems. There was one exception: ... At last on Hilbert's birthday a freshly printed set of Hilbert's collected papers was presented to the Geheimrat. Hilbert leafed through them carefully and did not notice anything." Source
I found this remarkable. Concepts can remain right even if proofs are wrong, while the opposite (right proofs for wrong concepts) is much rarer. This is related with what someone else said above, that is, when something is not correct, if widely used it won't survive for long in maths. Indeed, it has to be noted that the majority of maths discussed in this conversation is controversial, meaning that very few mathematicians would actually assume such results for granted in a paper right now. Contrast this with statements like P!=NP: we do not have any proof of this, nevertheless it is common to assume it to hold in many contexts, such as cryptography. People believe this holds even without proof and so they use it, without caring too much. When you think about it it's crazy, but somehow it works. So "social environment" in mathematics does not just refer to how people behave around publications and proofs. It's also very much about having a collective intuition that, albeit not often verified, and albeit not always correct, it is right 99% of the time. I think this gives people peace of mind, and I wouldn't necessarily disregard it as dangerous. It's like doing pobabilistic computation, and it has its perks.
Matteo Capucci (he/him) (Apr 05 2020 at 11:02):Indeed, the interaction between ideas-community-formal proofs is central to mathematics. One couldn't dispense with any one of them!
James Wood (Apr 05 2020 at 11:04):P ≠ NP seems like quite a different assumption from usual believed-to-be-true results. For one thing, while a P algorithm for SAT does not exist, P ≠ NP is as good as true for practical purposes. For another, there's great incentive to make such an algorithm, and given that we don't know of one, that's some good empirical evidence.
Fabrizio Genovese (Apr 05 2020 at 11:07):Yes, I was referring to the fact that nearly everyone believes P to be not equal to NP. The only notable exception I know of is Donald Knuth, which anyway believes that "P = NP, but an algorithm to reduce a NP-complete problem to a P one is too complicated for humans to be ever able to find it", which means, in practice, that for many things he still believes you can safely rely on what P != NP implies
(=_=) (Apr 05 2020 at 13:05):James Wood said:
P ≠ NP seems like quite a different assumption from usual believed-to-be-true results. For one thing, while a P algorithm for SAT does not exist, P ≠ NP is as good as true for practical purposes. For another, there's great incentive to make such an algorithm, and given that we don't know of one, that's some good empirical evidence.
That's the reason why I part company with Fabrizio et al. on the so-called "resilience" of mathematics. "For practical purposes" is good enough for the working computer scientist, but it isn't good enough for the working mathematician.
The Riemann hypothesis is just as good as true for practical purposes, and many papers have been written assuming its truth, yet we'd still demand a correct proof before we'd promote it to a theorem (unlike FLT, tsk tsk :sweat_smile: ).
The thing is, false positives ("right proofs for the wrong concepts", i.e. a purported proof of a widely believed proposition that is actually false) can happen, and have happened before: here's a list containing some false positives and another list of false positives on Mathoverflow.
(=_=) (Apr 05 2020 at 13:11):Also, I find it very disturbing that some here have taken to opine that it is the computer scientist who's more obsessed with the validity of a mathematical proof than the mathematician. I'm sure many mathematicians would find this to be news to them.
Jules Hedges (Apr 05 2020 at 13:22):Should this be migrated somewhere else after all? I can clearly see some more mileage in this coversation
(=_=) (Apr 05 2020 at 13:23):I'd move it back to Shaky foundations. Seems more appropriate.
Jules Hedges (Apr 05 2020 at 13:23):"Computer scientists are more obsessed with mathematical correctness than mathematicians" is also my experience. To some extent I think it's justified. If a pure mathematician has a bug in their proof, the worst case is that someone gets egg on their face. If a computer scientist has a bug in their proof, the worst case is that people die
Jules Hedges (Apr 05 2020 at 13:24):(I mean, off #general and out of everyone's way)
(=_=) (Apr 05 2020 at 13:25):Jules Hedges said:
If a pure mathematician has a bug in their proof, the worst case is that someone gets egg on their face. If a computer scientist has a bug in their proof, the worst case is that people die
Then I worry for ACT, because the "A" bit means it can be more than egg on face.
(=_=) (Apr 05 2020 at 13:26):Jules Hedges said:
(I mean, off #general and out of everyone's way)
You can't move to a different stream. At least, nobody seems to know how.
Dan Doel (Apr 05 2020 at 15:22):Paul Blain Levy said:
As long as you accept that there's a distinction between standard and nonstandard, I don't think we disagree.
I don't think Mike was arguing that there is no actual difference between any model of PA. They're obviously different, or they'd all be the same model.
One of the differences is that different models will match different applications of PA better (similar to how different theories can be more or less useful for different applications). The "standard" model (probably) matches what we're doing when we write symbols on a page. "Non-standard" models probably don't. That doesn't mean the first one is "the right" model of PA; it means it's the right one for this application.
Also this shows that it can be dubious to give informal descriptions of formal statements based on privileging one model. We call the proposition Con(PA) because it maps to what we think of as consistency in the page model. But PA is not only a theory of symbols on a page.
Paul Blain Levy (Apr 05 2020 at 15:31):Dan Doel said:
Paul Blain Levy said:
As long as you accept that there's a distinction between standard and nonstandard, I don't think we disagree.
I don't think Mike was arguing that there is no actual difference between any model of PA. They're obviously different, or they'd all be the same model.
One of the differences is that different models will match different applications of PA better (similar to how different theories can be more or less useful for different applications). The "standard" model (probably) matches what we're doing when we write symbols on a page. "Non-standard" models probably don't. That doesn't mean the first one is "the right" model of PA; it means it's the right one for this application.
Also this shows that it can be dubious to give informal descriptions of formal statements based on privileging one model. We call the proposition Con(PA) because it maps to what we think of as consistency in the page model. But PA is not only a theory of symbols on a page.
If you prefer the phrase "page model of PA" rather than "true model of PA" or "standard model of PA", that's fine by me. As long as you accept that there is just one page model (up to isomorphism at least). Mike's hypothetical person would not accept this (if I understand Mike correctly).
Dan Doel (Apr 05 2020 at 15:40):That doesn't look like what he said at all.
Paul Blain Levy (Apr 05 2020 at 15:44):Dan Doel said:
That doesn't look like what he said at all.
You mean that, on your reading of Mike's messages, his hypothetical person would accept that there is just one page model (up to isomorphism at least)?
Dan Doel (Apr 05 2020 at 15:49):Yes, because models are just objects in another mathematical theory where we're trying to mathematically model our application of theories to concrete scenarios. The point isn't that there are multiple "standard models". The point is that there are many models, and none of them deserves to be called "standard."
Dan Doel (Apr 05 2020 at 15:50):And by multiple standard models, I mean multiple non-isomorphic things that are somehow the same model (whatever that means).
Paul Blain Levy (Apr 05 2020 at 15:51):Dan Doel said:
Yes, because models are just objects in another mathematical theory where we're trying to mathematically model our application of theories to concrete scenarios. The point isn't that there are multiple "standard models". The point is that there are many models, and none of them deserves to be called "standard."
But one of them deserves to be called "page"?
Dan Doel (Apr 05 2020 at 15:57):Yes. Writing symbols on a page is particular concrete activity. Calling it the "standard" model suggests that writing symbols in a page is the "correct" interpretation of what PA formulas mean, and other applications of PA are wrong, or similar.
Dan Doel (Apr 05 2020 at 15:59):Or, like, homotopy types are the 'wrong' model of Martin-löf type theory.
Paul Blain Levy (Apr 05 2020 at 15:59):@Mike Shulman , who is interpreting you correctly?
Paul Blain Levy (Apr 05 2020 at 16:02):@Dan Doel I'm assuming it's not your intention that the "page" is bounded by the number of atoms in the universe. For with such a bound we couldn't obtain a PA model at all.
Dan Doel (Apr 05 2020 at 16:06):Right. It's more idealized than the reality it's allegedly representing.
Dan Doel (Apr 05 2020 at 16:09):Although the formal system for ultrafinite mathematics I mentioned earlier are pretty similar to PA, I think. It's like PA + '∀n. log(log n) < 100' - cut.
Paul Blain Levy (Apr 05 2020 at 16:11):Dan Doel said:
Although the formal system for ultrafinite mathematics I mentioned earlier are pretty similar to PA, I think. It's like PA + '∀n. log(log n) < 100' - cut.
I guess that what is "pretty similar" is somewhat subjective :wink:
Nathanael Arkor (Apr 05 2020 at 16:14):Paul Blain Levy said:
Dan Doel said:
Yes, because models are just objects in another mathematical theory where we're trying to mathematically model our application of theories to concrete scenarios. The point isn't that there are multiple "standard models". The point is that there are many models, and none of them deserves to be called "standard."
But one of them deserves to be called "page"?
it's the "page model" precisely the syntactic model?
Nathanael Arkor (Apr 05 2020 at 16:14):in which case, it's the initial model
Nathanael Arkor (Apr 05 2020 at 16:14):which is canonical in some respect, though still not necessarily deserving of the name "standard"
Paul Blain Levy (Apr 05 2020 at 16:17):@Nathanael Arkor said:
in which case, it's the initial model
What notion of morphism do you have in mind? The usual notion of morphism between models of a first order theory is "elementary embedding". The category of PA models and elementary embeddings does not have an initial object.
Paul Blain Levy (Apr 05 2020 at 16:21):Perhaps you mean "initial algebra" for the signature {Zero, Successor}.
Nathanael Arkor (Apr 05 2020 at 16:22):I was thinking of treating PA as an algebraic theory and considering some category of models
Nathanael Arkor (Apr 05 2020 at 16:22):Paul Blain Levy said:
Perhaps you mean "initial algebra" for the signature {Zero, Successor}.
yes, something like this
Dan Doel (Apr 05 2020 at 16:29):No, it's the 'standard model'.
Dan Doel (Apr 05 2020 at 16:33):Although I don't know what the syntactic model of PA is like, or how it's defined exactly, so maybe it's the same thing.
Mike Shulman (Apr 05 2020 at 16:35):My hypothetical person does not believe that any model of PA deserves to be called "standard" (or "page" or what have you).
I also never suggested that a person could intuit anything without proof. Seeing proofs is how we develop our intuition.
Just because a model contains more than the objects it was designed to model is no reason to doubt its efficacy at reaching conclusions about the objects it was designed to model; after all the designers probably knew what they were doing.
ALl that said, I've just about lost track of, and interest in, this conversation. It seems much better suited to talk about over a beer some evening after the pandemic is over than to try to reach a conclusion in this spaghetti thread. (-:
Paul Blain Levy (Apr 05 2020 at 19:37):David Michael Roberts said:
Paul Blain Levy said:
The basic problem is that the most important category of all, viz. the category of sets, doesn't exist. None of the proposed workarounds is entirely satisfactory. (I learnt a lot on this subject from Mike Shulman's paper "Set theory for category theory.")
Interested to hear why you say this.
ZFC people say "classes don't exist", but one can write down the syntactic category of definable classes in ZFC, and get a perfectly good infinitary pretopos, and indeed a model of Algebraic Set Theory. I would assume a similar syntactic category could exist for sets (isSet(x) is something you can say about a class x, no?), but I'm no expert. Unless working with such formal objects doesn't count as 'existence'?
You answered your own question :wink:
Martti Karvonen (Apr 05 2020 at 19:47):Maybe a bit off-topic for the current discussion in this stream, but it does fit "shaky foundations". Is it just me or is there a (slight, easily fixable) mistake in condition (iv) in the definition of universe given in Borceux vol 1? Namely, in def 1.1.2 a universe is defined as a set satisfying (i) transitivity, (ii) closure under unions of families, provided the indexing set and each member of the family is in , (iii) closure under powersets (iv) and surjective function (v) contains the naturals. It seems to me that (iv) should also require that is a subset of (otherwise any singleton is in by (iv) and (v), whence by transitivity contains all sets, a contradiction)
Paul Blain Levy (Apr 05 2020 at 19:57):Martti Karvonen said:
Maybe a bit off-topic for the current discussion in this stream, but it does fit "shaky foundations". Is it just me or is there a (slight, easily fixable) mistake in condition (iv) in the definition of universe given in Borceux vol 1? Namely, in def 1.1.2 a universe is defined as a set satisfying (i) transitivity, (ii) closure under unions of families, provided the indexing set and each member of the family is in , (iii) closure under powersets (iv) and surjective function (v) contains the naturals. It seems to me that (iv) should also require that is a subset of (otherwise any singleton is in by (iv) and (v), whence by transitivity contains all sets, a contradiction)
You're right.
John Baez (Apr 05 2020 at 20:33):That does sound like a mistake to me. This definition is fairly different from the definition on Wikipedia, which lacks (iv) and (v) and includes the requirement that .
By omitting the requirement that the set of natural numbers is in , the Wikipedia definition includes two very small universes, namely the empty set and the set of all hereditarily finite sets. But they point this out; most people usually do something to exclude these very small universes. Axiom (v) is one way to do that.
David Michael Roberts (Apr 05 2020 at 23:11):Regarding Borceaux, I pointed this out recently on the nCafé: https://golem.ph.utexas.edu/category/2020/02/2dimensional_categories.html#c057336
David Michael Roberts (Apr 05 2020 at 23:12):I think this erratum should be added to the nLab, but I'm feeling a little lazy at the moment.
sarahzrf (Apr 06 2020 at 04:19):Dan Doel said:
Although the formal system for ultrafinite mathematics I mentioned earlier are pretty similar to PA, I think. It's like PA + '∀n. log(log n) < 100' - cut.
bruh
sarahzrf (Apr 06 2020 at 04:19):the idea being that even tho u can prove this inconsistent traditionally, good luck exhibiting an actual proof of false in normal form?
Dan Doel (Apr 06 2020 at 04:21):The 'proofs' of inconsistency that your false mathematics says there will be are too big to be real proofs.
Dan Doel (Apr 06 2020 at 04:21):It doesn't sound pleasant to use, though.
Dan Doel (Apr 06 2020 at 04:29):I'm not sure it was a serious suggestion, though. More a demonstration of what considerations would be in play in a formal system for ultrafinitism. The idea that the usual notion of consistency is irrelevant is more important than the specific formal system, I think.
Eduardo Ochs (Apr 19 2020 at 02:42):sarahzrf said:
main.pdf
here's what i've written up so far—mostly an explanation of the idea of what a presheaf is, not so much touching on yoneda at all yet
id guess this is probably like a third of the way into my usual schtick
I think that a common convention - I learned it when I was studying fibrations - for drawing things like your presheaves and copreshaves is to draw each Hom(A,X) above the corresponding A, and to omit the upward-pointing `|->'s connecting each A to its Hom(A,X). Here's an example: sa.png
sarahzrf (Apr 19 2020 at 02:50):yeah ive seen things like that