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.
Alex Kreitzberg (Mar 28 2025 at 21:14):I want a simple way to get myself in trouble with equivalence.
Define a "finite" category to be a category with a finite number of objects and morphisms.
This is problematic because you could have an infinite number of objects all isomorphic, and therefore, equivalent to one object.
So "number of objects" isn't equivalence invariant.
But you could maybe define a Functor on an "essentially finite" category, by returning the number of objects in the "essentially finite" categories skeleton.
I saw "Finite category" was defined to be a category internal to FinSet on the nlab, which is very fun! This seems to me, to be phrased carefully in an equivalence invariant way. In particular, this implies a finite number of objects and morphisms.
In any case, could somebody help me see how "essentially finite" is safe and useful, where simply "finite", in the sense introduced, gets me into trouble?
The point here is to understand equivalence, not finite categories, so if folks have better examples to clarify equivalence feel free to share them.
John Baez (Mar 29 2025 at 00:41):It's hard for me to deliberately come up with ways to get in trouble by ignoring the fact that the finiteness of the set of objects is not invariant under equivalence.
John Baez (Mar 29 2025 at 00:45):There are some interesting concepts of the cardinality of an essentially finite category that are invariant under equivalence. Of course it's easy to come up with ones that aren't.
Chris Grossack (she/they) (Mar 29 2025 at 04:01):In my experience, equivalence of categories is less a case of "if you work with isomorphism bad things happen" and more a case of "if you work with isomorphism good things DON'T happen".
Alex Kreitzberg (Mar 29 2025 at 04:04):I see, interesting, so it's more a device to discover useful definitions?
Alex Kreitzberg (Mar 29 2025 at 04:05):Like I could focus on isomorphisms, but I'll just keep banging my head against a wall to make interesting conclusions?
Chris Grossack (she/they) (Mar 29 2025 at 04:05):For example, we informally think of the category whose objects are the "model vector spaces" (one for each ) and whose arrows are linear maps as being "the same" as the category whose objects are all vector spaces whose arrows are linear maps. But here "sameness" has to mean equivalence. For concreteness say that the map from model vector spaces to all vector spaces is the inclusion, and the map the other way is defined by dimension. Then if you start with , go to and then back, you end up at which is not the vector space you started with! It's merely isomorphic to
Chris Grossack (she/they) (Mar 29 2025 at 04:05):So if you want these categories to be the same, and morally they should be, then you need equivalence
Chris Grossack (she/they) (Mar 29 2025 at 04:05):Here's another example:
Chris Grossack (she/they) (Mar 29 2025 at 04:08):You probably want syntax and semantics to be "dual" to each other in some sense... How might one make this precise? Well you can start with a (cauchy complete) finite product category (thought of as a [[lawvere theory]]) then go to its category of models (finite product functors ). From its category of models you can look at the (opposite of the ) full subcategory of free models to recover .... But not on the nose! You only recover something equivalent to !
Chris Grossack (she/they) (Mar 29 2025 at 04:09):So if you want to be able to say that going from syntax to semantics and back gets you to the "same place you started", you're forced into considering equivalence as "the right notion of sameness". Isomorphism just doesn't work, since in general the full subcategory of free models might have more objects than the you started with (for basically the same reason Vect has more objects than the category of "model vector spaces" in the previous example)
Alex Kreitzberg (Mar 29 2025 at 04:20):What you're saying makes a ton of sense, I'm going to think on it a bit.
But I like the framing that "I want to" think up to isomorphism. This is very clarifying, it underscores how not problematic many would be aspects are, they're just "boring".
Ryan Wisnesky (Mar 29 2025 at 06:23):Re-stating a bit to introduce the concept of "evil" into this thread, asking that two categories be isomorphic is "evil" in that it requires comparing functors up to equality rather than natural isomorphism. Whereas equivalence of categories is not evil.
Nathanael Arkor (Mar 29 2025 at 09:23):I would really warn against using the term "evil", as in my experience it causes more confusion than it avoids (discussed a little in this previous thread: ).
Alex Kreitzberg (Mar 29 2025 at 14:47):I'm avoiding the word "Evil" because I don't want to start a fight in this thread.
That said, it's still confusing that "nobody is going to arrest you for using definitions that only work for isomorphic Functors" while languages are being built that make it impossible to state definitions that aren't invariant under equivalence.
Such a language feature feels like "inforcing the law" under this metaphor.
If nothing is "wrong" with definitions that only work up to functor isomorphisms, then banning them feels like implementing a geometry program that only lets you define definitions up to similarity.
Which is useful, but isn't that also more limiting?
Like is working with categories up to isomorphism similar to programming in assembly, or working directly with set theory axioms for everything?
Amar Hadzihasanovic (Mar 29 2025 at 15:05):I think the analogy with programming languages is exactly right: different programming languages are good for different purposes. I don't think any programmer thinks that everybody should adopt a single language, which is why it is puzzling to me that "language pluralism" is not the default attitude to foundations of mathematics. (Or perhaps it is for "working mathematicians" but not necessarily voiced as such.)
Amar Hadzihasanovic (Mar 29 2025 at 15:09):Languages that "automatically respect principle X" are supposed to help you, by giving you formal guarantees that X holds as long as you can complete your proof in the language, they are not supposed to constrain you; if principle X is not important to you, don't use that language.
John Baez (Mar 29 2025 at 15:30):Alex Kreitzberg said:
That said, it's still confusing that "nobody is going to arrest you for using definitions that only work for isomorphic [categories]" while languages are being built that make it impossible to state definitions that aren't invariant under equivalence.
Why would that be confusing? Some people like to only use definitions that are invariant under equivalence of categories. Some like it so much they set up languages where only these invariant definitions are possible. But there's no law saying you have use to such languages! Indeed, at least 99% of mathematicians don't.
Category theory where you care about isomorphism of categories is a somewhat different subject than category theory where you only care about equivalence of categories. If you learn theorems about both you can decide what you think about these two subjects and their relation.
In math each of us has a huge amount of freedom. That includes the freedom to choose the limitations we impose on ourselves.
Alex Kreitzberg (Mar 29 2025 at 16:37):Okay, I believe I get it now. I'll omit why I thought that was confusing, because you addressed it.
An aside, I think that means the use of "evil" here gives the same connotation programmers intend when they use the word "evil". For example it could be a warning to be careful working with lengths when working up to similarity, or it can communicate you think the ambient setting is too low level for the problem you're trying to solve.
In software the quote "premature optimization is the root of all evil" is commonly attributed to Knuth. Earnestly used, it's a suggestion to write programs that don't depend on details specific to the computer they run on. It's funny the joke/metaphor "evil" occured in such a similar circumstance.
It's also funny that, I don't think Knuth would agree with most contexts that quote is invoked, assuming he even said it.
In any case, a positive statement here, is working up to equivalence is the necessary tool to give mathematical content to "isomorphic objects are the same."
Mike Shulman (Mar 30 2025 at 01:09):Amar Hadzihasanovic said:
I don't think any programmer thinks that everybody should adopt a single language, which is why it is puzzling to me that "language pluralism" is not the default attitude to foundations of mathematics. (Or perhaps it is for "working mathematicians" but not necessarily voiced as such.)
Sadly, it's not, even for "working mathematicians". Although that's largely because working mathematicians don't think about foundations of mathematics at all.
I drew a comic strip about this.
Screenshot from 2025-03-29 18-08-25.png
Mike Shulman (Mar 30 2025 at 04:39):Amar Hadzihasanovic said:
Languages that "automatically respect principle X" are supposed to help you, by giving you formal guarantees that X holds as long as you can complete your proof in the language, they are not supposed to constrain you; if principle X is not important to you, don't use that language.
I agree. However, I would also point out that the existence of such a language indicates that someone thought it was important or useful to ensure that X holds, so you might want to think carefully before deciding that principle X isn't important to you. Perhaps a better question than "is X important to me?" is "are there other goals or principles that conflict with X that are more important to me right now?"
For instance, many modern programming languages are built on a principle that memory leaks and segmentation faults should never happen, using garbage collection to relieve the programmer from manual memory management. I think many people would agree that (with modern hardware) for most programming problems this is a good choice, and should probably be the "default" when programming. But there are still some situations where (one can at least argue) a garbage collector introduces unacceptable overhead or unpredictability.
To paraphrase Chesterton: don't take down a principle until you know why it was put up.
Ryan Wisnesky (Mar 30 2025 at 05:23):I mentioned the connection to the word evil not because I think the principle of equivalence is good or bad - fwiw, I'd call it both, depending on one's goals - but because the existing literature on the subject already uses the word 'evil' and hence that word might be helpful when learning.
Jencel Panic (Mar 30 2025 at 07:53):John Baez said:
Category theory where you care about isomorphism of categories is a somewhat different subject than category theory where you only care about equivalence of categories. If you learn theorems about both you can decide what you think about these two subjects and their relation.
Interesting. I didn't know that the former subject (where you care about isomorphism of categories) even existed, as I feel that all of the stuff that I read is related to the latter (where you only care about equivalence) e.g. products and coproducts and all other limits are isomorphism-invariant, and hence non-isomorphic categories are not relevant to them.
Jencel Panic (Mar 30 2025 at 08:15):Alex Kreitzberg said:
In any case, a positive statement here, is working up to equivalence is the necessary tool to give mathematical content to "isomorphic objects are the same."
Yes, a formulation of this principle that I have read somewhere, (but no idea where) is that "categorical properties are invariant with respect to isomorphism of objects (i.e. categorical properties are isomorphism-invariant)
Mike Shulman (Mar 30 2025 at 09:03):Jencel Panic said:
I didn't know that the former subject (where you care about isomorphism of categories) even existed
Nearly all the study of categories-up-to-isomorphism that I can think of is using them mainly as a tool to deduce facts about categories-up-to-equivalence without having to explicitly carry around so many isomorphisms. For instance, using strict 2-categories instead of bicategories. This is a powerful technique and there's a lot that one can do with it, but it seems a bit of a stretch to refer to it as caring about isomorphisms of categories when we only care about them as a tool to prove equivalence-invariant facts.
I don't know if John had something more than this in mind, or if he was just imagining that such a subject might exist. (Or, I suppose from a Platonist point of view it already exists, even if human mathematicians haven't been inspired to discover much about it.)
Alex Kreitzberg (Mar 30 2025 at 14:54):Maybe this will help clarify something for me. The sort of stuff I had in mind for thinking about categories up to isomorphism, would be things like "measuring the number of objects used in a given representation of a category", or "counting arrows used for a certain composition". Just really noodly shenanigans about "superficial features".
However whenever I have an idea like this I'm generally suspicious there's a reframing like "essentially finite", just around the corner that makes thinking in this way redundant, or much more useful somehow.
But the point is you can't be impressed by a "superficially large" contractible groupoid being equivalent to just one object, if you don't have a way to say that it's "superficially large".
Is there a better way to think about this than thinking of categories up to isomorphism?
John Baez (Mar 30 2025 at 15:48):I don't know if John had something more than this in mind, or if he was just imagining that such a subject might exist.
I think that the study of the 1-category Cat, where we consider categories as algebraic gadgets like groups or rings and care a lot about when they're isomorphic, is a subject that only exists in bits and pieces here and there. I've never seen a book or even a paper that comes out and advocates this study.
An example of what I mean is the study of the path algebra of a quiver. Here we
take a [[quiver]] (what category theorists often call a 'graph'),
form the free category on that,
and then
People study quiver algebras quite intensely, and I can imagine them generalizing these to the category algebras of other categories, for example finite categories or finitely generated categories. In fact I'd be shocked if they hadn't! And these people might wind up becoming interested in the 1-category Cat.
Alex Kreitzberg (Mar 30 2025 at 15:51):Are there any objects in that category that are isomorphic but not equal?
John Baez (Mar 30 2025 at 15:54):No, because when you take the free category on a graph none of its morphisms are isomorphisms except the identities: since it's 'free', nothing forces those other morphisms to be isomorphisms.
John Baez (Mar 30 2025 at 15:55):But I would not be shocked if someone had studied the category algebras of some groupoids which have nonequal but isomorphic objects.
John Baez (Mar 30 2025 at 15:56):Indeed, now I remember people study these in noncommutative algebra:
Alex Kreitzberg (Mar 30 2025 at 16:18):I think that's a real world example of the "shenanigans" I was trying to articulate then, thank you for sharing!
Mike Shulman (Mar 30 2025 at 16:28):That reminds me of the magnitude of a finite category with objects, which is defined by writing down an matrix whose -entry is the cardinality of the homset from object to object , inverting it, and summing the entries. This certainly doesn't look invariant under equivalence, but it's even worse than that: if the category contains any pair of unequal isomorphic objects, the matrix will have two identical rows (and columns) and hence won't even be invertible.
On the other hand, one might argue that it would be better to index the rows and columns by the isomorphism classes of objects, so that the construction applies directly to any essentially finite category.
John Baez (Mar 30 2025 at 16:41):That's one definition of the magnitude of a finite category, but there's a more general definition involving a 'weighting', and @Tom Leinster shows in Lemma 1.12 here that if two categories are equivalent and one has a weighting than the other does. Then in Proposition 2.4 he shows two categories that admit weightings have the same cardinality if they're equivalent... or even have an adjunction between them!
Alex Kreitzberg (Mar 30 2025 at 17:52):Mike Shulman's example does nicely show that an annoying problem will go away by embracing essentially finite categories and equivalence invariance. And he explained it in a manner that validates the heuristic I outlined.
But I also love the context and subtlety with Baez's presention of the possible meaningful distinctions.
In any case, I think both ends of my questions have been addressed.
But I love the conversation so far, so feel free to keep talking if you find this interesting!
Alex Kreitzberg (Mar 31 2025 at 05:23):(I'm going to add Baez's quote that was moved from this thread because it is still useful context for this thread)
John Baez said:
Similarly, I would not be surprised if two categories are equivalent if and only if their category algebras are Morita equivalent, i.e. have equivalent categories of representations. I don't actually know if this is true, but if it were true maybe one could argue that the 'category algebra' construction should be thought of, not as a mere functor from the 1-category Cat to the usual 1-category of algebras, but from the 2-category Cat to the 2-category of algebras, bimodules and bimodule homomorphisms.
So I think these issues can be debated, with the 'pro-evil' and 'anti-evil' attitudes to category theory both trying to prove their merit in these applications to fields where people treat categories as humble algebraic objects much like groups or rings.
I'd like to see these arguments be judged, not just by category theorists already committed to the principle of equivalence, but by 'practioners', like people who use category algebras in the study of quivers, or groupoid algebras in noncommutative algebra.
The category theorists can nudge the practitioners, of course, but it would be very interesting to discover if the 'inner logic' of these subjects pushes practitioners toward the principle of equivalence, or not.
John Baez (Mar 31 2025 at 06:04):Thanks! That comment was indeed aimed at the general questions being discussed in this thread.
Morgan Rogers (he/him) (Apr 01 2025 at 08:23):Also of possible relevance: the nerve construction on (1-)categories is not equivalence-invariant. When doing homotopy theory with simplicial sets one thing that one hopes to achieve is making simplicial sets (weakly) equivalent if they are nerves of equivalent categories.
John Baez (Apr 01 2025 at 16:25):What would it mean for the nerve construction on categories to be equivalent in the sense you're saying it's not? What 2-category structure are you putting on simplicial sets, to define equivalence for them?
Chris Grossack (she/they) (Apr 01 2025 at 17:01):Well if you view the 2-category of categories as a truncated oo-category, then the nerve construction is an embedding into the oo-category of spaces (modeled by simplicial sets)?
Amar Hadzihasanovic (Apr 02 2025 at 08:01):I think the embedding of the -category of small categories, functors, and natural isomorphisms into the -category of small -categories can be presented by the nerve functor, where the category of simplicial sets is endowed with the Joyal model structure and the category of small categories with its canonical model structure.
Matteo Capucci (he/him) (Apr 02 2025 at 09:36):Amar Hadzihasanovic said:
I don't think any programmer thinks that everybody should adopt a single language, which is why it is puzzling to me that "language pluralism" is not the default attitude to foundations of mathematics
Rant incoming...
I blame this on formalism, as a philosophy of mathematics. Formalism served us right a century ago, but then it got so ingrained that the majority view nowadays seems to be that what we study are formal proofs in a formal system, which for convenience we call 'geometry', 'number theory', etc., despite the very plain fact that we do not, in fact, work formally most of the time if not at all (the closest being people who do mathematics directly on proof assistants, though I'd argue they still don't do what strict formalism would say they do).
If you really believe all mathematics is shorthand for a formal system, then pluralism is hard to digest because it points at a 'psychosocial-objective' nature of mathematics rather than a 'formal-objective' one, so you better insist it's ZFC/ETCS/MLTT all the way down.
Mike Shulman (Apr 02 2025 at 15:30):I find that a very strange remark. It seems to me that formalism leads very naturally to pluralism: if all we do in mathematics is manipulate formal symbols, then the symbols could just as well obey any rules we feel like. And as an empirical observation, it seems to me the people most vocally opposed to pluralism, namely ZFC-theorists, also tend to be the most committed to a Platonist view of mathematics in which their favored fundamental objects (the cumulative hierarchy) are those that "truly exist".
Morgan Rogers (he/him) (Apr 02 2025 at 15:46):John Baez said:
What 2-category structure are you putting on simplicial sets, to define equivalence for them?
Good point... if a construction is only defined (a priori) on the 1-category of categories, it only makes sense for that construction to be equivalence-invariant if you specify a notion of equivalence in the codomain category (or more demandingly, upgrade the codomain to a 2-category; any 2-functor necessarily preserves equivalence)! If there isn't an obvious contender then by default that's taken to be isomorphism (resp. the "discrete" 2-category where the only 2-morphisms are identities). So I'm pointing out that equivalent categories are not sent to isomorphic simplicial sets when taking the nerve.
John Baez (Apr 02 2025 at 15:54):Okay. Luckily there's a more clever 2-category of simplicial sets such that the nerve sends equivalent categories to equivalent simplicial sets.
Kevin Carlson (Apr 02 2025 at 17:02):Mike Shulman said:
I find that a very strange remark. It seems to me that formalism leads very naturally to pluralism: if all we do in mathematics is manipulate formal symbols, then the symbols could just as well obey any rules we feel like. And as an empirical observation, it seems to me the people most vocally opposed to pluralism, namely ZFC-theorists, also tend to be the most committed to a Platonist view of mathematics in which their favored fundamental objects (the cumulative hierarchy) are those that "truly exist".
I see the criticism but I thought Matteo was pointing at something that might not be so off base. If you pretend to believe that mathematics is ultimately founded on the first-order theory of ZFC then I do think there’s some ontological terror in proposed changes of foundations, whereas with some more realist philosophy you at least have some basis to explain how HoTT and ZFC, say, can both serve as foundations for a mathematics that in some sense exists outside of them. Also, of course, plenty of actual set theorists are pluralists; it seems like “working mathematicians” are likelier to be more reactionary on these matters.
Alex Kreitzberg (Apr 02 2025 at 18:50):Matteo's comment about mathematicians' stress with multiple foundations reminds me of most adults' stress with PEMDAS being only one of many ambiguous conventions.
I suspect PEMDAS frustrations are due to vague ideas of what it means for math to be objective, and disappointment with needing to deal with multiple conventions.
I'm tempted to extend that last point to most adults. The Linux kernal team has been really struggling to culturally incorporate Rust. That makes sense to me because it's hard to learn a new language.
I'd be surprised if genuine foundational concerns were at the heart of most folks frustrations. Unless "vague ideas of objectivity" really is a specific foundation's fault.
Mike Shulman (Apr 02 2025 at 20:34):Kevin Carlson said:
If you pretend to believe that mathematics is ultimately founded on the first-order theory of ZFC
Perhaps, but I don't think that is what formalists (pretend to) believe. For instance, the wikipedia article that Matteo linked to first describes how Hilbert wanted to formalize everything in finitary arithmetic, which was frustrated by Gödel's theorem, but then cites as other examples
Other formalists, such as Rudolf Carnap, considered mathematics to be the investigation of formal axiom systems
and
Haskell Curry defines mathematics as "the science of formal systems."
both of which say "systemS", plural. And the stanford encyclopedia of philosophy entry on formalism in the foundations of mathematics does not once mention ZFC.
Mike Shulman (Apr 02 2025 at 20:37):Kevin Carlson said:
Also, of course, plenty of actual set theorists are pluralists; it seems like “working mathematicians” are likelier to be more reactionary on these matters.
I can believe that plenty of set theorists are pluralists, especially with the recent rise of "multiverse" thinking. But my own experience has been that the most vocal opponents of alternative foundations have also been set theorists. "Working" mathematicians tend to be more "passively" reactionary, since they don't think about foundations much at all, and more open to being convinced otherwise when good arguments are presented.
As additional evidence, I don't know what the current status of this is, but I know that at least not so very long ago, many set theorists professed to believe that there was a "fact of the matter" regarding whether the Continuum Hypothesis is true or false, which seems to me very hard to square with pluralism.
Alex Kreitzberg (Apr 02 2025 at 20:42):...Are Set theorists on the same page between the two options? Or do they think they haven't found the "right" Set theory yet, and so haven't determined the answer?
Mike Shulman (Apr 02 2025 at 20:44):There was (maybe still is) definitely a research programme to try to find the "right" (or at least a "better") set theory that would decide the question. I don't remember whether there is/was a weight of majority opinion on what the answer would turn out to be.
Alex Kreitzberg (Apr 02 2025 at 20:51):Thinking about these ideas, it clarifies I really like formalist methods, they seem self correcting. If the Formalist dream really was for there to be one canonical formal system, then its methods have deeply undermined it.
Alex Kreitzberg (Apr 02 2025 at 21:40):But I'm really liking Mac Lane's discussion in "mathematics Form & Function" and the logic intro you shared a bit ago, because they leave space for intuition in a really practical way.
John Baez (Apr 02 2025 at 22:23):@Mike Shulman wrote:
There was (maybe still is) definitely a research programme to try to find the "right" (or at least a "better") set theory that would decide the question. I don't remember whether there is/was a weight of majority opinion on what the answer would turn out to be.
There's actually a lot of controversy. For some reason Natalie Wolchover at Quanta magazine likes to report on this:
Natalie Wolchover, To settle infinity dispute, a new law of logic, November 26, 2013.
Natalie Wolchover, How many numbers exist? Infinity proof moves math closer to an answer, July 15, 2021.
A couple of quotes from near the end of the latter, involving some axioms that people are playing with:
The convergence of Martin’s maximum++ and () creates a solid foundation for a tower of infinities in which the cardinality of the continuum is . “The question is, is it true?” asks Peter Koellner, a set theorist at Harvard.
But....
Notably, the person who might have been most enthusiastic about ()’s correctness has also turned against it. “I’m considered a traitor,” Woodin said in one of our Zoom conversations this summer. Twenty-five years ago, when he posed (), Woodin thought the continuum hypothesis was false, and thus that () was a source of light. But about a decade ago, he changed his mind. He now thinks that the continuum has cardinality and that () and forcing are “doomed.”
My question is, where are these people getting their intuitions that some axioms are "true" or "false"? It seems quite mystical.
Kevin Carlson (Apr 02 2025 at 22:35):Not all beliefs about axioms of set theory need feel mystical. I really believe it's literally true that if I have two finite collections of anything (say, the items on my desk and the pets in my home), I can put them together. That's all the axiom of union says! One interpretation of Cantor's great insight is that you can just pretend that sets like "the natural numbers" behave in essentially this familiar manner of nice concrete finite sets, except that they can be in bijection with a proper subset. Well, if you take that seriously, that infinite sets are real and definite in more or less the same sense that finite ones are, then it becomes a real problem that we have obvious way to pin down whether there are sizes in between and This is not a problem that we ever run into with finite sets! So some people really really want there to be a correct answer. If there isn't one, which of course there are very serious reasons to suspect, then in a certain sense that undermines the whole Cantorian project, though very few people are likely to actually abandon the assumption that the natural numbers form a set over such issues.
John Baez (Apr 02 2025 at 23:19):I agree with what you say; what sounds mystical is that I'm not hearing enough in Wolchover's articles about why these people have their intuitions. Maybe she's just focusing on the dramatic, like this:
Most set theorists would like nothing more than to exit the mathematical multiverse and coalesce behind a single picture of Cantor’s paradise, one that’s beautiful enough to call true.
Kennedy, for one, thinks we may soon return to that “prelapsarian world.” “Hilbert, when he gave his speech, said human dignity depends upon us being able to decide things in mathematics in a yes-or-no fashion,” she said. “This was a matter of redeeming humanity, of whether mathematics is what we always thought it was: to establish the truth. Not just this truth, that truth. Not just possibilities. No. The continuum is this size, period.”
Kevin Carlson (Apr 02 2025 at 23:20):Sure, that checks out. I'm sure it's very hard to explain these intuitions (to probably anyone, but especially) at Quanta level, to be fair.
John Baez (Apr 02 2025 at 23:24):By the way, note that here Hilbert, the formalist, is supposedly claiming human dignity depends on us being able to establish the truth of the matter when it comes to things like the continuum hypothesis. Or maybe it's just Kennedy who thinks it's a matter of "redeeming humanity". (Where did we go wrong, to be cast out of Cantor's paradise?)
Kevin Carlson (Apr 02 2025 at 23:25):Yeah, I'm pretty confused about how "wir mussen wissen, wir werden wissen" can be said by a formalist.
Kevin Carlson (Apr 02 2025 at 23:27):Probably he was more sophisticated than what we now think of as formalism among his descendants.
John Baez (Apr 02 2025 at 23:33):I was going to mention that Hilbert said, regarding axiomatic geometry "One must be able to say at all times--instead of points, straight lines, and planes--tables, chairs, and beer mugs" but I discovered that nobody is sure he said that. That led me down a little rabbit hole.
Anyway, I suppose you can correctly notice that axiomatic reasoning must work just as well when you change the names of some types, yet still believe mathematics is about finding "the truth" - some sort of truth that motivates our choice of axioms. I think almost all of us believe some axioms are better, at least more interesting, than others.
Mike Shulman (Apr 03 2025 at 00:49):According to SEP,
“formalism” in this sense—the Heine/Thomae position as interpreted by Frege and its descendants—is to be distinguished from a more sophisticated position (it is claimed), namely Hilbertian formalism... The Hilbertian position differs because it depends on a distinction within mathematical language between a finitary sector, whose sentences express contentful propositions, and an ideal, or infinitary sector. Where exactly Hilbert drew the distinction, or where it should be drawn, is a matter of debate. Crucially, though, Hilbert adopted an instrumentalistic attitude towards the ideal sector. The formulae of this language are, or are treated as if they are, uninterpreted, having the syntactic form of sentences to which we can apply formal rules of transformation and inference but no semantics. Nonetheless they are, or can be useful, if the ideal sector conservatively extends the finitary, that is if no proof from finitary premisses to a finitary conclusion which takes a detour through the infinitary language yields a conclusion we could not have reached using finitary means alone, albeit perhaps (herein lies the utility) by a longer, more unwieldy proof. The goal of the Hilbert programme was to provide a finitary proof of this conservative extension result; most, though not all, think this goal was proved impossible by Gödel’s second incompleteness theorem.
Kevin Carlson (Apr 03 2025 at 01:10):Very clarifying!