Proper class sized monster models are typically formulated in a class theory like $NBG$ and they can reasonably be formalized in $ZFC$ with some kind of global choice, but for some theories you don't need either classes as a first-order object or global choice to exhibit proper class sized monster models.

For a complete first-order theory $T$, a class model, $\mathfrak{C}$, is a class $C$ (as in the class of sets satisfying some formula maybe with parameters) with relations and functions also given by formulas maybe with parameters, such that $\mathfrak{C}$ models $T$ in the obvious way (although there is a subtlety here with $ZFC$ proving that $\mathfrak{C}$ models $T$ uniformly vs. individually proving that it models each finite set of sentences in $T$). A proper class monster model is a class model $\mathfrak{C}$ such that $C$ is a proper class and which is 'proper class saturated,' i.e. for every sub*set* $A\subset C$, $\mathfrak{C}$ realizes every type in $S_1(A)$ (I'm not going to worry about homogeneity right now).

For uncountably categorical theories and other extremely nice theories there clearly are proper class monster models. For an uncountably categorical theory we can take an Ehrenfeucht-Mostowski model with $Ord$ for its spine (which, it should be noted, at least gives us the existence of a proper class model for any theory, which isn't a priori obvious). You should be able to do something similar with $\omega$-stable $\omega$-categorical theories in light of the coordinatization theorem (there's a finite collection of totally categorical strongly minimal sets that models of this theory are prime over). I'm pretty sure that if you take a class sized model of a unidimensional theory and take an appropriate ultrapower of it (which is well-defined for set sized index sets, using the index set and ultrafilter as parameters) that the ultrapower will be proper class saturated.

It is plausible that the same can be done for stable theories in general (or at least nice enough stable theories), although I haven't tried to think about the details. On the other hand there are a couple of amusing examples of unstable theories with simple to describe proper class monster models. The surreal numbers are a proper class monster model of $RCF$ (and therefore $DLO$ in the reduct) and if we define an edge relation on the class of all sets by $xEy$ iff $x\in y$ or $y\in x$, then we get a proper class monster model of the theory of the random graph.

Is there a general method for exhibiting proper class monster models in $ZFC$ without global choice? If not are there nice families of theories for which we can exhibit proper class monster models? Is there a model $V$ of $ZFC$ and a theory $T$ that does not have a proper class monster model in $V$?

EDIT: There were requests for details on the EM model with $Ord$ for a spine construction. There might be some subtlety that I wasn't aware of regarding the model satisfying the theory but I'm fairly confident that you can literally construct the class. The construction is not completely uniform in that it needs the EM functor ~~or at least a well-ordering of the language~~ as a parameter in the end.

First run the typical EM functor construction: Given a consistent theory $T$ with infinite models, find a complete Skolemization $T^{sk}$ and then find an EM type of a non-constant indiscernible sequence in $T^{sk}$.

To construct an EM model, assuming we Skolemized the theory the 'dumb' way, it's sufficient to consider terms of the form $f(\overline{a})$ where $f$ is a Skolem function and $\overline{a}$ is a strictly decreasing tuple of indiscernibles, because any more complicated Skolem terms and terms with permutations of variables are equivalent to some base Skolem function corresponding to a formula of the form $y=t(\overline{x})$. So to construct the base class of the model, first let $$C_0 = \{\left<f,\alpha\right>:f\text{ an }n\text{-ary Skolem fn, }\alpha\in Ord\text{ with CNF }\omega^{\beta_0}+\dots+\omega^{\beta_{n-1}}\},$$

with the intended interpretation that $\left<f,\alpha\right>$ is equal to $f(\beta_0,\dots,\beta_{n-1})$. You can define Skolem function application by setting $f(\left<f_0,\alpha_0\right>,\dots,\left<f_{n-1},\alpha_{n-1}\right>)$ equal to $\left<g,\gamma\right>$ where you choose $g$ and $\gamma$ algorithmically from the list $f,f_0,\dots,f_{n-1}$ and the set of the exponents in the CNFs of $\alpha_0,\dots,\alpha_{n-1}$ (basically by the same kind of reasoning as why we don't need Skolem terms that are more complicated than just single Skolem functions applied to indiscernibles).

Then you define an equivalence relation on $C_0$ by $\left<f,\alpha\right> \sim \left<g,\gamma\right>$ for $\alpha = \omega^{\beta_0}+\dots+\omega^{\beta_{n-1}}$ and $\gamma = \omega^{\delta_0}+\dots+\omega^{\delta_{m-1}}$ by looking at a set of indiscernibles in the original indiscernible sequence with the same order type as $\{\beta_0,\dots,\beta_{n-1},\delta_0,\dots,\delta_{m-1}\}$ and then checking equality of the original corresponding terms. Let $\left[ \left<f,\alpha\right>\right]$ be the equivalence class of $\left<f,\alpha\right>$ (which may be a proper class). Then define the actual base class of the model by the typical kind of trick to avoid picking representatives:

$$ C = \{ \left[\left<f,\alpha\right>\right] \cap V_\beta : \left<f,\alpha\right> \in C_0 , \, \beta \text{ minimal s.t. } \left[\left<f,\alpha\right>\right] \cap V_\beta \neq \varnothing \}.$$

(This only matters if you want to avoid picking a well-ordering of the set of Skolem functions, otherwise you can just pick representatives.) Since the Skolemized theory is complete the definition of Skolem function application on $C_0$ is consistent with $\sim$, so it defines functions on $C$. Then you can define predicates using a dumb encoding trick: Let $f_0$ be the 0-ary Skolem function for the formula $y=y$ and let $f_1$ be the 0-ary Skolem function for the formula $y\neq f_0$. Then for any $n$-ary predicate symbol $P$, let $f^\ast_P$ be the Skolem function corresponding to the formula $\left(P(\overline{x})\rightarrow y = f_0 \right) \wedge \left( \neg P(\overline{x}) \rightarrow y = f_1 \right)$. Then the predicate $P$ is defined by $P(\overline{x})$ if and only if $f^\ast_P(\overline{x})=\left[\left<f_0,0\right>\right]$. (EDIT2: Although note that this also works for formulas in general, so by Skolemizing a theory we've actually also constructed a truth predicate for models of the Skolemized theory.) Clearly we already have constants and functions defined in terms of the Skolem functions.

And then pretty much by construction this is a class model of the $\forall \exists$ part of $T^{sk}$ (uniformly? since it has bounded quantifier complexity and you can define truth in ZFC for sentences with bounded quantifier complexity), which entails all of $T^{sk}$. Also it seems like this should be uniform in the parameters $T^{sk}$ and the EM type.

And really I think the only parameter you need is a well-ordering of the language, because given that you can canonically pick $T^{sk}$ and the EM type by expanding $\mathcal{L}$ with Skolem functions in the typical way to $\mathcal{L}^{sk}$ and extending the well-ordering to $\mathcal{L}^{sk}$; adding constants $I=\{c_i: i < \omega\}$ for a sequence of indiscernibles; adding the Skolem function axioms, $\forall \overline{x} (\exists y \varphi(y;\overline{x}) \rightarrow \varphi(f_\varphi(\overline{x});\overline{x}))$, and the indiscernible sequence axioms, $\varphi(\overline{c})\leftrightarrow \varphi(\overline{c}^\prime)$ and $c_0 \neq c_1$, for all $\varphi$ and strictly increasing tuples $\overline{c},\overline{c}^\prime$; and then picking a completion by going through the $\mathcal{L}^{sk}_I$ sentences $\{\varphi_i : i < \lambda \}$ according to the well-order and adding $\varphi_i$ if it is consistent (according to some fixed proof system) and $\neg \varphi_i$ otherwise.

EDIT2: I didn't see this question before. Joel's argument works the same here: Once you pick a well-ordering of the language $\mathcal{L}$ you can encode it in ordinals and consider the inner model $L[\mathcal{L}]$ where global choice holds and you can construct class sized models easily. I think the EM functor construction accomplishes something slightly different in that having an EM functor for a theory (i.e. a Skolemization and then an EM type in the Skolemized theory) seems weaker than having a well-ordering of the language, which *might* be useful.

EDIT3: I realized that the random graph, $DLO$, and maybe some others have a property in common that allows this to work: There is a canonical procedure for, given a set of parameters $A$, constructing a complete $|S_1(A)|$-type whose component $1$-types hit every type in $S_1(A)$. For the random graph we can take an element for each subset of $A$ and add in no connections between the new elements and for $DLO$ we can add in each cut. Any theory with this property has a proper class monster model because we can just iterate it along $Ord$.

I think it's really close to something you can do with an arbitrary stable theory, specifically if every type in $S_1(A)$ is stationary you can take a product type, $\bigotimes_{p\in S_1(A)} p$ (I think?). The problem I'm having with this is that types over the new set of parameters won't necessarily be stationary, so I'd like to use strong types but it's not clear to me that there's a canonical way of passing from a set $A$ to its algebraic closure in $T^{eq}$. It seems like it might need some amount of global choice to do. But maybe that's how to get a counterexample? Something involving a model of $ZFC$ where global finite choice or global choice for pairs fails.

allconsistent theories have such models in ZFC. However, I can’t find it now. $\endgroup$ – Emil Jeřábek Jul 5 '18 at 7:35