# 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?

-
It seems to me that you're talking about Henkin semantics of second-order logic? – Asaf Karagila Feb 3 '13 at 22:46
Perhaps. To be honest, I'm trying to get my head around what you were talking about with regards to moving up to the metatheory. – goblin Feb 3 '13 at 22:52
Well, in a recent MO answer Joel Hamkins wrote about the sets and classes, and pointed that universes are crude to a set theorist, but they are easy to understand for the working mathematicians. I was trying to make a similar point. There's always a bigger fish and if you work under the assumption that you're theory is consistent then you might as well work within a model, which itself is a set and so it lives in a larger universe. So we can talk about subsets - which are classes, or not - of that model. And so on. – Asaf Karagila Feb 3 '13 at 22:55
I also have to point out that it took me about three years since I started with set theory until I finished coming to grips with this topic (I will remark that I started with set theory roughly three years ago), at least in a sufficient level to feel that I can move forward. My advice to you, if you are trying to learn it, is to continue onwards and see how this problem is addressed in actual research and advanced materials. It will get solved, but it's easier to solve it retrospectively, I think. – Asaf Karagila Feb 3 '13 at 22:58
Fair enough. Anyway, this question stands apart from all that to some extent. – goblin Feb 3 '13 at 23:34

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.

-
I think that the question involves somewhat of a semantic rather than syntactic approach; more of a question about $\mathsf{ZFC\to NBG}$ than first order to second. Or rather a combination of the two. – Asaf Karagila Feb 4 '13 at 0:42
There are semantics, of course. The intended semantics of second-order systems is that the class variables range over ''all'' classes. This is true in particular with NBG and MK, which have the same intended models, and are just specific axiom systems for second-order set theory, in almost exactly the same way that $\mathsf{ACA}_0$ and $Z_2$ are different axiom systems for second-order arithmetic but have the same intended model. But there can't be a semantics without a syntax to define them on. – Carl Mummert Feb 4 '13 at 0:50
I was thinking of only adding the definable collections, so the result would be a new first order theory. – goblin Feb 4 '13 at 1:39
@user18921: you can add any comprehension scheme you want for the new second-order objects. So you can add a comprehension scheme that just postulates the existence of classes definable by a formula in the original language; this is essentially what NBG and $\mathsf{ACA}_0$ do. In any case the language will be the same no matter what comprehension scheme you add (or even if you don't add any). – Carl Mummert Feb 4 '13 at 1:43
The same in what sense? – goblin Feb 4 '13 at 2:02