Tadeusz Litak ; Dirk Pattinson ; Katsuhiko Sano ; Lutz Schröder - Model Theory and Proof Theory of Coalgebraic Predicate Logic

lmcs:2645 - Logical Methods in Computer Science, March 20, 2018, Volume 14, Issue 1 - https://doi.org/10.23638/LMCS-14(1:22)2018
Model Theory and Proof Theory of Coalgebraic Predicate LogicArticle

Authors: Tadeusz Litak ORCID; Dirk Pattinson ; Katsuhiko Sano ORCID; Lutz Schröder ORCID

    We propose a generalization of first-order logic originating in a neglected work by C.C. Chang: a natural and generic correspondence language for any types of structures which can be recast as Set-coalgebras. We discuss axiomatization and completeness results for several natural classes of such logics. Moreover, we show that an entirely general completeness result is not possible. We study the expressive power of our language, both in comparison with coalgebraic hybrid logics and with existing first-order proposals for special classes of Set-coalgebras (apart from relational structures, also neighbourhood frames and topological spaces). Basic model-theoretic constructions and results, in particular ultraproducts, obtain for the two classes that allow completeness---and in some cases beyond that. Finally, we discuss a basic sequent system, for which we establish a syntactic cut-elimination result.


    Volume: Volume 14, Issue 1
    Published on: March 20, 2018
    Accepted on: March 7, 2018
    Submitted on: January 16, 2017
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1685 times.
    This article's PDF has been downloaded 738 times.