Can one justify Leibniz's formalism in a suitable algebraic or topological context?
We have published some papers recently where we argue that Leibniz's formalism for the calculus wasn't inconsistent as Berkeley claimed. For an insightful review see http://www.ams.org/mathscinet-getitem?mr=3053644
Berkeley claimed that Leibniz wanted to have it both ways: both $dx\not=0$ so as to form the differential ratio, and also $dx=0$ so as to get the right answer (i.e., a "standard" one). Starting about 140 years ago, Berkeley's claim of inconsistency of Leibnizian calculus acquired the status of dogma to such an extent that Robinson himself felt compelled to speak of Berkeley's "brilliant critique" of the calculus, and referred to the hyperreal framework as "a small price to pay for the removal of an inconsistency"–the implied assumption being that such an "inconsistency" was real.
The reason Berkeley was wrong is that Leibniz repeatedly emphasized that he is working with a generalized notion of equality. For example if $y=x^2$, the desired formula $\frac{dy}{dx} = 2x$ does not mean that the residual $dx$ is set equal to zero but rather that it is absorbed into the generalized relation of equality "up to" a negligible term, in an exact sense to be specified. Leibniz called this principle the transcendental law of homogeneity. The principle is mentioned, for example, in the title of his 1710 paper, as reported already in 1974 by Bos. Berkeley did not take this into account and merely misunderstood Leibniz.
Now this is fine for showing that Leibniz was not inconsistent (refuting Berkeley's claim). However, it is not quite enough for showing that Leibniz was actually consistent, or more precisely for formalizing Leibniz's approach. This is because it is not completely clear what the generalized relation is exactly. I will refer to such a generalized notion as "adequality" so as not be have to write "generalized equality up to" every time.
In other words, if we want to be able to work with adequality as we work with the ordinary equality, we need to explain how this is done and why this works and why whenever A=B one can replace A by B in computations. Robinson circumvented the problem by using the standard part function but this isn't completely faithul to Leibniz's formalism.
One attempted solution is to take the adequality 2x+dx=2x to mean that the difference of the two sides is infinitesimal. But if this is our notion of adequality, then this allows us to write down things like dx=0, as well, and if we are allowed to replace dx by 0 in calculations then we end up dividing by zero.
In Lawvere's approach (also Kock, Bell) they replace the ratio formula $f '(x)=dy/dx$ by the multiplication formula $dy=f '(x)dx$. Then they get equality on the nose by working with nilsquare infinitesimals. Thus their adequality is true equality on the nose. In this way they implement (some of) Leibniz's procedures. However, this is not entirely faithful to Leibniz because Leibniz worked with arbitrary order infinitesimals, and also divided by them freely.
Euler worked with what he called a generalized "geometric" equality where A=B means that the ratio of A to B is infinitely close to 1, but this does not automatically allow us to add such relations. Of course if all expressions involved are appreciable, this does work. On the other hand, we can't always assume both sides to be appreciable because this would disallow critical points, certainly a disturbing loss.
How does one address this problem? The idea is to continue working with Euler's "geometric equality" and somehow to make both sides appreciable by working globally rather than at a specific point; or perhaps evaluating the expressions at a generic (or perhaps nonstandard?) point. This would hopefully allow one to manipulate an adequality between expressions as an ordinary equality.
In the specific case of $y=x^2$ the problem is the zero of the derivative where Euler's geometric equality does not work, but at any other point we are OK.
Could one define such a relation in an algebraic (or algebraic-geometric) context? One needs to specify the sort of expressions one is allowed to work with, i.e. introduce a limitation on the objects one is allowed to use. Or perhaps it is enough to declare expressions adequal if they are geometrically equal at a nonstandard point.
Can one redefine the relation "=" in a suitable context, so that for example one could read the chain rule as literally saying $\frac{dz}{dx} = \frac{dz}{dy}\frac{dy}{dx}$ ? The relation can be rewritten in a simpler form in terms of differentials: $dz = \frac{dz}{dy}dy$ but this still depends on the "cancellation" of $dy$ in the numerator and denominator. This works with Euler's "geometric equality" but the problem is you can't add such equalities. Already chain rule with 2 variables requires addition.
Aside from the pedagogical value of being able to cancel out the two $dy$'s in $dz/dx =dz/dy\; dy/dx$, an application would be the solution of differential equations by separation of variables, etc. More generally, one would like to be able to take any argument using derivatives, and be authorized to replace $f ′ (x)$ by $dy/dx$ whenever it occurs without changing the argument otherwise. In nested arguments involving multiple derivatives this could be a significant simplification.
Differential geometry is a rich source of examples where salvaging Leibniz's formalism could simplify many proofs. Beyond being able to say that the center of curvature is the point of intersection of two infinitely close normals, numerous arguments in Gauss and Riemann are simpler in their original infinitesimal form (including formula for curvature) than their modern reformulations; see discussion in Spivak, Differential geometry, volume 2, and related MSE thread.
Best Answer
You seem to think that synthetic differential geometry only handles squarenil infinitesimals, but this is not so. The generalized Kock-Lawvere axiom allows us to work with infinitesimals of any order, and actually much more than that. So as far as I can tell synthetic differential geometry captures all the essential features of Leibniz's infinitesimals, and more, while working with a completely standard notion of equality. This is important because for algebraic manipulations we want a notion of equality that allows us to replace equals for equals.
It might be helpful to find out what sources you are using to find out about synthetic differential geometry. Already Bell's A Primer of Infinitesimal Analysis, the most basic text on SDG, talks about infinitesimals of order $n$.
Supplemental: since the discussion below talks about the chain rule, here is its derivation in SDG, for reference, where $dx$ is a square nilpotent infinitesimal: $$g(f(x + dx)) = g(f(x) + f'(x) \cdot dx) = g(f(x)) + g'(f(x)) \cdot f'(x) \cdot dx,$$ We just used twice the principle of Microaffinity. We can now directly read off $$(g \circ f)'(x) = g'(f(x)) \cdot f'(x).$$ I do not see how this derivation would be more straightforward if we were allowed to magically divide by infinitesimals.