|
|
|
|
|
|
by kmill
925 days ago
|
|
|
Yeah, I can imagine that, and I've used sigma types to carry it out (`Subtype`s in particular, or perhaps custom structures). Why does the proof in the sigma type have to be constructive? Certainly this is the road to "dependently typed hell" and it's good to avoid mingling proofs with data if you can, but avoiding the law of the excluded middle doesn't make any of that any easier. This is also a bit of a distraction since what I really mean regarding TCS is that in my experience is that they do not see the proofs themselves as being objects-with-properties. They're perfectly happy with non-constructive reasoning to support constructions. I am looking to be convinced that constructive logic is worth it, but this mathematician hasn't seen anything compelling beyond work on foundations themselves. Regarding mathlib, could you say what in particular you're talking about, since it's not ringing a bell, and I follow the changelogs. |
|
|
There's been several commits where general appeals to classical reasoning in some development have been replaced by more fine-grained assumptions of decidability for some objects, or marking uses of classical reasoning in some specific proofs. This has not happened throughout mathlib of course, just in some specific places. But it might still show one way of making the development a bit friendlier to alternate foundations.
> ...but avoiding the law of the excluded middle doesn't make any of that any easier.
Constructivist developments are not about "avoiding the law of excluded middle". They're more about leveraging the way we already structure mathematical proofs (and mathematical reasoning more generally) to make it easier to understand where simple direct reasoning has in fact been used, and a theorem can thus be said to be useful for such purposes. If all we did was proofs by contradiction and excluded middle, there would be no point to it - but direct proof is actually rather common.
> Why does the proof in the sigma type have to be constructive?
It doesn't, if the constructibility part has been stated separately (e.g. stating that some property is decidable, or that some object is constructible). That's in fact how one can "write the program/algorithm and the logic separately" in a principled way.
> I am looking to be convinced that constructive logic is worth it, but this mathematician hasn't seen anything compelling beyond work on foundations themselves.
This paper https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016... provides a reasonable summary of the relevant arguments. It's notable that a number of mathematicians are doing work that involves, e.g. the internal language of topoi, which pretty much amounts to invoking constructive foundations despite starting from what's otherwise a "classical" setting. That they go to all this trouble to do this certainly suggests that they find that work compelling enough. And indeed, it has practical implications wrt. e.g. alternate foundations for analysis, differential geometry etc.