[Back]

A. Lolic, M. Baaz:
"Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic";
Talk: LPAR-22: 22nd. International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Äthiopien; 11-16-2018 - 11-21-2018; in: "EPiC Series in Computing", EasyChair Publications, 56 (2018), ISSN: 2398-7340.

The Craig interpolation property is one of the most fundamental properties of logics. It states that whenever A ⊃ B is valid in a logic, one can find a formula I in the common language of A and B, such that A ⊃ I and I ⊃ B are valid. The formula I is called the interpolant of A ⊃ B. Interpolation was proved for classical first-order logic by Craig and for intuitionistic first-order logic by Schütte.

Lyndon interpolation is a strengthening of the interpolation property in the sense that propositional variables or predicate symbols are only allowed to occur positively (negatively) in the interpolant if they occur positively (negatively) on both sides of the implication. Lyndon interpolation for classical logic has been established by Lyndon.

Little was known about interpolation properties of intermediate logics until Maksimova solved the propositional interpolation problem showing that exactly 7 of these logics have the propositional interpolation property. Her work is based on the algebraic analysis of the logic in question. On first-order level, algebraic semantics are not as well understood and therefore first-order interpolation properties are notoriously hard to determine, even for logics where propositional interpolation is more of less obvious. Hence, it remained an open question which of these 7 logics admit first-order interpolation, among them first-order Gödel logic. Moreover, except of classical and intuitionistic logic, most logics do not seem to admit a Maehara style lemma w.r.t. their established calculi. This applies to e.g. all hypersequent calculi.

In this paper we extend Lyndon interpolation to the prenex ⊃ prenex fragment of Gödel logic using the proof of Lyndon interpolation for propositional Gödel logic from a recent paper of Lellmann and Kuznets. Note that first-order Lyndon interpolation is difficult to establish for first-order logics as most proof-theoretic methods fail.