series $\sum_n \frac{(-1)^n}{n}$ determined by the alternating sequence $\frac{(-1)^n}{n}$. We will refer to such a sequence as a ‘Leibniz sequence’ for the purposes of this subsection. This criterion seems to be quantifying over sequences (and therefore sets), thus transcending the FOL framework, but in fact this can be handled easily by introducing a free variable that can be interpreted later according to the chosen domain of discourse.

Thus, the criterion fits squarely within the parameters of $\text{FOL}+\square$ at level (3) (see Section \[FOL\]). In more detail, we are not interested here in arbitrary ‘Leibniz sequences’ with possibly inassignable terms. Leibniz only dealt with sequences with ordinary (assignable) terms, as in the two examples given above. Each real sequence is handled in the framework $\mathbb{R}\subset{}^\ast\mathbb{R}$ by the transfer principle, which asserts the validity of each true relation when interpreted over ${}^\ast\mathbb{R}$.

Product rule {#s23}
------------

We have $\frac{d(uv)}{dx}=\frac{du}{dx}v+\frac{dv}{dx}u$ and it looks like we need quantification over pairs of functions $(u,v)$. Here again we are only interested in natural extensions of real functions $u,v$, which are handled at level (3) as in the previous section.

In [@Le84], the product rule is expressed in terms of differentials as $d(uv)=udv+vdu$. In *Cum Prodiisset* [@Le01c 