Lyndon interpolation holds for the prenex \(\supset\) prenex fragment of Gödel logic. (English) Zbl 1416.03011

Baaz, Matthias; Lolic, Anela

Barthe, Gilles (ed.) et al., LPAR-22. 22nd international conference on logic for programming, artificial intelligence and reasoning, Awassa, Ethiopia, November 17–21, 2018. Selected papers. Manchester: EasyChair. EPiC Ser. Comput. 57, 95-110 (2018).

Summary: First-order interpolation properties are notoriously hard to determine, even for logics where propositional interpolation is more or less obvious. One of the most prominent examples is first-order Gödel logic. 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. Note that Lyndon interpolation is difficult to establish for first-order logics as most proof-theoretic methods fail. In this paper, we provide general derivability conditions for a first-order logic to admit Lyndon interpolation for the prenex \(\supset\) prenex fragment and apply the arguments to the prenex \(\supset\) prenex fragment of first-order Gödel logic.
For the entire collection see [Zbl 1407.68021].

MSC:

03B50	Many-valued logic
03C40	Interpolation, preservation, definability

Keywords:

Gödel logics; Herbrand expansions; interpolation; Lyndon interpolation; Skolemization