度量结构逻辑中的类型省略

本文讨论由 Ben Yaacov、Berenstein、Henson 和 Usvyatsov 引入的度量结构逻辑中的类型省略问题。虽然完整类型在可数完整理论的某个模型中可省略当且仅当它不是主类型，但根据 Ben Yaacov 的结果，这对于不完整类型并不成立。我们证明，不存在简单的测试来确定某个类型在可数语言中理论 $T$ 的模型中是否可省略。更确切地说，我们找到了一个可数语言中的理论，使得在其某些模型中可省略的类型集合是一个完整的 $\Sigma^1_2$ 集合；以及一个可数语言中的完整理论，使得在其某些模型中可省略的类型集合是一个完整的 $\Pi^1_1$ 集合。还给出了两个更出乎意料的例子：(i) 一个完整理论 $T$ 和一个可数类型集合，使得其每个有限子集可在 $T$ 的某个模型中联合省略，但整个集合却不能；(ii) 一个完整理论和两个类型，它们在其模型中分别可省略，但不能联合省略。