Timeline for Formalizations of the idea that something is a function of something else?
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 26, 2023 at 0:29 | comment | added | Mike Shulman | @AlexeyMuranov Of course, I agree. Indeed, the rest of my answer sketches one possible alternative formalization. I don't think there's any contradiction between being proud that we've found some way to formalize something, and also wanting to find new and better ways to do it. (Also, FWIW, I would say that Category Theory is actually quite often formalized in ZFC.) | |
| Feb 25, 2023 at 23:40 | comment | added | Alexey Muranov | """I think we should be proud that modern mathematics supplies a precise way to make sense of a previously vague concept""" -- it does so in one way, by formalising everything in ZF of in ZFC. This does not exclude the possibility that there could be a more natural (possibly drastically different) formalisation. For example, Category Theory is usually not formalised in ZFC, but it is not considered "vague" because of this. | |
| Apr 12, 2019 at 20:44 | comment | added | Mike Shulman | @MichaelBächtold The largest open subspace on which $x$ is locally constant is the union of all open subspaces on which $x$ is locally constant. | |
| Apr 12, 2019 at 19:53 | comment | added | Michael Bächtold | How is the largest open subspace on which $x$ is constant defined? I was imagining that "when $x$ is constant $y$ is constant" meant something like: Whenever $x:A\to R $ is restricted to a "context" $i:B\to A$, (not necessarily an open subset of $A$) such that $x\circ i$ is constant, then also $y\circ i$ is constant. I have to admit that I still don't have a solid enough grasp on modal type theories to understand your last comment. I hope to find more time this summer to study the references you quoted. | |
| Apr 12, 2019 at 16:37 | comment | added | Mike Shulman | By the way, I misspoke in my comment about modal type theories: in addition to the modality $\flat$ for discrete/constant types, "spatial type theory" has a modality $\sharp$ for codiscrete ones, and this rarely exists in sheaves on particular spaces $A$ (it's more characteristic of "big toposes" whose objects are regarded as spaces). | |
| Apr 12, 2019 at 16:36 | comment | added | Mike Shulman | As a simple example, if $x$ is a function $A\to R$ that is nowhere constant, regarded as a variable element of $R$ in $Sh(A)$, then the internal truth value of "$x$ is constant" is $\bot$. Therefore, "if $x$ is constant then $y$ is also constant" is true for any variable quantity $y$. But presumably we don't want to regard all such $y$ as a function of $x$. | |
| Apr 12, 2019 at 16:35 | comment | added | Mike Shulman | @MichaelBächtold I don't immediately see any way to do that. If $x$ is a fixed variable quantity, i.e. externally a map $A\to R$, then I believe the internal truth-value of "$x$ is constant" is the largest open subspace of $A$ on which $x$ is locally constant. So "whenever $x$ is constant, $y$ is also constant" would mean externally that on every open subspace where $x$ is locally constant, $y$ is also locally constant. In particular, it would say nothing about what happens where $x$ is not constant. | |
| Apr 12, 2019 at 12:07 | vote | accept | Michael Bächtold | ||
| Apr 12, 2019 at 12:06 | comment | added | Michael Bächtold | Hi @MikeShulman, I was wondering if your definition of "$y$ is a function of $x$" in such a modal type theory could also be reformulated along the lines of: "whenever $x$ is constant, it follows that also $y$ is constant." Or is this only expressible at the meta-level? I'm trying to mimic the old definitions which talked of values and didn't mention $f$. | |
| Aug 13, 2018 at 7:49 | comment | added | Mike Shulman | @MichaelBächtold Type theories with "higher modalities" like this are a recent innovation. If $A$ is connected, so $\Delta$ is fully faithful, the type theory is the one called "spatial" in arxiv.org/abs/1509.07584 and "crisp" in arxiv.org/abs/1801.07664 (with different applications in mind). A type theory for a not necessarily connected geometric morphism has not as far as I know been studied explicitly, but should be a special case of my work in progress with Licata and Riley which I talked about at HoTTEST: uwo.ca/math/faculty/kapulkin/seminars/hottest.html | |
| Aug 13, 2018 at 6:07 | comment | added | Michael Bächtold | This is great! Indeed, if you look at the old calculus, people always made the distinction between variables and constants inside their language. Calculus textbooks and physicists still do this, but it makes no sense inside set theory. Do you know if there is a place where I could read more about such a modal type theory? | |
| Aug 13, 2018 at 5:05 | history | answered | Mike Shulman | CC BY-SA 4.0 |