Living without Beth and Craig: Definitions and Interpolants in the Guarded and Two-Variable Fragments



Jung, Jean Christoph and Wolter, Frank
(2020) Living without Beth and Craig: Definitions and Interpolants in the Guarded and Two-Variable Fragments. In: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2021-6-29 - 2021-7-2.

[img] Text
lics21authoraccepted.pdf - Author Accepted Manuscript

Download (377kB) | Preview

Abstract

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).

Item Type: Conference or Workshop Item (Unspecified)
Additional Information: This is an updated version that also investigates the two-variable fragment of FO. The paper will appear in the proceedings of LICS 2021
Uncontrolled Keywords: cs.LO, cs.LO, 03B70
Divisions: Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User: Symplectic Admin
Date Deposited: 09 Jul 2021 07:16
Last Modified: 18 Jan 2023 21:37
DOI: 10.1109/lics52264.2021.9470585
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3127791