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.

  • 3
    The product rule follows from the chain rule and linearity using the fact that $4fg = (f+g)^2 - (f-g)^2$.2012-03-04
  • 1
    @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.2012-03-04
  • 1
    You could look into the Kock–Lawvere axiom of synthetic differential geometry, which is enough to prove many of the usual differential calculus results.2012-03-04
  • 0
    @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.2012-03-04
  • 0
    I guess you have to know what the derivative of $x^2$ is beforehand though, so you still need more than just the first four axioms.2012-03-04
  • 0
    @SantiagoCanez: Right, the question would then be whether it follows from Z through C that the derivative of $x^2$ is $2x$.2012-03-04
  • 0
    @ZhenLin: Synthetic differential geometry, and its link to nonaristotelian logic, always seemed fascinating to me, but I haven't come across a nontechnical account. Any suggestions?2012-03-04
  • 0
    @Ben: I'm afraid I haven't even read any technical accounts! I've just been fortunate enough to be able to attend a series of lectures on the subject.2012-03-04
  • 0
    I spent some time this morning trying to find a model of Z through C in which P fails, and haven't succeeded yet. The kind of ideas I'm coming up with are things like defining the derivative $Df$ of $f$ in terms of the standard Newton-Leibniz derivative $L$ but making the result depend in some way on $f$'s behavior far away. Regardless of whether P is independent of Z-C, it seems like one might want an axiom saying that if two functions are equal on $[a,b]$ and differentiable on $(a,b)$, then their derivatives are equal on $(a,b)$.2012-03-04
  • 1
    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.2012-03-09
  • 0
    @PeteL.Clark: Yes, that's a good point. However, one can make models of the axioms within, e.g., the set of smooth functions.2012-03-10
  • 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