When studying differential geometry, I often feel that infinitesimal approaches would do a deal for the intuition. There also seems to exist various examples like synthetic differential geometry or infinitesimal displacements.
However, I wonder if any of these serve as a conservative extension, i.e. everything which can be translated back into the language of first order logic and standard analysis must hold for classical differential geometry as well?
The approach to differential geometry using infinitesimal displacements was developed in this 2015 article in Journal of Logic and Analysis. (JLA). Note that JLA is the flagship journal for Robinson's framework for doing analysis (and other fields) with infinitesimals. Naturally, by the transfer principle all first-order statements translate back and forth. A more detailed presentation of this approach can be found in my lecture notes here.