In Mike Shulman's answer to Initiation to constructive mathematics, he discusses how "neutral constructive mathematics" is the fashionable topic in constructive mathematics. When contrasting historical surveys of constructivism which emphasize the "big schools" of INT, RUSS, and BISH, he says
[…] in my (humble) opinion, the trend of the future in constructivism is towards "neutral" constructive mathematics, which historically was a bit of a latecomer.
The three historical "big schools" all assume various principles that deviate from neutral constructivism, some of which are even classically contradictory. While some of those principles (notably ones like Markov's principle and countable choice, which are weak "computable" forms of LEM and AC and in particular are consistent with classical mathematics) are still in wide use today, it's become more fashionable to at least notice when they are used and attempt to avoid them if possible.
One important reason for this is that neutral constructivism is valid internal to any elementary topos, whereas these additional principles are not. Topos theory has also led to important insights into the best way to do mathematics constructively, such as the use of locales as a good notion of "space".
My main question is
Q: What is neutral constructive mathematics?
I tried to Google it, but I couldn't find much concrete. The best I could find was some comments on the nLab about the neutral point of view (nPOV). [Edit: The best I could find (at this time in writing my question) was this line in the nLab article constructive mathematics: "This is the neutral motivation for constructive mathematics from the nPOV.", referring to the applicability of constructive math to non-constructive category theory.]
To get the conversation started I have three guesses as to what neutral constructive mathematics means. I don't think these are mutually exclusive.
Guess 1: Neutral constructive mathematics is a philosophy
Rather than a specific foundational system, it could just be a philosophy of "don't assume more than you need to prove a theorem, because then you have a more general theorem". This is my interpretation of the nPOV, and also a philosophy I've seen debated many times in math (especially in logic and category theory). I think then the point would be that while Bishop thought his constructive framework was neutral because it is was compatible with Brouwer's Intuisionism, the Russian school of constructive math, and classical math, it turns out he was assuming, e.g., countable choice when he really didn't need to.
Of course we could do this ad infinitum until we are questioning every little detail of some proof and splitting hairs over every minute detail of a definition. So maybe it is more of an ideal that we shouldn't be afraid to generalize when we see a good generalization than a specific end goal.
Nonetheless, while constructivism has a long history of vague philosophies which resist concrete foundations, many others have found it very helpful to try to formalize those philosophies into explicit formal systems.
Guess 2: Neutral constructive mathematics is the internal theory of an elementary topos
I think for many category theorists and type theorists, elementary topoi are a really good foundation of mathematics that doesn't assume too much, but is still a place to do mathematics. Specifically from Mike's quote above, he suggests a neutral constructive theorem "is valid internal to any elementary topos".
[An aside for non-category theorists, especially logicians. When I first started learning about this topic it was really mysterious to me. But here is my short summary. An elementary topos is a type of category which generalizes the category of sets. Vaguely, many of the standard set theoretic operations hold, and the objects behave like "constructive sets", without necessarily things like the axiom of choice, replacement, or the law or excluded middle. The definition of an elementary topos is elementary, i.e. first-order axiomatizable, just like the axiomatic theory of groups or the axioms of ZFC set theory. Also, there are many naturally occurring categories which are elementary topoi.
Moreover, just like a first-order structure (in model theory) gives rise to a first order theory of that structure, any topos is a model category gives rise to a particular type theory. This type theory is called the internal language of the topos. The idea is that types are the objects of the category, and functions between types are the arrows. The elements of a type C are arrows going into the corresponding object $C$, and logical statements are terms of a particular type Prop of truth values (which corresponds to an object $\Omega$ in the topos called a subobject classifier). In particular, the type theory Intuisionistic Higher Order Logic (IHOL) captures the internal logic of all elementary topoi. A theorem that is provable in IHOL is (internally) valid in all elementary topoi. A theorem which is independent of IHOL, like the axiom of choice or the law of excluded middle is (internally) valid in some topoi but not others.]
If "provable in IHOL" / "valid in all elementary topoi" is the intended interpretation of neutral mathematics, then I have some (optional) follow up questions:
Q: What makes IHOL/topoi the right place for "neutral" constructive mathematics? Is it in some sense that this is the minimal setting for mathematics because it is the minimal categorical setting where we can develop mathematical propositions?
Q: Do you think there could be a good case for other settings to be the canonical "neutral" constructive math, like any of the following? Or are they too strong? (Please correct me if I get these type-theory/category pairs mixed up.)
- extensional Martin-Löf dependent type theory / locally cartesian closed categories
- HoTT+FunExt / locally cartesian closed $(\infty, 1)$-categories
- HoTT+Univalence+HIT / $(\infty, 1)$-topoi
- Others?
Guess 3: Neutral constructive mathematics is a type of reverse mathematics
Mike said (of various forms of LEM and AC) that it has "become more fashionable to at least notice when they are used and attempt to avoid them if possible". While this can be done informally by any mathematician to avoid using too powerful of results, it can also be done formally by asking "what is the minimal theory/model (over a base theory) for which a theorem is true/provable"? For example:
- In ZF set theory: "Every vector space has a basis" is equivalent to AC over ZF. (Also, there are similar results over ZFC.)
- In Freedman and Simpson's Reverse mathematics: "Every countable commutative ring has a prime ideal" is equivalent to WKL over RCA0.
- In constructive reverse mathematics: "Every bounded monotone sequence of real numbers converges" is equivalent to LPO over BISH.
One can do the same over any other base theory, like IHOL. Also, such equivalences can be viewed from a categorical perspective. (I think for example, knowing if AC holds in a topos tells us something about it being equivalent to its free exact completion, but I could be missing details.)
[Edit: I think the answers reveal a misunderstanding in what mean here. When I say "reverse mathematics", I don't explicitly mean Simpson's Subsystems of Second Order Arithmetic (who's base theory RCA0 uses LEM). I just mean a similar game. I'm think something similar to Ishihara's Constructive Reverse Mathematics, but using some formal categorical logic instead of BISH as a base theory.]
Also, as one throws away more axioms of mathematics, these results can get more and more pedantic. We get things like: "The fundamental theorem of algebra holds for Cauchy reals but not for Dedekind reals." One probably needs to ask if this is telling us something useful about these categories.
Last, in François G. Dorais's answer to Prospects for reverse mathematics in Homotopy Type Theory, he provocatively suggests that reverse mathematical style questions are the wrong questions to ask in these settings since they ignore proof relevance, so maybe I'm missing the larger point here (or maybe he was only being half serious).
Clarification: I have a tendency to ask long questions, but I'll accept the best answer which just answers "What is neutral constructive mathematics?" regardless of if it addresses my other subquestions.
Best Answer
You'll probably have better luck with the phrase "intuitionistic higher-order logic" (IHOL). A good place to start is the book by Lambek and Scott, Introduction to Higher Order Categorical Logic. But here is a shorter online article that may be helpful:
As Paul Taylor said in a comment, doing mathematics constructively (without proxies for excluded middle and choice principles) is that it maximizes the possibility for internalizing arguments to other types of categories -- not necessarily just toposes. It pays to examine how much "logic" is needed for an argument: purely equational logic? Horn logic? coherent logic? intuitionistic first-order logic? something higher-order? There's a sort of stratification of structured categories that goes with a stratification of logic -- one speaks of "fragments of logic" -- one is interested in "how much logic" can be successfully internalized in each type of structured categories. For example, an argument in "regular logic" can be enacted within any category of algebras for an algebraic theory. But the applicability of an argument that uses choice or excluded middle tends to be severely curtailed for these wider categorical contexts/semantics.
You could in a sense think of this correspondence between type of categorical structure and "fragment of logic" as constituting a categorical "reverse mathematics", although "reverse mathematics" as usually conceived is a little different (it typically accepts LEM).