[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] I should be looking at practical foundations again. I work in a pretopos with function sets, the set of natural numbers, and a terminal Archimedean ordered field satisfying the analytic LPO. In particular, I do not believe in neutral constructive mathematics, since I believe in the analytic LPO, as society at large believes in the analytic LPO. I still do not believe in the Heine-Borel theorem, and I cannot construct formal topologies, frames, locales, and topological spaces. Instead, I simply work with locally uniformly continuous functions everywhere. ---- What does the failure of neutrality mean for mathematics and its foundations? Against neutral constructivism: The real reason why is that I am tired of fighting the average person and average high school textbook on the topic of the real numbers. They all accept the real numbers come with a trichotomous strict order, and denying that just makes you look crazy to the average person. It's different with power sets and excluded middle (and logic in general) and the axiom of choice because the average person doesn't know about that stuff, so I would only be debating mathematicians on that topic. But I stop when society as a whole teaches facts to the entire population in childhood education. category: redirected to nlab