Omitting types in logic of metric structures

TL;DR

This paper investigates the complexity of omitting types in the logic of metric structures, revealing that there is no simple criterion for determining type omissibility and providing examples of high logical complexity.

Contribution

It demonstrates the high complexity of omissibility in metric logic, including the existence of theories with types whose omissibility sets are complete analytical sets.

Findings

No simple test exists for type omissibility in metric structures.

Existence of theories with omissibility sets as complete $oldsymbol{ ext{Σ}}^1_2$ or $oldsymbol{ ext{Π}}^1_1$ sets.

Examples of types that are separately but not jointly omissible in models.

Abstract

This paper is about omitting types in logic of metric structures introduced by Ben Yaacov, Berenstein, Henson and Usvyatsov. While a complete type is omissible in some model of a countable complete theory if and only if it is not principal, this is not true for the incomplete types by a result of Ben Yaacov. We prove that there is no simple test for determining whether a type is omissible in a model of a theory $T$ in a countable language. More precisely, we find a theory in a countable language such that the set of types omissible in some of its models is a complete $\Sigma^1_2$ set and a complete theory in a countable language such that the set of types omissible in some of its models is a complete $\Pi^1_1$ set. Two more unexpected examples are given: (i) a complete theory $T$ and a countable set of types such that each of its finite sets is jointly omissible in a model of $T$, but the whole set is not and (ii) a complete theory and two types that are separately omissible, but not jointly omissible, in its models.