Post #2645666

2026-04-30 16:27 UTC

1/ @RobJLow@mathstodon.xyz writes "MartinEscardo I suspect that there are at least some people who think that when they find the 'right' axioms, the scales will fall from everybody's eyes and those axioms will define the right mathematics." Let me try to explain my point of view in more detail. Which, by the way, is shared by many people in my mathematical community. (1) The sign "·" may mean many things. Multiplication on the reals, or in any group are examples (among others!). (2) In constructive mathematics "exists" means something different from what it means in classical mathematics. And the same goes for "or". (3) But it is perfectly possible, and it has been done, to accommodate both meanings in a single "foundation" (I so hate this terminology). (4) But now, more darlingly, just like "·" may mean different things (in different groups), "exists" and "or" may mean even more things than discussed in (2). (5) Oh, wait! Don't "exists" and "or" have fixed meanings? No, like "·" doesn't. (6) Just like we may let the meaning of "·" depend on the group we are working with, we can let the meaning of "exists" and "or" to depend on what "topos" we are working with. Never mind what toposes are, for the moment, but they are the analogues of groups in this discussion.

Replies (1)

@MartinEscardo@mathstodon.xyz 2026-04-30 16:30

2/ (7) Now the neat thing is this: (7.1) This accommodates both the classical and constructive meanings of "exists" and "or", by choosing suitable toposes. (7.2) There is a topos for classical mathematics. (7.3) There is a topos for computability. (7.4) And, I claim, all toposes are for constructive mathematics. This is because of the following item. (7.5) If you want to prove something in *all* toposes, all you have to do is not appeal to excluded middle or choice in your proof. (7.6) This is why I prefer to speak of "neutral" rather than "constructive" mathematics. (7.7) This is like working in "all groups" rather than, say, "just abelian groups". Both activities are interesting. The former is more general, and the latter can get more theorems, at the expense of considering fewer groups. I would like to, once again, link to my blog post https://math.andrej.com/2021/05/18/computing-an-integer-using-a-sheaf-topos/ In that post, I use geometry, rather the group theory, as an analogy. But the point is exactly the same. Now, should I be constructive or classical? I prefer to be allowed to be both, just like people are allowed to discuss arbitrary groups, but also just abelian groups when their ideas apply to just them. The counter-intuitive idea here, of course, is that "exists" and "or" may mean multiple different things. But this surely did happen at the beginning when mathematicians realized that multiplication can mean multiple different things (in particular, addition in abelian groups). @RobJLow@mathstodon.xyz

Open ##2645667