I guess to add, the thing about constructive math (which avoids excluded middle and unrestricted choice) is that it permits models where everything is computational. What I hope I’ve shown is that in some such models, the obstacle to choice really just boils down to excluded middle. (Probably—again it’s really difficult to combine mutable state with other stuff in pure math.)
I guess to add, the thing about constructive math (which avoids excluded middle and unrestricted choice) is that it permits models where everything is computational. What I hope I’ve shown is that in some such models, the obstacle to choice really just boils down to excluded middle. (Probably—again it’s really difficult to combine mutable state with other stuff in pure math.)