一句话:证明带原子可定义关系结构的可定义同构问题可判定,核心是参数消除。
本文研究可定义集合(等价于带原子集合)上的同构问题:给定两个可定义关系结构,判定它们之间是否存在可定义同构。作者在原子底层结构满足温和假设的前提下,证明该判定问题可判定。证明的核心结果是参数消除定理:只要存在带参数可定义的同构,就必然存在不带参数可定义的同构。该结果将可定义同构的存在性从带参数情形归约到无参数情形,从而为可定义关系结构的判定与分类提供了逻辑与模型论基础。评估为理论证明,未涉及实现或实验。
We investigate the isomorphism problem in the setting of definable sets (equivalent to sets with atoms): given two definable relational structures, are they related by a definable isomorphism? Under mild assumptions on the underlying structure of atoms, we prove decidability of the problem. The core result is parameter-elimination: existence of an isomorphism definable with parameters implies existence of an isomorphism definable without parameters.
@article{paperbot738,
title = {Definable isomorphism problem},
author = {Khadijeh Keshvardoost and Bartek Klin and Sławomir Lasota and Joanna Ochremiak and Szymon Toruńczyk},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 4},
year = {2019},
doi = {10.23638/lmcs-15(4:14)2019}
}