Lyndon interpolation theorem of instantial neighborhood logic - constructively via a sequent calculus

摘要

Instantial neighborhood logic (INL) is classical propositional logic enriched by a two-sorted operator square. In a neighborhood model, a formula like square(alpha(1), .. alpha(j); alpha(0)) (for an arbitrary natural number j) means that, the current point has a neighborhood in which alpha(0) universally holds and none of alpha(1), ..., alpha(j) universally fails. This paper offers to INL: (1) a cut-free sequent calculus, and (2) a constructive proof of its Lyndon interpolation theorem. (C) 2019 Elsevier B.V. All rights reserved.