Can every $\mathcal{L}_{\omega_1,\omega}$ formula be expressed as a type? What about canonical forms?

No. In the language of first-order arithmetic, with $[n]$ denoting the standard numeral for $n$, the formula $\bigvee_{n\in\mathbb N}(v=[n])$ expresses that $v$ is a standard natural number. There is no type (conjunction of first-order formulas) that is equivalent to it in all models of first-order arithmetic. Proof: If there were such a type, then the theorems of first-order arithmetic, the formulas in the alleged type, and the formulas $\neg(v=[n])$ would form an inconsistent set of first-order formulas with no finite inconsistent subset, contrary to the compactness theorem of first-order logic.


Another way to express the idea of Andreas' solution is that the negation of a type is not generally expressible as a type, but the negation of an $\cal{L}_{\omega_1,\omega}$ formula is just another $\cal{L}_{\omega_1,\omega}$ formula.

Theorem. The negation of a type is a type if and only if the type is principal.

Proof. A principal type is one that is equivalent to a single formula. If a type is principal, then clearly so is its negation. Conversely, if $p=\bigwedge_n\psi_n$ is a type whose negation is also expressible as a type $\neg p=\bigwedge_m \phi_m$, then the union of these theories $\{\psi_n\wedge\phi_m \mid n,m\in\mathbb{N}\}$ is inconsistent, and so there is some finite part of $p$ that is inconsistent with a finite part of $\neg p$, and from this it follows that $p$ is equivalent to that finite part of $p$, since nothing realizing that finite part can satisfy $\neg p$ and hence must satisfy $p$. So $p$ is principal, as desired. QED

This is what is going on in Andreas' example, since "$n$ is nonstandard" is expressible as a type, and Andreas gave the proof that the negation of it is not.


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.