Logics of Statements in Context-Category Independent Basics

Abstract

Based on a formalization of open formulas as statements in context, the paper presents a freshly new and abstract view of logics and specification formalisms. Generalizing concepts like sets of generators in Group Theory, underlying graph of a sketch in Category Theory, sets of individual names in Description Logic and underlying graph-based structure of a software model in Software Engineering, we coin an abstract concept of context. We show how to define, in a category independent way, arbitrary first-order statements in arbitrary contexts. Examples of those statements are defining relations in Group Theory, commutative, limit and colimit diagrams in Category Theory, assertional axioms in Description Logic and constraints in Software Engineering. To validate the appropriateness of the newly proposed abstract framework, we prove that our category independent definitions and constructions give us a very broad spectrum of Institutions of Statements at hand. For any Institution of Statements, a specification (presentation) is given by a context together with a set of first-order statements in that context. Since many of our motivating examples are variants of sketches, we will simply use the term sketch for those specifications. We investigate exhaustively different kinds of arrows between sketches and their interrelations. To pave the way for a future development of category independent deduction calculi for sketches, we define arbitrary first-order sketch conditions and corresponding sketch constraints as a generalization of graph conditions and graph constraints, respectively. Sketch constraints are the crucial conceptual tool to describe and reason about the structure of sketches. We close the paper with some vital observations, insights and ideas related to future deduction calculi for sketches. Moreover, we outline that our universal method to define sketch constraints enables us to establish and to work with conceptual hierarchies of sketches.

Keywords

• first-order logic
• abstract model theory
• institution
• sketch
• algebraic specification
• description logic