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.
Morgan Rogers (he/him) (Sep 17 2025 at 16:26):Observing that sets are constructed from the bottom up (a set is no more and no less than its elements), one could take a top-down approach, describing basic objects in terms of their parts. One way you could set this up might bring you to Boolean algebras, for instance, but depending on what kind of informal "space" you were basing the formalism on, you might end up with something more intuitionistic or potentially something else altogether.
Kevin Carlson (Sep 17 2025 at 16:53):David Michael Roberts said:
The first-order definition of category doesn't presuppose axioms on sets or classes. But I agree that you have a harder time trying to say what the Yoneda lemma is without talking about hom-"sets"
Well, I don’t personally take it that you can really define first order syntax without a fair bit of set theory, but I note that’s not the most mainstream position. But anyway, ETCS is a set theory; materialism versus structuralism is at least somewhat relevant to this discussion, but the objects of any well pointed topos with the axiom of choice are philosophically an awful lot like Cantorian sets, no?
Nathan Corbyn (Sep 17 2025 at 17:56):Kevin Carlson said:
Well, I don’t personally take it that you can really define first order syntax without a fair bit of set theory[…]
I don’t think you can really set up set theory without a fair bit of first order syntax
Kevin Carlson (Sep 17 2025 at 18:04):Yes, that's a common enough position. JP Mayberry explains it as based on a modern misapprehension that it's impossible to have an axiomatic system that's not fully syntactically formalized, which is not in fact something that any mathematician working with axiomatic systems believed between 400BC and about 1920 but has since slipped into the water supply without really ever being explicitly taught. Rather, basic notions like "Any two sets have a union, whose elements are precisely those elements of one or the other set" neither depend on nor benefit from formal syntax, whereas you will find you need to already believe this notion to be able to reasonably discuss addition of natural numbers, let alone concatenation of arbitrary strings in formal syntax.
Nathan Corbyn (Sep 17 2025 at 18:09):Kevin Carlson said:
you will find you need to already believe this notion to be able to reasonably discuss addition of natural numbers, let alone concatenation of arbitrary strings in formal syntax.
I don’t follow this
Kevin Carlson (Sep 17 2025 at 18:18):The second one is probably less philosophically dependent: a string is a function from a total order to its alphabet, and the concatenation of two strings is a function from the sum of those total orders, which is supported on the (disjoint) union of the supports of the starting orders, and so depends on the axiom of set union.
I guess many people would say something like "no, a string is an inscription on a page--or a screen--well, an inscription in principle, I can give some examples and you understand intuitively the general pattern for strings of arbitrary length--and to concatenate two strings you just stick them next to each other--well, of course in general you can't really do that, but you can do it 'in principle'--no, don't ask precisely what principle--" but that's really quite muddled compared to a proper, objective set-theoretic description.
This all boils down to the question of whether saying "you do step 1, then step 2, then go on forever, you know" is actually a satisfactory description of the induction principle to found your mathematics on. It was not for Dedekind and I'm quite convinced that it shouldn't be for anyone.
Mike Shulman (Sep 17 2025 at 18:23):You can't define first-order syntax formally without some kind of sets. But they don't have to be ZFC-sets, they could equally well be ETCS-sets. And that observation applies equally well to the first-order syntax of ZFC as to the first-order syntax of ETCS. Essentially it's just the observation that logic is a branch of mathematics, even though its object of study is also (an abstraction of) mathematics itself.
Kevin Carlson (Sep 17 2025 at 18:25):Yes, I agree with all of that. As I said, I saw this discussion as being pretty orthogonal to the old warhorse ZFC vs ETCS until David brought it in.
Nathan Corbyn (Sep 17 2025 at 18:26):“You can’t do X formally without a foundation” is tautologous, as formalising is a game played relative to a foundation. None of what’s been said precludes an informal first order syntax within which we axiomatise a set theory and then proceed. Indeed, Mayberry is more less or less suggesting we co-opt a fragment of natural language for this very purpose.
Kevin Carlson (Sep 17 2025 at 18:36):I guess I don't see how "informal first order syntax" is a meaningful phrase. You said you think you need a "fair bit of first order syntax" to set up set theory, but now you seem to be saying you can use "informal" syntax and indeed a sub-"syntax" of natural language, which sure sounds a lot like not needing a "fair bit of first order syntax" to me--presumably it goes without saying that you need at least as much syntax as natural language to do much of any intellectual activity!
Kevin Carlson (Sep 17 2025 at 18:37):In particular I don't see how we're really talking about syntax until we're talking about symbols that can be manipulated purely formally/algorithmically, without reference to their meanings, and I don't think that natural language has syntax in this sense, though of course it can be modeled to various extents with various kinds of formal syntax.
Nathan Corbyn (Sep 17 2025 at 18:41):As an example, I don’t think the sentence: “two sets are equal if and only if each of the elements of one is an element of the other and vice versa” is meaningful without taking an extreme amount of care with regard to the logical content, far beyond that which is done in daily use of natural language. I would argue that we’re more or less co-opting this expression to denote a first order sentence, helpfully more legibly than purely in symbols, but that we’re not doing mathematics otherwise. In fact, I’d say natural language is offering rather too much syntax and we’re better off doing mathematics with a lot less.
Nathan Corbyn (Sep 17 2025 at 18:43):I think syntax is very subtle, philosophically, and reducing it to symbols on a page or otherwise is a bit of a denigration.
Kevin Carlson (Sep 17 2025 at 18:47):Well, you haven't described any of your own thoughts about syntax, so I understand if I've been tilting at strawmen in reporting what many mathematicians seem to say. I don't really understand your first paragraph. It's not a particularly complicated sentence and people have been using such sentences very precisely, in mathematics, law, and sometimes other parts of life, for an order of magnitude longer than the notion of "first-order sentence" has existed in even inchoate form.
Alex Kreitzberg (Sep 17 2025 at 18:51):I feel compelled to note until very recently I understood the credibility of syntax to be based in interpretation of physical marks on paper somehow being more credible than other modes of thought, which I didn't like - but after thinking about stuff around it carefully I realized syntax is probably better thought of as an abstraction like any other, with very nice properties. With free monoids being the obvious basic example.
In any case, with respect to syntax, I ended up taking ten steps back because I realized I was still very confused about what exactly I was supposed to be frustrated with. :joy:
Regarding the primacy of Sets:
I think Roberts brought up ETCS not to underscore that ETCS was the point but to observe "why would someone think defining ETCS was a good idea if defining homsets was a Set motivating roadblock to category theory?"
That the Yoneda lemma is most naturally expressed with a Set theory, I think is probably the most plausible defense of having some Set theory as prior to category theory.
I appreciate you answering my questions the answers are helpful, I'll admit I'm somewhat surprised at how much controversy & tension there seems to be around these ideas.
Kevin Carlson (Sep 17 2025 at 19:47):Well, foundational conversations are philosophy of math, not math proper, which only gets started after you’ve laid out your basic assumptions. So like with all philosophy, nobody ever agrees about anything or probably ever will.
David Michael Roberts (Sep 18 2025 at 00:27):Yes, I didn't mean to hold ETCS vs ZFC as the solution, but rather point out that the question "what's a category? Isn't there a set, or at least a class, of arrows in between any two objects, and aren't the objects also a class?" is a known one, and has a standard answer ("no").
Regarding syntax, one doesn't need a full-powered set theory to define it, but rather a much weaker fragment. No one needs anything like Z[F[C]] to define syntax. Depending on how hardcore one wants to be with the coding, surely some Turing machine suffices. I don't know if I feel like I need a set theory to define what a Turing machine is (to prove its behaviour is a different matter, I think).
I managed to get an interlibrary loan on Mayberry (it took a while) and then I didn't get a chance to read much before I had to give it back. I appreciated his precise arguments, while simultaneously disagreeing with them quite strongly. I don't think I could recreate my reactions without getting the book again and sitting down and writing things out.
David Michael Roberts (Sep 18 2025 at 00:28):But this is all getting rather off topic, and perhaps the topic needs to split off. The hardcore formalist discussions based on current understanding about "what syntax really is" are, to me, not what dissecting things like how mathematical philosophy of the 18th and 19th century interrelates with dominant worldviews leading up to the present. I like this line from Minhyong Kim:
"the identity politics of the 18th and 19th century generated a complex collection of interests with a network of commitments that led to the story of mathematics being told in a specific way familiar to many of us now. The simplistic idea of proof was but one ingredient in a large ideological edifice, which is quite likely still an obstruction to the spread of mathematical culture and education around the world as well as of peace and understanding." https://www.ams.org/journals/notices/202508/noti3124/noti3124.html
Kevin Carlson (Sep 18 2025 at 00:47):David Michael Roberts said:
Yes, I didn't mean to hold ETCS vs ZFC as the solution, but rather point out that the question "what's a category? Isn't there a set, or at least a class, of arrows in between any two objects, and aren't the objects also a class?" is a known one, and has a standard answer ("no").
I don't follow how you've said anything about this point. ETCS gives a different way of axiomatizing sets than ZFC, but I don't see how it gives a different way of axiomatizing categories.
Kevin Carlson (Sep 18 2025 at 00:54):Oh, I guess you were referring more to your first message that "the first-order definition of category" doesn't rely on axioms about sets or classes. But basically in the same way as I was saying to Nathan, I really have no idea what people mean when they talk about "the first-order definition of category" without a pre-existing intended notion of model of a first order theory (besides the need to have at least some ability to induct in your background before you can describe what it is you're doing with first-order syntax.) It doesn't seem at all to me that writing down some syntactic manipulations you say you're allowed to do for anything called "categories" at all constitutes defining what a category is.
David Michael Roberts (Sep 18 2025 at 00:54):"I saw this discussion as being pretty orthogonal to the old warhorse ZFC vs ETCS until David brought it in."
I wasn't trying to bring up ZFC vs ETCS, but point out that the idea that you need a theory of sets to define hom-sets, to even define a category, has been raised before, in the context of people arguing against non-material set theory foundations, and claiming that categories (and hence categorical foundations like ETCS that posit a category with certain structure/properties) must be logically dependent on set theory for this reason. The people in those discussions weren't at the point of saying "to define raw syntax you need set theory, so clearly to define categories in first-order logic you need set theory". And that wasn't the point you started with.
David Michael Roberts (Sep 18 2025 at 00:55):Ah, snap.
David Michael Roberts (Sep 18 2025 at 00:57):Anyway, I've been editing a Springer publishing agreement for them this morning, and dealing with their outsourced typesetting company that apparently can't get my point that the right hand pdf contents hierarchy here is incorrect and needs to look like the left hand one
Screenshot 2025-09-18 at 10.26.44 AM.png
it's lessened my general patience, so apologies for not communicating in the best possible way.
Kevin Carlson (Sep 18 2025 at 00:58):Nothing to apologize for that I can see. Yeah, I got derailed by the ETCS thing but I see your point.
Notification Bot (Sep 18 2025 at 09:07):30 messages were moved here from #community: general > "Category Theory is Being Co-Opted" by Morgan Rogers (he/him).
Morgan Rogers (he/him) (Sep 18 2025 at 09:07):For future readers, "the article" mentioned in several messages above is the one in the above-linked topic.
James Deikun (Sep 18 2025 at 09:53):There's no reason first-order syntax can't be described in a way with inherent cohesion. For humans, a string or tree, laid out in some kind of at-least-conceptual space, but abstracting the identities of particular physical objects into recognizable categories, is probably just as basic an intellectual construct as a set, which arises originally by abstracting away the inherent position-in-space of identified physical objects.
John Baez (Sep 18 2025 at 10:59):Alex Kreitzberg said:
I feel compelled to note until very recently I understood the credibility of syntax to be based in interpretation of physical marks on paper somehow being more credible than other modes of thought, which I didn't like...
Digressing a bit: I grew up reading logicians and philosophers who talked a lot about physical marks on paper. But now many people rarely use the stuff! Kids these days would find it strange to treat scribbles of graphite on ground-up wood as the touchstone of utmost rigor. Now they prefer circuit elements etched on silicon chips. In a way it doesn't matter, but it shows we shouldn't be too fixated on the precise way we try to crystallize our thoughts into a discrete set of states of some durable physical system.
Alex Kreitzberg (Sep 18 2025 at 13:47):Actually I do spend time being fixated on how we physically embed math XD. I see pencil on paper as "me doing all the work" and formal proof assistants as "computers doing all the work" with respect to enforcing the "rules and structures" of math. I've wondered if a middle ground could be fruitfully explored, how do toys like Rubik's cubes fit into this story, etc.
Eventually I settled on basically James Deikun's opinion and that before that I was misunderstanding syntax. But it's still fun to think about.
Alex Kreitzberg (Sep 18 2025 at 14:21):I guess that's why a lot of my questions have involved trying to "synthetically" specify various physical/geometric systems with certain categories. Because if I can do it, then I can slap on a functor into Set, or whatever, to get a feeling for how it computes.
Just like how I can give a semantics to a simple syntax by defining a functor into Set from a free monoid. Conceiving the free monoid as "physical marks on paper" inspired the above analogy in my thought process.
Which is sort of funny because I don't think "physical marks" are the right way to think about syntax anymore.
Kevin Carlson (Sep 18 2025 at 21:03):James Deikun said:
There's no reason first-order syntax can't be described in a way with inherent cohesion. For humans, a string or tree, laid out in some kind of at-least-conceptual space, but abstracting the identities of particular physical objects into recognizable categories, is probably just as basic an intellectual construct as a set, which arises originally by abstracting away the inherent position-in-space of identified physical objects.
Interesting! But what is the actual proposal here? Defining a string as "a function from a total order into an alphabet" is a kind of definition of syntax with some internal cohesion, arising from the total order in the domain, and I might argue that this is precisely the amount of cohesion one needs to objectify the space in which (linear) syntax lies. But you seem to be suggesting you want to do this in a way that isn't founded on sets at all, do I have you right? What is that way?
Sam Speight (Sep 18 2025 at 22:44):My understanding of the proposal is as follows. To formalise set theory, we need some syntax; and to formalise syntax, we need some set theory. (We could replace set theory with something else, like type theory.) To make any progress (to prevent an infinite regress), at some level, we appeal to informal "intellectual constructs". Then @James Deikun's argument is that the informal intellectual consturcts of syntax (strings, trees) and of sets/collections are equally basic. So there is no good reason to appeal to one over the other.
John Baez (Sep 18 2025 at 22:54):James Deikun said:
There's no reason first-order syntax can't be described in a way with inherent cohesion [...]
This makes me wonder if someone has thought a lot about 'syntax with cohesion', namely syntaxes where there's a space or homotopy type or cohesive homotopy type of well-formed expressions. I've seen people study examples, like string diagrams thought of as submanifolds of a square or cube, but I haven't seen it studied in generality. We often think of discreteness as an important way of making syntax robust: i.e. if we draw the letter A a bit differently it means the same thing; its meaning doesn't vary continuously with how we draw it, so the idealized letters form a discrete 26-element set. But we can imagine trying to take a different attitude.
Mike Shulman (Sep 18 2025 at 23:23):Maybe I'm an old fuddy-duddy, but I would tend to regard something as "less syntactic" the more cohesive it gets. (Abstract) syntax for me is an inductively defined structure, and even in an ambient theory that includes higher homotopy types and cohesive types, inductively defined structures generally automatically turn out to be "discrete" unless you put non-discreteness into them by hand as parameters. I think one could argue that the discreteness of syntax is part of the whole point, as it enables us to define lots of important syntactic operations like typechecking algorithms that depend on properties like decidable equality.
Alex Kreitzberg (Sep 18 2025 at 23:49):If I'm following the conversation correctly, I've mused about Baez's last point as something like "can calligraphy add to mathematical meaning?" Is that a fair interpretation?
I've assumed folks don't want computers/math that requires they know how to draw. And that working with continuous data was harder.
If the deeper reason is "You generally can't make inductively defined structures meaningfully better this way." That'd be good to know.
Mike Shulman (Sep 18 2025 at 23:51):To be clear: non-discrete inductively defined structures, such as with non-discrete parameters (or with higher constructors), are certainly important, interesting, and useful in certain contexts. I'm just dubious about calling them "syntax" any more.
Alex Kreitzberg (Sep 18 2025 at 23:54):Is there a cool paper that explores this middle ground of concepts?
Kevin Carlson (Sep 19 2025 at 00:04):Mike Shulman said:
Maybe I'm an old fuddy-duddy, but I would tend to regard something as "less syntactic" the more cohesive it gets. (Abstract) syntax for me is an inductively defined structure, and even in an ambient theory that includes higher homotopy types and cohesive types, inductively defined structures generally automatically turn out to be "discrete" unless you put non-discreteness into them by hand as parameters. I think one could argue that the discreteness of syntax is part of the whole point, as it enables us to define lots of important syntactic operations like typechecking algorithms that depend on properties like decidable equality.
The inductivity of the definition of syntax is a key part of why I continue to think you can found syntax on set theory more completely than the other way around. (I wouldn't say I'm talking about "formalizing set theory with a bit of syntax", which doesn't make sense to me; I would rather say you can formalize syntax using informal set theory, and then formalize set theory using formal syntax should you want to do that, so as to study models of the formal theory as mathematical objects in their own right.)
My claim's that you can't make any objective sense of what an inductive definition is--in particular, why an inductive definition should uniquely determine a particular result--without already having the axiom of infinity in your pocket. In particular, reasoning from formalizations of set theory for the sake of argument, in the absence of the axiom of infinity there can be many different proper classes which the assertion of that axiom would make into isomorphic sets of "natural numbers", so there's no longer any reason to believe that "a string is what you get from starting with a letter, concatenating a letter to any string, and going on forever" is at all well-defined. So you need to know what the natural numbers are to give a precise definition of a string, but you don't need to know what a string is to give a precise definition of (say, the von Neumann) natural numbers.
James Deikun (Sep 19 2025 at 00:45):John Baez said:
This makes me wonder if someone has thought a lot about 'syntax with cohesion', namely syntaxes where there's a space or homotopy type or cohesive homotopy type of well-formed expressions. I've seen people study examples, like string diagrams thought of as submanifolds of a square or cube, but I haven't seen it studied in generality. We often think of discreteness as an important way of making syntax robust: i.e. if we draw the letter A a bit differently it means the same thing; its meaning doesn't vary continuously with how we draw it, so the idealized letters form a discrete 26-element set. But we can imagine trying to take a different attitude.
In the case of string diagrams, it's actually the fact that things are (mostly) continuous that makes them robust, which I think shows there's something to the notion. In fact, to the extent that things are "discrete" in string diagrams, the discreteness arises out of the continuous nature of the interpretation of the syntax because continuous maps into a discrete semantics must be locally constant.
Mike Shulman (Sep 19 2025 at 00:50):@Kevin Carlson What do you think about inductive definitions in Martin-Lof type theory? For instance, here's an inductive definition in Rocq syntax of the set of strings, which doesn't refer explicitly to the natural numbers:
Inductive string : Type :=
| nil : string
| cons : letter -> string -> string.
This definition and its resulting induction principle uniquely characterize the set of strings (inside MLTT). Would you say that this is "not objective"? Or "not precise"? Or that when making it we "already know what the natural numbers are" in some implicit sense?
James Deikun (Sep 19 2025 at 01:11):Kevin Carlson said:
My claim's that you can't make any objective sense of what an inductive definition is--in particular, why an inductive definition should uniquely determine a particular result--without already having the axiom of infinity in your pocket. In particular, reasoning from formalizations of set theory for the sake of argument, in the absence of the axiom of infinity there can be many different proper classes which the assertion of that axiom would make into isomorphic sets of "natural numbers", so there's no longer any reason to believe that "a string is what you get from starting with a letter, concatenating a letter to any string, and going on forever" is at all well-defined. So you need to know what the natural numbers are to give a precise definition of a string, but you don't need to know what a string is to give a precise definition of (say, the von Neumann) natural numbers.
How can you "have the axiom of infinity in your pocket" without being able to work with (informal) syntax? You can't state it without syntax, so you can only have it as an intuition. And a string doesn't need to be defined to be used informally any more than a set does, so you don't need an inductive definition of strings (or trees), only induction principles for them, for which you can appeal directly to an intuition about which kinds of properties are local in nature.
It's not like you get every induction principle you want for finitely-describable mathematical constructs from the axiom of infinity anyway, you need the axiom of replacement and large cardinal axioms, or else you need large countable ordinal axioms. And the idea that these strong induction principles "should be" true is the main supporting column of set theorists' attempts to convince mainstream mathematicians (and even some of each other) that these "large number" axioms should be true of "the" mathematical sets, once you unwind the way it's couched in stuff like Ramsey theory. (If you don't unwind it, then the main supporting column is the intuition that strong finitary reflection principles "should be" true of cohesive structures, which is just as far from really being based in intuitions about sets!)
Kevin Carlson (Sep 19 2025 at 01:12):@Mike Shulman I’d accept the first and the last one—it’s clear enough that this definition specifies something that’s unique if it exists, but I guess you just have to assert that it exists. Of course you’ll need some assumption to get anything infinite to exist, but it feels like it carves the situation more finely to construct some candidate class of natural numbers and then decide whether to assume that one of them forms a genuine set, then if so prove the theorem that your result is unique.
Kevin Carlson (Sep 19 2025 at 01:17):@James Deikun
-I continue not to have any idea how “informal syntax” is supposed to be distinguished from “language.” I agree that you need language to say “a set is infinite if it’s in bijection with some proper subset.”
-I’m not at all personally convicted of basically any propositions about infinite sets, and in fact one of my favorite parts of Mayberry’s work is his serious effort at providing a foundation of math in terms of (informal) set theory together with the negation of the axiom of infinity, though it seems unlikely to ever go far. So I’ll demur from defending any large-whatever assertions.
Mike Shulman (Sep 19 2025 at 01:18):If you like, you could phrase a direct definition of strings in set theory in the same way that you do the natural numbers, by constructing some candidate collection of "classes of strings", postulating one of them is a set, and proving it is unique.
Kevin Carlson (Sep 19 2025 at 01:19):Well, yes! Somewhere way up thread I observed that what I think a string is is “a function from a finite total order to the alphabet”. So that’s exactly how I’d like to found formal syntax on set theory.
James Deikun (Sep 19 2025 at 01:27):@Kevin Carlson To clarify your position, do you actually believe it's possible to conceive of any mathematical objects without implicitly defining them in terms of sets? Or is your point specific in some way to syntactic objects like strings and proof trees?
Kevin Carlson (Sep 19 2025 at 01:35):Ah, it’s more that I’m rather fuzzy on what it means to conceive of a mathematical object at all. When I think about natural number arithmetic I’m thinking about actual finite sets, like the set whose two elements are my hands, not “mathematical objects” like “2”, whatever “2” is supposed to be. I’d note that thinking about mathematical objects is a bit déclassé among structuralists, too: they won’t generally have an opinion about what “2” is, it’s just the appropriate element of any of the unlimited number of guys with the universal property of
James Deikun (Sep 19 2025 at 01:48):I might ask at that point which particular set of physical symbols you're thinking of when you think of a function from a finite total order to "the" alphabet, and how you manage to relate that to a string written on paper or a screen which might contain multiple physical signs, say. (Personally, I find that ontologically, it's easier to be rid of concrete particulars--the Mathematical Universe Hypothesis works--than of abstract generalizations.)
Mike Shulman (Sep 19 2025 at 01:55):Kevin Carlson said:
Well, yes! Somewhere way up thread I observed that what I think a string is is “a function from a finite total order to the alphabet”. So that’s exactly how I’d like to found formal syntax on set theory.
That definition depends on having the natural numbers already (to define "finite"). But my point was that you can also give a direct definition of strings in set theory that doesn't rely on already having the natural numbers, following the induction principle of strings in type theory. Given a set of letters, a set of strings is a set together with an element and a function such that if is any subset of that contains and is closed under then .
So, I claim, you don't
Kevin Carlson said:
need to know what the natural numbers are to give a precise definition of a string
You need something in order to ensure that a set of all strings exists, but you can postulate that just as well as you can postulate that a set of all natural numbers exists, and you can prove either of those postulates from the other one. So there's nothing really very special about the natural numbers amongst inductive definitions.
Kevin Carlson (Sep 19 2025 at 01:56):Oh, sure, I fully agree with the non-specialness of here.
Kevin Carlson (Sep 19 2025 at 01:57):Mike Shulman said:
Kevin Carlson said:
Well, yes! Somewhere way up thread I observed that what I think a string is is “a function from a finite total order to the alphabet”. So that’s exactly how I’d like to found formal syntax on set theory.
That definition depends on having the natural numbers already (to define "finite").
Hm? I just mean a total order supported on a set not in bijection with any of its proper subsets.
James Deikun (Sep 19 2025 at 02:01):Kevin Carlson said:
Hm? I just mean a total order supported on a set not in bijection with any of its proper subsets.
This definition (Dedekind finiteness) only leads to a satisfactory definition of string classically, and MLTT is often used for constructive or intuitionistic reasoning.
Mike Shulman (Sep 19 2025 at 02:07):In fact, the equivalence of finiteness to Dedekind finiteness requires not only classical logic but some form of the axiom of choice.
It's also possible to define finite sets directly without the axiom of infinity, so your definition doesn't need the natural numbers in that sense. However, there are a proper class of finite sets, so I'm not sure how "a string is a function from a finite total order to the alphabet" leads to a definition of a set of strings.
Kevin Carlson (Sep 19 2025 at 02:18):James Deikun said:
I might ask at that point which particular set of physical symbols you're thinking of when you think of a function from a finite total order to "the" alphabet, and how you manage to relate that to a string written on paper or a screen which might contain multiple physical signs, say. (Personally, I find that ontologically, it's easier to be rid of concrete particulars--the Mathematical Universe Hypothesis works--than of abstract generalizations.)
-I think I’m not thinking of any particular set; the sentence “a string in is a function from a finite total order to ” is parametric in $$A.$
-I suppose you and I understand how the visual impression comprising the string “visual impression” I currently see on my screen defines a function from any particular 17-element total order to any particular set of ASCII characters, so I don’t particularly see a problem here. And I don’t really see how imagining that one true “abstract ASCII alphabet” exists changes your story about any of that, though the mathematical universe hypothesis seems reputable enough.
James Deikun (Sep 19 2025 at 02:25):Under what I understand to be your view it seems like we would need to agree on a particular exemplar for each ASCII character (and for a 17-element total order) before we could both view the visual impression of "visual impression" and have the same string in mind. This seems strange and I don't think you believe it, but I can't figure out the reason why you don't believe it given your other assumptions.
(The best I can do is some form of structuralism, but this seems to me to smuggle in abstract objects through the back door, so maybe the essential disagreement here is in what structuralism entails?)
Alex Kreitzberg (Sep 19 2025 at 03:26):Excuse me for reaffirming this question:
But do folks have an answer for what Baez's "cohesive homotopy type of well formed expressions" might look like? Looking through references on nlab @Mike Shulman it seems you have a lot of interesting papers on cohesive homotopy type theory, and maybe about spaces that you might have at one point hoped to call "syntax"? Do you have recommendations for where to learn more about this, or is there a paper of yours in particular you'd recommend?
Mike Shulman (Sep 19 2025 at 04:15):Mike Shulman said:
Maybe I'm an old fuddy-duddy, but I would tend to regard something as "less syntactic" the more cohesive it gets. (Abstract) syntax for me is an inductively defined structure, and even in an ambient theory that includes higher homotopy types and cohesive types, inductively defined structures generally automatically turn out to be "discrete" unless you put non-discreteness into them by hand as parameters. I think one could argue that the discreteness of syntax is part of the whole point, as it enables us to define lots of important syntactic operations like typechecking algorithms that depend on properties like decidable equality.
Alex Kreitzberg (Sep 19 2025 at 04:39):Right, but when you said
To be clear: non-discrete inductively defined structures, such as with non-discrete parameters (or with higher constructors), are certainly important, interesting, and useful in certain contexts. I'm just dubious about calling them "syntax" any more.
I understood your clarification as acknowledging important analogous structure that were, in your view nevertheless, distinct from syntax in essential ways.
I'd like to learn more about these analogous structures, or maybe why the discreteness was typical for the more usual ones - and because you've written a lot about cohesive homotopy types, I was hoping for some indication on what to read. (Or am I still misunderstanding the point of what you've wrote?)
Mike Shulman (Sep 19 2025 at 05:15):There's an immense variety of kinds of inductive definition that are used all throughout mathematics, particularly when formulating it inside of type theory. Coproducts, more general colimits, free monoids, free groups and other algebraic structures, factorization systems, localizations, and so on, are all instances of inductive definitions. And when these constructions are performed in a background theory that is cohesive or homotopical, the cohesion or homotopy of the parameters carries through to them.
In addition, introductory texts on [[homotopy type theory]], such as the [[HoTT Book]] or Rijke's [[Introduction to homotopy type theory]], will generally discuss [[higher inductive types]], a kind of inductive definition that gets higher homotopy "put in by hand" rather than inherited from the parameters. And my single paper on cohesive homotopy type theory discusses one example of a "cohesive higher inductive type", the shape modality, which "puts in cohesion by hand" -- although in that specific instance it is sort of the opposite in that the parameter may starts out nontrivially cohesive but the shape puts in new cohesion to kill off the old cohesion and ends up being cohesively discrete (though perhaps nontrivially homotopical).
Alex Kreitzberg (Sep 19 2025 at 05:36):I also saw you were an author on Quantum Gauge Field Theory in Cohesive Homotopy Type Theory, and "Homotopy type theory: the logic of space" inspired me to dive deeper into understanding math via programming - that's why I used the plural when referring to your work on cohesive homotopy types. I really appreciate your writing.
Thank you for your clarification here - it really helps!
John Baez (Sep 19 2025 at 07:39):@Alex Kreitzberg wrote:
If I'm following the conversation correctly, I've mused about Baez's last point as something like "can calligraphy add to mathematical meaning?" Is that a fair interpretation?
Right. It was a deliberately odd question because the usual answer is "no, if the meaning varies continuously as a function of your handwriting that's not math - that's something else."
E.g. we can imagine someone saying that Goedel's increasingly jagged handwriting revealed increasing psychological disturbance as he starved himself to death, but not that it gradually affected the meaning of the symbol in his manuscripts.
In artistic expression, like playing the violin, meaning does seem to vary continuously as a function of the expression. But that seems to be exactly what we want to avoid doing math.
(Perhaps this is why some people think of math as 'uncreative', 'stiff', or 'robotic'.)
@Mike Shulman wrote:
Maybe I'm an old fuddy-duddy, but I would tend to regard something as "less syntactic" the more cohesive it gets. (Abstract) syntax for me is an inductively defined structure, and even in an ambient theory that includes higher homotopy types and cohesive types, inductively defined structures generally automatically turn out to be "discrete" unless you put non-discreteness into them by hand as parameters. I think one could argue that the discreteness of syntax is part of the whole point, as it enables us to define lots of important syntactic operations like typechecking algorithms that depend on properties like decidable equality.
I agree with all this. But sometimes mathematicians like to take crazy leaps, like imagine that -1 has a square root, before formalizing the complex numbers, or - closer to what I'm wondering about now - study 'infinitary logic': logic with infinitely long sentences. (Link for those who haven't looked into this yet.)
These weird things produce feelings of "well, you're just pretending to do math that way" - the feeling that made people call 'em 'imaginary' numbers, or say "you're not really using infinitary logic, you're using ordinary logic to reason about an imaginary world of infinitary logic".
But sidestepping that sort of debate, I'm wondering if someone has tried doing (or pretending to do) non-discrete logic, with non-discrete syntax. Homotopy type theory could be seen as a move in that direction, generalizing sets to homotopy types, but I agree with you that it doesn't really make that leap, which would be a more crazy sort of leap.
@James Deikun wrote:
In the case of string diagrams, it's actually the fact that things are (mostly) continuous that makes them robust, which I think shows there's something to the notion. In fact, to the extent that things are "discrete" in string diagrams, the discreteness arises out of the continuous nature of the interpretation of the syntax because continuous maps into a discrete semantics must be locally constant.
You're right - good point. The fact that string diagrams can be continuously varied is what makes a lot of mathematicians very nervous when first encountering them. But we reassure these mathematicians by proving that the meaning of a string diagram varies continuously but also discretely, and is thus locally constant.
I'm reminded yet again of the quote by Manin:
“I am pretty strongly convinced that there is an ongoing reversal in the collective consciousness of mathematicians: the right hemispherical and homotopical picture of the world becomes the basic intuition, and if you want to get a discrete set, then you pass to the set of connected components of a space defined only up to homotopy.”
Morgan Rogers (he/him) (Sep 19 2025 at 07:40):Kevin Carlson said:
My claim's that you can't make any objective sense of what an inductive definition is--in particular, why an inductive definition should uniquely determine a particular result--without already having the axiom of infinity in your pocket.
This argument only makes sense if you assume ahead of time that an inductive definition is supposed to specify a set. The inductive definition of strings (in some alphabet) tells me how to build strings, and I can prove that something is a string by exhibiting a construction according to the rules set out in the induction principle. I don't need to believe in a unique, coherent collection of all strings to recognize any particular instance of a string, or argue about properties of strings that follow from the inductive definition, let alone believe that such a collection would satisfy any of the axioms (formal or informal) required of a set.
Morgan Rogers (he/him) (Sep 19 2025 at 07:42):There are independent questions about representing strings, but these are no more or less difficult than questions of representing circles and lines in Euclidean geometry.
John Baez (Sep 19 2025 at 07:48):Yes, logicians often take the view that reasoning correctly with symbol strings, following syntactic rules, is more primitive - has fewer ontological commitments - than talking about the set of all symbol strings.
Damiano Mazza (Sep 19 2025 at 08:22):Maybe I don't understand formal set theory (I probably do not), but how does one even define, say, ZF without accepting that strings on a finite alphabet and string-rewriting rules are primitive mathematical objects that do not require a pre-existing notion of set?
Damiano Mazza (Sep 19 2025 at 08:24):By "primitive" I mean that we just posit that everyone understands intuitively what they are, without a formal definition.
Damiano Mazza (Sep 19 2025 at 08:37):My understanding of the foundational ladder has always been:
I'm not sure I have this right, I never looked in depth at anything before level 3, so I may be wrong!
Damiano Mazza (Sep 19 2025 at 08:41):(Notice that, as stressed by Morgan and John, at level 1 you never need to talk about the "set" of all formulas or proofs).
Damiano Mazza (Sep 19 2025 at 10:05):In fact, now that I think about it, a more modern version of the above ladder makes it even more evident how sets are not present at the first stage (or stages):
John Baez (Sep 19 2025 at 14:45):I agree with your old version of the foundational ladder:
Damiano Mazza said:
My understanding of the foundational ladder has always been:
- we accept some finite formal syntax as primitive, and define some basic proof theory with it (formulas and proofs);
- we define a set theory on top of this;
- once we have sets, we formalize model theory and more advanced proof theory (the non-trivial part that requires sets).
- once we have model theory and proof theory, we can do formal math of all sorts.
It goes back at least to Hilbert's program. All the following is about steps 1 and 2:
Whereas the operating with abstract concepts was considered “inadequate and uncertain,” [Hilbert said that] there is a realm of
extra-logical discrete objects, which exist intuitively as immediate experience before all thought. If logical inference is to be certain, then these objects must be capable of being completely surveyed in all their parts, and their presentation, their difference, their succession (like the objects themselves) must exist for us immediately, intuitively, as something which cannot be reduced to something else. (Hilbert 1922b, 202; the passage is repeated almost verbatim in Hilbert 1926, 376, Hilbert 1928, 464, and Hilbert 1931b, 267)
These objects were, for Hilbert, signs. The domain of contentual number theory consists in the finitary numerals, i.e., sequences of strokes. These have no meaning, i.e., they do not stand for abstract objects, but they can be operated on (e.g., concatenated) and compared. Knowledge of their properties and relations is intuitive and unmediated by logical inference. Contentual number theory developed this way is secure, according to Hilbert: no contradictions can arise simply because there is no logical structure in the propositions of contentual number theory.
The intuitive-contentual operations with signs forms the basis of Hilbert’s metamathematics. Just as contentual number theory operates with sequences of strokes, so metamathematics operates with sequences of symbols (formulas, proofs). Formulas and proofs can be syntactically manipulated, and the properties and relationships of formulas and proofs are similarly based in a logic-free intuitive capacity which guarantees certainty of knowledge about formulas and proofs arrived at by such syntactic operations. Mathematics itself, however, operates with abstract concepts, e.g., quantifiers, sets, functions, and uses logical inference based on principles such as mathematical induction or the principle of the excluded middle. These “concept-formations” and modes of reasoning had been criticized by Brouwer and others on grounds that they presuppose infinite totalities as given, or that they involve impredicative definitions (which were considered by the critics as viciously circular). Hilbert’s aim was to justify their use. To this end, he pointed out that they can be formalized in axiomatic systems (such as that of Principia or those developed by Hilbert himself), and mathematical propositions and proofs thus turn into formulas and derivations from axioms according to strictly circumscribed rules of derivation. Mathematics, so Hilbert said, “becomes an inventory of provable formulas.”
Alex Kreitzberg (Sep 19 2025 at 16:53):John Baez said:
Right. It was a deliberately odd question because the usual answer is "no, if the meaning varies continuously as a function of your handwriting that's not math - that's something else."
Maybe you'll find this interesting, perhaps you've heard of Bryne's Euclid published in the 19th century, there's a web recreation of it https://www.c82.net/euclid/book1/. It denotes geometric figure with similar geometric figures instead of variables.
Screenshot_20250919_085402_Chrome.jpg
Of course variations or "errors" drawing small figures simply make the proofs "wrong" instead of different. So we don't have the advantage of constant valued functions on continuously varying data.
The French mathematical and physical biologist D'yves Bouligand; would draw pictures to predict the results of experiments. Although not a "syntax" he makes me think of these sorts of ideas:
Whenever I see arrows in really technical drawings like this, I wonder if there's maybe a categorical story:
I find these sorts of drawings compelling to think about, because it seems to me there could be modern analogs that are perhaps still hard to simulate with a computer, unless you understood their "visual logic".
Of course this isn't handwriting, but I've wondered if drawings like the above could become proofs in a more modern sense.
I've sort of decided this wasn't something I personally could move forward, because an artist with strong visual accuracy once told me they didn't believe people could accurately draw sin curves by hand. Which means you need machines to draw those curves, and what machines do that best? Programs grounded in some constructive foundation like Android's calculator
The math foundations and computer science folks really punch above their "discrete" weight class.
That said, I find your musings about math tied to handwriting encouraging to my interest in this stuff. When I first learned Hilbert wanted "intuitively recognized signs, or sequences of strokes" as an isolated premathematical layer, it made me wonder if I was missing the point.
It's just so easy to imagine obstructions. For example, you can nest function calls and variables for days. Adding continuously meaningful syntax seems like it'd break this. Sort of like how adding continuous voltages to discrete circuits makes them less reliable, but "no more expressive".
Kevin Carlson (Sep 19 2025 at 17:59):Morgan Rogers (he/him) said:
Kevin Carlson said:
My claim's that you can't make any objective sense of what an inductive definition is--in particular, why an inductive definition should uniquely determine a particular result--without already having the axiom of infinity in your pocket.
This argument only makes sense if you assume ahead of time that an inductive definition is supposed to specify a set. The inductive definition of strings (in some alphabet) tells me how to build strings, and I can prove that something is a string by exhibiting a construction according to the rules set out in the induction principle. I don't need to believe in a unique, coherent collection of all strings to recognize any particular instance of a string, or argue about properties of strings that follow from the inductive definition, let alone believe that such a collection would satisfy any of the axioms (formal or informal) required of a set.
Ah, that's very interesting! And yet, wouldn't it be hard to imagine a cartesian closed category of types if that's how you think about a type? Or even more to the point, it seems like talking about the notion of a function between types really requires considering and as actual entities, not just potential ones: to define , you need to give a term of corresponding to every term of . Or maybe now you'll say something like, no, a term of a function type is just an expression with a variable in it that I can evaluate at any term of to get a term of ? Well, that take still feels like you're quantifying over the totality of -terms...
Kevin Carlson (Sep 19 2025 at 18:02):OK, so, I could just about see how you can sleep at night with this, but it seems like a motte to me--I'm dubious that type theorists really are thinking, when they defining the type of strings, "well, who knows what all the strings are, really," let alone "well, who knows what all the loops in the circle are, really". If so, then again, that's really interesting! But I think it's at least as radical a shift from mainstream 20th-century foundations as denying the axiom of infinity in set-theoretic foundations.
Kevin Carlson (Sep 19 2025 at 18:05):@Damiano Mazza @John Baez Yes, this is the implicit defense of formalism that I always find rather bewildering. We're all aware here that Hilbert was proven about as wrong as it's possible to be proven in a foundational program, right? So what's with the idea that his sketch of an approach to establish all mathematics on some finite axiom system is still relevant today?
Kevin Carlson (Sep 19 2025 at 18:11):Let me spell out my idea of a set-theoretic foundation in a bit more detail. There are some things called sets, such as the set of items on my desk right now. Some things, presumably, are not sets; I don't think my mug is a set, personally. For any two things you give me, I can definitely affirm there is a set whose two elements are those two things. If you give me a set whose elements are all sets, I can definitely affirm there's a set whose elements are all the elements of the first set. Two sets are the same if they have all the same elements; there's no notion of order and it doesn't matter how the elements are related to each other. For any two things, there's an ordered pair of those things, which you know how to define in terms of sets from college, so you don't need to imagine some new primitive notion of order. This leads to cartesian products and functions and all that in the usual way.
This is obviously only the very beginning, but you can go on in this way as long as you want, up to and including all of mathematics. There is at no point any need whatsoever to define a formal first-order theory such as ZF to "found" your mathematics on, and it seems to me to be a straightforward confusion that anyone thinks there's any relationship between formal theories and foundations. Whatever is required for formal theories, they are definitely mathematical objects, and it's prima facie absurd to try to found your mathematics on a mathematical object!
Kevin Carlson (Sep 19 2025 at 18:12):(Probably the likeliest objection to the last point is to deny that mathematics needs foundations, which is a reputable position though I disagree; I was responding to the proposed "foundational ladder", which seems to me not to be a reputable position at all.)
Kevin Carlson (Sep 19 2025 at 18:14):Damiano Mazza said:
In fact, now that I think about it, a more modern version of the above ladder makes it even more evident how sets are not present at the first stage (or stages):
- we accept as primitive some basic data structures that may be implemented on a modern-day computer;
- we write a computer program which uses those data structures to provide a core set theory or type theory;
- once we have the core (or "kernel", as people usually call it), we develop a proof assistant;
- once we have a proof assistant, we do formal math of all sorts.
As for this, my main response is that this is simply not how mathematics is in fact founded. Only a miniscule percentage of all mathematics has been "formalized," and it would beg the question to assume that, once a proof has been formalized in a computer, that's somehow a faithful representation of the mathematics itself. If this were an accurate representation of how mathematics is founded, mathematics would really be a formal game of symbol-pushing, and very, very few people would care about it at all.
Alex Kreitzberg (Sep 19 2025 at 18:52):I really resonate with how modern logicians frame foundations, like the way Carlson just did, in part because it seems to me to potentially allow for quite a bit of open mindedness about how mathematics could be done. Is that true?
Shulman recommended the intro to "Mathematical Logic A course with exercises" by Cori and Lascar, and I really liked it. Would this be a good book to work through, or are there better intros to foundations from a modern or cs point of view?
I've been sort of assuming I'd absorb foundational knowledge via HoTT by osmosis, but now I'm not sure that's the most efficient approach.
Mike Shulman (Sep 19 2025 at 19:17):It may be helpful to remind everyone that "foundations" is used in different ways by different people. Sometimes it simply means a theory into which all of mathematics can be encoded, i.e. a theory that is "mathematics-complete". A formal theory can be "foundational" in this sense without implying any formalist philosophy regarding "what mathematics is really about". Other times a "foundation" is asked to supply some philosophical "justification" or "explanation" for mathematics. If we're going to disagree about what is foundational, first we have to agree on what we mean by "foundational".
Kevin Carlson (Sep 19 2025 at 19:22):Yeah, maybe that’s what people are thinking of when they describe foundations by starting with some formal syntax—that first perspective on foundations as providing a formal theory in which all others can be encoded. I’m thinking of the second one, though I wouldn’t phrase it quite that way, mores like “foundations is the practice of finding collections of non-mathematical facts sufficient, once agreed on, to let mathematicians get started doing mathematics.” This second sense is one that probably a lot of people say they don’t think is necessary at all.
Damiano Mazza (Sep 19 2025 at 21:12):Yes I was definitely thinking in terms of the first foundational sense. I am part of those "lot of people" to whom it wouldn't even occur to have to find a foundation for mathematics in the sense of a "justification". Also, adding to what Mike said, I think that insisting that mathematics may be written down as a formal system does not make it a game of symbol-pushing any more than musical notation makes composing music into a game of symbol-pushing.
Damiano Mazza (Sep 19 2025 at 21:22):About Hilbert: he was certainly proven wrong about the fact that the foundational ladder could rest on provably consistent grounds, but the foundational ladder itself is still, as far as I understand, the basis of contemporary foundations (in the sense of "writing mathematics in a formal system"). People working in set theory still use systems built out of strings of symbols, accepting that those strings of symbols do not need any prior formal system to be defined on. I guess that's the "non-mathematical" part of foundations that you (Kevin) are attached to. I prefer to call it "primitive", in the sense of agreed upon without formal justification, but it's the same idea.
Damiano Mazza (Sep 19 2025 at 21:31):In fact, strictly speaking it is not even true that the foundational ladder does not rest on provably consistent grounds. It's just that we need a bigger leap of faith than the one Hilbert was believing to be necessary. In fact, even if Hilbert's program had succeeded (i.e., no Gödel's incompleteness), we would still have needed some faith, namely the faith in the "kernel" system which would have proved the consistency of, say, ZF. It turns out that, instead, we must have faith in ZF itself, or in even bigger systems that can prove the consistency of ZF. I guess people got used to it, and it doesn't seem such a big leap of faith to us now!
Kevin Carlson (Sep 19 2025 at 21:33):You seem to be just saying the same thing I'm saying now. If you are going to establish the consistency of first-order logic on the basis of ZF, then you are just saying you need to believe a description of ZF that does not rely on first-order logic before you can start doing first-order logic. No?
Kevin Carlson (Sep 19 2025 at 21:35):Or probably not, I guess you're imagining an infinite regress of purely formal systems, with ZF proving PA consistent, etc. I certainly would not want to explain mathematics on the basis that it's "turtles all the way down" myself, though.
Kevin Carlson (Sep 19 2025 at 21:35):Damiano Mazza said:
Yes I was definitely thinking in terms of the first foundational sense. I am part of those "lot of people" to whom it wouldn't even occur to have to find a foundation for mathematics in the sense of a "justification". Also, adding to what Mike said, I think that insisting that mathematics may be written down as a formal system does not make it a game of symbol-pushing any more than musical notation makes composing music into a game of symbol-pushing.
I'm finding the analogy to musical notation rather mysterious and perhaps question-begging in the same sense as the claim that mathematics "may be written down" in a formal system.
Anyway, perhaps more interesting is this question of what foundations is for. It's not at all the case historically that what Cantor, Dedekind, and their successors thought they had done in founding mathematics on set theory is the discovery that you can encode many first-order theories into the first-order theory called ZFC. For my part, it would never really have occurred to me to think of calling "formalized mathematics" "foundations." They seem like almost entirely unrelated activities to me, except insofar as Hilbert's program did actually try, unsuccessfully, to give a genuine foundation on a formal system, setting mathematics free of any reason to appeal to extra-mathematical realities. That seems to me to have been a terrible goal, incidentally, which brings us back a bit to the thread this originally spun out of!
Damiano Mazza (Sep 19 2025 at 21:37):As I said, my understanding of these things is shaky, but I think that ZF can be written down so that it "pre-exists" first-order logic. The thing is that it looks exactly like a first-order theory, so we might think we need the whole apparatus of first-order logic (including model theory), but we don't.
Kevin Carlson (Sep 19 2025 at 21:38):Mmhm, I guess at that point I would say that whether you write "Every two sets can be paired" or "" is just a matter of taste (though it's pretty clear which one's more tasteful :) ). Either way, you're not really writing formal syntax.
Damiano Mazza (Sep 19 2025 at 21:38):It's kind of like enriched categories. After you define them, you discover that "plain" categories are -enriched categories. But "plain" categories "pre-exist" enriched ones (you need monoidal categories to define enrichment).
Damiano Mazza (Sep 19 2025 at 21:40):Kevin Carlson said:
Mmhm, I guess at that point I would say that whether you write "Every two sets can be paired" or "" is just a matter of taste (though it's pretty clear which one's more tasteful :) ). Either way, you're not really writing formal syntax.
I guess this is where you and all logicians disagree :smile:
Kevin Carlson (Sep 19 2025 at 21:40):I'm not sure exactly which point you think I disagree with all logicians on, but I doubt it.
Damiano Mazza (Sep 19 2025 at 21:42):That writing a sentence in English and in symbols is in both cases "not really writing formal syntax".
Damiano Mazza (Sep 19 2025 at 21:42):(If I understood you correctly)
Kevin Carlson (Sep 19 2025 at 21:43):You claim all logicians think that both are formal syntax or that one is and the other is not?
Damiano Mazza (Sep 19 2025 at 21:43):A formula is a formal object acceptable by a logician, a sentence in English is not.
Kevin Carlson (Sep 19 2025 at 21:44):Sure, a formula is a formal object, once you've defined what a formula is. But you were proposing to pseudo-formalize ZF before defining what a formula is.
Damiano Mazza (Sep 19 2025 at 21:47):That's the thing: I don't think formulas need to be "defined" in the sense you appear to be thinking! For me, a formula is an object that can be agreed upon much more easily than a freely written English sentence.
Kevin Carlson (Sep 19 2025 at 21:49):I don’t see how two people are really doing anything when they agree on a formula like the one I wrote other than translating it in their heads to a mental representation of the sentence “for any two things there’s a set whose elements are exactly those two things”, which is so obviously easier to agree on that I’m sure I’m entirely missing your point.
Damiano Mazza (Sep 19 2025 at 21:49):I think we both agree on this: we must agree on some objects that we both consider to be "self evident". You consider "sets", described in plain English, to be such objects. I (and, I think, all logicians) take formulas.
Kevin Carlson (Sep 19 2025 at 21:50):I don’t even know what it would mean for formulas to be self-evident, and I don’t really think that’s what I claim about sets.
Damiano Mazza (Sep 19 2025 at 21:51):I mean the syntax of formulas, the definition of "what is a formula". It's not hard to agree on what is a first-order formula in the language of set theory (for example).
Damiano Mazza (Sep 19 2025 at 21:52):Ok then I misunderstood your claim about sets. I thought you were saying that we all intuitively understand what a set is (and I agree with you).
Damiano Mazza (Sep 19 2025 at 21:53):Don't you agree that there are ambiguities in natural language that formulas avoid?
Kevin Carlson (Sep 19 2025 at 21:54):Sure, it’s important to learn to use formulas at some point in your education so you notice than “any” is ambiguous and stuff like that. But I don’t think it’s related to much of what I’ve been saying.
Kevin Carlson (Sep 19 2025 at 21:55):That’s all about the semantics of formulas, anyway. It doesn’t seem very important to me to know much about the formal manipulation of syntax to do good math.
Kevin Carlson (Sep 19 2025 at 21:56):(Unless you’re studying formal syntax, of course!)
Damiano Mazza (Sep 19 2025 at 21:56):I am not talking about "doing good math". I am talking about writing down math in a completely unambiguous way.
Damiano Mazza (Sep 19 2025 at 21:56):Which is something absolutely necessary for foundational purposes.
Kevin Carlson (Sep 19 2025 at 21:57):Well, isn’t it relevant to this question that a minuscule proportion of math for human consumption is in fact written down in logical formulas? Formulas occur almost exclusively in logic papers, because logicians are often studying formulas, not just using them.
Kevin Carlson (Sep 19 2025 at 21:58):Damiano Mazza said:
Which is something absolutely necessary for foundational purposes.
I agree that foundations need to be unambiguous but I deny that people have any ambiguity about the meaning of basic properties of sets expressed in natural language.
Kevin Carlson (Sep 19 2025 at 21:58):I’d be intrigued to see a proposed counterexample.
Kevin Carlson (Sep 19 2025 at 21:59):Of course you need to know that classes and sets are different to avoid paradoxes, but it’s not formulas that fixed that problem, but understanding the concept of class better. Frege invented both formal logic and inconsistent foundations!
Damiano Mazza (Sep 19 2025 at 22:34):Sorry, I had to leave for a moment (and I'll have to go soon, it's late here).
About an example of ambiguity : you already gave one above. When you write "every two sets can be paired", I don't even know what you mean. What does "pairing" mean? How do you "pair" sets? Sure, you add more words, you give a more accurate description. But how do you know I won't misinterpret? A formula cannot be misinterpreted.
About the usefulness of formulas: remember that the key point is formalizing proofs. Like formulas, these are certain labelled trees (a primitive concept that needs no pre-existing formal system). Formulas allow you to do this very nicely: introduction of connectives, elimination of connectives, etc. Defining formal proofs using plain English sentences instead of formulas seems impossible to me.
Now I have the feeling that you are going to question the usefulness of formal proofs, because you've been doing fine all your life writing proofs in plain English. So have I! But try, without formal proofs, to prove that a certain statement written in plain English is unprovable in your system of axioms written in plain English with a proof written completely freely in plain English. Good luck!
Kevin Carlson (Sep 19 2025 at 22:40):Formal proofs are, of course, great and quite necessary if you want to prove something about proofs! You need to give a definition of any object you're going to try to prove something about. And I agree that you need formal syntax for formal proofs. I haven't said anything that was intended to disagree with any of that. I just think the obvious definition of a formal proofs is in terms of some inductively defined set, and your induction principle is most reasonably founded on pre-formal understandings about sets. But we're not in disagreement about anything about formal proofs. I just don't see what formalization of proofs has to do with foundations, and didn't mean to be talking about it.
I very much disagree that a formula cannot be misinterpreted; indeed formulas have no interpretation, in their own right, and of course it's possible to apply some given interpretation incorrectly, and such errors comprise a substantial difficulty in mathematical education during the brief period that relies a lot on formulas. Dually I don't think it's possible in any pragmatically significant sense to misinterpret the sentence “for any two things there’s a set whose elements are exactly those two things”.
Kevin Carlson (Sep 19 2025 at 22:40):Sorry to keep you up late! I was trying to slow down the rhythm myself but happened to see your last just as you sent it.
John Baez (Sep 19 2025 at 22:45):Kevin Carlson said:
Damiano Mazza John Baez Yes, this is the implicit defense of formalism that I always find rather bewildering. We're all aware here that Hilbert was proven about as wrong as it's possible to be proven in a foundational program, right?
I don't think so. Yes, his hopes for purely finitary proofs of the consistency and completeness of rich systems of mathematics were dashed - but they were dashed by theorems, and we've learned to live with those theorems. We (or at least I) still think that there's something really sturdy and useful about stating axioms that are rules for manipulating symbol strings, where we can check whether the rules are being followed without needing to think about what the symbol strings mean, or using any complicated concepts. In fact this way of thinking helped lead to computers, which are great at following precise rules without caring about meaning. So I tend to think that his formal approach is fundamental to our modern computer-based civilization.
I'm not saying this is all there is to math, of course! Hilbert didn't think that either.
Damiano Mazza (Sep 19 2025 at 22:46):Yes I understand (I now remember that you (Kevin) had written it before but the conversation went elsewhere) that you (Kevin, again) are separating the concepts of "foundations" and "formalization". I think that the former is not fully satisfactory without the latter, but I do see that it is possible to develop foundational questions without necessarily doing formal mathematics, and I will certainly not object to you doing that!
Kevin Carlson (Sep 19 2025 at 22:58):John Baez said:
I don't think so. Yes, his hopes for purely finitary proofs of the consistency and completeness of rich systems of mathematics were dashed - but they were dashed by theorems, and we've learned to live with those theorems. We (or at least I) still think that there's something really sturdy and useful about stating axioms that are rules for manipulating symbol strings, where we can check whether the rules are being followed without needing to think about what the symbol strings mean, or using any complicated concepts. In fact this way of thinking helped lead to computers, which are great at following precise rules without caring about meaning. So I tend to think that his formal approach is fundamental to our modern computer-based civilization.
I'm not saying this is all there is to math, of course! Hilbert didn't think that either.
Sure, I can't help but agree that computers are important and related to formal syntax systems. And a Turing machine is, famously, an ordered septuple... :innocent:
But, yeah, I don't think that the influence of formalism on computers has anything to do with foundations.
James Deikun (Sep 19 2025 at 23:01):Kevin Carlson said:
This is obviously only the very beginning, but you can go on in this way as long as you want, up to and including all of mathematics. There is at no point any need whatsoever to define a formal first-order theory such as ZF to "found" your mathematics on, and it seems to me to be a straightforward confusion that anyone thinks there's any relationship between formal theories and foundations. Whatever is required for formal theories, they are definitely mathematical objects, and it's prima facie absurd to try to found your mathematics on a mathematical object!
Hm. I would say that sets are mathematical objects, though. Sure, you can just about defend a claim that sets of physical objects are physical objects, although there then is no distinction between a singleton and its element, but sets of sets are not physical objects and have a mathematical component and I'm not sure what the sets of the cumulative hierarchy (with no atoms) could possibly be but purely mathematical objects.
Kevin Carlson (Sep 19 2025 at 23:01):Certainly, mathematics is not whatsoever "an inventory of provable formulas", and nobody thinks it is; if you try to insist that number theory is about numerals, that's where you inevitably end up if you're as serious a thinker as Hilbert was. If you, as I think category theorists usually do, realize that a statement about "numerals" can be interpreted as a general theorem about finite sets, then you don't seem to end up saying anything quite so silly!
John Baez (Sep 19 2025 at 23:04):@Kevin Carlson wrote:
But, yeah, I don't think that the influence of formalism on computers has anything to do with foundations.
I guess we use the word "foundations" in different ways! To me, the solid rock of syntactic manipulation is the bottom-most "foundations".
John Baez (Sep 19 2025 at 23:04):Anyway, I should let you talk with Damiano, because my desire to discuss this is essentially exhausted - it's enough work just watching other people talk!
Kevin Carlson (Sep 19 2025 at 23:05):James Deikun said:
Hm. I would say that sets are mathematical objects, though. Sure, you can just about defend a claim that sets of physical objects are physical objects, although there then is no distinction between a singleton and its element, but sets of sets are not physical objects and have a mathematical component and I'm not sure what the sets of the cumulative hierarchy (with no atoms) could possibly be but purely mathematical objects.
No, I don't think that a set whose elements are physical objects is a physical object. I'm probably not sure whether it's a "mathematical" object, or exactly what that means...It's certainly an object that I can do some math to and/or about, but that's true of most objects...What I'm sure it's definitely not is an abstract or ideal object, which is the kind of thing I was really trying to complain about, which every kind of modern approach to mathematics has banished one way or another. I think a set whose elements are two particular and concrete objects is, itself, particular and concrete, and that's great.
James Deikun (Sep 19 2025 at 23:08):But what about a set like ? This has no particular, concrete component, it is purely abstract and ideal. Thus, further, a similar set like may have a concrete and particular component, but also an abstract and ideal component.
James Deikun (Sep 19 2025 at 23:18):Furthermore, even if you accept all sets as concrete, particular objects, then you're left with questions of "the unreasonable effectiveness of mathematics", because reducing abstractions to sets doesn't tautologically justify their use to reason about concrete particulars in the way we do. (You can make the case for natural number arithmetic, maybe, but not for, say, geometry.)
Kevin Carlson (Sep 19 2025 at 23:19):I don't think "the set with no elements" is particularly abstract. There's only one of them! But if you don't like the empty or the singleton, you can just pick your two favorite things and encode set theory such that instead of the empty set you use as if it's the empty set, with every other set building from there. This is actually what Mayberry does in his book, mostly on the basis that the Greek concept of "arithmos" he builds off of probably didn't allow for empties or singletons.
Kevin Carlson (Sep 19 2025 at 23:22):James Deikun said:
Furthermore, even if you accept all sets as concrete, particular objects, then you're left with questions of "the unreasonable effectiveness of mathematics", because reducing abstractions to sets doesn't tautologically justify their use to reason about concrete particulars in the way we do. (You can make the case for natural number arithmetic, maybe, but not for, say, geometry.)
I think I agree that set-theoretic foundations explain arithmetic's connectedness to the real world much better than they explain that of geometry. Analysis is, perhaps, some intermediate case. But it seems to me that other foundational proposals explain none of this connectedness, so I don't see that as much of a problem.
Alex Kreitzberg (Sep 19 2025 at 23:28):I think of sets as "geometric", they're one take on an absolute minimum "geometry" to get started. I just feel weird calling them "geometry" because I think "geometry" ought to have a metric.
But I'll draw them as a bag of dots.
Is Deikun saying the "+ structure" part of math does more than what we usually think of ZFC style axiomatic set theory as doing?
Or is that take something like HoTT style axiomatics allow geometric/topological interpretations more naturally?
James Deikun (Sep 19 2025 at 23:30):I still think
owes all of its mathematical properties to the abstract, ideal part of its essence rather than to the concrete particular part that ties it to the Eiffel Tower and the Golden Gate Bridge, and that mixing in some concrete particularity here is simply a sleight of hand.
Kevin Carlson (Sep 19 2025 at 23:34):Isn't it just constitutive of how you're going to use the word "mathematical" that mathematical properties of a set don't depend on concrete details about the elements of the set? But it's still a world of difference to say that, basically, "two isomorphic sets have all the same mathematical [or perhaps, "abstract"] properties" versus "this particular set is, itself, an abstract object", no?
Kevin Carlson (Sep 19 2025 at 23:35):Alex Kreitzberg said:
I think of sets as "geometric", they're one take on an absolute minimum "geometry" to get started. I just feel weird calling them "geometry" because I think "geometry" ought to have a metric.
But I'll draw them as a bag of dots.
Is Deikun saying the "+ structure" part of math does more than what we usually think of ZFC style axiomatic set theory as doing?
Or is that take something like HoTT style axiomatics allow geometric/topological interpretations more naturally?
I think James was saying that founding something like Euclidean geometry on set theory, whether in a synthetic or an analytic presentation, doesn't seem to clarify how it is that we find many physical objects approximately obeying the theorems of Euclidean geometry, in contrast with the situation where, if we found natural number arithmetic on finite set manipulations by essentially categorifying the arithmetic operations, then it's almost tautological why theorems of arithmetic reflect the behavior of real-world objects.
James Deikun (Sep 19 2025 at 23:41):I think a higher-rank set that contains concrete items as atoms is a composite of an abstract, ideal object describing its structure as an -tree, some concrete, particular objects, and an abstract, particular object that relates them, and the first one is doing all the mathematical work. (Not all the "abstract" work--"is a set of things I don't own" is an abstract property...)
Kevin Carlson (Sep 19 2025 at 23:44):OK, I see. It's fun to see somebody defending abstract ideal objects explicitly, even if it seems to me that, historically, much of the point of giving set-theoretic definitions of mathematical objects was to avoid abstract ideals. I guess you see those set-theoretic definitions as arbitrary encodings of the "real" abstract objects? Do you imagine there's something answering to the name of "" which is neither a set or class, but is an individual specific object?
James Deikun (Sep 19 2025 at 23:48):I guess that depends on how I end up deciding to feel about numerical identity of objects, which I haven't exactly decided on yet. The way I'm leaning, though, is that fundamentally the only "the" is the categorist's "the" and other kinds of "the" are context-dependent.
Kevin Carlson (Sep 19 2025 at 23:50):So you'd say that "" is just referring to "a -element set, considered essentially up to isomorphism"? Because I'd agree with that; I thought you'd say something quite different with all the abstract ideals floating around.
James Deikun (Sep 19 2025 at 23:52):That is, I don't really think there's a meaningful difference between saying "" is equally any -element set you care to name, saying "" is a particular object that lies in a certain relation to all -element sets, and "" is the property of being a -element set, among others. I don't think it's possible to pin down the boundaries between "" and the rest of the world sufficiently to distinguish those possibilities. (In a physics analogy, the distinctions here would all be "pure gauge".)
Kevin Carlson (Sep 19 2025 at 23:55):Oh, wow!
David Michael Roberts (Sep 20 2025 at 08:57):But, you might say, "none of this shakes my belief that 2 and 2 are 4." You are quite right, except in marginal cases -- and it is only in marginal cases that you are doubtful whether a certain animal is a dog or a certain length is less than a meter. Two must be two of something, and the proposition "2 and 2 are 4" is useless unless it can be applied. Two dogs and two dogs are certainly four dogs, but cases arise in which you are doubtful whether two of them are dogs. "Well, at any rate there are four animals," you may say. But there are microorganisms concerning which it is doubtful whether they are animals or plants. "Well, then living organisms," you say. But there are things of which it is doubtful whether they are living organisms or not. You will be driven into saying: "Two entities and two entities are four entities." When you have told me what you mean by "entity," we will resume the argument.
https://old.maa.org/press/periodicals/convergence/quotations/russell-bertrand-1872-1970-10
David Michael Roberts (Sep 20 2025 at 09:02):Kevin Carlson said:
Let me spell out my idea of a set-theoretic foundation in a bit more detail. There are some things called sets, such as the set of items on my desk right now. Some things, presumably, are not sets; I don't think my mug is a set, personally. For any two things you give me, I can definitely affirm there is a set whose two elements are those two things. If you give me a set whose elements are all sets, I can definitely affirm there's a set whose elements are all the elements of the first set. Two sets are the same if they have all the same elements; there's no notion of order and it doesn't matter how the elements are related to each other. For any two things, there's an ordered pair of those things, which you know how to define in terms of sets from college, so you don't need to imagine some new primitive notion of order. This leads to cartesian products and functions and all that in the usual way.
I was thinking that one could approach concrete syntax—actual marks or signs—in the same way: there are some things called strings, made of ordered symbols, and for any two strings given to be in order, I can definitely affirm there's a string whose symbols are those that .... etc.
If you want, you can call the collection of glyphs "sets" of symbols and the glyphs the elements. This is of course taking a rather formalist approach to mathematics. But I don't have to say that the strings are made of the usual symbols of first-order logic. They can be the everyday usual strings of symbols working mathematicians use.
David Michael Roberts (Sep 20 2025 at 09:05):I used to joke, when I was a lecturer, that I was in the business of rewiring student's brains. Ultimately the mathematics they learn (to whatever level of completeness) is neural patterns in their brain that can be said to correspond to other patterns in other brains. This can be communicated by a shared language. Kevin Buzzard liked to highlight the process of transmission of mathematics in talks a few years back, via the path brain > tex > pdf on writer's machine > pdf on reader's machine > brain (roughly; his point was that one could use Lean and get better detail recorded and less scope for errors)
Alex Kreitzberg (Sep 20 2025 at 15:51):When I originally asked "Why not start with Category theory as your foundation" I think I had in mind formal systems for encoding mathematics that looked a lot like category theory, not unlike tools like CatColab.
I was wondering "Why not use a math proof assistant that tracked how much energy calculations used" or however you would try to model how mathematical arguments might relate to a broader ecology. And I probably left it too implicit how I imagined this might relate to category theory. I see a lot of Baez's work as ecologically inspired in a manner that seems hard to model in a straightforward way with lambda calculus or ZFC inspired systems, for example.
I don't see this as unrelated to how one might argue garbage collectors actually obscure information about how the cost of various data are related, as opposed to linear type systems.
Now, it isn't actually clear to me that foundations in the "how do we justify math" sense are actually unrelated to this. I agree that my basic conclusions about sets will agree with other mathematicians, and that I can be certain about this agreement, even if I don't know why. I interpreted the original article inspiring the thread as trying to ask something like "is this notion of a set we readily agree on - bad for the environment? If so, is it possible to replace it with something else we can be certain about that isn't?"
Is it "foundational" to ask "Can we think of our primitive notion of set as having a cost associated to its size?" For example? Or am I mixing levels?
The way I'm thinking about this is a finitest might put up front an infinite price for infinite sets, "they don't like them". Or exact representations of numbers worked out as far as you could want, have associated asymptotic costs that we would think of as "baked in".
But maybe this framing is confused or not really about "justifying math" foundations?
Kevin Carlson (Sep 20 2025 at 16:43):David Michael Roberts said:
I was thinking that one could approach concrete syntax—actual marks or signs—in the same way: there are some things called strings, made of ordered symbols, and for any two strings given to be in order, I can definitely affirm there's a string whose symbols are those that .... etc.
I think it’s essentially true that you can do that kind of thing, but that there are much bigger difficulties in doing so with strings than with sets. You will have to immediately define a much more abstruse notion of equivalence of strings than the simple notion for sets, for instance, if you want to understand when people are writing essentially the same thing. You will have questions about whether a string can break off the end of a page, or off the end of a universe, or whether it can be represented via electrical signals, and all kinds of pretty tricky stuff. This is all perfectly resolvable but it seems clear to me that what the resolution actually is is to say “a string in an alphabet is a function from a finite total order to that alphabet.” Why would you want your mathematical definition to start out relying on details of physics when you could have the latter definition instead?
Kevin Carlson (Sep 20 2025 at 16:50):The Russell quote is cute but I don’t see why I should have to define entities to say “whenever you have two things you accept as entities and two other such things, putting them together will get 4.” The idea is that mathematicians might need to agree about sets to get math off the ground, not that they need to agree about general metaphysics, which is clearly hopeless.
James Deikun (Sep 20 2025 at 17:20):Despite all these metaphysical complexities, though, it seems at least as easy to get actual mathematicians to agree on what a string is as what a set is. As long as they don't go out of their way to get into the metaphysics, anyway.
Alex Kreitzberg (Sep 20 2025 at 17:26):Why shouldn't we worry about physical issues in foundations?
James Deikun (Sep 20 2025 at 17:32):Possibly we should. If you push a little, though, a "definite entity" like "the Eiffel Tower" is really about as fraught as a "symbol" like "A" though. We know perfectly well how to make strings by arranging "symbols" along a "line", though "symbol" and "line" are themselves complex, nebulous concepts, similarly to how we know how to make sets by aggregating "entities" though "entity" is itself a complex, nebulous concept.
James Deikun (Sep 20 2025 at 17:34):(Note that if you get into fundamental physics there are no entities with distinct identities, only fields. The fields themselves hardly qualify as entities since we can't even say how many there are!)
John Baez (Sep 20 2025 at 18:07):The physical world is probably even more mysterious than the mathematical world. It keeps getting more removed from everyday common sense the more we learn about it, and there's no sign that we're almost done. So the idea that math is fundamentally about the physical world is pretty terrifying to me. There's also a strange circularity here, given that if you ask me what, say, a quark is, I'd have to say it's an operator-valued distribution taking values in the tautologous representation of .
Kevin Carlson (Sep 20 2025 at 18:19):James Deikun said:
Despite all these metaphysical complexities, though, it seems at least as easy to get actual mathematicians to agree on what a string is as what a set is. As long as they don't go out of their way to get into the metaphysics, anyway.
I don’t exactly disagree with that—it just seems to me, like I’ve been saying, is that what mathematicians agree that a string is, is a function from a finite total order to its alphabet. Certainly nobody disagrees that that’s a correct definition, though some would prefer to characterize what they are inductively rather than define them directly.
Kevin Carlson (Sep 20 2025 at 18:22):(deleted)
Kevin Carlson (Sep 20 2025 at 18:22):Alex Kreitzberg said:
Why shouldn't we worry about physical issues in foundations?
Mathematical fact isn’t dependent on the specific nature of the physical universe we happen to be in. I think that claim would find almost universal acceptance. If it were, it’d just be physics.
As James says, if you’re going to bother with foundations of math, you want to find the least controversial possible foundations that’ll let you get on with it. Many things about physics are controversial and even unknown; deep thinking about metaphysics is even worse. You want to allow people to bring their own understanding of physics and metaphysics as much as possible and end up doing the same math. It turns out, I think, that math is almost perfectly parametric in your metaphysics and doesn’t depend on physics in any way at all.
Alex Kreitzberg (Sep 20 2025 at 18:24):I feel as my understanding of the issues that foundations are trying to solve improves - the more dubious the original premise of the article, or at least my understanding of the original article, is.
Alex Kreitzberg (Sep 20 2025 at 18:29):I'm maybe getting indirectly convinced, that practically speaking, if you found an ecologically relevant formal theory, that was really good at solving problems. Then folks would then be motivated to sort out foundational issues with it, if they seemed relevant.
But then again, this seems like an overly pessimistic view on my part. Because I'm understanding Bishop's constructive mathematics, for example, to be a result of carefully thinking about foundational issues with the continuum. And it has practical consequences on how people do math.
Alex Kreitzberg (Sep 20 2025 at 18:42):Maybe math is independent of physics, but physics has some opinions on how much math we're allowed to have
Mike Shulman (Sep 20 2025 at 18:53):Kevin Carlson said:
it just seems to me, like I’ve been saying, is that what mathematicians agree that a string is, is a function from a finite total order to its alphabet. Certainly nobody disagrees that that’s a correct definition, though some would prefer to characterize what they are inductively rather than define them directly.
I might have gotten lost somewhere in this spaghetti thread, but did you respond to my point that if you take that as a definition in set theory (or any non-univalent theory, really) then there is a proper class of strings in any nonempty alphabet?
Kevin Carlson (Sep 20 2025 at 19:35):Oops, no, I had missed that point, thanks. Yeah, you’ll have to pick a particular preferred set of total orders with one per cardinality to define a good set of all strings, presumably whichever ones form your favorite natural numbers. I still think if I wanted to say what a single string is I’d say the same thing I’ve been saying. It’s too much to expect that people would agree on exactly what the set of strings is, insofar as is such a set.
Kevin Carlson (Sep 20 2025 at 19:37):Alex Kreitzberg said:
Maybe math is independent of physics, but physics has some opinions on how much math we're allowed to have
I’m not entirely sure what you mean by that. Just that humans have cognitive abilities that are bounded by physical constraints? That’s certainly true but I don’t see how it’s relevant.
Alex Kreitzberg (Sep 20 2025 at 20:01):To clarify my understanding of the terms.
If tomorrow we discovered a computer design that could calculate the basic Surreal number operations in O(1) time, that wouldn't necessarily have any implications on the foundations of mathematics; because, it wouldn't necessarily change what we agree mathematics is?
John Baez (Sep 20 2025 at 20:07):By the way, people call this sort of thing hypercomputation, although most people in that subject dream of machines that can compute non-computable functions .
There are only functions ; I don't know if any people have thought hard about "bigger universes" with laws of physics that let you build machines that can compute even more functions.
(People think about a lot of weird stuff.)
Mike Shulman (Sep 20 2025 at 20:09):Kevin Carlson said:
It’s too much to expect that people would agree on exactly what the set of strings is
One nice thing about type-theoretic foundations is that because elements of types don't have any spurious "internal identity" like elements of sets do, in type theory everyone can agree on exactly what the set of strings is.
Alex Kreitzberg (Sep 20 2025 at 20:32):I risk asking questions that I think make me look silly, because then you guys just drop these nuggets. It's especially fun to learn things I didn't know were learnable.
Kevin Carlson (Sep 20 2025 at 22:17):Mike Shulman said:
Kevin Carlson said:
It’s too much to expect that people would agree on exactly what the set of strings is
One nice thing about type-theoretic foundations is that because elements of types don't have any spurious "internal identity" like elements of sets do, in type theory everyone can agree on exactly what the set of strings is.
Arguably it’s a bit more like agreeing not to worry about it :smiling_face:
John Baez (Sep 20 2025 at 23:14):Come on, stop arguing about whether people are agreeing about what strings are, or agreeing to not worry about it. :upside_down:
James Deikun (Sep 21 2025 at 00:10):I think mathematics would at least be thought about very differently in a universe where you could write infinitely long strings. First order logic as we know it and finite/recursive axiomatizations would be much less important than they are to mathematicians in our universe, and a theory like ZFC would probably be considered a super weak foundation.
Alex Kreitzberg (Sep 21 2025 at 00:32):It could be fun to write a sci-fi story based on that premise - mathematician checks in on how folks go about mathematics in the, even bigger, universe next door.
Wasn't trying to make a straw man with that question, thought I finally understood the point :sweat_smile:
Alex Kreitzberg (Sep 21 2025 at 03:50):Thanks for the above discussion in this thread, I believe I understand foundational issues and methods a lot better now.
It's really given me some nice context for how special it is that we can talk about infinite things at all.
John Baez (Sep 21 2025 at 10:20):I like that sci-fi idea. I decided to popularize it on Mathstodon:
It's Sunday, time for idle speculations:
If spacetime had far more points than it does in our unvierse, then the way we do logic might be very different.
In our universe, most logicians act like we can write down infinitely many different strings of symbols. But this is just the smallest infinity, called ℵ₀. There are a lot more real numbers, namely 2 to the ℵ₀. This larger infinity sets the limits on how many points there are in space. But since there's a limitation to the accuracy of our measurements, we can only write down ℵ₀ different symbol strings. In our universe.
There are much larger infinities, though. Logicians have thought about logic with infinitely long statements - even for one of these much larger infinities. It's called 'infinitary logic'. We can't really use infinitary logic, but we can prove theorems about what it would be like.
I don't know if physicists have imagined laws of physics that would give infinitely bigger universes, whose inhabitants could actually use infinitary logic. For example, imagine a universe whose inhabitants use an alphabet with 2 to the ℵ₀ different symbols - and can actually recognize the difference between them! They could talk about vastly more complex things than we can. Their math would be much deeper. ℵ₀ would seem small to them.
I think someone should give it a try, just for fun. It could at least make for a good science fiction story.
Here's an easy intro to infinitary logic:
https://en.wikipedia.org/wiki/Infinitary_logic
Here's a deeper intro:
https://plato.stanford.edu/entries/logic-infinitary/
I spend a lot of time talking math on the Category Theory Community Server. When I raised the possibility of a physical universe that let us a larger infinity of symbols in our math, James Deikun wrote
"I think mathematics would at least be thought about very differently in a universe where you could write infinitely long strings. First order logic as we know it and finite/recursive axiomatizations would be much less important than they are to mathematicians in our universe, and a theory like ZFC would probably be considered a super weak foundation."
Ordinary first-order logic is 'compact'. This means that if you have a theory in first-order logic with infinitely many axioms, and every finite subset of these axioms has a model, then the whole set of axioms has a model. This is extremely important in logic, and it connects logic to topology:
https://en.wikipedia.org/wiki/Compactness_theorem
Infinitary logics are usually not compact. But there's a generalization of compactness that's pretty interesting.
If you give me a cardinal κ, we can talk about a logic that allows infinitely many variable names, infinitely long conjunctions, and formulae with infinitely many alternating quantifiers ∀∃∀ ... - but only if these infinities are less than κ. This logic is called L(κ,κ).
Then we say κ is 'strongly compact' if whenver you have a theory in this logic with infinitely many axioms, and every subset of axioms with cardinality < κ has a model, the whole theory has a model.
Logicians would like to live in a universe where people used the logic L(κ,κ) for a strongly compact cardinal κ.
But it turns out strongly compact cardinals bigger than have to be really, really, really, really, really large.
Alex Kreitzberg (Sep 21 2025 at 14:27):I actually have a handful of ideas for mathematical video games I'd like to make! But this idea wants to be a novel because we don't have hypercomputation.
I've heard writing described as "Expressing with words - what can't be expressed with words"
Defining higher infinities with our finite sentences resonates with this sentiment in a disarmingly literal way. So of course a sci-fi story about higher infinities should be expressed with writing as well :relieved:
Sam Speight (Sep 21 2025 at 16:19):Kevin Carlson said:
Alex Kreitzberg said:
I think of sets as "geometric", they're one take on an absolute minimum "geometry" to get started. I just feel weird calling them "geometry" because I think "geometry" ought to have a metric.
But I'll draw them as a bag of dots.
Is Deikun saying the "+ structure" part of math does more than what we usually think of ZFC style axiomatic set theory as doing?
Or is that take something like HoTT style axiomatics allow geometric/topological interpretations more naturally?
I think James was saying that founding something like Euclidean geometry on set theory, whether in a synthetic or an analytic presentation, doesn't seem to clarify how it is that we find many physical objects approximately obeying the theorems of Euclidean geometry, in contrast with the situation where, if we found natural number arithmetic on finite set manipulations by essentially categorifying the arithmetic operations, then it's almost tautological why theorems of arithmetic reflect the behavior of real-world objects.
I thought that the categories of physical/concrete objects and of abstract objects are complementary in the universe of all objects.
Mike Shulman (Sep 21 2025 at 16:43):Kevin Carlson said:
Arguably it’s a bit more like agreeing not to worry about it :smiling_face:
I don't see any argument for that, unless you beg the question by starting from a set-theoretic perspective that everything has internal identity in the first place.
Kevin Carlson (Sep 22 2025 at 18:42):It just seems to me very deeply baked in to the nature of type theory that you're never saying "what a type really is"; you're just saying various things you can do with types and various things you can do with their terms and everybody agrees that that's sufficient to accomplish their common mathematical/computational goals. I don't see how type theory has any opinion about whether it's more correct to say "we all agree on what the type of natural numbers is" or "we all agree on what the functional properties of the type of natural numbers is, and beyond that we're agnostic."
Kevin Carlson (Sep 22 2025 at 18:42):I suppose you might say that type theory says that types that have all the same functional properties are (by the definition of "same") the same, but I'm not really convinced it necessarily does do that. Even univalent type theories, of course, have (some of) their semantics in places where univalent equality and literal equality diverge, and it seems that it's perfectly valid for me to do type theory while imagining that what I'm talking about is some such model.
Kevin Carlson (Sep 22 2025 at 18:43):Sam Speight said:
I thought that the categories of physical/concrete objects and of abstract objects are complementary in the universe of all objects.
I'm not sure whether you're asking a question here or how that's related to what you quoted. Certainly in some sense "abstract" should be the negation of "concrete", though I definitely wouldn't identity "concrete" with "physical."
Sam Speight (Sep 23 2025 at 08:01):Kevin Carlson said:
Sam Speight said:
I thought that the categories of physical/concrete objects and of abstract objects are complementary in the universe of all objects.
I'm not sure whether you're asking a question here or how that's related to what you quoted. Certainly in some sense "abstract" should be the negation of "concrete", though I definitely wouldn't identity "concrete" with "physical."
You seemed to be suggesting that there were objects that were neither physical nor abstract, and I was curious to hear what you meant.
Kevin Carlson (Sep 23 2025 at 19:16):Yeah, so, for instance "Raskolnikov, the protagonist of Crime and Punishment" seems to me to be no more abstract than any particular actual human, even though he does not physically exist: he's concrete in that he's a completely specific individual. I'm saying that while trying to avoid taking any particular position on in what sense "Raskolnikov" "really exists."
Mike Shulman (Sep 23 2025 at 19:32):Kevin Carlson said:
It just seems to me very deeply baked in to the nature of type theory that you're never saying "what a type really is"; you're just saying various things you can do with types and various things you can do with their terms and everybody agrees that that's sufficient to accomplish their common mathematical/computational goals. I don't see how type theory has any opinion about whether it's more correct to say "we all agree on what the type of natural numbers is" or "we all agree on what the functional properties of the type of natural numbers is, and beyond that we're agnostic."
I'm struggling to understand what you mean by this. There seems to me to be a very clear difference between
def ℕ : Type ≔ data [ zero. | suc. : ℕ → ℕ ]
which defines the natural numbers to be one specific type, which contains concrete specific elements such as zero. and suc. zero. and suc. (suc. zero.), and
def ℕs : Type := sig (
ℕ : Type,
zero : ℕ,
suc : ℕ → ℕ,
ind : (P : ℕ → Type) (z : P zero) (s : (n:ℕ) → P n → P (suc n)) (n : ℕ) → P n
)
which defines the collection of types that have the functional properties of the type of natural numbers.
Kevin Carlson (Sep 23 2025 at 20:11):Yes, that makes sense. I think I’m cavilling with the sense in which the first definition defines “one specific type.” It doesn’t seem that type theory cares what I think this thing ‘zero’ in Nat is: whether it’s a string, or a memory address, or the empty set, or whatever. Probably actually type theory would get mad at me for trying to ask the question, because of course ‘zero’ is by definition a natural number! It just cares that Nat is something that has some term which we’re willing to call ‘zero’, etc. At the next level up, it doesn’t seem to me that type theory attempts to define what, exactly a type is. It just tells you which ones you have and what you’re allowed to do with them. Insofar as I can interpret type theory into Set, it seems a type could be a set for me, but of course it need not be, and maybe it need not be anything sharply defined at all?
Mike Shulman (Sep 23 2025 at 20:43):Kevin Carlson said:
It doesn’t seem that type theory cares what I think this thing ‘zero’ in Nat is: whether it’s a string, or a memory address, or the empty set, or whatever. Probably actually type theory would get mad at me for trying to ask the question, because of course ‘zero’ is by definition a natural number!
That's one way to look at it. But I don't think that's the type-theoretic way to look at it. I would say that type theory does care what you think the thing 'zero' is, and in fact it tells you the answer: 'zero' is by definition a natural number.
This is also the answer to your "next level up" question: A type is, by definition, the kind of thing that can be the answer to a question "what kind of thing is X?". So ℕ is a type, and it is the answer to the question "what kind of thing is 'zero'?".
Mike Shulman (Sep 23 2025 at 20:46):Type theory doesn't have to feel compelled to answer (or refuse to answer) questions like this by interpreting itself into set theory or machine language or whatever. It has its own ontology.
Mike Shulman (Sep 23 2025 at 21:22):And if by "what this thing is" you mean what specifically rather than what kind of thing, then the answer is even simpler: 'zero' is 'zero'. It doesn't have to be anything else. The definition of the type ℕ introduces its elements as well, and they are what they are. It's not that we don't care whether 'zero' is a string or a memory address; it's that it isn't any of them. It's itself.
David Michael Roberts (Sep 23 2025 at 22:21):I mean, "zero" as a number is not a fact if you go back far enough in time (and people still quibble over whether it should be a natural number). When this number qua number emerged it was a concept in someone's mind (or rather collectively in people's minds), which as an arrangement of neurons and whatever, is on par with certain arrangements of electrons storied in a semiconductor in a computer, representing a string "0" or whatever.
My colleague here at Adelaide talks to students about how number are only numbers because of all the numbers together act like, well, numbers (something like a rig, in the case of naturals).
David Michael Roberts (Sep 23 2025 at 22:22):One might only want something like the ordinal structure on natural numbers, i.e. you counted a single thing, but that's really just coming from the succ operation in the type of natural numbers.
Mike Shulman (Sep 23 2025 at 22:30):Sorry David, is that a response to me and/or Kevin?
David Michael Roberts (Sep 24 2025 at 02:03):@Mike Shulman inspired somewhat by @Kevin Carlson 's
"It doesn’t seem that type theory cares what I think this thing ‘zero’ in Nat is: whether it’s a string, or a memory address, or the empty set, or whatever."
specifically, the "or whatever" part.
Sam Speight (Sep 25 2025 at 08:13):Kevin Carlson said:
Yeah, so, for instance "Raskolnikov, the protagonist of Crime and Punishment" seems to me to be no more abstract than any particular actual human, even though he does not physically exist: he's concrete in that he's a completely specific individual. I'm saying that while trying to avoid taking any particular position on in what sense "Raskolnikov" "really exists."
Thanks, I think I better understand now. So "particular" lives along a different axis to "physical" and "abstract"?
Though I'm not sure I agree that Raskolnikov is completely specified. For instance, does he have a mole on his left leg? (For my example to work, I really hope Crime and Punishment doesn't specify either way!) This kind of situation makes it more intuitive for me that there are undecidable statements in mathematics (within a fixed formal system). What formal systems do is ensure rigour, not completeness of specification of the objects they talk about.
Btw, what are some examples of non-particulars? What about "2"? Maybe that depends if you're a structuralist. What about "justice"?
John Baez (Sep 25 2025 at 08:37):Though I'm not sure I agree that Raskolnikov is completely specified. For instance, does he have a mole on his left leg?
As a fictional character, Raskolnikov is not the sort of entity that has all the same properties as a biological organism. Your question is like asking whether I'm the "protagonist".
Morgan Rogers (he/him) (Sep 25 2025 at 09:03):David Michael Roberts said:
My colleague here at Adelaide talks to students about how number are only numbers because of all the numbers together act like, well, numbers (something like a rig, in the case of naturals).
This seems ripe for an analogy of mathematicians existing (and having an identity as mathematicians) not in isolation but as participants in a broader society, that's fun.
Sam Speight (Sep 25 2025 at 10:43):John Baez said:
Though I'm not sure I agree that Raskolnikov is completely specified. For instance, does he have a mole on his left leg?
As a fictional character, Raskolnikov is not the sort of entity that has all the same properties as a biological organism. Your question is like asking whether I'm the "protagonist".
So what kinds of question are sensible to ask of Raskolnikov? In case it helps, I mean to ask if the fictional character Raskolnikov has a fictional mole on his fictional left leg. Call this an "object-level" question. I wouldn't want to say that we can only ask "meta-level" questions like: "in the real world, does Dostoevsky write in Crime and Punishment that Raskolnikov has a mole on his left leg?"
I agree that there's something iffy about asking whether you're the protagonist. But I think what I find iffy is a different: just that the question is not well-formed. Someone can be the protagonist of a story. So if you tell me what story you mean, we should be able to say (or sensibly debate) whether you're the protagonist.
Alex Kreitzberg (Sep 25 2025 at 12:31):This particular vein of question reminds me I don't like the word "abstract". One reason I got excited about category theory was that it gave me terminology beyond "more abstract".
Certain "Abstract data types" become objects uniquely specified by universal properties. Or certain algorithms between containers "abstracted over the type of their data" are really natural transformations.
When thinking about Raskolnikov, maybe it's possible to write something like "Raskolnikov : FictionalCharacter". We always have access to the question "isProtagonist : FictionalCharacter → Bool" but not "hasMole : FictionalCharacter → Bool" because that's not well defined across all stories. But then we can ask of "Baez : BiologicalHuman" the question "hasMoleOnLeftLeg : BiologicalHuman → Bool" because this question usually makes sense to ask of biological humans.
Now Speight correctly observed, that if you can give a story that includes Baez, "(Baez, someStory) : " you could then ask whether Baez was the protagonist. I say it's because we have a meaningful ambient conversion " → FictionalCharacter" (Oh no, Baez isn't fictional! My types got confused! Maybe I can fix it if I'm careful?)
In any case, perhaps both "Baez" and "Raskolnikov" are "concrete" as "ground level" terms of their own respective Types.
If I'm not strongly familiar with the context the other person is talking in, I fall off the cliff when the word "abstract" is used.
Alex Kreitzberg (Sep 25 2025 at 15:11):Now that I wrote that all out, I wonder how often "More abstract" means "higher up the infinity category ladder"
Kevin Carlson (Sep 25 2025 at 16:05):Sam Speight said:
So what kinds of question are sensible to ask of Raskolnikov? In case it helps, I mean to ask if the fictional character Raskolnikov has a fictional mole on his fictional left leg. Call this an "object-level" question. I wouldn't want to say that we can only ask "meta-level" questions like: "in the real world, does Dostoevsky write in Crime and Punishment that Raskolnikov has a mole on his left leg?"
I'm not sure this is any different than the question "Did George Washington have a mole on his left leg?" Like very many questions in our world, the answer might be yes or no, but it also might be "it's impossible for us to know this", if nobody ever happened to write down a sufficiently detailed description of Washington's left leg while it existed. I think you can ask about any question about Raskolnikov you might ask about a real person; for questions about psychology, you will generally be able to get more definitive answers than you would about most real people, while for concrete questions you'll find it easier to answer most of them for a person now living who you have direct access to, whereas the comparison to historical figures or those far away from you will be a toss-up depending on how much documentation you have of this other.
Sam Speight (Sep 25 2025 at 16:27):But the nature of our uncertainty is different in each case. In one case, it's feasible that I answer yes or no; in the other, it's not (unless we allow for the possibility that Dostoevsky writes in this detail).
Though, reading back, I now think I misread "specific" as "specified" in your earlier message, so I kind of dragged us off point - sorry!
Kevin Carlson (Sep 25 2025 at 17:34):I don't follow. In both cases, there is a limited amount of potentially relevant information, fixed for all time, and you go and look and see whether your fact is in that information, and if not, you don't get to know the answer.
Sam Speight (Sep 25 2025 at 21:19):I just mean that one question has a determinate answer, the other one doesn't.
Kevin Carlson (Sep 25 2025 at 22:15):OK, so your intuition is what, exactly, that concrete things have a maximal possible set of questions that have determinate answers, or something like that? But I can just ask whether George Washington would have made himself king had he not chopped down the cherry tree and immediately get indeterminate questions about him as well, and it seems like this one's indeterminate in much the same way as a question about details of Raskolnikov's appearance--we could have had the answer had the, er, author made different decisions, but as it turns out it's not present in the text.
Sam Speight (Sep 26 2025 at 08:08):Yes, I think I agree. Though you're giving yourself a more expressive language (with modalities, or something like that) to ask such counterfactual questions.
John Baez (Sep 26 2025 at 08:34):Sam Speight said:
So what kinds of question are sensible to ask of Raskolnikov?
I think it works like this: you can ask various questions about Raskolnikov, but if Dostoevsky's Crime and Punishment doesn't answer that question I'll say "sorry, that's not in the book". So yeah, if Dostoevsky said whether or not Raskolnikov had a mole on his left leg I could answer that question. But he didn't.
So it's not exactly that the question is ill-formed in some way that's easily determined from the syntax or the 'type' of Raskolnikov, it's just that the question might be unanswerable because it relies on a mistaken assumption. I imagine linguists and logicians have thought about this kind of thing, which is not merely about fictional characters: it applies to entities of many kinds.
For example you're allowed to ask me "what is your uncle's oldest daughter's name?" and I'll say "Joan", and you're allowed to ask me to say "what is your uncle's oldest son's name?" and I'll say "sorry, he had no sons".
John Baez (Sep 26 2025 at 08:42):By the way, a really spooky feature of quantum mechanics is that quantum uncertainty applies not only to the future but to some past events. It's possible that the answer to the question "Did George Washington have a mole on his left leg?" is not only unknown but unknowable in the same strict sense as "will this electron have spin up if I measure its spin along the z axis?" - meaning that the current state of the world is a superposition of states in which the question has different answers.
Some facts about the past are fixed because we have records of those facts, but most facts are not of that sort - there's just not stuff around to store all data about all past events. So, while for some questions about the past it is merely impractical to dig through currently available data to determine what happened, for some others it is strictly impossible.
(It's very hard to tell which is which: we might someday discover a journal where George Washington complained about the mole on his left leg, or carry out some sophisticated analysis of the soil in Mount Vernon, beyond the abilities of current technology, to answer this question.)
Sam Speight (Sep 26 2025 at 12:18):Makes sense. To what extent do you think answering "sorry, that's not in Crime and Punishment" to the question about the mole and answering "sorry, that's not determined by the axioms of ZF" to the question "does every epi in Set split?" are analogous?
John Baez (Sep 26 2025 at 13:03):Sounds similar. Philosophers like to talk about whether there's a "fact of the matter" about this or that. I don't think there's a "fact of the matter" about questions of whether epis split in Set, over and above the axioms we choose to define Set.
Maybe the axioms of set theory are less like Crime and Punishment than some tale that comes in many variant versions that people argue over, like a Greek myth.
Sam Speight (Sep 26 2025 at 14:14):That's a nice comparison (something to mention to my classicist wife).
Kevin Carlson (Sep 26 2025 at 18:05):So we're agreed that Raskolnikov is concrete, right? :grinning_face_with_smiling_eyes:
Sam Speight (Sep 26 2025 at 21:32):A particular, sure. But I think concrete is usually contrasted with abstract, and it seems that there's debate about where fictional characters fall (see eg. https://plato.stanford.edu/entries/abstract-objects/).
James Deikun (Sep 26 2025 at 21:33):Rather than that Raskolnikov is concrete, I'd say that George Washington is abstract. We abstract George Washington from various material instantiations that we regard as particular points in his life, and it's not just a matter of collecting these material instantiations as we need a certain level of abstraction to even be able to ask counterfactual questions about George Washington. Further, you get slightly different abstractions in case you consider George Washington as a particular human person versus an historical personage. In the latter case, in particular, you might want to regard things he hasn't and actually definitely wouldn't do as part of "George Washington", or for example consider thoughts he expected to be inferred as more important than actual thoughts, because both these things impinge heavily on the historical narrative, both actually and as-told.
Kevin Carlson (Sep 26 2025 at 21:34):But surely that will just lead to arguing that everything is abstract? That would be defensible but rather disappointing.
James Deikun (Sep 26 2025 at 21:35):I think abstractness is really a relative rather than essential trait. Ask not whether something is abstract, but rather what it abstracts over.
James Deikun (Sep 26 2025 at 21:48):Further, I would strongly argue, when it comes to phenomenology, that is, objects, concepts, events, etc that we perceive within our minds, we don't have access to any "bottom" to the abstraction "ladder" as sensory perception is a process of abstraction from beginning to end. It's not all that clear that there's a "bottom" to the "ladder" ontologically either, although in that case I think you could at least argue for it, but it wouldn't be anything close to what we perceive as a "thing".