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.
