I know that unsorted FOL is equivalently expressive to finitely-many-sorted FOL. The only semantic criteria placed on the sorts in the many-sorted FOL are that every object in the domain is in one of the sorts, and the sorts are disjoint subsets of the domain. All the statements in unsorted FOL can be trivially mapped to statements in just one of the sorts of the many-sorted logic, in both the finite & infinite case, and both should have all the same models.

To translate from N-sorted FOL to unsorted FOL, we can add unary relation symbols $S_1, ..., S_N$ and then we add axioms that state that they are disjoint and cover the whole set:

$\forall x, S_1(x) \vee ... \vee S_N(x)$

and for every pair of sort-symbols $S, S'$, the axiom:

$\neg(\exists x, S(x) \wedge S'(x))$

For every constant symbol c meant to be interpreted as being in sort S, we add the axiom:


Then anywhere you do a quantification over a sort S in N-sorted logic like

$\forall x : S, P(x)$

we can translate this to an equivalent unsorted FOL statement in our new theory:

$\forall x, S(x) \implies P(x)$

To attempt to translate from infinitely-many-sorted FOL to unsorted FOL, we can add unary relation symbols $S_1, S_2,...$ for each sort, and then add the axioms

$\forall x, \phi(x)$

and for every pair of sort-symbols $S, S'$, the axiom

$\neg(\exists x, S(x) \wedge S'(x))$

and for every constant symbol c meant to be interpreted as being in sort S, the axiom:


Where $\phi(x)$ stands for an FOL formula expressing that the object $x$ is in at least one of the sorts. We'll call this theory $T$. The formula $\phi(x)$ must be semantically equivalent to the following infinite disjunction of statements:

$S_1(x) \vee S_2(x) \vee ...$

The negation of $\forall x, \phi(x)$ must therefore be equivalent to the statement:

$\exists x, \neg S_1(x) \wedge \neg S_2(x) \wedge ...$

Skolemizing, we can add a fresh constant symbol $\sigma$ and create an equisatisfiable formula:

$\neg S_1(\sigma) \wedge \neg S_2(\sigma) \wedge ... $

This is an infinite conjunction of finite first-order statements, and thus represents a first-order theory, call it $\neg T$. Because we assumed $T$ was a first-order theory, then $T \cup \neg T$ is also a first-order theory.

$T \cup \neg T$ is not satisfiable, because $\neg T$ semantically contradicts $\forall x, \phi(x)$, in the case where $x = \sigma$. By the compactness theorem, there must exist some finite subset of $T \cup \neg T$ which is not satisfiable.

However, it's straightforward to see that every finite subset is satisfiable: choose a structure where the objects are the constant symbols $c$ such that the axiom $S(c)$ is included in your subset, for some sort symbol $S$, and map every sort symbol $S$ to the unary relation that holds for an object $c$ iff the axiom $S(c)$ is included in your subset; choose your structure such that for the interpretations of any two sort symbols $S, S'$ are disjoint sets of the domain; if for every axiom $S(c)$ included in your subset, the axiom $\neg S(\sigma)$ is also included in your subset, then choose another sort symbol $S'$ such that the axiom $\neg S'(\sigma)$ is not included in your subset, add a new object in the domain to represent $\sigma$ and map $S'$ to a unary relation on the domain that only contains $\sigma$; otherwise, there exists an axiom $S(c)$ in your subset such that the axiom $\neg S(\sigma)$ is not included in your subset, in which case interpret $\sigma$ as the same object that $c$ is interpreted as. Whatever finite subset of the theory is chosen, there should exist a structure defined in this fashion which models that subset.

This contradicts the compactness theorem. Therefore, $T \cup \neg T$ could not actually be a first-order theory. But since $\phi(x)$ is the only thing in the theory which hasn't been expressed directly with a first-order sentence, it follows that $\phi(x)$ must not be expressible in unsorted FOL.

Is my reasoning correct here? If so does this imply that unsorted FOL is not capable of simulating infinitely-many-sorted FOL, as a consequence of the compactness theorem, and that the latter is therefore more expressive?

  • 1
    $\begingroup$ This seems correct. However, there might be other possible translations, especially if the theory allows encoding the natural numbers in any way.. $\endgroup$ – Berci Jun 25 '18 at 1:33

If we had infinitely many sorts $\tau_1, \tau_2, \ldots$, why not add an infinite collection of unary predicates $S_1, S_2, \ldots$, add axioms for all $i \not = j$: $$ (\exists x) S_i(x) \\ S_i(x) \to \lnot S_j(x) $$ along with the axioms for constants of particular sorts, and replace each quantifier $(\exists x^{\tau_i}) \ldots$ with $(\exists x)[S_i(x) \land \ldots]$ and similarly for $(\forall x^{\tau_i})$. For notation, say that this interpretation takes a sentence $\phi$ in infinitely many sorts to $\phi^*$ in one sort with new unary relations.

This seems to interpret any model with infinitely many sorts into a model of the expanded theory with only one sort. Conversely, a model in the new language and expanded theory might have some elements that do not satisfy $S_i$ for any $i$, but if we discard those then the resulting model immediately leads to an equivalent model in infinitely many sorts. The elements that are not in any sort are irrelevant to sentences of the form $\phi^*$, because the quantifiers in $\phi^*$ are explicitly tied to particular sorts.

Letting $T^*$ be the interpretation and expansion of a theory $T$, in this way we still have that $T$ has a model with infinitely many sorts if and only if $T^*$ has a model with one sort.

  • 1
    $\begingroup$ It is worth noting that this one-sorted theory can be chosen in a canonical way: just declare that any relation symbol is false when applied to elements from incorrect sorts, and any function symbol applied to incorrect sorts is just the projection onto the first coordinate. The only significant difference is that (as far as I know) the resulting theory is never categorical: there can be any number of the "unsorted" elements. There are ways to work around this, see doi.org/10.4064/fm214-3-5 . $\endgroup$ – tomasz Jun 25 '18 at 13:27
  • $\begingroup$ @tomasz: thanks. I was imagining it would be easier to switch to a relation language, to avoid having to add even more axioms that ensure that the functions take inputs of the correct sort to outputs of the correct sort. There may be other axioms needed for relations as well, as you point out. Thanks also for the reference. $\endgroup$ – Carl Mummert Jun 25 '18 at 13:30
  • $\begingroup$ Thanks! Can you let me know if this is an accurate summary? 1) that infinite disjunction actually isn't expressible due to compactness; 2) by dropping the axiom that every object has a sort, we can have a first-order theory that preserves disjointness of sorts, but allows the existence of unsorted objects; 3) despite this "limitation", they can be seen to be equivalent in the sense that if T has a model M then T* has a model M* and M is isomorphic to a (designated!) subset of M* (the axiomatically-sorted objects of M*), and vice versa, for an appropriate definition of isomorphism $\endgroup$ – stoopkid Jun 25 '18 at 15:50
  • $\begingroup$ Right, that is the situation. $\endgroup$ – Carl Mummert Jun 25 '18 at 16:01
  • 1
    $\begingroup$ It's slightly stronger than that in that models of $T^\ast$ are characterized precisely by models of $T$ and a cardinal corresponding to the number of unsorted elements. In principle something much wilder could happen with the 'unintended' models. $\endgroup$ – James Hanson Jun 25 '18 at 21:36

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.