离开 Beth 与 Craig 而生存：守护片段与两变量片段中的定义与插值
计算机科学中的逻辑
2021-04-20 v2
摘要
在具有 Craig 插值性质（CIP）的逻辑中，蕴含式的插值子的存在性由其有效性推出。在具有投射 Beth 可定义性性质（PBDP）的逻辑中，关系的显式定义的存在性由表达其隐式可定义性的公式的有效性推出。一阶逻辑的两变量片段 FO2 与守护片段 GF 均不满足 CIP 与 PBDP。我们证明，尽管如此，在这两个片段中插值子与显式定义的存在性都是可判定的。在 GF 中，这两个问题一般而言是 3ExpTime 完全的，若关系符号的元数被一个不小于 3 的常数 c 所界，则为 2ExpTime 完全。在 FO2 中，我们证明这两个问题的上界为 coN2ExpTime，下界为 2ExpTime。因此，对 GF 与 FO2 而言，插值子与显式定义的存在性是可判定的，但比有效性更难（在 FO2 情形下依据标准复杂度假设）。
引用
@article{arxiv.2007.01597,
title = {Living without Beth and Craig: Definitions and Interpolants in the Guarded and Two-Variable Fragments},
author = {Jean Christoph Jung and Frank Wolter},
journal= {arXiv preprint arXiv:2007.01597},
year = {2021}
}
备注
This is an updated version that also investigates the two-variable fragment of FO. The paper will appear in the proceedings of LICS 2021