Do saturated models require choice? Let $T$ be a first-order theory, and suppose we want to build a saturated model $\mathbb U$ of $T$. That is, we want a model $\mathbb U$ of cardinality bigger than $|T|$, saturated in its own cardinality. In particular $\mathbb U$ will be universal and homogeneous for models of smaller cardinality.
In order to do this, one often assumes GCH or the universe axiom. I believe that GCH implies choice, so I opt in the following to assume that there is an inaccessible cardinal $\kappa$ with $T \in V_\kappa$. This theory (call it ZFCI) proves the existence of a saturated model $\mathbb U$ of cardinality $\kappa$.
Question 1: Does ZFI (analogous to above but without choice) prove the existence of a saturated model $\mathbb U$ of $T$?
Question 2: If not, can the exsitence of $\mathbb U$ be proven with less than the full axiom of choice?
Question 3: In the absence of choice, is there an alternative notion of saturatedness which is preferable to work with? In the above, by "saturated in its own cardinality", I think I mean "saturated with respect to subsets which do not admit a surjection to $\mathbb U$", but perhaps I should mean something slightly different.
If it's easier to discuss models saturated in some fixed cardinality, or universal and homogeneous with respect to some fixed cardinality, I'd find results about such constructions interesting too.
 A: On request, I summarize here some of the results mentioned in the comments (now unfortunately deleted), even though they do not really answer the question.
For definiteness, I assume that $M$ is saturated means that for every $A\subseteq M$ that does not surject onto $M$, every partial $1$-type over $A$ which is finitely satisfiable is satisfied in $M$.

Proposition. If every theory with a model has a saturated model, then:

*

*The Boolean Prime Ideal Theorem (aka Ultrafilter Lemma) holds.


*For every cardinal $l$, there exists a cardinal $k>l$ such that for all $m\le k$, either $m$ surjects onto $k$, or $k$ surjects onto $k^m$. (Here, none of the cardinals is assumed well ordered.)

Proof: For 1, if $X$ is an arbitrary set, endow $X$ with the first-order structure with unary predicates $P_Y$ for each $Y\subseteq X$, let $T$ be the elementary diagram of $X$, and let $M$ be a saturated model of $T$. If $F\subseteq\mathcal P(X)$ is a nontrivial filter, then $p_F(x)=\{P_Y(x):Y\in F\}$ is a finitely satisfiable partial type over $\varnothing$, hence there is $a\in M$ such that $M\models p_F(a)$. Then $\{Y:M\models P_Y(a)\}$ is an ultrafilter extending $F$.
For 2, let $T$ be, say, the Vaught set theory (VS), with axioms postulating for each standard natural number $n$ the existence of $\{x_0,\dots,x_{n-1}\}$ for all $x_0,\dots,x_{n-1}$. If $M\models T$ is saturated, let $k=|M|$. Fix $c\in M$. For any $f,u\in M$, we define
$$ap(f,u)=\begin{cases}v&\text{if $v$ is unique such that $\langle u,v\rangle\in f$,}\\c&\text{if no such $v$ exists.}\end{cases}$$
If $m\le k$, fix $A\subseteq M$ such that $|A|=m$, and define a function $F\colon M\to M^A$ by $(F(u))(a)=ap(u,a)$. If $A\times2$ does not surject onto $M$, then $F$ is onto: for any $f\colon A\to M$, $p_f(u)=\{ap(u,a)=b:f(a)=b\}$ is a finitely satisfiable partial type over $A\cup f[A]$, and its realization is an $u\in M$ such that $F(u)=f$.
[This only gives that $2m$ surjects onto $k$, or $k$ surjects onto $k^m$. However, restricting the argument to $f\colon A\to A$, we also get: $m$ surjects onto $k$, or $k$ surjects onto $m^m$, hence onto $2^{2m}$ (if $m\ge4$). In the latter case, $2m$ cannot surject onto $k$ due to Cantor’s theorem, hence $k$ surjects onto $k^m$ as wanted.]
In order to ensure $k>l$, it suffices to expand $T$ with $l$ many pairwise distinct constants. QED
One can strengthen condition 2 as follows: for any sequence $\langle A_u:u\in M\rangle$ of subsets $A_u\subseteq M$ that do not surject onto $M$, $M$ surjects onto $\bigcup_{u\in M}M^{A_u}$. To see this, modify $F$ such that if $w=\langle u,v\rangle$, then $F(w)$ is the function $A_u\to M$ defined by $(F(w))(a)=ap(v,a)$ for $a\in A_u$.
Instead of VS, we can take any consistent theory with a definable function $ap(-,-)$ that satisfies the axioms
$$\forall x_1,\dots,x_n,y_1,\dots,y_n\:\exists z\:\Bigl(\bigwedge_{i\ne j}x_i\ne x_j\to\bigwedge_iap(z,x_i)=y_i\Bigr)$$
for each $n$.
Note that in ZFC, condition 2 says that there are arbitrarily large cardinals $\kappa$ such that $\kappa^{<\kappa}=\kappa$, which is equivalent to the existence of saturated models for every theory. Without AC, the conditions are likely only necessary, not sufficient.
The question specifically invokes inaccessible cardinals. By the (now unfortunately deleted) comment by Asaf, I’m taking inaccessibility to mean: uncountable regular well-ordered cardinal $\kappa$ such that no $x\in V_\kappa$ surjects onto $\kappa$.
Whether the inaccessibility of $\kappa$ implies the existence of some saturated model for any consistent theory $T\in V_\kappa$ is something I strictly speaking cannot answer. However, if I take the question to mean if it implies the existence of saturated models of size $\kappa$ (which is how inaccessibles work in the classical case), this cannot work without assuming, essentially, that choice holds up to $V_\kappa$:

Corollary. If $\kappa$ is an inaccessible cardinal, the following are equivalent:

*

*Every theory with a countable model has a saturated model of cardinality $\kappa$. (We really just need this to hold for VS.)


*Every consistent theory $T\in V_\kappa$ has a saturated model of cardinality $\kappa$.


*$V_\kappa$ is well orderable (hence necessarily of cardinality $\kappa$).

Proof: If $V_\kappa$ can be well ordered, this gives enough of choice so that the usual construction of saturated models of size $\kappa$ goes through.
On the other hand, by the Proposition, 1 implies that $\kappa$ surjects onto $\kappa^\mu$ for all $\mu<\kappa$; this makes $\kappa^\mu$ well orderable, hence in fact (using the inaccessibility of $\kappa$) $\kappa^\mu=\kappa$, and $2^\mu<\kappa$. A standard argument by induction on $\alpha<\kappa$ then shows that $V_\alpha$ is well orderable of cardinality $<\kappa$ (see e.g. the proof of Theorem 9.1 (b) in Jech, The Axiom of Choice.)
In fact, this inductive argument gives the well-orderability of $V_\kappa$ itself if we can prove that $\bigcup_{\alpha<\kappa}\mathcal P(\alpha)$ can be well ordered, such as by showing that $\kappa$ surjects onto $\bigcup_{\alpha<\kappa}\kappa^\alpha$. This follows by the strengthening  mentioned below the Proposition. QED
