If $\mathcal{L}$ is a countable, first-order language, it is easy to see that every $n$-type $p$ (over $\emptyset$) can be expressed as an $\mathcal{L}_{\omega_1,\omega}$-formula, namely $\bigwedge_{\psi\in p} \psi$. Does the converse hold? Namely, given an $\mathcal{L}_{\omega_1,\omega}$ formula $\psi(v_1,\ldots,v_n)$ is there an $n$-type $p$ such that $\mathfrak{A}\models\psi(\bar{a})$ if and only if $\bar{a}$ realizes $p$ in $\mathfrak{A}$?

On a related note, are there any nice canonical forms for such infinitary formulas?

  • $\begingroup$ Already from a nice canonical form for formulas in the infinitary propositional language $\mathcal L_{\omega_1}$ you could derive a nice canonical form for Borel sets, and I don't think that such a canonical form exists. (But, like Borel sets, each such formula has a canonical "rank", the rank of the well-founded tree describing the formula.) $\endgroup$ – Goldstern Mar 8 '18 at 17:06

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.

| cite | improve this answer | |

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.

| cite | improve this answer | |
  • $\begingroup$ I fixed a typo; one $\psi$ should have been $\phi$. $\endgroup$ – Andreas Blass Jun 20 '12 at 13:11

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.

| cite | improve this answer | |
  • $\begingroup$ I probably should have mentioned that the reduction theorem also holds with a single type $p$ in place of the sequence $\{p_n:n<\omega\}$, but the proof is slightly more complicated. $\endgroup$ – Emil Jeřábek Jun 21 '12 at 12:45
  • $\begingroup$ @Emil: Do you have a reference for the reduction to a single type? I am actually studying the result of Morley that you mentioned, and am trying to find the cleanest way to adapt the argument which omits a single type in large models to instead satisfy an $\mathcal{L}_{\omega_1,\omega}$ sentence in large models. I know that this can be done in various ways, but what you just mentioned would be a very clean way of going about it. $\endgroup$ – Iian Smythe Jun 21 '12 at 15:41
  • $\begingroup$ I have expanded the answer with a simple way of doing it. I realized that I don’t know whether this strengthening actually holds also for finite models, but this is not relevant in your application. $\endgroup$ – Emil Jeřábek Jun 21 '12 at 16:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.