Are the models of infinitesimal analysis (philosophically) circular?

Question

Infinitesimal analysis (by which I mean that originating from topos theory---not the nonstandard analysis of Robinson) seeks to recover the pre-limit notions of calculus (which are sufficiently useful to persist in applications and intuition) in a formal way by throwing out the law of the excluded middle, which led to the paradoxes remedied in the 19th century.

My question relates not to the theory, which is certainly able to be constructed from scratch, and, rather, with how the models by which we're assured of the theory's consistency are founded.

As I understand it, from what little I've read of John Bell's 2008 monograph par excellence, these models are toposes into which it's possible to embed $\mathbf{Man}$ without introducing nonsmooth entities. However, if our goal is to completely supplant limit analysis (for, say, pedagogical or constructivist reasons; it's a noble crusade either way), it seems like this is a dependency loop: we need machinery to define $\mathbf{Man}$ as "the category of smooth manifolds and maps," but the entire utility of atlases is their reduction of computation on manifolds to flat analysis---which is what we're trying to replace.

Is this actually a problem? Is it known? Tractable?

Answer 1

It is not circular for us to prove the consistency of noneuclidean geometry by providing an interpretation of noneuclidean geometry within euclidean geometry, such as with the Poincaré disk model of hyperbolic geometry. Rather, these interpretations are important because they establish the basic coherence of the other theory—they give us the relative consistency result, which gives us the confidence that the other theory has its own basic integrity, at least as much as the standard alternative.

Similarly, it is not circular when we construct a model of ZF+$\neg$AC by forcing over a model of ZFC, or a model of ZFC+$\neg$CH by forcing over a model of ZFC+CH. Rather these arguments show the basic coherence and relative consistency of the other theory. The theories ZF+AC, ZF+$\neg$AC, ZFC+CH, ZFC+$\neg$CH are all equiconsistent with each other, equally safe from a consistency point of view.

It seems to be the same situation in your case. At issue historically was the worry whether the infinitesimal approach to calculus might simply be incoherent. Robinson's nonstandard analysis and the approach you mention show various (different) senses in which it is coherent.

Answer 2

Yes, there is some degree of philosophical circularity, if you take the view that the only "non-circular" way to build up a subject is to start with conceptually simple primitives, and work your way up to more complex concepts. On this view, it is illegitimate to claim that you're developing a foundation for analysis that avoids suspicious features of the conventional approach, if your "new foundation" takes (the very sophisticated concept of) manifolds as primitive and you don't have any way to explain what manifolds are without appealing to the suspicious conventional approach.

This line of reasoning is used by people like Harvey Friedman to argue that it doesn't make sense to claim that, say, category theory provides a completely self-contained approach to foundations that entirely avoids set theory, since the only way we know how to explain what infinite categories are is by appealing to our understanding of infinite sets. Sets, by contrast, are about as primitive as one can get, and we don't find ourselves appealing to more primitive concepts to explain what sets are.

That said, mathematicians tend not to worry too much about this kind of "circularity," if it doesn't manifest itself in the form of incorrect proofs. For a proof to be correct, it just has to start with your axioms and follow the prescribed rules. It's not necessary for you to have already developed a fully coherent explanation of your intended model in terms of "primitive" concepts. If the proofs are all fine, mathematicians tend to regard questions of philosophical circularity as being largely irrelevant to mathematical practice.