Completeness Results for Fibred Parchments Beyond the Prepositional Base

摘要

In [6] it was shown that fibring could be used to combine institutions presented as c-parchments, and several completeness preservation results were established. However, their scope of applicability was limited to propositional-based logics. Herein, we extend these results to a broader class of logics, possibly including variables, terms and quantifiers. On the way, we need to consider an enriched notion of proof-calculus that deals explicitly with the substitution provisos that often appear in schematic inference rules. For illustration of the concepts, constructions and results, we shall adopt modal first-order logic as a working example.