2020/07/03 by Jean Christoph Jung, Jung, Jean Christoph, Frank Wolter +1
Computer Science · #03B70 #Advanced Algebra and Logic #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2007.01597
openalex publication_date 2020/07/03 · openalex created_date 2022/07/26 · openalex updated_date 2026/07/28
In logics with the Craig interpolation property (CIP) the existence of an\ninterpolant for an implication follows from the validity of the implication. In\nlogics with the projective Beth definability property (PBDP), the existence of\nan explicit definition of a relation follows from the validity of a formula\nexpressing its implicit definability. The two-variable fragment, FO2, and the\nguarded fragment, GF, of first-order logic both fail to have the CIP and the\nPBDP. We show that nevertheless in both fragments the existence of interpolants\nand explicit definitions is decidable. In GF, both problems are\n3ExpTime-complete in general, and 2ExpTime-complete if the arity of relation\nsymbols is bounded by a constant c not smaller than 3. In FO2, we prove a\ncoN2ExpTime upper bound and a 2ExpTime lower bound for both problems. Thus,\nboth for GF and FO2 existence of interpolants and explicit definitions are\ndecidable but harder than validity (in case of FO2 under standard complexity\nassumptions).\n