What is neutral constructive mathematics

Question

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.

Answer 1

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:

• J. Lambek and P.J. Scott, Reflections on a categorical foundations of mathematics.

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).

Answer 2

I suppose I ought to contribute an answer to this. Maybe I should start by saying that I did not originate the term "neutral constructive mathematics". I believe I picked it up from Martin Escardo; I'm not sure whether he originated it. On the other hand, of course I can only speak to what I mean by it myself.

It's easier to say what I don't mean by it than what I do mean. I don't mean any kind of reverse mathematics (even in the looser sense described by Todd), or a philosophy of always using the minimal foundational system for any given theorem. It's compatible with those, but when I say "neutral constructive mathematics" I'm generally thinking of a kind of mathematics as done by a working mathematician, who isn't constantly changing their foundational axioms or going through contortions to weaken them, but generally just sticks to a particular foundation — the only difference with classical mathematics is that the foundation is a "constructive" one.

On the other hand, neither do I intend to refer to one specific formal system (such as IHOL) or even one specific class of models (such as elementary 1-toposes with NNO). Those are a good baseline, but there are various other formal systems that I would also regard as at least potentially acceptable for neutral constructive mathematics, such as:

• Various other formulations of an internal logic for elementary 1-toposes, such as Intuitionistic ETCS, certain forms of MLTT, or even their corresponding membership-based set theories such as "Intuitionistic Bounded Zermelo".
• Extensional MLTT without universes, but with function extensionality, W-types, and and effective coproducts and quotients: the internal language of $\Pi W$-pretoposes. (The internal language of merely locally cartesian closed categories is also "sufficiently constructive", but hard to do very much mathematics in.)
• Intensional MLTT with all those same things, for some meaning of "quotient": conjecturally the internal language of some class of locally cartesian closed $\infty$-categories.
• Either of the above with universes.
• Intensional MLTT with all those things plus univalent universes: conjecturally the internal language of "elementary $\infty$-toposes" (whatever those are).
• Any of the above augmented by the existence of some class of higher inductive types.
• Any of the above augmented by "constructive" set-theoretic axioms such as full separation, collection, set-induction, etc. For instance, we have membership-based set theories like IZF.
• Any of the above augmented by weak choice principles such as WISC.

If someone held a gun to my head and forced me to give a specific criterion for a formal system to be appropriate for neutral constructive mathematics, I might say something like "it suffices for reasoning internal to any Grothendieck 1-topos defined over ZFC plus Grothendieck's axiom of universes". All the above systems have the property that any such 1-topos either is, or can be enlarged to, a categorical model of them. Moreover, this criterion rules out the obvious things that some so-called "constructive" systems include but that we don't want to allow: no countable choice, no Markov's principle, no definition of "sets" as an exact completion of "pre-sets", since all of these fail in some Grothendieck topos.

However, in the absence of such imminent threat, I would resist giving any specific criterion. The reason I stated the above criterion with Grothendieck toposes instead of elementary ones is that I don't necessarily want to exclude additional axioms that are "constructive" but don't hold in all elementary toposes, and we do know that all the above theories do have models in Grothendieck toposes. But from a philosophical point of view it's not clear how to argue for any primacy of Grothendieck toposes; what about, say, realizability toposes? Or cocomplete toposes without small generators? Or filterquotients of such toposes? Or exact completions of such toposes? Many of these categories also model many of the same additional axioms that Grothendieck toposes do; but not all of them model all the same axioms, and not all of them can easily be enlarged to $\infty$-toposes. Thus, someone who cares about some of these categories might object to some of the systems I mentioned above.

One reasonable perspective is that there's a gradation of "neutrality" from systems that are inarguably neutral, like IHOL, to systems that are inarguably non-neutral, like BCM, CRM, and ZFC, through systems like the above that are "less neutral" than IHOL but still arguably "pretty neutral". The reason IHOL and elementary 1-toposes are such a good baseline to call "fully neutral" is essentially a pragmatic one: they suffice for huge amounts of mathematics and also admit a very wide class of models. On one hand, additional axioms are sometimes needed for specialized purposes, but any such assumption reduces the class of models. On the other hand, while it's easy to find non-Grothendieck elementary toposes, it's significantly harder to find interesting $\Pi W$-pretoposes that aren't toposes, and predicative constructive mathematics often requires rather more contortions than the impredicative sort permitted by IHOL.

Answer 3

Surely the way that we should define neutral constructivity is not by legislating particular systems but by considering how those interested in (constructive) foundations should interact with others in the community of mathematicians and vice versa.

This is becoming more relevant as interest grows, not just in formalising individual proofs with particular proof-assistant programs but in building libraries of such proofs. [I will add links to these if people tell me them by email.] These give a more concrete meaning than journals can to what I call the corpus of mathematics.

My thoughts were prompted by one of @KevinBuzzard's online talks about LEAN. I take issue with his judgement of mathematics by Fields Medals, but that is not meant as a personal criticism because it's great that he is engaging with other (people who identify as) mathematicians. I commented that he was only interested in skyscrapers when others are trying to build a city.

Perhaps it's better to think of Mathematics as a huge machine, for instance like your (laptop, desktop or bigger) computer, attached to the Internet. Maybe you are primarily interested in a Theorem Prover, or a computational model of the climate, but you make use of a wordprocessor, a web client, an operating system, a wifi router, an ISP and cables under the ocean.

At every level in this machine, there are people with PhDs (many in maths, indeed) spending their careers trying to make their particular component work better. (Apart from the Web Designers, that is.)

We as a community of mathematicians need to see each other as fellow professionals, as engineers, working on different parts of this huge machine. Maybe the latest improvement to fibre optics or the Linux kernel is not going to generate an immediate publication for you in number theory, theorem proving or climate modelling. But it's all part of the whole.

To take Kevin as an example again (without meaning to pick on him), in his undergraduate lectures on algebraic geometry maybe he assumes that fields have characteristic zero, but in his research on number theory he considers prime characteristic. Likewise, those of us who are interested in "foundational" questions like to take mathematical arguments that use the axiom of choice or excluded middle and rework them to be "constructive".

In both cases we obtain not just generalisation for their own sake, but a better understanding of the subtleties and symmetries of mathematics. To blow my own trumpet with two examples,

• the different forms of constructive topology and analysis have shown up overt (sub)spaces as lattice duals of compact ones
• the intuitionistic study of the ordinals has produced plump ones, which have subsequently been used in other research.

I'm not going to claim knowledge of past Fields Medals, but they have been given for work with significant foundational components.

To return to the question as Jason posed it,

I certainly believe in reverse mathematics, meaning the deduction of axioms from theorems, but I do not subscribe to Reverse Mathematics™, because it presupposes a particular codification of mathematical statements. As a categorist, I assert my right to re-formulate them as I see fit.

Doing mathematics in an elementary topos with natural numbers does seem to be a reasonable compromise with the rest of the community of mathematicians and the corpus of mathematics.

By way of a worked example, I (privately) promised Monroe Eskew an answer to his question, but maybe now I'll write that separately.

Answer 4

I don't know the history of the phrase "neutral constructive mathematics", but I would guess that it is meant to be analogous to "neutral geometry". Neutral geometry (or absolute geometry) is the part of plane geometry which makes no assumption about the truth or falsehood of the parallel postulate. A theorem of neutral geometry is valid in both Euclidean geometry and hyperbolic geometry. So, I would assume the idea of "neutral constructive mathematics" is that we don't allow the use of things like law of the excluded middle, but we also don't add any axioms that are classically false, such as "all functions on the reals are continuous". For instance, Bishop's constructivism is neutral but Brouwer's intuitionism is not.

(Edit: Now I see that the phrase "Bishop's constructivism" has multiple possible meanings, possibly leading to further confusion. When I wrote the previous sentence, I didn't have in mind the system described on that nLab page, which I don't really understand.)

Again I'm not that familiar with the historical context, but it stands to reason that one would investigate the anti-classical/non-neutral constructive systems first, if only to demonstrate that there are indeed interesting non-classical examples to which the general, neutral theory applies.