Structured theory presentations and logic representations (Q1326777): Difference between revisions

The paper proposes an adequate language of structured theory presentations, focusing on ``lifting'' the structured presentations from the level of the object logic to the level of the metalogic and, particularly, on the conditions under which proofs in the metalogic for lifted structured presentations soundly represent proofs for structured presentations in the object logic. These ideas are made explicit in the context of Logical Framework (LF) [\textit{R. Harper, F. Honsell} and \textit{G. Plotkin}, J. Assoc. Comput. Mach. 40, 143-184 (1993; Zbl 0778.03004)]as metalogic, a three-level typed \(\lambda\)-calculus with \(\pi\)-types, and a suitable meta-language for defining formal systems. LF provides the basic machinery not only for ``putting together theories'' through structured theory presentations, but also allows for ``putting together logics'' through structured logic presentations. LF opens the possibility of using several logical systems at the same time: e.g., the encoding of S4 modal logic as a combination of the truth and validity consequence relations of S4, the parametrization of Hoare logic of assertions, or adding a connective to a logic. Section 2 introduces a general definition of a logical system as a family of consequence relations indexed by signatures that satisfy a certain uniformity condition with respect to change of signature. The sorts of consequence relations that are considered to encoding in LF are limited to one-sided consequence relations which are closed under weakening, permutation, contraction, and cut, and satisfy the compactness property. Section 3 defines structured theory presentations in an arbitrary logical system, the natural proof system induced by the structure of the presentations being discussed in Section 4. Generalizing the LF approach, Section 5 defines the notion of a representation of one logical system in another and considers the problem of ``lifting'' a structured presentation along a representation of one logical system in another. The notion of proof is defined by the conditions of the representation and by the restrictions imposed by the metalogic. Section 6 introduces the LF metalogic as a logical system and defines the notion of logic presentation as an LF signature together with a representation of the object logic in the logical system by the representation. Section 7 returns to the problem of proof in structured theory presentations for the specific setting of logics encoded in LF, while Section 8 explores the colimit construction as a tool for building logics in a structured way. Finally, Sections 9 and 10 discuss related work and future research directions.