3 of 3
Replaced double-backslash-comma with single-backslash-comma, to fix rendering.

As noted in the other answers, not every $L_{\omega_1,\omega}$ formula is expressible as a type. Nevertheless, there is some sense in which $L_{\omega_1,\omega}$ is equivalent to omitting types:

Theorem: For every $L_{\omega_1,\omega}$ sentence $\phi$, there exists a countable first-order theory $T$ and a countable set of types $\{p_n:n<\omega\}$ such that any model $A$ satisfies $\phi$ if and only if $A$ can be expanded into a model of $T$ which omits every $p_n$.

One can construct $T$ and the $p_n$ as follows: introduce a new relation symbol $R_\psi(x_1,\dots,x_n)$ for every subformula $\psi(x_1,\dots,x_n)$ of $\phi$. If $\psi$ is atomic or constructed by the usual first-order operations from other subformulas, include in $T$ a corresponding axiom: for example,

$$R_{\exists x_{n+1}\,\chi(x_1,\dots,x_{n+1})}(x_1,\dots,x_n)\leftrightarrow\exists x_{n+1}\,R_{\chi(x_1,\dots,x_{n+1})}(x_1,\dots,x_{n+1}).$$

The only problem is to deal with countable conjunctions and disjunctions. If for instance $\psi(\vec x)=\bigwedge_{n<\omega}\psi_n(\vec x)$, we include in $T$ the axioms $R_\psi(\vec x)\to R_{\psi_n}(\vec x)$ for all $n$, and we include the type

$$p_\psi(\vec x)=\{R_{\psi_n}(\vec x):n<\omega\}\cup\{\neg R_\psi(\vec x)\}$$

as one of the $p_n$'s. Notice that $A$ omits $p$ iff it validates the implication

$$\bigwedge_{n<\omega}R_{\psi_n}(\vec x)\to R_\psi(\vec x).$$

The rest of the proof is easy.

If we work only with infinite models, a single type $p$ is sufficient instead of countably many. This can be seen as follows. Introduce a new predicate $N(x)$ and constants $\{c_n:n<\omega\}$, and consider the type $$p(x)=\{N(x)\}\cup\{x\ne c_n:n<\omega\}.$$ Then for each $\psi(\vec x)=\bigwedge_{n<\omega}\psi_n(\vec x)$ introduce a new predicate $S_\psi(u,\vec x)$ together with the axioms

$$\begin{gather*} R_{\psi_n}(\vec x)\to S_\psi(c_n,\vec x),\\ \forall u\,(N(u)\to S_\psi(u,\vec x))\to R_\psi(\vec x), \end{gather*}$$

which will serve together with $p$ as a replacement for $p_\psi$.

This result has various interesting consequences: for example, Hanf numbers of $L_{\omega_1,\omega}$ and of FO with omitting types are the same. (The Hanf number of a logic $L$ is the smallest cardinal $\kappa$ such that for every $L$-sentence $\phi$, if $\phi$ has a model of size at least $\kappa$, then it has models of arbitrarily large cardinality. The axiom of replacement implies that every logic whose formulas do not form a proper class has a Hanf number.) As a matter of fact, both Hanf numbers equal $\beth_{\omega_1}$, but this beautiful result of Morley has a considerably more difficult proof.

Emil Jeřábek
  • 35363
  • 3
  • 110
  • 170