Nested sequents for intermediate logics: the case of Gödel-Dummett logics

Journal of Applied Non-Classical Logics 33 (2):121-164 (2023)
  Copy   BIBTEX


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.



    Upload a copy of this work     Papers currently archived: 91,202

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Prefixed tableaus and nested sequents.Melvin Fitting - 2012 - Annals of Pure and Applied Logic 163 (3):291 - 313.
Maehara-style modal nested calculi.Roman Kuznets & Lutz Straßburger - 2019 - Archive for Mathematical Logic 58 (3-4):359-385.
Proof analysis in intermediate logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1):71-92.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.
Intermediate Logics and Visser's Rules.Rosalie Iemhoff - 2005 - Notre Dame Journal of Formal Logic 46 (1):65-81.
On the rules of intermediate logics.Rosalie Iemhoff - 2006 - Archive for Mathematical Logic 45 (5):581-599.
Reflexive Intermediate First-Order Logics.Nathan C. Carter - 2008 - Notre Dame Journal of Formal Logic 49 (1):75-95.
On intermediate justification logics.Nicholas Pischke - forthcoming - Logic Journal of the IGPL.


Added to PP

8 (#1,243,760)

6 months
4 (#678,769)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Tim Lyon
Technische Universität Dresden

Citations of this work

No citations found.

Add more citations

References found in this work

Modal Logic.Yde Venema, Alexander Chagrov & Michael Zakharyaschev - 2000 - Philosophical Review 109 (2):286.
Untersuchungen über das logische Schließen. I.Gerhard Gentzen - 1935 - Mathematische Zeitschrift 35:176–210.
Zum intuitionistischen aussagenkalkül.K. Gödel - 1932 - Anzeiger der Akademie der Wissenschaften in Wien 69:65--66.
Untersuchungen über das logische Schließen. II.Gerhard Gentzen - 1935 - Mathematische Zeitschrift 39:405–431.
Proof analysis in intermediate logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1):71-92.

View all 30 references / Add more references