Decidability and complexity of fibred logics without shared connectives∗

Fibring is a powerful mechanism for combining logics, and an essential tool for designing and understanding complex logical systems. Abstract results about the semantics and proof-theory of fibred logics have been extensively developed, including general preservation results for metalogical properties like soundness and (sufficient conditions for) completeness. Decidability, however, a key ingredient for the automated support of the fibred logic, has not deserved similar attention. In this paper, we extend the preliminary results obtained in [28] regarding theoremhood, and address the problem of deciding the consequence relation of fibred logics, assuming that the logics do not share connectives. Namely, under this assumption, we provide a thorough characterization of the mixed patterns of reasoning that can occur in the fibred logic, and use it to obtain the first general decidability preservation result for fibring. The complexity of the decision procedure we obtain is also analyzed.