How is implicit differentiation formally defined? I get that differentiation is an operation used on a function, so if a function is defined $x\mapsto x^2$, the derivative is 
$$
(x\mapsto x^2)'
   = x \mapsto \lim_{h\to 0} \frac{x^2+2xh+h^2-x^2}{h} = x\mapsto 2x.
$$
But how can you extend the definition $f' = \dfrac{f_h-f}{h}$ in such a way that it works with implicit functions/multifunctions? I know that it works, but I don't understand how it works for equations like $y^2 = 4-x^2$.
 A: I would say that implicit differentiation uses the chain rule. The implicit function theorem states that at any point $p=(x_0,y_0)$ on the curve (subject to some small niceness condition), there is a small section of the curve around the point that is the graph of some function $y_p(x)$.
We know that this function must obey $y_p(x)^2=4-x^2$. Now we just differentiate with respect to $x$, using the chain rule on $y_p(x)^2$, and we get
$$
2y_p(x)y_p'(x)=4-2x
$$
This then gives that the implicit derivative $y'$ of the curve at $p$ satisfies $2y_0y'=4-x_0$, which can easily be solved.
Note that the final expression doesn't feature the implicit function. The result doesn't depend on what that function is, only that it exists.
I don't know if this is how implicit differentiation is defined, but that's how I think about it.
A: Implicit differentiation just means the process of doing calculations with the rules for computing derivatives; e.g. supposing that $f'(x)$ exists, you don't have to know anything about the map $x \mapsto f'(x)$ is in order to know that the derivative of $x \mapsto f(x)^2$ is $x \mapsto 2 f(x) f'(x)$.
Or in Leibniz notation, you don't need to know anything about $\frac{dy}{dx}$ (other than it exists) in order to know that $\frac{d(y^2)}{dx} = 2y  \frac{dy}{dx}$.

More generally (and, IMO, more naturally too), there is the notion of differentials and/or the exterior derivative. Formalizing this notion in terms of differential geometry, if $y$ is a scalar (that is, a differentiable scalar field), then its exterior derivative is defined, and written as $dy$.
If $x$ and $y$ are two scalars related by an equation $y^2 = 4 - x^2$, then the exterior derivatives are the same too: $d(y^2) = d(4-x^2)$, and we can compute that this simplifies to $2y \, dy = -2x \, dz$.
Differentials do have the suggested relation to Leibniz notation; from here we can go on to infer that where $y \neq 0$, we have $dy = -\frac{x}{y} \, dx$, and thus $\frac{dy}{dx} = -\frac{x}{y}$.
Of course, this only makes sense when there are only two differentials involved; if we had three variables related by $z^2 = 4 - x^2 - y^2$, then we could conclude that $x \, dx + y \, dy + z \, dz = 0$, but it doesn't make sense to ask for $\frac{dy}{dx}$.
I, unfortunately, don't know of any source that introduces this in an elementary way; I've only seen it rigorously defined for the purposes of differential geometry or algebraic geometry/commutative algebra.
A: I struggled with this a lot as well. Let's look at the equation you mentioned, $$y^2=4-x^2$$ We define the function $f$  for all $-2<x<2$. 
$f(x)=$the unique y such that $y^2=4-x^2$ and $y>0$,
By that definition, we can conclude from the original equation that
$$(f(x))^2=4-x^2$$ for all $-2<x<2$.
Now let's look at that equation we just defined. Let $g$ be the function defined by $g(x)=(f(x))^2$ for all $-2<x<2$ and $h$ the function defined by $h(x)=4-x^2$ for all $-2<x<2$.  Then we have $$g(x)=h(x)$$ for all $x$ in their domains ($-2<x<2$), and therefore $g$ and $h$ are the same function. Since $g$ and $h$ are the same function, their derivatives are equal, i.e., $$g'(x)=h'(x)$$ for all $-2<x<2$, i.e. we can take the derivative of each side.
We can argue similarly for $k(x)=$ the unique $y$ such that $y^2=4-x^2$ and $y<0$.
A: It seems to me this is just a direct use of chain rule.
Differentiating the LHS by chain rule you would get $2y y'$ and RHS yields $-2x$, so you can solve for $y'$ directly using algebra:
$$
y' = \frac{-2x}{2y} = \frac{-x}{y} = \frac{-x}{\pm\sqrt{4-x^2}}
$$
In other words, you can prove from your definition above that
$$
f(g(x))' = \ldots = x \mapsto f'(g(x)) g'(x)
$$
and use that to deal with implicit differentiation.
A: Start with a function $f(x,y)$, in your case $f(x,y)= x^2+y^2-4$.  Obviously there is for some points a function $y(x)$ satisfying $f(x,y(x))=0$, namely $y(x)=\pm\sqrt{4-x^2}$, depending on the point. (Note that there are points where such a function doesn't exist.)
In general you can't solve $f(x,y)=0$ for $y$, but you can easily calculate $y'$ in terms of $x$ and $y(x)$ as follows.  Differentiate $0=f(x,y(x))$:
$$0=\langle\nabla f\left(x,y(x)\right),\left(1,y'(x)\right)\rangle=
f_x(x,y(x))+f_y(x,y(x))\cdot y'(x)$$
and solve easily for $y'(x)$.
In our case
$$0=\langle\nabla f\left(x,y(x)\right),\left(1,y'(x)\right)\rangle=
\langle (2x,2y),(1,y')\rangle=2x+2yy'.$$
