SDG is not elementary (inside a topos). The KockâLawvere axiom involves an exponential object, which is not first-order.

]]>Is a synthetic theory necessarily elementary (that is, first-order)? As an example, synthetic differential geometry is elementary while analytic differential geometry is maybe third-order inside a set theory. As another example, HoTT is (to my knowledge) elementary while oo-topos theory is maybe third-order inside a set theory. I do not know how to account for Euclid's elements. ]]>

We discussed a similar point at the Cafe. I think an important source of the terminology is the nineteenth century distinction between synthetic geometry (done with figures) and analytic geometry (done with coordinates) (see, e.g., here). Someone like Sophus Lie is using geometric intuition to do his work, and this includes intuition of infinitesimals.

For Kant, all of mathematics concerns the synthetic a priori, arithmetic relies on the inner sensual intuition and geometry the outer.

]]>That sounds exactly right to me as far as the maths is concerned. (I am however not well informed about the philosophical history of the terminology.)

]]>From reading Kock's book "Synthetic differential geometry" and seeing how he introduces axiom after another and seeing the care he takes to inform the reader which axiom he is using in which section, it would seem to me that synthetic differential geometry is a syntactic way of doing geometry. In a later part his book, Kock them introduces models of this geometry. As such, analytic differential geometry appears to be our original semantics of his theory.

The theory of synthetic differential geometry appears to be a Rusellian syntactical crystallization from philosophers of real mathematics, made after careful observation of the manner in which differential geometers create arguments about their original model. ]]>