Inception Display Calculi
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909052064235520 |
|---|---|
| author | De Domenico, Andrea Greco, Giuseppe Palmigiano, Alessandra |
| author_facet | De Domenico, Andrea Greco, Giuseppe Palmigiano, Alessandra |
| contents | Display calculi were introduced by Nuel Belnap in `Display logic' (1982) as a natural extension of Gentzen's sequent calculi, as a uniform and modular framework capable of encompassing broad classes of logics. In `Unified correspondence as a proof-theoretic tool', the properly displayable (D)LE-logics are syntactically characterized as the logics axiomatised by analytic inductive axioms for any signature. We extend the framework of proper display calculi for LE-logics to include axiomatic extensions with axioms that are inductive but not necessarily analytic inductive. This class of axioms covers and properly extends all Sahlqvist axioms. The present framework takes inspiration from Schroeder-Heister's calculus of Higher-Level Rules and captures the whole acyclic fragment of the substructural hierarchy when generalized to arbitrary signatures. We apply unified correspondence theory and the algorithm ALBA to uniformly generate analytic rules for the aforementioned axiomatic extensions. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_17175 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Inception Display Calculi De Domenico, Andrea Greco, Giuseppe Palmigiano, Alessandra Logic Display calculi were introduced by Nuel Belnap in `Display logic' (1982) as a natural extension of Gentzen's sequent calculi, as a uniform and modular framework capable of encompassing broad classes of logics. In `Unified correspondence as a proof-theoretic tool', the properly displayable (D)LE-logics are syntactically characterized as the logics axiomatised by analytic inductive axioms for any signature. We extend the framework of proper display calculi for LE-logics to include axiomatic extensions with axioms that are inductive but not necessarily analytic inductive. This class of axioms covers and properly extends all Sahlqvist axioms. The present framework takes inspiration from Schroeder-Heister's calculus of Higher-Level Rules and captures the whole acyclic fragment of the substructural hierarchy when generalized to arbitrary signatures. We apply unified correspondence theory and the algorithm ALBA to uniformly generate analytic rules for the aforementioned axiomatic extensions. |
| title | Inception Display Calculi |
| topic | Logic |
| url | https://arxiv.org/abs/2605.17175 |