Coalgebraic correspondence theory (bibtex)

by Lutz Schröder and Dirk Pattinson

Abstract:

We lay the foundations of a first-order correspondence theory for coalgebraic logics that makes the transition structure explicit in the first-order modelling. In particular, we prove a coalgebraic version of the van Benthem/Rosen theorem stating that both over arbitrary structures and over finite structures, coalgebraic modal logic is precisely the bisimulation invariant fragment of first-order logic.

Reference:

Lutz Schröder and Dirk Pattinson: Coalgebraic correspondence theory, In Luke Ong, ed.: Foundations of Software Science and Computation Structures (FoSSaCS 2010), Lecture Notes in Computer Science, vol. 6014, pp. 328–342, Springer, 2010. [preprint]

Bibtex Entry:

@InProceedings{SchroderPattinson10b,
  author = {Lutz Schr{\"o}der and Dirk Pattinson},
  title = {Coalgebraic correspondence theory},
  year = {2010},
  editor = {Luke Ong},
  booktitle = {Foundations of Software Science and Computation Structures (FoSSaCS 2010)},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6014},
  pages = {328--342},
  keywords = {coalgebra modal logic correspondence theory rosen van benthem theorem first order logic},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/correspondence.pdf"> [preprint] </a>},
  abstract = {  We lay the foundations of a first-order correspondence theory for
  coalgebraic logics that makes the transition structure explicit in the
  first-order modelling. In particular, we prove a coalgebraic version
  of the van Benthem/Rosen theorem stating that both over arbitrary
  structures and over finite structures, coalgebraic modal logic is
  precisely the bisimulation invariant fragment of first-order logic. 
},
}