一句话：证明守卫片段和二变量片段中插值与显式定义的存在性可判定，并刻画其复杂度。
Craig 插值性质与 projective Beth 可定义性质在二变量片段 FO2 和守卫片段 GF 中均不成立，因此不能从蕴含有效性或隐式可定义性直接推出插值项/显式定义的存在。本文转而研究这两个片段中判断插值项和显式定义是否存在这一问题。结果显示，在 GF 和 FO2 中两者仍是可判定的。GF 中两个问题一般为 3EXPTIME-complete，当关系元数被常数 c≥3 界定时为 2EXPTIME-complete。FO2 中两个问题分别有 CON2EXPTIME 上界和 2EXPTIME 下界。因此存在性判定虽可判定，但比有效性验证更难（在 FO2 的标准复杂度假设下）。
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 ≥ 3. In FO2, we prove a CON2EXPTIME upper bound and a 2EXPTIME lower bound for both problems. Thus, both for GF and FO2existence of interpolants and explicit definitions are decidable but harder than validity (in case of FO2under standard complexity assumptions).
@inproceedings{paperbot6165,
title = {Living without Beth and Craig: Definitions and Interpolants in the Guarded and Two-Variable Fragments},
author = {Jean Christoph Jung and Frank Wolter},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470585}
}