10
$\begingroup$

Normally we develop differential calculus by defining a derivative constructively as something related to a quotient (maybe an $\epsilon$-$\delta$-style limit of a quotient, or maybe the standard part of a $dy/dx$ quotient in NSA). I've been toying with the idea of developing the subject axiomatically instead. It seems like the following axioms allow me to do a reasonable amount of calculus:

Z. $\exists f : f'\ne 0$

U. $1'=0$

A. $(f+g)'=f'+g'$

C. $(g \circ f)'=(g'\circ f)f'$

P. $(fg)'=f'g+g'f$

(I'm leaving out the obvious $\forall f \forall g$ on most of these.)

For example, I can prove that $(cf)'=cf'$ for any rational number $c$, and that $(x^c)'=cx^{c-1}$ if $c$ is rational, at points where $x^{c-1}$ is defined. I think I can also prove the right result for, e.g., $x^\sqrt{2}$, since $(x^\sqrt{2})^\sqrt{2}=x^2$.

Some things I haven't figured out: (1) It's not obvious to me how one could start from this system and make contact with the usual constructive approaches and with transcendental functions. (2) Does it follow from these axioms that the derivative is local?

Maybe issues 1 and 2 above tell us that we need another axiom relating to continuity or something...?

Although I can't figure out how to prove P from the other axioms, I also can't figure out how to construct a model in which P fails, so it's not clear to me whether P is independent of the others. Can anyone construct such a model?

The system fails, as it should, to prove that a derivative exists at a point where the standard treatment of calculus says the function is nondifferentiable. On the other hand, none of the axioms allow us to prove affirmatively that any function is ever nondifferentiable.

  • 0
    I refined this a little, posted it at http://mathoverflow.net/questions/108773/independence-of-leibniz-rule-and-locality-from-other-properties-of-the-derivative , and got a very nice answer from Tom Goodwillie.2012-10-04

2 Answers 2

6

This is called "differential algebra". Google the term.

Sometimes the product rule (or "Leibniz rule") is stated as follows: (fg)' = f'g + fg', with $f$ on the left and $g$ on the right in every term. In that way, this can be applied to noncommutative rings.

  • 3
    Thanks, this is a very helpful answer. However, what I was trying to describe was somewhat more specific than differential algebra. If I'm understanding correctly, differential algebra involves a derivation that acts on any ring or field at all. I'm specifically interested in derivations that act on fields of functions, so that it makes sense to talk about the chain rule.2012-03-08
4

Related to Michael Hardy's answer, you could look at the concepts of derivations and of Kähler differentials in commutative algebra. These are used to formalize the concepts of differential forms and exterior derivatives in the context of algebraic geometry over fields other than $\mathbb R$ of $\mathbb C$.