Successor axiom systems and sequences of axiom systems Let $A$ denote a system of first-order axioms. Is there a canonical way to form a successor system $A'$ extending the ontology of $A$ to include all definable collections?
Edit: Importantly we want that if a system already has $\in$ in its signature, then its successor language extends $\in$.
Edit2: By the phrase "definable collection," here's what I had in mind. For every statement $P$ in the language of $A$ such that precisely one variable is free, call it $x$, add $\{x\,|\,P(x)\}$ to the constant symbols, and add $\forall y(y \in \{x\,|\,P(x)\} \leftrightarrow P(y))$ to the successor axiom system $A'$. Assume also that $\in$ is extensional over the domain of discourse associated with successor system $A'$.
Now suppose there is such a notion of successor axiom system. Consider a sequence of such systems. Suppose we take the "union" or "limit" of that sequence. What do we get?
 A: If you start with a first-order theory, whose elements are "individuals", and then you extend the language with new variables and quantifiers to talk about collections of individuals ("classes"), the resulting thing is usually just called "second order".  For example, "second order arithmetic" has variables for numbers and variables for sets of numbers, and "second order ZFC" has variables for sets and variables for classes of sets. For theories that do not have built-in pairing functions, it is typical to add not only classes, but also variables for all sorts of finitary relations on the individuals, e.g. binary relations, ternary relations, etc. 
If you extend the second-order system with new variables and quantifiers for "classes of classes", you get the "third order" theory, and so on through the natural numbers.  These systems are just type theories built on top of the original first-order theory. 
If you extend the original language indefinitely, through all the natural numbers, you still have a form of type theory. For example, the result of starting with Peano arithmetic and adding classes, classes of classes, and so on is the theory of "arithmetic in all finite types".  Similarly, one could study "ZFC in all finite types". 
If you want to go farther, beyond the finite types, you are now looking essentially at a set theory which has individuals from the original first-order theory as urelements.
