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).
The reason Berkeley was wrong is that Leibniz repeatedly emphasized that he is working with a generalized notion of equality. For example if y=x2, the desired formula 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. 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=x2 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 dz/dx =
dz/dy dy/dx ? 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.
See also
this related mathoverflow discussion.