Set theory bootstrapping

Let me describe how I understand the question. You want to consider assertions in the infinitary language $\newcommand\L{\mathcal{L}}\L_{\infty,\infty}$, and assert instances of replacement for formulas in this language.

Thus, our meta-theoretic context should have considerable set-theoretic resources, in order to handle the manipulations of these infinitary assertions, even if we interpret those assertions only in the object theory.

So basically, we have the realm of objects, a universe $V$ of the sets that the theory is about, and then we have a meta-theoretic or background set-theoretic context, let me call it $V^*$, which is a set-theoretic world of its own in which the formulas live and in which we undertake the truth analysis of those formulas. Let me assume ZFC in the meta-theory.

You ask:

Does one get a 'standard' model of set theory?

The answer is yes. I claim that $V$ must be well-founded with respect to $V^*$, and the reason is that with your replacement axiom, we can easily derive the $\L_{\infty,\infty}$-separation axiom, and with this, we can proceed to define the class of all sets $a$ that have no actual $\in$-descending $\omega$-sequence below them. This is expressible by an $\L_{\infty,\infty}$ formula of $V^*$, using the standard $\omega$ as $V^*$ sees it, and it would define the well-founded part of $V$, as $V^*$ sees it. In particular, by separation, using this definable property, the collection of nonstandard sets inside any given set would itself be a set. But this cannot happen unless every set is standard, for otherwise by the foundation axiom there would have to be an $\in$-minimal nonstandard set, which is impossible. Therefore, all the $V$-sets are standard with respect to $V^*$.

It follows now that every element $a\in V$ is definable an $\L_{\infty,\infty}$ formula. Namely, $a$ will be the unique satisfying instance of the formula $\phi_a$, defined as follows: $$\phi_a(x)=\forall y\left[ y\in x\leftrightarrow\bigvee_{b\in a} \phi_b(y)\right].$$ That is, $a$ is the unique set $x$ whose elements are the objects that satisfy the definitions of the various elements of $a$. This idea is used all over admissible set theory.

From this, it follows from your theory that $V$ must have the actual power set operation, since for any set $A\in V$, and any subset $B\subseteq A$ in $V^*$, we can write down the formula $\phi(x)=\bigvee_{b\in B}\phi_b(x)$, which asserts that $x$ is one of the objects in $B$. By separation, we will have deduced that $B$ is in $V$.

It follows in turn that $V=V^*_\kappa$ for some cardinal. One can show furthermore that $\kappa$ must be a strong limit, as well as regular. So $\kappa$ is an inaccessible cardinal, and these models $V_\kappa$ are also known as Zermelo-Grothendieck universes.

Conversely, I claim that if $\kappa$ is inaccessible, then $V_\kappa$ satisfies your theory. The reason is that $V_\kappa$ satisfies every instance of replacement using any means whatsoever in $V^*$, not just $\L_{\infty,\infty}$ assertions, because every set $A\in V_\kappa$ has size less than $\kappa$, and every subset of $V_\kappa$ of size less than $\kappa$ is bounded in some $V_\alpha$ for $\alpha<\kappa$, by the inaccessibility of $\kappa$. From this, it follows that we can define exactly that range using only a $\L_{\kappa,\kappa}$ formula.

So the models of your theory are exactly the $V_\kappa$ for $\kappa$ inaccessible, in the meta-theory.

All the preceding analysis is essentially similar to the result of Zermelo proved a century ago, when he proved that second-order ZFC set theory is true exactly in the $V_\kappa$ when $\kappa$ is inaccessible.

What I take the analysis to show, is that questions of these infinitary assertions amount to first-order assertions of set theory in the meta-theory. The subject becomes in a sense the same as the model theory of set theory undertaken in the meta-theory. In this sense, the infinitary theory amounts to a change in the level of analysis, moving from infinitary assertions in the object theory to first-order assertions about formulas in the meta-theory.


The idea of studying ZF and its subsystems formulated in infinitary languages, to my knowledge, seems to have begun and ended with the work of Klaus Gloede, in the 1970s.

The following paper of Gloede provides a useful synopsis of his work, which began with his doctoral dissertation (it is available here behind a paywall, the first two pages are freely visible, they consist of the table of contents and the first page of the paper).

K. Gloede, Set theory in infinitary languages. ⊨ISILC Logic Conference (Proc. Internat. Summer Inst. and Logic Colloq., Kiel, 1974), pp. 311–362. Lecture Notes in Math., Vol. 499, Springer, Berlin, 1975.