Article3093: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Keine Bearbeitungszusammenfassung |
Keine Bearbeitungszusammenfassung |
||
| Zeile 6: | Zeile 6: | ||
|Referiert=1 | |Referiert=1 | ||
|Title=Nested Sequents for Intermediate Logics: The Case of Gödel-Dummett Logics | |Title=Nested Sequents for Intermediate Logics: The Case of Gödel-Dummett Logics | ||
|To appear= | |To appear=0 | ||
|Year=2023 | |Year=2023 | ||
|Journal=Journal of Applied Non-Classical Logics | |Journal=Journal of Applied Non-Classical Logics | ||
|Volume=33 | |||
|Number=2 | |||
|Pages=121-164 | |||
}} | }} | ||
{{Publikation Details | {{Publikation Details | ||
|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 linearizing 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 generalize our nested sequents to include signatures (i.e. finite collections of variables) in the first-order cases, thus giving rise to a generalization of the usual nested sequent formalism. Our calculi exhibit favorable 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. | |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 linearizing 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 generalize our nested sequents to include signatures (i.e. finite collections of variables) in the first-order cases, thus giving rise to a generalization of the usual nested sequent formalism. Our calculi exhibit favorable 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. | ||
|DOI Name=10.1080/11663081.2023.2233346 | |||
|Projekt=DeciGUT | |Projekt=DeciGUT | ||
|Forschungsgruppe=Computational Logic | |Forschungsgruppe=Computational Logic | ||
Aktuelle Version vom 4. Oktober 2023, 12:10 Uhr
Tim Lyon
Nested Sequents for Intermediate Logics: The Case of Gödel-Dummett Logics
Journal of Applied Non-Classical Logics, 33(2):121-164, 2023
Nested Sequents for Intermediate Logics: The Case of Gödel-Dummett Logics
Journal of Applied Non-Classical Logics, 33(2):121-164, 2023
- KurzfassungAbstract
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 linearizing 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 generalize our nested sequents to include signatures (i.e. finite collections of variables) in the first-order cases, thus giving rise to a generalization of the usual nested sequent formalism. Our calculi exhibit favorable 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. - Projekt:Project: DeciGUT
- Forschungsgruppe:Research Group: Computational LogicComputational Logic
@article{L2023,
author = {Tim Lyon},
title = {Nested Sequents for Intermediate Logics: The Case of
G{\"{o}}del-Dummett Logics},
journal = {Journal of Applied Non-Classical Logics},
volume = {33},
number = {2},
year = {2023},
pages = {121-164},
doi = {10.1080/11663081.2023.2233346}
}
