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

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

Axiom A: $(f+g)'=f'+g'$

Axiom C: $(g \circ f)'=(g'\circ f)f'$

A bunch of the following is my presentation of reasoning given in a post by Tom Goodwillie: http://mathoverflow.net/questions/108773/independence-of-leibniz-rule-and-locality-from-other-properties-of-the-derivative/108804#108804 This whole answer is a shortened and cleaned up presentation of what was worked out in that MO question.

Theorems:

(1) The derivative of the identity function $I$ is 1. -- Applying axiom C to $I=I\circ I=I\circ I\circ I$ shows that $I'$ is equal to either 0 or 1 everywhere. Since continuity is assumed, $I'$ has the same value everywhere. By Z and C, that value can't be 0.

(2) The derivative of a constant function is 0. -- From A and (1) we can show that the derivative of $-I$ is $-1$. Composition of the constant function with $-I$ then shows that the derivative of the constant is 0, evaluated at 0.

(3) The derivative of $cx$, where $c$ is a constant, is $c$. -- By pre- or post-composing with a translation, we see that the derivative must be a constant $h(c)$. The function $h$ is a homomorphism of the reals with $h(1)=1$, so $h=c$.

(4) The derivative of $cf$, where $c$ is a constant, is $cf'$. -- This follows from (3) and C.

(5) The derivative of an even function at 0 is 0. -- Axiom C.

(6) The derivative of $s(x)=x^2$ is $2x$. -- Let $u(x)=s(x+1)-s(x)=2x+1$. Then $u'=2$. By (5), $s'(0)=0$. Therefore $s'(1)=2$. Precomposition with a scaling function then establishes the result for all $x$.

(7) For any functions $f$ and $g$, $(fg)'=f'g+g'f$. -- Write $2fg=(f+g)^2-f^2-g^2$ and apply (6).

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

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

Axiom A: $(f+g)'=f'+g'$

Axiom C: $(g \circ f)'=(g'\circ f)f'$

A bunch of the following is my presentation of reasoning given in a post by Tom Goodwillie: https://mathoverflow.net/questions/108773/independence-of-leibniz-rule-and-locality-from-other-properties-of-the-derivative/108804#108804 This whole answer is a shortened and cleaned up presentation of what was worked out in that MO question.

Theorems:

(1) The derivative of the identity function $I$ is 1. -- Applying axiom C to $I=I\circ I=I\circ I\circ I$ shows that $I'$ is equal to either 0 or 1 everywhere. Since continuity is assumed, $I'$ has the same value everywhere. By Z and C, that value can't be 0.

(2) The derivative of a constant function is 0. -- From A and (1) we can show that the derivative of $-I$ is $-1$. Composition of the constant function with $-I$ then shows that the derivative of the constant is 0, evaluated at 0.

(3) The derivative of $cx$, where $c$ is a constant, is $c$. -- By pre- or post-composing with a translation, we see that the derivative must be a constant $h(c)$. The function $h$ is a homomorphism of the reals with $h(1)=1$, so $h=c$.

(4) The derivative of $cf$, where $c$ is a constant, is $cf'$. -- This follows from (3) and C.

(5) The derivative of an even function at 0 is 0. -- Axiom C.

(6) The derivative of $s(x)=x^2$ is $2x$. -- Let $u(x)=s(x+1)-s(x)=2x+1$. Then $u'=2$. By (5), $s'(0)=0$. Therefore $s'(1)=2$. Precomposition with a scaling function then establishes the result for all $x$.

(7) For any functions $f$ and $g$, $(fg)'=f'g+g'f$. -- Write $2fg=(f+g)^2-f^2-g^2$ and apply (6).

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

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

Axiom A: $(f+g)'=f'+g'$

Axiom C: $(g \circ f)'=(g'\circ f)f'$

A bunch of the following is my presentation of reasoning given in a post by Tom Goodwillie: http://mathoverflow.net/questions/108773/independence-of-leibniz-rule-and-locality-from-other-properties-of-the-derivative/108804#108804 This whole answer is a shortened and cleaned up presentation of what was worked out in that MO question.

Theorems:

(1) The derivative of a constant function is 0. -- This follows from axiom C and composition with functions of the form $x\rightarrow a-x$.

(2) The derivative of the identity function $I$ is 1. -- The proof follows from axioms Z and C and $I=I\circ I$.

(3) The derivative of $cx$, where $c$ is a constant, is $c$. -- By pre- or post-composing with a translation, we see that the derivative must be a constant $h(c)$. The function $h$ is a homomorphism of the reals with $h(1)=1$, so $h=c$.

(4) The derivative of $cf$, where $c$ is a constant, is $cf'$. -- This follows from (3) and C.

(5) The derivative of an even function at 0 is 0. -- Axiom C.

(6) The derivative of $s(x)=x^2$ is $2x$. -- Let $u(x)=s(x+1)-s(x)=2x+1$. Then $u'=2$. By (5), $s'(0)=0$. Therefore $s'(1)=2$. Precomposition with a scaling function then establishes the result for all $x$.

(7) For any functions $f$ and $g$, $(fg)'=f'g+g'f$. -- Write $2fg=(f+g)^2-f^2-g^2$ and apply (6).

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

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

Axiom A: $(f+g)'=f'+g'$

Axiom C: $(g \circ f)'=(g'\circ f)f'$

A bunch of the following is my presentation of reasoning given in a post by Tom Goodwillie: http://mathoverflow.net/questions/108773/independence-of-leibniz-rule-and-locality-from-other-properties-of-the-derivative/108804#108804 This whole answer is a shortened and cleaned up presentation of what was worked out in that MO question.

Theorems:

(1) The derivative of the identity function $I$ is 1. -- Applying axiom C to $I=I\circ I=I\circ I\circ I$ shows that $I'$ is equal to either 0 or 1 everywhere. Since continuity is assumed, $I'$ has the same value everywhere. By Z and C, that value can't be 0.

(2) The derivative of a constant function is 0. -- From A and (1) we can show that the derivative of $-I$ is $-1$. Composition of the constant function with $-I$ then shows that the derivative of the constant is 0, evaluated at 0.

(3) The derivative of $cx$, where $c$ is a constant, is $c$. -- By pre- or post-composing with a translation, we see that the derivative must be a constant $h(c)$. The function $h$ is a homomorphism of the reals with $h(1)=1$, so $h=c$.

(4) The derivative of $cf$, where $c$ is a constant, is $cf'$. -- This follows from (3) and C.

(5) The derivative of an even function at 0 is 0. -- Axiom C.

(6) The derivative of $s(x)=x^2$ is $2x$. -- Let $u(x)=s(x+1)-s(x)=2x+1$. Then $u'=2$. By (5), $s'(0)=0$. Therefore $s'(1)=2$. Precomposition with a scaling function then establishes the result for all $x$.

(7) For any functions $f$ and $g$, $(fg)'=f'g+g'f$. -- Write $2fg=(f+g)^2-f^2-g^2$ and apply (6).