带受限量词与有限枚举的三类型集合论片段的判定问题
计算机科学中的逻辑
2015-06-05 v1
摘要
我们解决了三类型集合论片段（记为 ）的满足性问题，该片段允许对个体与集合变量进行受限形式的量化，并允许对个体变量使用有限枚举算子 ；我们通过证明其具有小模型性质，即 的任何可满足公式 都有一个有限模型，其大小仅依赖于 本身的长度。若干集合论构造可由 -公式表达，例如幂集算子的某些变体以及无序笛卡尔积。特别地，关于无序笛卡尔积，我们证明当使用有限枚举来表示该构造时，所得公式比不使用此类项所能构造的公式指数级更短。
引用
@article{arxiv.1506.01476,
title = {The decision problem for a three-sorted fragment of set theory with restricted quantification and finite enumerations},
author = {Domenico Cantone and Marianna Nicolosi-Asmundo},
journal= {arXiv preprint arXiv:1506.01476},
year = {2015}
}