Coalgebraic predicate logic: Equipollence results and proof theory

The recently introduced Coalgebraic Predicate Logic (CPL) provides a general first-order syntax together with extra modal-like operators that are interpreted in a coalgebraic setting. The universality of the coalgebraic approach allows us to instantiate the framework to a wide variety of situations, including probabilistic logic, coalition logic or the logic of neighbourhood frames. The last case generalises a logical setup proposed by C.C. Chang in early 1970's. We provide further evidence of the naturality of this framework. We identify syntactically the fragments of CPL corresponding to extended modal formalisms and show that the full CPL is equipollent with coalgebraic hybrid logic with the downarrow binder and the universal modality. Furthermore, we initiate the study of structural proof theory for CPL by providing a sequent calculus and a cut-elimination result.