Logics of Statements in Context-Category Independent Basics

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 D...

Full description

Bibliographic Details
Main Author: Uwe Wolter
Format: Article
Language:English
Published: MDPI AG 2022-03-01
Series:Mathematics
Subjects:
Online Access:https://www.mdpi.com/2227-7390/10/7/1085
_version_ 1827623109022187520
author Uwe Wolter
author_facet Uwe Wolter
author_sort Uwe Wolter
collection DOAJ
description 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.
first_indexed 2024-03-09T11:38:47Z
format Article
id doaj.art-004b84e7ff584eb6943fefce0c6f9d13
institution Directory Open Access Journal
issn 2227-7390
language English
last_indexed 2024-03-09T11:38:47Z
publishDate 2022-03-01
publisher MDPI AG
record_format Article
series Mathematics
spelling doaj.art-004b84e7ff584eb6943fefce0c6f9d132023-11-30T23:36:57ZengMDPI AGMathematics2227-73902022-03-01107108510.3390/math10071085Logics of Statements in Context-Category Independent BasicsUwe Wolter0Department of Informatics, University of Bergen, 5020 Bergen, NorwayBased 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.https://www.mdpi.com/2227-7390/10/7/1085first-order logicabstract model theoryinstitutionsketchalgebraic specificationdescription logic
spellingShingle Uwe Wolter
Logics of Statements in Context-Category Independent Basics
Mathematics
first-order logic
abstract model theory
institution
sketch
algebraic specification
description logic
title Logics of Statements in Context-Category Independent Basics
title_full Logics of Statements in Context-Category Independent Basics
title_fullStr Logics of Statements in Context-Category Independent Basics
title_full_unstemmed Logics of Statements in Context-Category Independent Basics
title_short Logics of Statements in Context-Category Independent Basics
title_sort logics of statements in context category independent basics
topic first-order logic
abstract model theory
institution
sketch
algebraic specification
description logic
url https://www.mdpi.com/2227-7390/10/7/1085
work_keys_str_mv AT uwewolter logicsofstatementsincontextcategoryindependentbasics