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.