[Ferrotin]

Define lim without infinite sets. Define how you quantify over all values of n without infinite sets. The parameterization you describe would be a function mapping an infinite set of sets of natural numbers to their maximum elements, that function itself being (or containing) an infinite set of ordered pairs.

You might be able to pull it off without creating something equivalent to the axiom of infinity — I wouldn’t know if it’s possible. But the naïve implementation of your ideas involves the construction of infinite sets.

I think you can do this rigorously outside the theory, talking about it, but not inside.