Title: A Complete Axiomatisation of Partial Differentiation
Abstract. Looking at recent work on categories equipped with differential structure (e.g., Blute, Cockett, and Seely’s cartesian differential categories) one naturally asks if the categorical axioms are not only sound but also complete for natural examples, (e.g., smooth functions). Here we look at a related question: whether the well-known rules of partial differentiation are complete for smooth functions.
To do so, we first formalise these rules in second-order equational logic, a version of equational logic with function variables and binding constructs. We prove the resulting theory is complete with respect to smooth functions, indeed even with respect to polynomial interpretations. The proof makes use of Severi’s interpolation theorem that all multivariate Hermite problems are solvable.