Morse—Kelley set theory (hereafter MK) is the impredicative counterpart of von Neumann—Bernays—Gödel set theory (NBG), where formulas containing class quantifiers are permitted in the comprehension scheme. A fruitful analogy might be drawn between the predicative theory of second order arithmetic $\mathsf{ACA}_0$ and full $\mathsf{Z}_2$.

Now, MK proves the consistency of NBG, and consequently ZF(C), as well as all finite fragments of itself (and thus cannot itself be finitely axiomatised). Call $\Pi^1_n\mathrm{-MK}$ the theory where class comprehension is restricted to $\Pi^1_n$ formulas in the two-sorted language of set theory.

I would guess that the same situation obtains here as does in second order arithmetic: that $\Pi^1_{n+1}\mathrm{-MK}$ proves the existence of (code for) a model $M^\Pi_n$ of $\Pi^1_n\mathrm{-MK}$, such that $M^\Pi_n \not\models \Pi^1_{n+1}\mathrm{-MK}$. (There is a natural way to extend this conjecture to $\Delta^1_n\mathrm{-MK}$.) Such models would be the equivalent of countably coded $\beta_n$ models of theories of second order arithmetic; see chapter VII of Simpson's book on systems of second order arithmetic, particularly §VII.7. The natural way to think about this is to fix an inaccessible cardinal $\kappa$ so that $V_\kappa \models ZFC$; $(V_\kappa, Def(V_\kappa)) \models NBG$; and $(V_\kappa, V_{\kappa + 1}) \models MK$, where models of the intermediate systems are expanded from the model of NBG by adding in sets definable by $\Pi^1_1$ formulas, $\Pi^1_2$ formulas, and so on.

I have three questions. Firstly, is my conjecture correct? If so, is this just folk knowledge or are there specific references in the literature that I should attend to? And can we prove all this within MK, by working with codes for models, rather than assuming the existence of an inaccessible cardinal?

*Update, January 2014.* Kentaro Fujimoto has kindly let me know that these theories do indeed properly extend one another ($\Pi^1_{n+1}\mathrm{-MK}$ proves the consistency of $\Pi^1_n\mathrm{-MK}$), in the presence of global choice and $\in$-induction for the full language. This is proved as corollary 10 in his paper, by a cut elimination argument.

Fujimoto, Kentaro (2012). Classes and truths in set theory. *Annals of Pure and Applied Logic* 163 (11):1484-1523.

This makes me more confident in my conjecture about $\beta_n$ models, and points out something I hadn't thought about, namely that we will most likely need to include global choice and full induction in order to show that comprehension stratifies in the expected way.