Thanks for the thoughts! I look forward to reading whatever you have to contribute, whenever you have time.

]]>i’m still too absorbed by other stuff to finish what i started in intuitionistic mathematics, although i admit i sometimes spend a disproportional amount of time on mathoverflow, on questions which probably could have waited…sorry.

but i do intend to return to the issues mentioned above, to see if i can help formulate some essential points in a way that many mathematicians can readily understand or at least get a feel for.

i just read the article Bishop’s constructive mathematics, and i have to say that it is quite extensive and well thought-out. but it also, somewhat, adds to the confusion, simply by pointing out how much is still unclear.

the difficulty, i find, often lies in finding a simple way to phrase both the mathematical keypoints AND the key philosophical perspectives, without doing too much injustice to their own complexity and that of their interplay.

i’m not saying i can do better for Bishop’s constructive mathematics than the current page! just saying what i would like to see ideally.

on the intuitionistic mathematics page, i can probably try to clarify what i see as the relation between bishop’s constructive mathematics and intuitionism.

the relation between bishop’s constructive mathematics and intuitionism cannot, i believe, be easily summarized. it is often emphasized that there are key elements of INT which are not accepted in BISH. seldom emphasized but true nonetheless is that there are key elements of BISH which are unacceptable in INT as well. mostly of course around predicativity issues as we discussed before, but this also affects axioms of choice i believe.

please have some more patience, i promise i will first add something here before doing anything on mathoverflow. cheers, frank

]]>Thanks!

]]>It’s true that it’s *regarded as* such a specialization, but I’m personally somewhat dubious that it *is*, at least if by “Bishop’s constructive mathematics” one means what Bishop did rather than what some of his “followers” do, since Bishop worked with setoids and I doubt that Brouwer did. But I added a note to intuitionistic mathematics.

I also updated the page Bishop’s constructive mathematics based on an email discussion with some folks, adding references and clarifying that not all “Bishopites” actually use the same framework as Bishop.

]]>At *Bishop’s constructive mathematics* it says that Brouwer’s intuitionistic mathematics is regarded as a specialization of BISH.

I find that a useful statement. If true, this should be mentioned at *intuitionistic mathematics*.

No one else is sure how to draw the line either. I think the standout warning box at the top of intuitionistic mathematics is sufficient, as long as no links mistakenly point there when they should go to constructive mathematics.

]]>intuitionistic mathematics points to constructive+mathematics which points to Bishop’s constructive mathematics, which is OK I think.

]]>We had had discussion here with Frank Waaldijk a while back regarding related clarification concerning the editing of the entry *intuitionistic mathematics*. Now I see that this entry doesn’t mention the name “Bishop”. Should it? I am never sure how to draw the line between “constructive” and “intuitionistic”.

That’s a nicely clear and clarifying account.

]]>I created Bishop’s constructive mathematics by moving some material from Errett Bishop and adding some more discussion of what it is and isn’t. Comments and suggestions are very welcome; I’m still trying to figure out the best way to describe the relationship of this theory to other things like topos logic.

]]>