Category Theory
Zulip Server
Archive

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.


Stream: theory: philosophy

Topic: Mathematics founded on (located) action


view this post on Zulip 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 nn 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.

view this post on Zulip 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.

view this post on Zulip David Corfield (Mar 14 2025 at 13:22):

Some scattered thoughts:

view this post on Zulip 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:

and it would be done; a little bit like interacting with a doctor,

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

I don't know if this is something that can actually be “fixed” by some change of language; I am just wondering.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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"?

image.png

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Amar Hadzihasanovic (Mar 15 2025 at 19:40):

And also, the “existentialist” principle I suggested earlier: