3 ms·

As a mathematician, I have yet to encounter a reason as to why I should care about 'constructive mathematics' or 'neutral mathematics'. Bauer brings up non-Euc

As a mathematician, I have yet to encounter a reason as to why I should care about 'constructive mathematics' or 'neutral mathematics'. Bauer brings up non-Euclidean geometry but the thing there is about 40-ish years into it Beltrami and then Klein started showing why hyperbolic geometry is interesting and important (per Milnor[0]). Constructive mathematics is older than that by now ('Foundations of Constructive Analysis' came out in 1967, and the field was old even then), where are its applications to other fields of math? By 'application' I'm meaning stuff like, for example, how certain isometries of the plane (PSL2(R)) are connected to the Poincare disk. I'm even less impressed by 'neutral mathematics'. OK, you proved a well-known result without using excluded middle or choice, that's cool, I beat Doom with only the pistol. Tell me why that's not just stunts and gimmickry. [0]: https://projecteuclid.org/journals/bulletin-of-the-american-mathematical-society-new-series/volume-6/issue-1/Hyperbolic-geometry-The-first-150-years/bams/1183548588.full https://projecteuclid.org/journals/bulletin-of-the-american-... Also of note by the same author: https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016...

Y_Y 5y ago
You don't have do it because it might be useful somewhere else. There's definitely richness to the topic, and it attracts curiosity and answers questions at least some people thought were worth answering. It would be an anomaly if it never found some profound link with stone mainstream more applied field. All the same, when it does prove "useful" that will just be incidental. It won't be a pay-off or vindication or anything. (At least this is my half-baked mathematical philosophy, reasonably people may certainly differ.)
- n4r9 5y ago
  > You don't have do it because it might be useful somewhere else. Agreed, and I think this is something mathematicians generally can relate to.
- bigbillheck 5y ago
  > It would be an anomaly if it never found some profound link with stone mainstream more applied field. I'm not asking for a 'mainstream more applied field', I'm asking for some other flavor of math, no matter how abstract.
zozbot234 5y ago
https://en.wikipedia.org/wiki/Synthetic_differential_geometry https://en.wikipedia.org/wiki/Synthetic_differential_geometr... is worth mentioning. It builds on topos theory which as OP says is closely linked to non-classical mathematics.
ufo 5y ago
In the context of programming languages, constructive mathematics maps well to type systems. There are type systems that correspond to non constructive logics, but those are the weirder ones.
- johncolanduoni 5y ago
  Contemporary type theories have little issue with adding the law of excluded middle as an axiom, though for some intensional type theories it will end up being the only axiom that doesn’t reduce (i.e. have a computational rule associated during simplification) in a useful way. Programming language type systems rarely form consistent logics so there introducing it has no real effect either way.
scapp 5y ago
Setting philosophy aside, one of the major applications of constructive logic is that it's the internal language of toposes (and related kinds of categories). This usually simplifies proofs considerably and can produce new results. Some examples, Joyal and Tierney's An extension of the Galois theory of Grothendieck, CJ Mulvey's papers from the 70s (Intuitionistic algebra and representations of rings for example) and Blechschmidt's A General Nullstellensatz for Generalized Spaces. Johnstone's Sketches of an Elephant often has both internal and external proofs for comparison and it's easily seen that the internal version is both easier to write and to understand. For an article explicitly focused on using internal languages in algebraic geometry, see Blechschmidt's notes [0]. In particular, section 20 is dedicated to proving things that are difficult without the internal language. [0] https://github.com/iblech/internal-methods https://github.com/iblech/internal-methods
- C-x_C-f 5y ago
  Thank you for the link! Very interesting read. I kinda knew about this stuff but reading about it in sources like the nlab would always confuse me. This, on the other hand, feels very accessible. Incidentally, I studied algebraic geometry with a functorially oriented professor; one day, in passing, he said something along the lines of not wanting to use the axiom of choice in the proof of some result. At the time I didn't understand and I didn't ask for clarification, but the puzzlement stayed with me for a while. Having read this, it looks like his remark might have been related to this kind of stuff (e.g. chapter 12).
myWindoonn 5y ago
I'll assume that Bauer's not yet convinced you, even though you fully grok their examples. One application for computer scientists is to focus on computability of the real numbers. Turing's proof that there are uncomputable real numbers is nonconstructive, and it turns out that we can choose "all reals are computable" as an axiom of a topos. (This is the "Russian school" of constructive maths, ala Markov, IIUC.) This is "interesting and important" for both theory and engineering. For Poincaré-level mindblowing moments, we'll have to search across the landscape of topos theory, a landscape which was only dried out because of constructive maths damming up the floods of LEM and Choice. From homotopy type theory, we have the idea that types are like spaces; objects of the same type are related precisely by the possibility that one object might be deformable into the other. From higher category theory, we have the idea that sets are like 0-categories, and that set theory is just the bottommost slice of a 3D pyramid of category theories. Proving results neutrally to LEM and Choice is "not just stunts and gimmickry", because the proofs may be reused in any topos, and thus a neutral result is more true or less contextual than one which relies upon LEM. Bauer gives Johnstone, Diff, and RT as example topoi where LEM simply isn't true, but where neutral proofs would be reusable. Since RT is realizeable (by definition, it's the "realizability topos!") this means that neutral proofs each give runnable computer programs. This is sort of like beating Halo with only the pistol, and developing a sort of "pistol speedrun theory" where we study speedruns with games that have pistols. We aren't saying that there's not non-pistol speedruns, but emphasizing that pistols are a common feature. (Of course, the analogy breaks down here, since not all speedruns are pistol speedruns. Not all topoi are Grothendieck topoi, I suppose.)
- C-x_C-f 5y ago
  I'm curious, what do you mean by "Poincaré-level mindblowing moments"? Specifically, I wonder how/where Poincaré enters the story.

Y_Y 5y ago

You don't have do it because it might be useful somewhere else. There's definitely richness to the topic, and it attracts curiosity and answers questions at least some people thought were worth answering. It would be an anomaly if it never found some profound link with stone mainstream more applied field. All the same, when it does prove "useful" that will just be incidental. It won't be a pay-off or vindication or anything. (At least this is my half-baked mathematical philosophy, reasonably people may certainly differ.)

n4r9 5y ago
> You don't have do it because it might be useful somewhere else. Agreed, and I think this is something mathematicians generally can relate to.
bigbillheck 5y ago
> It would be an anomaly if it never found some profound link with stone mainstream more applied field. I'm not asking for a 'mainstream more applied field', I'm asking for some other flavor of math, no matter how abstract.

zozbot234 5y ago

https://en.wikipedia.org/wiki/Synthetic_differential_geometry https://en.wikipedia.org/wiki/Synthetic_differential_geometr... is worth mentioning. It builds on topos theory which as OP says is closely linked to non-classical mathematics.

ufo 5y ago

In the context of programming languages, constructive mathematics maps well to type systems. There are type systems that correspond to non constructive logics, but those are the weirder ones.

johncolanduoni 5y ago
Contemporary type theories have little issue with adding the law of excluded middle as an axiom, though for some intensional type theories it will end up being the only axiom that doesn’t reduce (i.e. have a computational rule associated during simplification) in a useful way. Programming language type systems rarely form consistent logics so there introducing it has no real effect either way.

scapp 5y ago

Setting philosophy aside, one of the major applications of constructive logic is that it's the internal language of toposes (and related kinds of categories). This usually simplifies proofs considerably and can produce new results. Some examples, Joyal and Tierney's An extension of the Galois theory of Grothendieck, CJ Mulvey's papers from the 70s (Intuitionistic algebra and representations of rings for example) and Blechschmidt's A General Nullstellensatz for Generalized Spaces. Johnstone's Sketches of an Elephant often has both internal and external proofs for comparison and it's easily seen that the internal version is both easier to write and to understand. For an article explicitly focused on using internal languages in algebraic geometry, see Blechschmidt's notes [0]. In particular, section 20 is dedicated to proving things that are difficult without the internal language. [0] https://github.com/iblech/internal-methods https://github.com/iblech/internal-methods

C-x_C-f 5y ago
Thank you for the link! Very interesting read. I kinda knew about this stuff but reading about it in sources like the nlab would always confuse me. This, on the other hand, feels very accessible. Incidentally, I studied algebraic geometry with a functorially oriented professor; one day, in passing, he said something along the lines of not wanting to use the axiom of choice in the proof of some result. At the time I didn't understand and I didn't ask for clarification, but the puzzlement stayed with me for a while. Having read this, it looks like his remark might have been related to this kind of stuff (e.g. chapter 12).

myWindoonn 5y ago

I'll assume that Bauer's not yet convinced you, even though you fully grok their examples. One application for computer scientists is to focus on computability of the real numbers. Turing's proof that there are uncomputable real numbers is nonconstructive, and it turns out that we can choose "all reals are computable" as an axiom of a topos. (This is the "Russian school" of constructive maths, ala Markov, IIUC.) This is "interesting and important" for both theory and engineering. For Poincaré-level mindblowing moments, we'll have to search across the landscape of topos theory, a landscape which was only dried out because of constructive maths damming up the floods of LEM and Choice. From homotopy type theory, we have the idea that types are like spaces; objects of the same type are related precisely by the possibility that one object might be deformable into the other. From higher category theory, we have the idea that sets are like 0-categories, and that set theory is just the bottommost slice of a 3D pyramid of category theories. Proving results neutrally to LEM and Choice is "not just stunts and gimmickry", because the proofs may be reused in any topos, and thus a neutral result is more true or less contextual than one which relies upon LEM. Bauer gives Johnstone, Diff, and RT as example topoi where LEM simply isn't true, but where neutral proofs would be reusable. Since RT is realizeable (by definition, it's the "realizability topos!") this means that neutral proofs each give runnable computer programs. This is sort of like beating Halo with only the pistol, and developing a sort of "pistol speedrun theory" where we study speedruns with games that have pistols. We aren't saying that there's not non-pistol speedruns, but emphasizing that pistols are a common feature. (Of course, the analogy breaks down here, since not all speedruns are pistol speedruns. Not all topoi are Grothendieck topoi, I suppose.)

C-x_C-f 5y ago
I'm curious, what do you mean by "Poincaré-level mindblowing moments"? Specifically, I wonder how/where Poincaré enters the story.