Seifan, Fatemeh ;
Schröder, Lutz ;
Pattinson, Dirk
Uniform Interpolation in Coalgebraic Modal Logic
Abstract
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, finitemonoidweighted logics, and coalition logic. We introduce a notion of onestep (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 onestep interpolation. Moreover, we identify preservation of finite surjective weak pullbacks as a sufficient, and in the monotone case necessary, condition for onestep interpolation. We thus prove or reprove uniform interpolation for most of the examples listed above.
BibTeX  Entry
@InProceedings{seifan_et_al:LIPIcs:2017:8041,
author = {Fatemeh Seifan and Lutz Schr{\"o}der and Dirk Pattinson},
title = {{Uniform Interpolation in Coalgebraic Modal Logic}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {21:121:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770330},
ISSN = {18688969},
year = {2017},
volume = {72},
editor = {Filippo Bonchi and Barbara K{\"o}nig},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/8041},
URN = {urn:nbn:de:0030drops80415},
doi = {10.4230/LIPIcs.CALCO.2017.21},
annote = {Keywords: modal logic, coalgebraic logic, uniform interpolation, preservation of weak pullbacks}
}
17.11.2017
Keywords: 

modal logic, coalgebraic logic, uniform interpolation, preservation of weak pullbacks 
Seminar: 

7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Issue date: 

2017 
Date of publication: 

17.11.2017 