We present nested sequent systems for propositional G\"odel-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\"odel-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.

翻译：本文基于直觉主义逻辑的嵌套演算，提出了命题哥德尔-杜梅特逻辑及其具有非常数域和常数域的一阶扩展的嵌套矢列式系统。为构建这些哥德尔-杜梅特逻辑的嵌套系统，我们引入了一种称为"线性规则"的新结构规则，该规则通过（自底向上）线性化给定嵌套矢列式中的分支结构进行操作。此外，我们演算体系的一个显著特点是包含了可达性规则，这是一类通过沿嵌套矢列式内特定路径传播数据和/或检查数据存在性来运作的特殊逻辑规则。此类规则要求我们将一阶情形下的嵌套矢列式推广至包含签名（即变量的有限集合），从而产生了对常规嵌套矢列式形式的推广。我们的演算展现出优良性质：所有逻辑规则均具有高度保持的可逆性，且大量结构规则与可达性规则具有（高度保持的）可容许性。我们证明了所有系统的可靠性与切消除完备性，并验证了直觉主义系统可实现语法切消除。最后，通过讨论可能的扩展与修改方案，我们提出了一系列可用于为大规模中间逻辑类构建切消除嵌套矢列式系统的结构规则。