The claims in this article, such as those suggesting recursion has something to do with the infinite, are all relative to the set-theoretic foundation. This is not essential.

In contrast, in the type theories behind proof assistants like Coq, Lean, and Agda, recursion is intimately tied to _finite_ structures. Instead of the vague "intersection of all sets such that" which we see in the article here, recursion is a well-defined computational process, and defined in a rather obvious way once you're familiar with the background.