利用圆柱模态代数对时态和拓扑有限变量片段的代数分析

我们研究了为每个序数$\alpha$定义的所谓拓扑圆柱代数和时态圆柱代数。前者是维度为$\alpha$的圆柱代数，扩展了由$\alpha$索引的$\sf S4$模态算子。可表示拓扑代数的语义是由其基上定义的拓扑相对于内部运算诱导的。时态圆柱代数是通过模态算子$F$（未来）和$P$（过去）扩展的圆柱代数，实现了谓词时态逻辑的代数化。我们证明，对于有限维$n>2$的时态和拓扑圆柱代数，包含且涵盖维度$n$的可表示代数簇的无限多个簇都不是原子规范的。我们证明，任何包含具有弱 neat 嵌入性质的完全可表示代数类的类都不是初等的。从这两个结果中，我们对谓词拓扑逻辑和时态逻辑的有限变量片段得出了关于省略类型的相同结论。我们证明，当变量数$>2$时，局限于此类片段的省略类型定理的通常版本即使在我们大幅扩大允许在可数原子理论中省略单个非主类型（即由余原子构成的非主类型）的模型类时，也会严重失效。