Strongly Complete Logics for Coalgebras
Coalgebras for a functor model different types of transition systems in a uniform way. This paper focuses on a uniform account of finitary logics for set-based coalgebras. In particular, a general construction of a logic from an arbitrary set-functor is given and proven to be strongly complete under...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2012-09-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1231/pdf |
| _version_ | 1797268693484306432 |
|---|---|
| author | Alexander Kurz Jiri Rosicky |
| author_facet | Alexander Kurz Jiri Rosicky |
| author_sort | Alexander Kurz |
| collection | DOAJ |
| description | Coalgebras for a functor model different types of transition systems in a
uniform way. This paper focuses on a uniform account of finitary logics for
set-based coalgebras. In particular, a general construction of a logic from an
arbitrary set-functor is given and proven to be strongly complete under
additional assumptions. We proceed in three parts. Part I argues that sifted
colimit preserving functors are those functors that preserve universal
algebraic structure. Our main theorem here states that a functor preserves
sifted colimits if and only if it has a finitary presentation by operations and
equations. Moreover, the presentation of the category of algebras for the
functor is obtained compositionally from the presentations of the underlying
category and of the functor. Part II investigates algebras for a functor over
ind-completions and extends the theorem of J{\'o}nsson and Tarski on canonical
extensions of Boolean algebras with operators to this setting. Part III shows,
based on Part I, how to associate a finitary logic to any finite-sets
preserving functor T. Based on Part II we prove the logic to be strongly
complete under a reasonable condition on T. |
| first_indexed | 2024-04-25T01:36:32Z |
| format | Article |
| id | doaj.art-5bc4fd0194154db08200605fd8a8a35b |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:32Z |
| publishDate | 2012-09-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-5bc4fd0194154db08200605fd8a8a35b2024-03-08T09:28:00ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742012-09-01Volume 8, Issue 310.2168/LMCS-8(3:14)20121231Strongly Complete Logics for CoalgebrasAlexander Kurzhttps://orcid.org/0000-0002-8685-5207Jiri RosickyCoalgebras for a functor model different types of transition systems in a uniform way. This paper focuses on a uniform account of finitary logics for set-based coalgebras. In particular, a general construction of a logic from an arbitrary set-functor is given and proven to be strongly complete under additional assumptions. We proceed in three parts. Part I argues that sifted colimit preserving functors are those functors that preserve universal algebraic structure. Our main theorem here states that a functor preserves sifted colimits if and only if it has a finitary presentation by operations and equations. Moreover, the presentation of the category of algebras for the functor is obtained compositionally from the presentations of the underlying category and of the functor. Part II investigates algebras for a functor over ind-completions and extends the theorem of J{\'o}nsson and Tarski on canonical extensions of Boolean algebras with operators to this setting. Part III shows, based on Part I, how to associate a finitary logic to any finite-sets preserving functor T. Based on Part II we prove the logic to be strongly complete under a reasonable condition on T.https://lmcs.episciences.org/1231/pdfcomputer science - logic in computer sciencemathematics - category theoryf.3.2f.4.1 |
| spellingShingle | Alexander Kurz Jiri Rosicky Strongly Complete Logics for Coalgebras Logical Methods in Computer Science computer science - logic in computer science mathematics - category theory f.3.2 f.4.1 |
| title | Strongly Complete Logics for Coalgebras |
| title_full | Strongly Complete Logics for Coalgebras |
| title_fullStr | Strongly Complete Logics for Coalgebras |
| title_full_unstemmed | Strongly Complete Logics for Coalgebras |
| title_short | Strongly Complete Logics for Coalgebras |
| title_sort | strongly complete logics for coalgebras |
| topic | computer science - logic in computer science mathematics - category theory f.3.2 f.4.1 |
| url | https://lmcs.episciences.org/1231/pdf |
| work_keys_str_mv | AT alexanderkurz stronglycompletelogicsforcoalgebras AT jirirosicky stronglycompletelogicsforcoalgebras |