一句话：提出余代数谓词逻辑，给出若干自然类的公理化与完备性，并建立基本序列演算的句法切消去。
本文从 C. C. Chang 一项被忽视的工作出发，提出一种一阶逻辑的推广：为任何可重铸为 Set-余代数的结构提供自然且通用的对应语言。作者研究若干自然类逻辑的公理化与完备性，并证明完全一般的完备性不可能；随后比较该语言与余代数混合逻辑以及针对特殊 Set-余代数类（关系结构、邻域框架、拓扑空间）的已有一阶方案的表达力。对于允许完备性的两个类（部分情形可超出），基本模型论构造与结果（尤其超积）仍然成立。最后给出一个基本序列系统，并建立句法切消去结果。
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.
@article{paperbot419,
title = {Model Theory and Proof Theory of Coalgebraic Predicate Logic},
author = {Tadeusz Litak and Dirk Pattinson and Katsuhiko Sano and Lutz Schröder},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 1},
year = {2018},
doi = {10.23638/lmcs-14(1:22)2018}
}