Document

# Uniform Interpolation in Coalgebraic Modal Logic

## File

LIPIcs.CALCO.2017.21.pdf
• Filesize: 0.51 MB
• 16 pages

## Cite As

Fatemeh Seifan, Lutz Schröder, and Dirk Pattinson. Uniform Interpolation in Coalgebraic Modal Logic. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CALCO.2017.21

## 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, 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.
##### Keywords
• modal logic
• coalgebraic logic
• uniform interpolation
• preservation of weak pullbacks

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. Jiří Adámek, Horst Herrlich, and George Strecker. Abstract and Concrete Categories. Wiley Interscience, 1990. Republished in Reprints in Theor. Appl. Cat. 17 (2006).
2. Michael Barr. Terminal coalgebras in well-founded set theory. Theoret. Comput. Sci., 114:299-315, 1993.
3. Marta Bílková. Uniform interpolation and propositional quantifiers in modal logics. Stud. Log., 85:1-31, 2007.
4. Brian Chellas. Modal Logic. Cambridge University Press, 1980.
5. William Craig. Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log., 22:250-268, 1957.
6. Giovanna D'Agostino and Marco Hollenberg. Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski. J. Symb. Log., 65:310-332, 2000.
7. Stéphane Demri and Denis Lugiez. Complexity of modal logics with Presburger constraints. J. Appl. Log., 8:233-252, 2010.
8. Dov Gabbay. Craig’s interpolation theorem for modal logics. In Conference in Mathematical Logic—London’70, volume 255 of LNM, pages 111-127. Springer, 1972.
9. Dov Gabbay. Craig interpolation theorem for intuitionistic logic and extensions Part III. J. Symb. Log., 42:269-271, 1977.
10. Silvio Ghilardi. An algebraic theory of normal forms. Ann. Pure Appl. Log., 71:189-245, 1995.
11. Silvio Ghilardi and Marek Zawadowski. Undefinability of propositional quantifiers in the modal system S4. Stud. Log., 55:259-271, 1995.
12. H. Peter Gumm and Tobias Schröder. Coalgebraic structure from weak limit preserving functors. In Coalgebraic Methods in Computer Science, CMCS 2000, volume 33 of ENTCS, pages 111-131. Elsevier, 2000.
13. H. Peter Gumm and Tobias Schröder. Monoid-labeled transition systems. In Coalgebraic Methods in Computer Science, CMCS 2001, volume 44 of ENTCS, pages 185-204. Elsevier, 2001.
14. Helle Hansen and Clemens Kupke. A coalgebraic perspective on monotone modal logic. In Coalgebraic Methods in Computer Science, CMCS 2004, volume 106 of ENTCS, pages 121-143. Elsevier, 2004.
15. Helle Hansen, Clemens Kupke, and Eric Pacuit. Neighbourhood structures: Bisimilarity and basic model theory. Log. Meth. Comput. Sci., 5, 2009.
16. Leon Henkin. An extension of the Craig-Lyndon interpolation theorem. J. Symb. Log., 28:201-216, 1963.
17. Dexter Kozen. Results on the propositional μ-calculus. Theor. Comput. Sci., 27:333-354, 1983.
18. Alexander Kurz and Raul Leal. Modalities in the Stone age: A comparison of coalgebraic logics. Theor. Comput. Sci., 430:88-116, 2012. URL: http://dx.doi.org/10.1016/j.tcs.2012.03.027,
19. Carsten Lutz and Frank Wolter. Foundations for uniform interpolation and forgetting in expressive description logics. In International Joint Conference on Artificial Intelligence, IJCAI 2011, pages 989-995. IJCAI/AAAI, 2011.
20. Johannes Marti. Relation liftings in coalgebraic modal logic. Master’s thesis, Universiteit van Amsterdam, 2011.
21. Johannes Marti, Fatemeh Seifan, and Yde Venema. Uniform interpolation for coalgebraic fixpoint logic. In Algebra and Coalgebra in Computer Science, CALCO 2015, volume 35 of LIPIcs, pages 238-252. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
22. Johannes Marti and Yde Venema. Lax extensions of coalgebra functors and their logic. J. Comput. Syst. Sci., 81:880-900, 2015.
23. Larry Moss. Coalgebraic logic. Ann. Pure Appl. Logic, 96:277-317, 1999.
24. Rob Myers, Dirk Pattinson, and Lutz Schröder. Coalgebraic hybrid logic. In Foundations of Software Science and Computation Structures, FoSSaCS 2009, volume 5504 of LNCS, pages 137-151. Springer, 2009.
25. Dirk Pattinson. Coalgebraic modal logic: Soundness, completeness and decidability of local consequence. Theoret. Comput. Sci., 309:177-193, 2003.
26. Dirk Pattinson. Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Log., 45:19-33, 2004.
27. Dirk Pattinson. The logic of exact covers: Completeness and uniform interpolation. In Logic in Computer Science, LICS 2013, pages 418-427. IEEE, 2013.
28. Dirk Pattinson and Lutz Schröder. Cut elimination in coalgebraic logics. Inf. Comput., 208:1447-1468, 2010.
29. Marc Pauly. A modal logic for coalitional power in games. J. Log. Comput., 12:149-166, 2002.
30. Andrew Pitts. On an interpretation of second order quantification in first order intuitionistic propositional logic. J. Symb. Log., 57:33-52, 1992.
31. Jan Rutten. Universal coalgebra: A theory of systems. Theor. Comput. Sci., 249:3-80, 2000.
32. Luigi Santocanale and Yde Venema. Uniform interpolation for monotone modal logic. In Advances in Modal Logic, AiML 2010, pages 350-370. College Publications, 2010.
33. Lutz Schröder. A finite model construction for coalgebraic modal logic. J. Log. Algebr. Prog., 73:97-110, 2007.
34. Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theor. Comput. Sci., 390:230-247, 2008.
35. Lutz Schröder and Dirk Pattinson. Strong completeness of coalgebraic modal logics. In Symposium on Theoretical Aspects of Computer Science, STACS 2009, volume 3 of LIPIcs, pages 673-684. Schloss Dagstuhl - Leibniz-Center of Informatics, 2009.
36. Lutz Schröder and Dirk Pattinson. Rank-1 modal logics are coalgebraic. J. Log. Comput., 20(5):1113-1147, 2010.
37. Daniele Turi. Functorial operational semantics and its denotational dual. PhD thesis, Vrije Universiteit, Amsterdam, 1996.
38. Albert Visser. Uniform interpolation and layered bisimulation. In Gödel ’96 (Brno, 1996), volume 6 of Lect. Notes Log., pages 139-164. Springer, 1996.
39. Kewen Wang, Zhe Wang, Rodney Topor, Jeff Pan, and Grigoris Antoniou. Concept and role forgetting in ALC-ontologies. In The Semantic Web, ISWC 2009, volume 5823 of LNCS. Springer, 2009.
X

Feedback for Dagstuhl Publishing