没有贝丝和克雷格的生活：被保护和双变量片段中的定义和插值
Living without Beth and Craig: Definitions and Interpolants in the Guarded and Two-Variable Fragments
摘要：
在具有Craig插值性质（CIP）的逻辑中，蕴涵的插值的存在性来自于蕴涵的有效性。在具有投射贝斯可定义性性质（projective Beth definability property，PBDP）的逻辑中，一个关系的显式定义的存在性是由一个表示其隐式可定义性的公式的有效性所决定的。一阶逻辑的双变量片段FO 2和保护片段GF都不具有CIP和PBDP。我们表明，然而，在这两个片段的存在插值和明确的定义是可判定的。在GF中，这两个问题一般都是3ExpTime-完全的，如果关系符号的数量由一个不小于3的常数c限定，则是2 ExpTime-完全的。在FO 2中，我们证明了这两个问题的coN 2 ExpTime上界和2 ExpTime下界。因此，对于GF和FO 2，插值和显式定义的存在性都是可判定的，但比有效性更难（在标准复杂性假设下的FO 2情况下）。
英文摘要：
In logics with the Craig interpolation property (CIP) the existence of an interpolant for an implication follows from the validity of the implication. In logics with the projective Beth definability property (PBDP), the existence of an explicit definition of a relation follows from the validity of a formula expressing its implicit definability. The two-variable fragment, FO2, and the guarded fragment, GF, of first-order logic both fail to have the CIP and the PBDP. We show that nevertheless in both fragments the existence of interpolants and explicit definitions is decidable. In GF, both problems are 3ExpTime-complete in general, and 2ExpTime-complete if the arity of relation symbols is bounded by a constant c not smaller than 3. In FO2, we prove a coN2ExpTime upper bound and a 2ExpTime lower bound for both problems. Thus, both for GF and FO2 existence of interpolants and explicit definitions are decidable but harder than validity (in case of FO2 under standard complexity assumptions).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
