TY - GEN

T1 - Uniform interpolation in coalgebraic modal logic

AU - Seifan, Fatemeh

AU - Schröder, Lutz

AU - Pattinson, Dirk

N1 - Publisher Copyright:
© Fatemeh Seifan, Lutz Schröder, and Dirk Pattinson; licensed under Creative Commons License CC-BY.

PY - 2017/11/1

Y1 - 2017/11/1

N2 - A logic has uniform interpolation if its formulas can be projected down to given subsignatures, preserving all logical consequences that do not mention the removed symbols; the weaker property of (Craig) interpolation allows the projected formula - the interpolant - to be different for each logical consequence of the original formula. These properties are of importance, e.g., in the modularization of logical theories. We study interpolation in the context of coalgebraic modal logics, i.e. modal logics axiomatized in rank 1, restricting for clarity to the case with finitely many modalities. Examples of such logics include the modal logics K and KD, neighbourhood logic and its monotone variant, finite-monoid-weighted logics, and coalition logic. We introduce a notion of one-step (uniform) interpolation, which refers only to a restricted logic without nesting of modalities, and show that a coalgebraic modal logic has uniform interpolation if it has one-step interpolation. Moreover, we identify preservation of finite surjective weak pullbacks as a sufficient, and in the monotone case necessary, condition for one-step interpolation. We thus prove or reprove uniform interpolation for most of the examples listed above.

AB - A logic has uniform interpolation if its formulas can be projected down to given subsignatures, preserving all logical consequences that do not mention the removed symbols; the weaker property of (Craig) interpolation allows the projected formula - the interpolant - to be different for each logical consequence of the original formula. These properties are of importance, e.g., in the modularization of logical theories. We study interpolation in the context of coalgebraic modal logics, i.e. modal logics axiomatized in rank 1, restricting for clarity to the case with finitely many modalities. Examples of such logics include the modal logics K and KD, neighbourhood logic and its monotone variant, finite-monoid-weighted logics, and coalition logic. We introduce a notion of one-step (uniform) interpolation, which refers only to a restricted logic without nesting of modalities, and show that a coalgebraic modal logic has uniform interpolation if it has one-step interpolation. Moreover, we identify preservation of finite surjective weak pullbacks as a sufficient, and in the monotone case necessary, condition for one-step interpolation. We thus prove or reprove uniform interpolation for most of the examples listed above.

KW - Coalgebraic modal logic

KW - Uniform interpolation

KW - Weak pullback

UR - http://www.scopus.com/inward/record.url?scp=85037090542&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.CALCO.2017.21

DO - 10.4230/LIPIcs.CALCO.2017.21

M3 - Conference contribution

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - 7th Conference on Algebra and Coalgebra in Computer Science, CALCO 2017

A2 - Konig, Barbara

A2 - Bonchi, Filippo

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

T2 - 7th Conference on Algebra and Coalgebra in Computer Science, CALCO 2017

Y2 - 14 June 2017 through 16 June 2017

ER -