Nested Sequents for Intermediate Logics: The Case of Gödel-Dummett Logics
Research output: Contribution to journal › Research article › Contributed › peer-review
Contributors
Abstract
We present nested sequent systems for propositional Gödel-Dummett logic and its first-order extensions with non-constant and constant domains, built atop nested calculi for intuitionistic logics. To obtain nested systems for these Gödel-Dummett logics, we introduce a new structural rule, called the linearity rule, which (bottom-up) operates by linearising branching structure in a given nested sequent. In addition, an interesting feature of our calculi is the inclusion of reachability rules, which are special logical rules that operate by propagating data and/or checking if data exists along certain paths within a nested sequent. Such rules require us to generalise our nested sequents to include signatures (i.e. finite collections of variables) in the first-order cases, thus giving rise to a generalisation of the usual nested sequent formalism. Our calculi exhibit favourable properties, admitting the height-preserving invertibility of every logical rule and the (height-preserving) admissibility of a large collection of structural and reachability rules. We prove all of our systems sound and cut-free complete, and show that syntactic cut-elimination obtains for the intuitionistic systems. We conclude the paper by discussing possible extensions and modifications, putting forth an array of structural rules that could be used to provide a sizable class of intermediate logics with cut-free nested sequent systems.
Details
| Original language | English |
|---|---|
| Pages (from-to) | 121-164 |
| Number of pages | 44 |
| Journal | Journal of applied non-classical logics |
| Volume | 33 |
| Issue number | 2 |
| Publication status | Published - 2023 |
| Peer-reviewed | Yes |
External IDs
| Scopus | 85165202291 |
|---|---|
| ORCID | /0000-0003-3214-0828/work/173054741 |