The following is meant to be an axiomatization of differential calculus of a single variable. To avoid complications, let's say that $f$, $g$, $f'$, and $g'$ are smooth functions from $\mathbb{R}$ to $\mathbb{R}$ ("smooth" being defined by the usual Cauchy-Weierstrass definition of the derivative, not by these axioms, i.e., I don't want to worry about nondifferentiable points right now). In all of these, assume the obvious quantifiers such as $\forall f \forall g$.

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$

L. The value of $f'(x)$ is determined by knowing $f$ in any neighborhood of $x$.

Axioms A and P hold in any differential algebra. C and L mean that we're talking about something more specific than a differential algebra; they're meaningful only because we're talking about a ring of functions.

I could choose to omit U, since it can be proved from the others. I would prefer to keep U and omit P. Is P superfluous, or can anyone find a model in which P fails?

Likewise, is L independent of the others?

What seems to be tricky is to rule out models of the general flavor of $f'(x)=f^{CW}(x-17)$, where $f^{CW}$ is the usual Cauchy-Weierstrass derivative of $f$.

Are there models that are not the same as CW? Is this a nice axiomatization? Could it be improved?

[EDIT] Tom Goodwillie didn't say so explicitly, but his answer, along with one of my comments below his answer, shows that Z, A, and C suffice, so U, P, and L are not needed.

It looks like you can also take P as an axiom and recover the standard derivative, i.e., either P or C can be proved from the other: Do these properties characterize differentiation?