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

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.
