Solution (source code)

= Solution

A sentence $\forall\bar x\,\exists\bar y\,\varphi(\bar x,\bar y)$ with quantifier-free $\varphi$ is preserved by a union of an embedding chain: a tuple $\bar a$ occurs at some stage, a witness $\bar b$ exists at that stage, and quantifier-free formulas are preserved in the union. Thus every forall-exists axiomatized theory is <inductive first-order theory>[inductive].

Conversely, let $T_0$ contain all forall-exists consequences of $T$ and suppose $M\models T_0$. The diagram-and-compactness sandwich lemma says that one can construct
$$
M=M_0\subseteq N_0\subseteq M_1\subseteq N_1\subseteq\cdots
$$
where every $N_i\models T$ and every $M_i\preccurlyeq M_{i+1}$. For completeness, the first extension is obtained by adding to $T$ the diagram of $M_i$ together with all universal formulas over $M_i$ true there. A finite inconsistency would give a forall-exists consequence of $T$ false in $M_i$. The resulting extension embeds into an elementary extension $M_{i+1}$ by the method of diagrams.

The $N_i$ form an embedding chain and have the same union $N$ as the $M_i$. By the assumed preservation, $N\models T$; by the <elementary chain theorem>, $M\preccurlyeq N$. Hence $M\models T$, so $T_0\models T$. The two theories are equivalent, proving the characterization.