Nested Sequents for Intermediate Logics: The Case of Gödel-Dummett Logics

TL;DR

This work develops uniform, analytic nested-sequent calculi for six Gödel–Dummett/intermediate logics (I, GD, ND, CD, GN, GC) and their first-order extensions, introducing a novel linearity rule $(lin)$ and reachability rules with signatures to capture both non-constant and constant-domain semantics. The authors prove soundness, cut-free completeness, and height-preserving invertibility for the base calculi, and establish comprehensive hp-admissibility/invertibility results for a wide class of structural and FO rules, enabling counter-model extraction. They show syntactic cut-elimination for the intuitionistic and FO-less GD variants, while noting that full cut-elimination for the GD family remains open and may be resolved by stronger linearization $(lin^{+})$. The work also outlines extensions via DLC/DBC frame conditions and discusses potential unification with hypersequent approaches, aiming to cover a broad class of intermediate logics with analytic 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.

Figures (3)

• Figure 1: Inference rules for $\mathsf{N}_{\textrm{I}}$ and $\mathsf{N}_{\textrm{GD}}$.
• Figure 2: First-order inference rules. When $\mathsf{X}$ is $\textrm{ND}$, the rule is subject to the associated ND side condition, and when $\mathsf{X}$ is $\textrm{CD}$, the rule is subject to the associated CD side condition. The first-order calculi that employ such rules are specified in Definition \ref{['def:nns-ncd']}.
• Figure 3: Admissible rules. We let $\star \in \{\bullet,\circ\}$ in $(ctr^{\star})$ and note that $\Delta^{\circ}$ and $\Pi^{\bullet}$ represent multisets of output and input formulae, respectively, in the $(lwr)$ and $(lft)$ rules.

Theorems & Definitions (43)

• Definition 2.1: Frame, Model
• Definition 2.2: Semantic Clauses
• Proposition 2.3
• Definition 2.4: Axioms
• Theorem 2.5: Soundness and Completeness
• Definition 2.6: Frame, Model
• Definition 2.7: Semantic Clauses
• Proposition 2.8
• Definition 2.9: Axioms
• Theorem 2.10: Soundness and Completeness