# Axiomatic approach to differential calculus?

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.

-
The product rule follows from the chain rule and linearity using the fact that $4fg = (f+g)^2 - (f-g)^2$. – Santiago Canez Mar 4 '12 at 1:59
@SantiagoCanez: How do you differentiate the squares in your expression without already having established the product rule? In Z through C, the only place where multiplication is even referred to explicitly is C. – Ben Crowell Mar 4 '12 at 2:08
You could look into the Kock–Lawvere axiom of synthetic differential geometry, which is enough to prove many of the usual differential calculus results. – Zhen Lin Mar 4 '12 at 2:13
@Ben, C implies that the derivative of $(f+g)^2$ is $2(f+g) (f+g)'$, and then A implies that this is $2(f+g)(f'+g')$. Similarly for the second term. – Santiago Canez Mar 4 '12 at 2:20
One thing that seems missing from this approach is the notion of differentiable function. It is notoriously hard to say something about the class of differentiable functions beyond the fact that it is a subclass of the continuous functions. I fear this makes it unsuitable for axiomatization. – Pete L. Clark Mar 9 '12 at 6:26

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.
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$.