Categorial Fibring of Logics with Terms and Binding Operators.
Amı́lcar Sernadas, Cristina Sernadas, Carlos Caleiro, Till Mossakowski · 1998
Categorial characterizations are given of both unconstrained and constrained fibring of Hibert calculi and interpretation systems for languages with variables, terms, variable binding operators and modal like operators. Some preliminary transference results are established. A brief comparison with model theoretic parchments is included. 1 Introduction Combination of logics has been attracting much attention [BdR97]. Among the most interesting mechanisms, fibring deserves close attention [Gab96a, Gab96b, Gab98]. Herein, we extend the work in [SSC98] to logics with variables, terms and binding operators. For example, one can obtain first order temporal logic by fibring first order logic and propositional temporal logic. Our main goal is to provide a categorial characterization of both proof and model theoretic fibring of such logics. Following the approach proposed in [SSC97a, SSC97b, SSC98] we define free unconstrained fibring as a coproduct and constrained fibring (by sharing of symbo...