How different are types in the single-sorted case of first-order logic vs the many-sorted case

first-order-logicmodel-theorysoft-question

How different are types in the single-sorted case of first-order logic vs the many-sorted case?

Marker's Model Theory: An Introduction, which I'm reading, uses a single sort for FOL (or, perhaps more properly, doesn't have a notion of sorts). Alex Kruckman's lecture notes (types are covered beginning on page 46 by pdf and internal numbering) uses multi-sorted FOL.

For most concepts in model theory that I've encountered so far, the presence or absence of sorts does not seem to make a huge difference. Sorts can be paraphrased away by replacing each sort $S$ with a unary predicate $R$ and using bounded quantifiers (i.e. $\forall x : S \mathop. \varphi(x)$ is sent to $\forall x \mathop. R(x) \to \varphi(x)$ and similarly for $\exists$).

However, in the case of types, it seems like the presence or absence of sorts matters when we consider whether types are complete or not.

Single-sorted FOL can emulate multi-sorted FOL by considering wffs of the form.

$$ R_1(x_1) \cdots R_n(x_n) \land \varphi(x_1\cdots x_n) $$

However, performing this paraphrase and replacing the sorts with predicates has changed our notion of what completeness is.

More concretely, the wff below is not the translation of any multi-sorted wff because the "guard clause" is in the scope of the negation instead of outside it.

$$ \lnot(R_1(x_1) \cdots R_n(x_n) \land \varphi(x_1\cdots x_n)) $$

Single-sorted FOL is a special case of multi-sorted FOL, so I'm wondering whether the new expressiveness lets us talk about models with complete types that differ in material ways from the single-sorted case.

Best Answer

To make your question more precise, consider a structure $M$ in a multi-sorted language $L$, with sorts $(S_i)_{i\in I}$, and let $M'$ be a single-sorted with language $L'$ which consists of the same symbols as in $L$ and an additional predicate $P_i$ for each $S_i$, with the same underlying set as $M$, such that:

  • for each constant $c$, $c^{M'}=c^M$,
  • for each predicate $R\in L$, $R^{M'}=R^{M}$,
  • for each function symbol $f$ and $\bar a\in M'$ of the appropriate length, if $\bar a\in \operatorname{dom} f^M$, then $f^{M'}(\bar a)=f^M(\bar a)$, and if $\bar a\notin \operatorname{dom} f^M$, then $f^{M'}(\bar a)=a_0$ (the first element of $\bar a$).

Then for any $A\subseteq M=M'$, write $S^{M'}_{P_i}(A)$ for the (clopen) subset of $S^{M'}_x(A)$ consisting of types containing $P_i(x)$, and consider $S^M_{x_i}(A)$, where $x_i$ is a single variable of the sort $P_i$.

Then there is a natural homeomorphism between $S^{M'}_{P_i}(A)$ and $S^M_{x_i}(A)$ (coming from an isomorphism of the underlying Boolean algebras).

The translation of formulas from $M$ to $M'$ is straightforward: you change unrestricted quantifiers to restricted quantifiers. Let me just explain how you can reverse it. For example, if $R(x,y)$ is a relational symbol on $S_1\times S_2$ and $f(x,z)$ is a symbol for a binary function $S_3\times S_4\to S_3$, then the formula $$ S_1(x)\land \exists y\forall z (R(x,y)\lor f(x,z)\neq x) $$ can be translated as $$ \exists y_2 R(x_1,y_2), $$ we can completely forget the $f(x,z)\neq x$ part, since it is false by hypothesis (I'm assuming there are actually are multiple sorts in $M$).

Similarly, if $g$ is a symbol for an unary function $S_3\to S_1$, the formula $S_1(x)\land \exists y (R(x,y)\lor g(y)=x)$ translates into $\exists y_2\exists y_3 R(x_1,y_2)\lor g(y_3)=x_1$, while $S_1(x)\land \exists y (R(x,y)\land g(y)=x)$ is simply false (because $y$ cannot satisfy both $R(x,y)$ and $g(y)=x$ simultaneously, because the sorts don't match).

However, if $I$ is infinite, then $S_1^{M'}(A)\supsetneq \bigcup_{i\in I}S^{M'}_{P_i}(A)$.

An analogous fact is true for formulas in multiple variables.

In all, translating a many-sorted structure to one-sorted structure in this simple way is mostly faithful, as far as types are concerned, but it produces some artifacts. Typically, these artifacts can be safely disregarded, but there are other, more complicated constructions which allow us to, for example, preserve $\aleph_0$-categoricity.

Related Question