# Determining all the $1$-types of a given theory

I'm trying to solve an exercise in my lecture notes. I'm given the following theory of infinitely many disjoint infinite unary predicates:

Let $$L_n$$ be the language with $$n$$ unary predicate symbols $$P_1, . . . , P_n$$. Let $$T_n$$ be the theory asserting that each $$P_i$$ is infinite, the $$P_i$$ are disjoint, and there are infinitely many elements not in any $$P_i$$, for $$i \leq n$$. Finally, let $$T = \bigcup_n T_n$$.

After having proved that both $$T_n$$ and $$T$$ are complete, I'm then asked to determine all the $$1$$-types of $$T$$, show that there's a unique 1-type $$p_n$$ including $$P_n(x)$$, and a unique type $$q$$ that is not one of the $$p_n$$.

I have no idea how I'd go about determining all the $$1$$-types, and while I can certainly find a $$1$$-type $$p_n$$ including $$P_n(x)$$ (by setting $$p_n =$$ tp$$_A(a) = \lbrace ϕ(x) : A \models ϕ(a)\rbrace$$, where $$A$$ is some model with $$a\in A$$ such that $$a\in P_n^A$$), but I'm not sure how I'd show it's unique.

I know that if If $$π : A → B$$ is an isomorphism, $$a ∈ A$$, $$b ∈ B$$ and $$π(a)= b$$ that tp$$_A(a) =$$tp$$_B(b)$$, so clearly there's only one $$p_n$$ obtained by taking a set like tp$$_A(a) = \lbrace ϕ(x) : A \models ϕ(a)\rbrace$$, but I don't know how to show there are no other $$1$$-types containing $$p_n$$ (perhaps this will become clearer once I know what all the $$1$$-types are). I also have no idea how I'd go about finding the $$q$$ I'm asked for.

• Are you possibly the same user who asked this recent question? If so, you should use the same account, rather than creating a new one for each new question. If not, maybe they're in your class! Commented Nov 24, 2020 at 2:15
• @AlexKruckman no, that wasn't me, and I didn't see that question, but that does look very similar to an earlier problem I solved so you might be right - they could well be taking the same course as me! Commented Nov 24, 2020 at 11:01

Your reasoning is quite in the right direction.

To show that these types are unique, first note that if $$A$$ is any model of $$T$$, then elements of $$A$$ which are in the same disjoint part realise the same type. Indeed, if $$a,b \in P_n^A$$ then we may define $$σ: Α \to A$$ by $$σ(a) = b, σ(b)=a, σ(x)=x$$ otherwise. It is easy to check that this is an automorphism of $$A$$, and automorphisms fix types so $$tp_A(a) = tp_A(b)$$. We can see that any type of this form contains $$P_n(x)$$, as $$A \models P_n(a)$$.

So, let p,q be two types that include $$P_n(x)$$. We may find $$M \models T$$ which realises both p and q, i.e. $$\exists m_1, m_2 \in M$$ with $$p = tp_M(m_1), q = tp_M(m_2)$$. Since both types contain $$P_n(x)$$, we see that both $$m_1$$ and $$m_2$$ lie in $$P_n^M$$, and so using the above we have $$p = tp_M(m_1) = tp_M(m_2) = q$$. Hence the type containing $$P_n(x)$$ is unique. (From there, it is relatively straightforward to show that this unique type $$p_n$$ is also principal, with principal formula $$P_n(x)$$)

Now if $$A \models T$$ with $$A' = A \setminus \bigcup_{n} P_n^A$$ non-empty, then any element $$c \in A'$$ defines a type different from the $$p_n$$, since $$A \not\models P_n(c)$$ for any n, i.e. $$P_n(x) \not\in tp_A(c)$$. By using automorphisms which swap two elements of $$A'$$, and a similar argument to the above, we can show that this type is unique, and furthermore it's non principal as it's not realised in all models of T (some models have $$A'$$ empty, for example $$M = ω \times ω$$ with $$P_n^M = ω \times \{n\}$$).

• why is there a single $M \models T$ which realises both p and q? Obviously every type is realised by some model, but why can it be the same model for both types here? Commented Nov 24, 2020 at 13:26
• There's a standard theorem that says that given a structure A and a set P of size κ of partial types for Th(A), then there is some structure B of size κ, extending A elementarily, that realises all types from P (note $κ \geq max\{ \vert{A}, \vert{L}\}$). Our theory is complete so Th(A) = T, so any model of T may be extended to one which realises p and q. Alternatively, you could first show that $tp_A(a)$ (with $a \in P_n^A$) is principal for any such model A, and then note that principal types are realised in all models. Commented Nov 24, 2020 at 13:58
• We can't have $A'$ empty, it's specified to have an infinite cardinality by the definition of T. Commented Nov 30, 2021 at 19:39

First, you should know that in general determining all the 1-types of a given theory is difficult and that there is no automatic recipe to do it.

One particularly useful way to simplify the task is to show that the given theory admits quantifier elimination, that is, that every first-order formula $$\phi(x)$$ is logically equivalent modulo $$T$$ to a quantifier-free formula $$\psi(x)$$. Then understanding a 1-type amounts to understanding the possible quantifier-free formulas that it contains.

Proving quantifier elimination can be done "by hand", by exhibiting a quantifier-free formula for every existential positive formula (i.e., a first-order formula of the form $$\exists \bar y(\bigwedge ...)$$ where inside the conjunction only atomic formulas appear). Perhaps you can already see how to do this for your example.

Another way to do it is to use properties of the models of $$T$$ (which is particularly useful when $$T$$ is $$\omega$$-categorical for example, since it only has one countable model). For example, if $$T$$ is $$\omega$$-categorical, it has quantifier elimination iff its unique countable model is ultrahomogeneous (i.e., every partial isomorphism between finitely generated substructures extends to an automorphism of the whole model). You can for example check that the unique countable model of every $$T_n$$ is indeed ultrahomogeneous. Even if $$T$$ is not $$\omega$$-categorical, this is enough for your purposes: every fo-formula only involves finitely many of the predicates $$P_i$$, therefore by quantifier-elimination for $$T_n$$, it is equivalent modulo $$T_n$$ to a quantifier-free formula. This equivalence is still true modulo $$T$$, therefore $$T$$ has quantifier elimination.