Timeline for What are the differences between MLTT and CIC?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 10, 2023 at 13:29 | comment | added | Gro-Tsen | @LawrencePaulson Perhaps you'd like to weigh in on this MathOverflow question as to the relation you see between constructivism and predicativism (or what each of them means)? | |
| Mar 30, 2022 at 18:00 | comment | added | Jonathan Sterling | And you may ask, why do we want a result that holds over an arbitrary space? Because a simple such result often implies something much more complicated when translated into classical mathematics (== math over the point), so this is in many cases the best way to achieve the latter result. From this point of view, predicativity plays no role and it is very natural indeed to do constructive math in an impredicative setting. | |
| Mar 30, 2022 at 17:59 | comment | added | Jonathan Sterling | @LawrencePaulson Many (most?) of the people currently doing serious constructive mathematics are doing t for neither of the reasons you bring up: we neither care about extraction nor about philosophy. The reason is that we want to get a result that is valid over a topological space, or a topos. I agree with you that the "executable code" thing is not a convincing motivation of constructive math, and personally I believe the philosophical angle is not to convincing either. | |
| Mar 16, 2022 at 11:16 | comment | added | Lawrence Paulson | Let's turn this around and ask, why are you doing constructive mathematics? Is it out of a philosophical belief or with a technical objective such as obtaining executable code? I've read countless papers referring to constructive proofs as if it were an obligation, like saying grace before dinner. Sometimes they were proved over a classical axiomatisation, which is like having a starter of foie gras with your vegan meal. And I have been waiting 40 years for a convincing demonstration of executable code from a proof. People need to make their objectives clear. | |
| Feb 16, 2022 at 9:43 | comment | added | Pierre-Marie Pédrot | Impredicative systems such as CIC, or for that matter F with inductive types, satisfy both canonicity and strong normalization. This is enough for me to consider them to be constructive. I know there is a philosophical stance against impredicativity, but part of it is due to the Type : Type debacle. | |
| Feb 15, 2022 at 10:50 | comment | added | Blaisorblade | Constructive and predicative do not coincide, so I'm confused by the confusion :-). | |
| Feb 10, 2022 at 15:02 | comment | added | Pedro Abreu | Thanks for the answer! Could you expand a little more on why using CIC to do constructive mathematics doesn't make sense? | |
| Feb 10, 2022 at 14:11 | history | answered | Lawrence Paulson | CC BY-SA 4.0 |