4 ms·

Speaking of the foundations: is intuitionism still alive? How is constructive math doing nowadays? Do mathematicians embrace or reject it? Did the recent HoTT c

Speaking of the foundations: is intuitionism still alive? How is constructive math doing nowadays? Do mathematicians embrace or reject it? Did the recent HoTT change their attitude towards constructive math?

ocfnash 7y ago
I'm not at all qualified to answer such a broad question but I'll share my amateur opinions for what they're worth. I believe people are gradually coming round to the point of view that constructive mathematics (including intuitionism) is a useful generalization of classical mathematics, rather than a handicap. Proof assistants, while still fairly niche, continue to get more attention and the fact that constructive mathematics tends to give "proofs that compute" helps. For what it's worth, I waffled on about this a little a few months ago right here: https://news.ycombinator.com/item?id=18404914 https://news.ycombinator.com/item?id=18404914 In my opinion HoTT is the most interesting subject in this area but we have yet to figure out exactly what its role is, and the extent to which it should serve in foundations. However the fact that it is a deep theory with significant value independent of its foundational role must surely help the constructive point of view. I think it's fair to say "Book HoTT" is not fully constructive since univalence is an axiom but this seems to have been resolved with the introduction of cubical type theory. I also suspect the majority of mathematicians still spend very little time thinking about foundations.
maxiepoo 7y ago
Constructive mathematics is alive and well for 2 reasons. 1. The type theorists/homotopy theorists that are exploring homotopy/cubical type theory as a foundational approach. 2. The objective fact that in general the internal language of a topos (in general) does not validate the law of excluded middle or the axiom of choice. This means that if you prove a result while using constructive logic you can apply it to a broader class of models than classical logic. This viewpoint of logic makes the whole "argument" between constructive and classical logic seem very silly: it's like arguing whether or not it is "true" that groups are abelian. Some are and some aren't! Intuisionism as in Brouwerian intuitionism with choice sequences etc that disprove LEM is still a niche subject, especially foundationally but is still being explored, with the help of understanding of sheaf models that allow it to be studied from a classical perspective.
Gondolin 7y ago
Oh yes, it is very much alive. For instance any topos (with a nno) is a model of intuitionist set theory. And since topos are a very natural type of categories (a topos= acategory which has finite limits and a power object), intuitionist logic is important in category theory. Two examples: in algebraic geometry, mathematicians use schemes (introduced by Grothendieck), which have allowed to make tremendous progress. But from the point of view of intuitionist logic, a scheme is just a ring, and a quasi-coherent sheave is just a module over this ring (in more details they are ring objects and module objects in the big Zariski topos). In synthetic differential geometry, one use a certain intuitionist topos to formalize intuitive aspects of reasoning with infinitesimal quantities (without relying on delta and epsilons). Note that non standard analysis also allows to work with infinitemismal quantities (by using ultraproducts), but has the same power has standard analysis (and in particular is classical). Synthetic differential geometry is intuitionnist, so is less powerful, but on the other hands its theorems are automatically valid for more models (complex models, formal smooth schemes...). In SDG, your reals R are a field with an (actually several) element epsilon !=0 (the infinitesimals) and such that epsilon^2=0 (that's why this only work in intuitionist logic, in classical logic R being a field would imply that epsilon=0). In this model every function f: R->R is differentiable, and we have f(x+epsilon)=f(x)+f'(x) epsilon. In proof theory (like coq) one work with Martin Lof type theory, which is the type theory of topoi (and so is intuitionist). A recent development is to work with homotopy type theory instead, the type theory of \infty-topos. This is more powerful (and can be used as fundations for all of maths), and solve real problems, like correctly defining equality (equality is actually a tricky concept, for instance it may not be the case in the prover's theory that "for any two functions f and g such that forall x, f(x)=g(x); then f=g", but this is obviously a feature we want.) On the other hand it is quite a bit trickier to define (we need (infty,1)-categories).
- Gondolin 7y ago
  On the other hand, constructive set theory is still rather a niche part of mathematics (this may change with the recent development of HOTT). It is hard not to use the LEM (and I am not good at it, I am not an expert on this subject. Expert say it gets easier over time to get used to not use LEM). For instance, in the intuitionist reals, from "x >= 0 and x != 0" you cannot conclude that "x != 0". To prove x>0 you would need to exhibit a natural number n such that x>=1/n (so in other words you need a constructive proof that x>0). But this is not always possible, you have models of R where there is an x != 0 which is smaller than all the 1/n. There is however one nice feature of intuitionist theory: every geometric sentence which is provable in classical theory is actually true in intuitionist theory. So if you have a geometric sentence (https://ncatlab.org/nlab/show/geometric+theory https://ncatlab.org/nlab/show/geometric+theory) you can use LEM in your proofs, the proof will still be valid intuitionally!

ocfnash 7y ago

I'm not at all qualified to answer such a broad question but I'll share my amateur opinions for what they're worth. I believe people are gradually coming round to the point of view that constructive mathematics (including intuitionism) is a useful generalization of classical mathematics, rather than a handicap. Proof assistants, while still fairly niche, continue to get more attention and the fact that constructive mathematics tends to give "proofs that compute" helps. For what it's worth, I waffled on about this a little a few months ago right here: https://news.ycombinator.com/item?id=18404914 https://news.ycombinator.com/item?id=18404914 In my opinion HoTT is the most interesting subject in this area but we have yet to figure out exactly what its role is, and the extent to which it should serve in foundations. However the fact that it is a deep theory with significant value independent of its foundational role must surely help the constructive point of view. I think it's fair to say "Book HoTT" is not fully constructive since univalence is an axiom but this seems to have been resolved with the introduction of cubical type theory. I also suspect the majority of mathematicians still spend very little time thinking about foundations.

maxiepoo 7y ago

Constructive mathematics is alive and well for 2 reasons. 1. The type theorists/homotopy theorists that are exploring homotopy/cubical type theory as a foundational approach. 2. The objective fact that in general the internal language of a topos (in general) does not validate the law of excluded middle or the axiom of choice. This means that if you prove a result while using constructive logic you can apply it to a broader class of models than classical logic. This viewpoint of logic makes the whole "argument" between constructive and classical logic seem very silly: it's like arguing whether or not it is "true" that groups are abelian. Some are and some aren't! Intuisionism as in Brouwerian intuitionism with choice sequences etc that disprove LEM is still a niche subject, especially foundationally but is still being explored, with the help of understanding of sheaf models that allow it to be studied from a classical perspective.

Gondolin 7y ago

Oh yes, it is very much alive. For instance any topos (with a nno) is a model of intuitionist set theory. And since topos are a very natural type of categories (a topos= acategory which has finite limits and a power object), intuitionist logic is important in category theory. Two examples: in algebraic geometry, mathematicians use schemes (introduced by Grothendieck), which have allowed to make tremendous progress. But from the point of view of intuitionist logic, a scheme is just a ring, and a quasi-coherent sheave is just a module over this ring (in more details they are ring objects and module objects in the big Zariski topos). In synthetic differential geometry, one use a certain intuitionist topos to formalize intuitive aspects of reasoning with infinitesimal quantities (without relying on delta and epsilons). Note that non standard analysis also allows to work with infinitemismal quantities (by using ultraproducts), but has the same power has standard analysis (and in particular is classical). Synthetic differential geometry is intuitionnist, so is less powerful, but on the other hands its theorems are automatically valid for more models (complex models, formal smooth schemes...). In SDG, your reals R are a field with an (actually several) element epsilon !=0 (the infinitesimals) and such that epsilon^2=0 (that's why this only work in intuitionist logic, in classical logic R being a field would imply that epsilon=0). In this model every function f: R->R is differentiable, and we have f(x+epsilon)=f(x)+f'(x) epsilon. In proof theory (like coq) one work with Martin Lof type theory, which is the type theory of topoi (and so is intuitionist). A recent development is to work with homotopy type theory instead, the type theory of \infty-topos. This is more powerful (and can be used as fundations for all of maths), and solve real problems, like correctly defining equality (equality is actually a tricky concept, for instance it may not be the case in the prover's theory that "for any two functions f and g such that forall x, f(x)=g(x); then f=g", but this is obviously a feature we want.) On the other hand it is quite a bit trickier to define (we need (infty,1)-categories).

Gondolin 7y ago
On the other hand, constructive set theory is still rather a niche part of mathematics (this may change with the recent development of HOTT). It is hard not to use the LEM (and I am not good at it, I am not an expert on this subject. Expert say it gets easier over time to get used to not use LEM). For instance, in the intuitionist reals, from "x >= 0 and x != 0" you cannot conclude that "x != 0". To prove x>0 you would need to exhibit a natural number n such that x>=1/n (so in other words you need a constructive proof that x>0). But this is not always possible, you have models of R where there is an x != 0 which is smaller than all the 1/n. There is however one nice feature of intuitionist theory: every geometric sentence which is provable in classical theory is actually true in intuitionist theory. So if you have a geometric sentence (https://ncatlab.org/nlab/show/geometric+theory https://ncatlab.org/nlab/show/geometric+theory) you can use LEM in your proofs, the proof will still be valid intuitionally!