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.
Amar Hadzihasanovic (Mar 14 2025 at 09:51):Just sharing some semi-idle thoughts.
I often find, in practice, that our ordinary mathematical language struggles with referring to things which are “located” or “embodied”, as in: “this thing here that I am pointing at”, and it is not hard to see why; logical foundations of all flavours postulate that mathematical objects can only be “created”---added to our context---as variables, that is as disembodied names, and all we can do to refer to names is give them other names.
Even works that try to explicitly ground logic into location such as Girard's Locus Solum accept that location be encoded e.g. in a list of numbers.
One thing I find is that this creates a kind of “cognitive barrier” between abstract and computational mathematics, since indeed computation is naturally “embodied and located”, which is modelled by e.g. the head of a Turing machine or concretely a memory cell accessed by a processor, but these very here-and-now concepts also can only be referred to through an encoding if one is to prove something about them.
Recently I've been reading something about Piaget's theory of cognitive development and it struck me how different this creation of mathematical objects as “disembodied names” is from our own creation as individuals, which is as an embodied, located “I” which interacts with the world around itself.
It got me wondering: could we have taken (or take) a different turn, where instead of mathematical objects as names, we went for mathematical objects as actors---have a foundation of mathematics where the primitive specification is what can I do, what can I experience, as an embodied mathematical object of a certain type?
Then instead of starting our proofs with
Let be a natural number.
perhaps we would start them with
I am a natural number.
Philosophically, such a turn could have something in common with set-theoretic foundations, in the focus on the “concrete embodiment” of objects, as well as categorical foundations, in the focus on the structural and relational aspect (an object is what an object does in relation with everything else), as well as Laws of Form in the focus on action and creation, but I feel it would also have something different from all of them.
I am very much an amateur in mathematical philosophy, so I am wondering if you know some precedents of this sort of idea, or you see obvious flaws, or have anything to say about it.
Patrick Nicodemus (Mar 14 2025 at 12:18):Off-topic, but the quote from the Cordwainer Smith novel at the beginning of Locus Solum is so fascinating. One of the more engaging starts to a paper I've seen.
David Corfield (Mar 14 2025 at 13:22):Some scattered thoughts:
Certain forms of maths education looks to embody the concepts. Have your class of children physically move themselves into two equal groups. What is it to embody a set of even cardinality? I've tried to mime modus ponens in my logic classes before. I recall some dance company danced the Snake Lemma.
The non-indexical quality of mathematics carries through to physics. You're provided with a map, but don't know where you're located on it.
There was a trend in Science Studies which looked to give scientific objects more agency. Cf. Bruno Latour's 'actor-network theory' which includes non-human actors. Aimed though at laboratory science.
Is this tied to your idea of types as their own little “computational universes”?
Amar Hadzihasanovic (Mar 14 2025 at 13:47):Thank you David, those are really nice points. The terminology of “indexical” vs “non-indexical” was not part of my vocabulary but seems clearly appropriate.
The “types as computational universes” idea [sorry to other readers, this was discussed in a non-public platform] is somewhat tangentially related; one of the things that sparked this thought was reflecting on the “terms as pasting diagrams” part of it.
So, there, you have terms which have a spatial/geometric nature, and that nature is entirely effective, explicit, and computable; and also one of the most useful operations that one can perform is to paste two such terms at some subterm of one of them, that is a “located part”.
So I was thinking about how there is something very simple and very concrete about this operation of pasting, how if I was a term, I would just know about my subterms, and if I wanted to paste with another term, it would go something like:
- Where should I paste myself?
- Here.
and it would be done; a little bit like interacting with a doctor,
- Where does it hurt?
- Here.
But instead I have to pick a specific encoding and then have to explicitly describe the location with respect to this encoding, and there is something a little bit perverse and unnatural about it, like every interaction with the doctor having to be like
- Where does it hurt?
- Under my right fifth rib, about an inch from the sternum.
I don't know if this is something that can actually be “fixed” by some change of language; I am just wondering.
fosco (Mar 14 2025 at 13:54):Funny, I have recently resorted to the term "indexical property" while trying to explain why it is mathematically nontrivial to encode a proposition like "it's raining" because it underlies subtle details like time specification and all sorts of other restraints, plus some sentences contain the "I" pronoun and all other sorts of mysterious tokens.
I was left with a question similar to what @Amar Hadzihasanovic asked, ever since.
Amar Hadzihasanovic (Mar 14 2025 at 14:14):I should add that I think many ideas of categorical logic already resonate with this; the idea itself of “internal logic”, as well as languages such as FOLDS (or univalent HoTT) that cannot “tell apart equivalent objects”, I think, go in the direction of putting ourselves in the “perspective” of a mathematical object living inside its own universe and with a more limited set of “probes” for gaining information about its surroundings...
David Corfield (Mar 14 2025 at 14:15):fosco said:
why it is mathematically nontrivial to encode a proposition like "it's raining" because it underlies subtle details like time specification
Did you ever see my treatment of the indexicality of "It rains"?
Amar Hadzihasanovic (Mar 14 2025 at 14:41):Is there such a thing as a multimodal logic that is suited for expressing a kind of “existentialist” system, where “everything that happens, happens to someone”?
I feel that would give some kind of solution in the spirit I am suggesting:
“Every time John lights a cigarette, it rains”
could be parsed as
“[Suppose] I am John. Every time I light a cigarette, it rains.”
where the fact that the raining is happening here is simply the default given by the statement being “from John's viewpoint”; in fact, just as in natural language, it is the opposite case that needs to be made explicit, by reference to an explicit location.
David Corfield (Mar 14 2025 at 14:54):Funny how one mentions the time but not the place. But then maybe one doesn't need to.
"I light a cigarette, and it rains."
But maybe it's because "time" is playing the role of something like "occasion" or more technically "spacetime event".
David Corfield (Mar 14 2025 at 17:54):David Corfield said:
I recall some dance company danced the Snake Lemma.
I still think there was something like that, but I've come across also this dance representation of the [[hexagon diagram]] of differential cohomology.
Thinking more about giving voice to mathematical entities, I think it does form a part of mathematical pedagogy. Your treating a quadratic equation with a child and you say after a time "It's crying out to be factorized".
Terms of a type are crying out to have elimination rules applied to them.
Amar Hadzihasanovic (Mar 14 2025 at 20:17):Yes, I was thinking about elimination rules (or destructors) when I wrote about pasting diagrams knowing about their subdiagrams...
I feel like, if I were a term of a type, destructors would be something like the parts of me that are readily accessible to me, the way that certain parts of my body are readily accessible for my use, to the point that they are not conceptualised as having a separate existence from me.
E.g. the relation between a term of a pair type and its left and right projection is somewhat like the relation between myself and my left and right hand... I can see them as separate entities but they are integrated and immediately accessible to me as an agent in the world...
Amar Hadzihasanovic (Mar 14 2025 at 20:21):Of course, my main question remains--- what could be a rigorous form of mathematics that is adapted to the metaphor of mathematical objects as agents?
David Corfield (Mar 15 2025 at 07:48):The only thing I can think to mention here is two-dimensional semantics which is trying to get at a logic of indexicals and designation across worlds. It's trying to navigate a way between speaking of things picked out by description and picked out by indexical designation.
David Corfield (Mar 15 2025 at 09:37):In the case of mathematics, it would be dealing with things like
2 could have been 3.
In one typical reading this is absurd. Like saying
The least prime could have been 3.
But is OK in the sense of
I'm thinking of a number. It's 2 but it could have been 3.
It's like
The 44th POTUS needn't have been POTUS.
In the sense of Obama, it's true; in the sense of the person holding that office, it's false.
It's much to do with the essence of something. How far can one go before
Obama needn't have been X
doesn't make sense?
Obama needn't have had anything like the genome he has?
Presumably with mathematics we usually take the essence of an entity to be its structural role, so can't think of counterfactuals.
Madeleine Birchfield (Mar 15 2025 at 14:38):David Corfield said:
In the case of mathematics, it would be dealing with things like
2 could have been 3.
In one typical reading this is absurd. Like saying
The least prime could have been 3.
But is OK in the sense of
I'm thinking of a number. It's 2 but it could have been 3.
It's like
The 44th POTUS needn't have been POTUS.
In the sense of Obama, it's true; in the sense of the person holding that office, it's false.
More generally, I think the context is necessary to make sense of whether a statement is true or false or absurd or unprovable or whatever.
Amar Hadzihasanovic (Mar 15 2025 at 19:25):At least some of these examples look like ones in which the ambiguity would be resolved if the computational “engine” evaluating a sentence was made explicit---for example,
The 44th POTUS needn't have been POTUS.
would presumably lead to different outcomes if “The 44th POTUS” is evaluated eagerly rather than lazily.
Some of the ideas I've expressed both here and in the “types as small computational universes” proposal go in this direction; I think the following are all compatible:
Amar Hadzihasanovic (Mar 15 2025 at 19:40):And also, the “existentialist” principle I suggested earlier: