The notation $\frac{\partial}{\partial x}$ is ubiquitous and totally useful, but also kind of weird. It seems to be doing the following:
- Bind $x$
- Compute the derivative
- Evaluate at $x$
To formalize this, we might write:
$$\frac{\partial}{\partial x} f(x,\tilde{y}) := (D(\lambda x. f(x,\tilde{y})))(x)$$
This gives the correct behaviour when other variables are around. For example, it can be shown that:
$$\forall x,y\left[\frac{\partial}{\partial x}\left(f(x)g(y)\right) = \!\left(\frac{\partial}{\partial x}f(x)\right)g(y)\right]$$
This also gives a decent account of the Leibniz linearity rule and product rule. For example, the product rule reads:
$$\forall x \left[\frac{\partial}{\partial x}(f(x)g(x)) = \left(\frac{\partial}{\partial x}f(x)\right)g(x)+f(x)\left(\frac{\partial}{\partial x}g(x)\right)\right]$$
However, its not at all clear how to formalize the various chain rules. For example, the single-variable chain rule says:
$$\forall x\left[\frac{\partial z}{\partial x} = \frac{\partial z}{\partial y}\frac{\partial y}{\partial x}\right]$$
The problem is that $y$ is being used both as a variable symbol, and also as a stand-in for an expression $y(x)$.
Similar problems occur when trying to formalize the single-variable inversion rule:
$$\forall x,y \left[\frac{\partial y}{\partial x} = f(x,y) \leftrightarrow \frac{\partial x}{\partial y} = \frac{1}{f(x,y)}\right]$$
On the LHS $x$ is a variable; on the RHS, $x$ denotes an expression.
Question. Has anyone succeeded in formalizing Leibniz notation, in such a way as to make the inversion rule and chain rules formal and correct?
It is "almost" legitimate to ask :
<< However, its not at all clear how to formalize the various chain rules. For example, the single-variable chain rule says: $$\forall x\left[\frac{\partial z}{\partial x} = \frac{\partial z}{\partial y}\frac{\partial y}{\partial x}\right]$$ The problem is that $y$ is being used both as a variable symbol, and also as a stand-in for an expression $y(x)$. >>
But it is more legimimate to ask if $z=z(x)$ is a correct symbolism because $z$ is used as the symbol of a function on the right side and is used as the symbol of a variable on the left (i.e. a value of function corresponding to a value of $x$ ). If this convention is accepted, there is no problem.
The heart of the problem is not in the Leibnitz notation, but is in the symbolism of function commonly used.
For example, let $z=f(x)=g(y)$ and $y=h(x)$ where a distinction is made between variables $x, y, z$ and functions $f, g, h$. Especially, two different symbols are used $f$ and $g$ for the same variable $z$ because corresponding recpectively to two different variables $x$ and $y$.
$$\forall x\left[\frac{\partial f(x)}{\partial x} = \frac{\partial g(y)}{\partial y}\frac{\partial h(x)}{\partial x}\right]$$
The drawback is this way, which increases the number of symbols, is overbearing. It is also of few interest for one which well master the common symbolism of functions.
Also, there is no problem when formalizing the single-variable inversion rule:
Let $y=f(x)$ and $x=g(y)$ $$\frac{\partial g(y)}{\partial y}=\frac{1}{\frac{\partial f(x)}{\partial x}}$$ This formalism is unambiguous but not commonly used because overbearing.