| Publication type: |
Article in Collection |
| Author: |
A. Sernadas, C. Sernadas, C. Caleiro, T. Mossakowski |
| Editor: |
D. Gabbay, Rijke, M. de |
| Title: |
Categorical Fibring of Logics with Terms and Binding Operators |
| Book / Collection title: |
Frontiers of Combining Systems 2 |
| Page(s): |
295 – 316 |
| Series: |
Studies in Logic and Computation |
| Year published: |
2000 |
| Publisher: |
Research Studies Press |
| Abstract: |
The problem of combining logics has been attracting much attention. Among the most interesting mechanisms, fibring deserves close attention. Herein, we extend our earlier work to logics with variables, terms and binding operators. For example, in order to 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 earlier work, we define free unconstrained fibring as a coproduct and constrained (by sharing of symbols) fibring as a cocartesian lifting in the appropriate categories (of Hilbert calculi and interpretation systems). Furthermore, we establish that soundness is preserved by the construction and that completeness is not always preserved. The extension of the approach to logics with variables, terms and binding operators is by no means trivial, at both proof and model theoretic levels. At the level of the Hilbert calculi, we need an abstract solution to deal with the meta requirements in inference rules related to binding (such as, term t is free for variable x in formula F) having in mind that inference rules should be preserved by morphisms of Hilbert calculi. We are able to do so by dealing with binding on the terminal signature where binding operators of the same kind are confused. Indeed, we consider two quite different kinds of binding operators: those that bind variables (like quantifiers and lambda abstraction) and those that bind flexible symbols (like modal operators). At the level of the interpretation systems, the main problem was to cope with the different semantics of rigid and flexible symbols at the envisaged degree of generality. In this paper, we assume that values of variables are rigid. This assumption makes the semantics simpler but is the key reason for not achieving preservation of completeness. Indeed, by fibring first order logic and propositional temporal logic we obtain a logic where the Barcan formulae are valid but are not obtained from the axioms. The proposed categorial approach was essential in finding a suitably abstract treatment of binding. Furthermore, for the simpler case of propositional logics, the categorial imperative was very helpful in fine tuning the envisaged semantics of fibring with explicit models and satisfaction and in establishing the technical lemmata for preservation of soundness. We compare our semantics to model-theoretic parchments that are also defined in a categorial way. |
| PostScript Version: |
http://www.informatik.uni-bremen.de/~till/papers/98-SSCM-fiblog2.ps |
| Status: |
Reviewed |
| Last updated: |
04. 05. 2004 |
|
 |
