Hacker News new | past | comments | ask | show | jobs | submit login

I don't know, normalizing at least seems reasonable constructively, sorry about the handwavyness in my reply as well!

In lean specifically there is a bit more information here: https://leanprover.github.io/theorem_proving_in_lean/axioms_...

"and quotient construction which in turn implies the principle of function extensionality"

There is also, Michael Beeson's "Extensionality and choice in constructive mathematics" https://projecteuclid.org/euclid.pjm/1102779710

So it seems at least that the definition of quotients in lean is classical, and justified by axioms, NuPRL at least seems constructive, this at least leads me to believe quotients as defined in lean aren't constructive. But i'm not sure we can take the step to "quotients aren't constructive".

Anyhow it's an interesting question, and one which I too wish I had more clarity on.






Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: