Has there been any attempt to formalize Bishop's "Foundations of Constructive Analysis" in any proof assistant? (Lean, Coq, Isabelle, ...) Or "Foundations of Constructive Probability Theory" by Yuen-Kwok Chan ? Or any book that is related to constructive mathematics?
5
-
$\begingroup$ I could be mistaken, but one thing possibly holding this back is that I think modern constructivists don't particularly like Bishop's approach. For example, my understanding (possibly wrong) is that Bishop uses dependent choice and there is therefore no distinction between Dedekind and Cauchy reals. (Again, please correct me if I'm saying something dumb.) Another barrier is that for at least some subjects like probability theory, there isn't even that much classically formalized. $\endgroup$– Jason RuteCommented Sep 18 at 0:43
-
$\begingroup$ Having said that, I've heard of github.com/coq-community/corn/pull/88 which formalizes at least some of Bishop and Cheng 1972 in Coq's corn package. I recall reading that this person used Cauchy sequences (unquotiented) as the "reals" which probably avoids some difficulties. If someone knows more about it, they can make it into a real answer. $\endgroup$– Jason RuteCommented Sep 18 at 0:46
-
$\begingroup$ When I said "dependent choice above", I meant countable choice (ncatlab.org/nlab/show/…). $\endgroup$– Jason RuteCommented Sep 18 at 1:44
-
$\begingroup$ You were correct the first time around, Bishop in general uses Dependent choice. $\endgroup$– Andrej BauerCommented Sep 18 at 15:09
-
1$\begingroup$ If you're going to formalise Bishop, then it's probably best to use setoids in my opinion. That makes dependent choice etc into theorems rather than axioms to assume, and IIRC there are proofs in Roq along those lines. $\endgroup$– awsCommented Sep 19 at 9:14
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
Here are some libraries of formalized constructive mathematics. Click on the links to see their scope:
- C-CoRN
- agda-unimath
- UniMath
- Coq-HoTT
- TypeTopology
- agda-categories
- Intuitionistic logic explorer in Metamath
I am sure there are other libraries, these are just the ones inside my head.
$\begingroup$
$\endgroup$
1
-
$\begingroup$ It’s hard to know what the OP is looking for, but does this go beyond the definition of real numbers? Is any interesting analysis formalized? What makes Bishop’s works so interesting is that he covered large chunks of analysis especially in measure and probability theory. $\endgroup$ Commented Sep 18 at 14:21