often be interesting. However, in the case of the calculus/analysis as it was practiced in the 17th century, we are not aware of a single significant result that cannot be formulated in a system of type $\text{FOL}+\square$ (see Section \[one\] for examples of results that can). Arguably it was calculus (rather than analysis) that Leibniz invented, in the sense that there don’t appear to be any essentially second order statements there.

It may seem surprising that there could be a kind of pre-established harmony between a modern logical category, namely, first-order results, and a historical category, namely, results of 17th century calculus. This idea suggests further questions: does this only hold for the calculus, or is it always or often the case that a historically earlier realization of a theory covers only the first-order part of its successor. How do arithmetic and geometry behave in this respect? Would it really make sense to systematically distinguish between Leibniz and Leibniz1, Euclid and Euclid1, etc.?

Not standalone
--------------

Let us return to the comment *In the context of Skolem’s construction of nonstandard natural numbers and some related stuff, one is impressed by how many nonstandard numbers one needs to move from $\mathbb 