Towards a uniform presentation of logical systems by indexed categories and adjoint situations

摘要

Logical Systems are paramount to almost every subject in computer science. This vast number of application areas had a deep influence on us and thus on how we perceive what a formal specification of a logical system should be. Lawvere's (1963, Proc. NatlAcad. Sci., 50, 869-872; 2006, Theor. Appl. Categor., 16, 1-16) essential idea is that the fundamental relationship between syntax and semantics can be precisely formulated by adjoint functors. In this work, we show that Institutions from Goguen and Burstall (1992, J. ACM, 39, 95-146) and Entailment Systems from Meseguer (1989, 'General logics' in Logic Colloquium' 87, 275-329) are in its essence, a family of local adjoint situations between the syntactical and semantical aspects underlying these systems. These abstractions are named Indexed Frames. Also, from a categorical perspective, Tarski's (1930, Fundamentale Begriffe der Methodologie der Deduktiven Wissenschaften Ⅰ. Monatshefte fur Mathematik und Physik, 37, 361-404) consequence operator can be formalized as Indexed Closure Operators, a construction that maps each language to the corresponding co-monad. Finally, in the framework of preorder categories, both concepts, Indexed Frames and Indexed Closure Operators are equivalent.