Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations

Lyon, Tim S.

doi:10.4230/LIPIcs.CSL.2025.42

Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations

Tim S. Lyon

Technische Universität Dresden, Germany

Abstract

We demonstrate the inter-translatability of proofs between the most prominent sequent-based formalisms for Gödel-Löb provability logic. In particular, we consider Sambin and Valentini’s sequent system $\mathsf{GL_{seq}}$ , Shamkanov’s non-wellfounded and cyclic sequent systems $\mathsf{GL_{\infty}}$ and $\mathsf{GL_{circ}}$ , Poggiolesi’s tree-hypersequent system $\mathsf{CSGL}$ , and Negri’s labeled sequent system $\mathsf{G3GL}$ . Shamkanov provided proof-theoretic correspondences between $\mathsf{GL_{seq}}$ , $\mathsf{GL_{\infty}}$ , and $\mathsf{GL_{circ}}$ , and Goré and Ramanayake showed how to transform proofs between $\mathsf{CSGL}$ and $\mathsf{G3GL}$ , however, the exact nature of proof transformations between the former three systems and the latter two systems has remained an open problem. We solve this open problem by showing how to restructure tree-hypersequent proofs into an end-active form and introduce a novel linearization technique that transforms such proofs into linear nested sequent proofs. As a result, we obtain a new proof-theoretic tool for extracting linear nested sequent systems from tree-hypersequent systems, which yields the first cut-free linear nested sequent calculus $\mathsf{LNGL}$ for Gödel-Löb provability logic. We show how to transform proofs in $\mathsf{LNGL}$ into a certain normal form, where proofs repeat in stages of modal and local rule applications, and which are translatable into $\mathsf{GL_{seq}}$ and $\mathsf{G3GL}$ proofs. These new syntactic transformations, together with those mentioned above, establish full proof-theoretic correspondences between $\mathsf{GL_{seq}}$ , $\mathsf{GL_{\infty}}$ , $\mathsf{GL_{circ}}$ , $\mathsf{CSGL}$ , $\mathsf{G3GL}$ , and $\mathsf{LNGL}$ while also giving (to the best of the author’s knowledge) the first constructive proof mappings between structural (viz. labeled, tree-hypersequent, and linear nested sequent) systems and a cyclic sequent system.

Keywords and phrases:

Cyclic proof, Gödel-Löb logic, Labeled sequent, Linear nested sequent, Modal logic, Non-wellfounded proof, Proof theory, Proof transformation, Tree-hypersequent

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Proof theory ; Theory of computation

\rightarrow

Modal and temporal logics ; Theory of computation

\rightarrow

Constructive mathematics

Funding:

Work supported by European Research Council, Consolidator Grant DeciGUT (771779).

DOI:

10.4230/LIPIcs.CSL.2025.42

Event:

33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Editors:

Jörg Endrullis and Sylvain Schmitz

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Provability logics are a class of modal logics where the $\Box$ operator is read as “it is provable that” in some arithmetical theory. One of the most prominent provability logics is Gödel-Löb logic ( $\mathsf{GL}$ ), which arose out of the work of Löb, who formulated a set of conditions on the provability predicate of Peano Arithmetic (PA). The logic $\mathsf{GL}$ can be axiomatized as an extension of the basic modal logic $\mathsf{K}$ by the single axiom $\Box(\Box\varphi\rightarrow\varphi)\rightarrow\Box\varphi$ , called Löb’s axiom. It is well-known that the axioms of $\mathsf{GL}$ are sound and complete relative to transitive and conversely-wellfounded relational models [38]. In a landmark result, Solovay [41] remarkably showed that $\mathsf{GL}$ is complete for PA’s provability logic, i.e., $\mathsf{GL}$ proves everything that PA can prove about its own provability predicate.

The logic $\mathsf{GL}$ enjoys a rich structural proof theory, possessing a number of cut-free sequent-style systems. Sequent systems in the style of Gentzen were originally provided by Sambin and Valentini in the early 1980s [36, 37]; see also Avron [2]. (NB. In this work, we take a Gentzen system to be a proof system whose rules operate over Gentzen sequents, i.e., expressions of the form $\varphi_{1},\ldots,\varphi_{n}\vdash\psi_{1},\ldots,\psi_{k}$ such that $\varphi_{i}$ and $\psi_{j}$ are logical formulae.) Since then, a handful of alternative systems have been introduced, each of which either generalizes the structure of sequents or generalizes the notion of proof. The labeled sequent system $\mathsf{G3GL}$ was provided by Negri [31] and uses labeled sequents in proofs, which are binary graphs whose nodes are Gentzen sequents. In a similar vein, the tree-hypersequent system $\mathsf{CSGL}$ was provided by Poggiolesi [35] and uses tree-hypersequents in proofs, which are trees whose nodes are Gentzen sequents. The use of (types of) graphs of Gentzen sequents in proofs (as in $\mathsf{G3GL}$ and $\mathsf{CSGL}$ ) allows for the systems to possess properties beyond those of the original Gentzen systems [36, 37]. For example, both $\mathsf{G3GL}$ and $\mathsf{CSGL}$ enjoy invertibility of all rules, rules are symmetric (i.e., for each logical connective, there is at least one rule that introduces it in the antecedent and at least one rule that introduces it in the consequent of the rule’s conclusion), and the close connection between the syntax of such sequents and $\mathsf{GL}$ ’s relational semantics makes such systems suitable for counter-model extraction.

Rather than generalizing the structure of sequents, Shamkanov [39] showed that one could obtain alternative cut-free sequent systems for $\mathsf{GL}$ by generalizing the structure of proofs. In particular, by taking the sequent calculus for the modal logic $\mathsf{K4}$ and allowing for non-wellfounded proofs, one obtains a non-wellfounded sequent system $\mathsf{GL_{\infty}}$ for $\mathsf{GL}$ . Non-wellfounded proofs were introduced to capture (co)inductive reasoning, and are potentially infinite trees of sequents such that (1) every parent node is the conclusion of a rule with its children the corresponding premises and (2) infinite branches satisfy a certain progress condition, which ensures soundness (cf. [5, 11, 32, 39]). For $\mathsf{GL}$ , non-wellfounded proofs correspond to regular trees (i.e., only contain finitely many distinct sub-trees), which means such proofs can be “folded” into finite trees of sequents such that leaves are “linked” to internal nodes of the tree, giving rise to cyclic proofs (cf. [1, 3, 4, 10]). Shamkanov [39] additionally showed that one could obtain a cut-free cyclic sequent system $\mathsf{GL_{circ}}$ for $\mathsf{GL}$ by allowing cyclic proofs in $\mathsf{K4}$ ’s sequent calculus, which was then used to provide the first syntactic proof of the Lyndon interpolation property for $\mathsf{GL}$ .

Due to the diversity in $\mathsf{GL}$ ’s proof theory, it is natural to wonder about the relationships between the various systems that have been introduced. Typically, proof systems are related by means of proof transformations, which are functions that map proofs from one calculus into another, are sensitive to the structure of the input proof, and operate syntactically by permuting rules, replacing rules, or adding/deleting sequent structure in the input proof to yield the output proof. Studying proof transformations between sequent systems is a beneficial enterprise as it lets one transfer results from one system to another, thus alleviating the need of independent proofs in each system (e.g., [9, 15]). Moreover, one can measure the relative sizes or certain characteristics of proofs, giving insight into which systems are better suited for specific (automated) reasoning tasks, and letting one “toogle” between differing formalisms when one is better suited for a task than another (e.g., [24, 23]).

Indeed, the question of the relationship between $\mathsf{G3GL}$ and $\mathsf{CSGL}$ was asked by Poggiolesi [35] and answered in full by Goré and Ramanayake [15], who provided constructive mappings of proofs between the two systems. Similarly, Shamkanov [39] provided syntactic mappings of proofs between the systems $\mathsf{GL_{\infty}}$ and $\mathsf{GL_{circ}}$ , and the Gentzen system $\mathsf{GL_{seq}}$ (an equivalent reformulation of Sambin and Valentini’s systems [36, 37]). Nevertheless, the inter-translatability of proofs between the former two structural sequent systems ( $\mathsf{G3GL}$ and $\mathsf{CSGL}$ ) and the latter three sequent systems ( $\mathsf{GL_{seq}}$ , $\mathsf{GL_{\infty}}$ , and $\mathsf{GL_{circ}}$ ) has yet to be identified, and presents a non-trivial open problem that we solve in this paper. Thus, our first contribution in this paper is to “complete the picture” and establish complete correspondences between the above five mentioned sequent systems by means of syntactic proof transformations.

There is an inherent difficulty in transforming proofs that use structural sequents (e.g., labeled sequents or tree-hypersequents) into proofs that use Gentzen sequents. This is due to the fact that structural sequents are (types of) graphs of Gentzen sequents, and thus, possess a more complicated structure that must be properly “shed” during proof transformations [23, 26]. To overcome this difficulty and define proof transformations from $\mathsf{G3GL}$ and $\mathsf{CSGL}$ to $\mathsf{GL_{seq}}$ , we rely on three techniques: first, we show how to restructure proofs in $\mathsf{CSGL}$ so that they are end-active (cf. [21]), meaning rules only affect data at leaves or parents of leaves in tree-hypersequents. Second, we introduce a novel linearization technique, whereby we show how to shed the tree structure of tree-hypersequents in end-active proofs, yielding a proof consisting solely of linear nested sequents [21], i.e., lines whose nodes are Gentzen sequents. Linear nested sequents were introduced as an alternative (albeit equivalent) formalism to 2-sequents [29, 30] that allows for sequent systems with complexity-optimal proof-search that also retain fundamental admissibility and invertibility properties [21]. The presented linearization technique is new and shows how to extract linear nested sequent systems from tree-hypersequent systems, serving as the second contribution of this paper. We conjecture that this method can be generalized and applied in other settings to provide new linear nested sequent systems for modal and related logics. The technique also yields the first (cut-free) linear nested sequent calculus for $\mathsf{GL}$ , which we dub $\mathsf{LNGL}$ , and which is the third contribution of this paper. Last, we show that proofs in $\mathsf{LNGL}$ can be put into a specific normal form that repeats in stages of modal and local rules. Such proofs are translatable into $\mathsf{GL_{seq}}$ proofs, which are translatable into $\mathsf{G3GL}$ proofs, thus establishing purely syntactic proof transformations between the most prominent sequent systems for $\mathsf{GL}$ . These proof transformations and systemic correspondences are summarized in Figure 1 below.

Outline of Paper.

In Section 2, we recall the language, semantics, and axioms of Gödel-Löb logic. In Section 3, we discuss Negri’s labeled system $\mathsf{G3GL}$ [31], Poggiolesi’s tree-hypersequent system $\mathsf{CSGL}$ [35], and Goré and Ramanayake correspondence result for the two systems [15]. In Section 4, we show how to put proofs in $\mathsf{CSGL}$ into an end-active form (Theorem 18) and specify our novel linearization method (Theorem 19), which yields the new linear nested sequent system $\mathsf{LNGL}$ for $\mathsf{GL}$ . In Section 5, we recall the sequent calculus $\mathsf{GL_{seq}}$ due to Sambin and Valentini [36, 37], Shamkanov’s non-wellfounded system $\mathsf{GL_{\infty}}$ and cyclic system $\mathsf{GL_{circ}}$ , as well as Shamkanov’s correspondence result for the aforementioned three systems [39]. We then show how to transform proofs in $\mathsf{LNGL}$ into proofs in $\mathsf{GL_{seq}}$ (Theorem 24) and how to transform proofs in $\mathsf{GL_{seq}}$ into proofs in $\mathsf{G3GL}$ (Theorem 25). This establishes a six-way correspondence between the systems $\mathsf{G3GL}$ , $\mathsf{CSGL}$ , $\mathsf{GL_{seq}}$ , $\mathsf{GL_{\infty}}$ , $\mathsf{GL_{circ}}$ , and $\mathsf{LNGL}$ . Last, in Section 6, we conclude and discuss future work.

Name	Type of System
$\mathsf{G3GL}$	Labeled Sequent System
$\mathsf{CSGL}$	Tree-Hypersequent System
$\mathsf{LNGL}$	Linear Nested Sequent System
$\mathsf{GL_{seq}}$	Gentzen System
$\mathsf{GL_{\infty}}$	Non-Wellfounded Sequent System
$\mathsf{GL_{circ}}$	Cyclic Sequent System

Figure 1: Proof transformations and correspondences between sequent systems for

\mathsf{GL}

.

2 Gödel-Löb Provability Logic

We let $\mathsf{Prop}:=\{p,q,r,\ldots\}$ be a countable set of propositional atoms and define the language $\mathcal{L}$ to be the set of all formulae generated via the following grammar in BNF:

\varphi::=p\ |\ \neg\varphi\ |\ \varphi\lor\varphi\ |\ \Box\varphi

where $p$ ranges over $\mathsf{Prop}$ . We use $\varphi$ , $\psi$ , $\chi$ , $\ldots$ to denote formulae in $\mathcal{L}$ and define $\varphi\land\psi:=\neg(\neg\varphi\lor\neg\psi)$ and $\varphi\rightarrow\psi:=\neg\varphi\lor\psi$ as usual.

Definition 1 (Model).

We define a model to be a tuple $M=(W,R,V)$ such that

$\blacksquare$

$W$ is a non-empty set of worlds $w$ , $u$ , $v$ , $\ldots$ (occasionally annotated);
$\blacksquare$

$R\subseteq W\times W$ is transitive and conversely-wellfounded;¹¹1We note that $R$ is conversely-wellfounded iff it does not contain any infinite ascending $R$ -chains.
$\blacksquare$

$V:\mathsf{Prop}\mapsto 2^{W}$ is a valuation function.

Definition 2 (Semantic Clauses).

We define the satisfaction of a formula $\varphi$ in a model $M$ at world $w$ , written $M,w\models\varphi$ , recursively as follows:

$\blacksquare$

$M,w\models p$ iff $w\in V(p)$ ;
$\blacksquare$

$M,w\models\neg\varphi$ iff $M,w\not\models\varphi$ ;
$\blacksquare$

$M,w\models\varphi\lor\psi$ iff $M,w\models\varphi$ or $M,w\models\psi$ ;
$\blacksquare$

$M,w\models\Box\varphi$ iff $\forall u\in W$ , if $(w,u)\in R$ , then $M,u\models\varphi$ ;
$\blacksquare$

$M\models\varphi$ iff $\forall w\in W$ , $M,w\models\varphi$ .

We write $\models\varphi$ and say that $\varphi$ is valid iff for all models $M$ , $M\models\varphi$ . Gödel-Löb logic ( $\mathsf{GL}$ ) is defined to be the set $\mathsf{GL}\subset\mathcal{L}$ of all valid formulae.

As shown by Segerberg [38], the logic $\mathsf{GL}$ can be axiomatized by extending the axioms of the modal logic $\mathsf{K}$ with Löb’s axiom $\Box(\Box\varphi\rightarrow\varphi)\rightarrow\Box\varphi$ .

3 Labeled and Tree Sequent Systems

In this section, we review the labeled sequent calculus $\mathsf{G3GL}$ by Negri [31] and its correspondence (proven by Goré and Ramanayake [15]) with a notational variant of Poggiolesi’s tree-hypersequent system for $\mathsf{GL}$ [35]. Labeled sequents are binary graphs of traditional Gentzen sequents, which encode the relational semantics of a logic directly in the syntax of sequents. The formalism of labeled sequents has been extensively studied with the inception of the formalism dating back to the work of Kanger [18] and achieving its modern form in the work of Simpson [40]. It has been shown that labeled sequent systems can capture sizable and diverse classes of logics in a cut-free manner while exhibiting fundamental properties such as the admissibility of various structural rules and the invertibility of rules [40, 43, 31].

By contrast, tree-hypersequents, which are more traditionally known as nested sequents, are trees of Gentzen sequents. The formalism was introduced independently by Kashima [19] and Bull [7] with further influential works provided by Brünnler [6] and Poggiolesi [34, 35]. Such systems arose out of a call for cut-free sequent-style systems for logics not known to possess a cut-free Gentzen system, such as the tense logic $\mathsf{K_{t}}$ and the modal logic $\mathsf{S5}$ . Like labeled sequents, tree-hypersequent systems exhibit fundamental admissibility and invertibility properties, having been defined for large classes of various logics such as tense logics [14], intuitionistic modal logics [42, 25], and first-order non-classical logics [13, 27].

As observed by Goré and Ramanayake [15], restricting labeled sequents to be trees, rather than more general, binary graphs (which may be disconnected or include cycles), yields labeled tree sequents (cf. [17]), which are a notational variant of tree-hypersequents/nested sequents. Via this observation, the authors established bi-directional proof transformations between Negri’s labeled sequent calculus and Poggiolesi’s tree-hypersequent calculus for $\mathsf{GL}$ . Proof theoretic correspondences between labeled and nested systems for various other logics have been established in recent years as well; e.g., for tense logics [9], first-order intuitionistic logics [23, 22], and intuitionistic modal logics [25]. Recently, it was proven in a general setting that correspondences between labeled and nested systems are a product of two underlying proof transformation techniques, structural rule elimination and introduction, and that (Horn) labeled and nested systems tend to come in pairs, being dual to one another [28].

Reducing Negri’s labeled sequent system to one that uses trees, as opposed to binary graphs, is the first step in establishing syntactic correspondences between the various sequent systems for $\mathsf{GL}$ . As shown in the sequel, we will systematically reduce the structure of sequents in proofs: first, going from binary graphs of Gentzen sequents to trees of Gentzen sequents (this section), then from trees of Gentzen sequents to lines of Gentzen sequents (Section 4), and last from lines of Gentzen sequents to Gentzen sequents themselves, which are easily embedded in labeled sequent proofs, completing the circuit of correspondences (Section 5). This yields correspondences between the most widely regarded sequent systems for $\mathsf{GL}$ , as depicted in Figure 1.

Figure 2: Labeled Sequent Calculus

\mathsf{G3GL}

for

\mathsf{GL}

. The

\Box\mathsf{R}

rule is subject to a side condition

{\dagger}

, namely, the rule is applicable only if the label

y

is fresh.

3.1 Labeled Sequents

We let $\mathrm{Lab}=\{x,y,z,\ldots\}$ be a countably infinite set of labels, define a relational atom to be an expression of the form $x R y$ with $x,y\in\mathrm{Lab}$ , and define a labeled formula to be an expression of the form $x:\varphi$ such that $x\in\mathrm{Lab}$ and $\varphi\in\mathcal{L}$ . We use upper-case Greek letters $\Gamma,\Delta,\Sigma,\ldots$ to denote finite multisets of labeled formulae. For a set $\mathcal{R}$ of relational atoms and multiset $\Gamma$ of labeled formulae, we let $\mathrm{Lab}(\mathcal{R})$ , $\mathrm{Lab}(\Gamma)$ , and $\mathrm{Lab}(\mathcal{R},\Gamma)$ be the sets of all labels occurring therein. For a multiset $\Gamma$ of labeled formulae, we define the multiset $\Gamma(x):=\{\varphi\ |\ x:\varphi\in\Gamma\}$ , for a multiset of formulae $\Gamma:=\varphi_{1},\ldots,\varphi_{n}$ , we define $x:\Gamma:=x:\varphi_{1},\ldots,x:\varphi_{n}$ , and for multisets $\Gamma$ and $\Delta$ of labeled formulae, we let $\Gamma,\Delta$ denote the multiset union of the two. We define a labeled sequent to be an expression of the form $\mathcal{R},\Gamma\vdash\Delta$ with $\mathcal{R}$ a set of relational atoms and $\Gamma,\Delta$ a multiset of labeled formulae. Given a labeled sequent $\mathcal{R},\Gamma\vdash\Delta$ , we refer to $\mathcal{R},\Gamma$ as the antecedent and $\Delta$ as the consequent. Below, we clarify the interpretation of labeled sequents by explaining their evaluation over models.

Definition 3 (Labeled Sequent Semantics).

Let $M=(W,R,V)$ be a model. We define an $M$ -assignment to be a function $\mu\colon\mathrm{Lab}\to W$ . A labeled sequent $\mathcal{R},\Gamma\vdash\Delta$ is satisfied on $M$ with $M$ -assignment $\mu$ iff if for all $xRy\in\mathcal{R}$ and $x:\varphi\in\Gamma$ , $(\mu(x),\mu(y))\in R$ and $M,\mu(x)\models\varphi$ , then there exists a $y:\psi\in\Delta$ such that $M,\mu(y)\models\psi$ . A labeled sequent is defined to be valid iff it is satisfied on all models $M$ with all $M$ -assignments; a labeled sequent is defined to be invalid otherwise.

Figure 3: Admissible rules.

Negri’s labeled sequent calculus $\mathsf{G3GL}$ (adapted to our signature) is shown in Figure 2. The labeled calculus consists of three initial rules $\mathsf{id_{1}}$ , $\mathsf{id_{2}}$ , and $\mathsf{ir}$ . We refer to the conclusion of an initial rule as a initial sequent. The $\mathsf{tr}$ rule is a structural rule that bottom-up adds transitive edges to labeled sequents, and the remaining rules form pairs of left and right logical rules, introducing complex logical formulae into either the antecedent or consequent of the rule’s conclusion. We note that the $\Box\mathsf{R}$ rule is subject to a side condition, namely, the label $y$ must be fresh in any application of the rule, i.e., the label $y$ is forbidden to occur in the conclusion. We refer to the distinguished formulae in the conclusion (premises) of a rule as the principal formulae (auxiliary formulae, respectively). For example, $x:\Box\varphi$ is principal in $\Box\mathsf{R}$ and $xRy,x:\Box\varphi,y:\varphi$ are auxiliary.

$\blacktriangleright$ Remark 4.

Negri’s original labeled system $\mathsf{G3GL}$ includes the following $\Box\mathsf{L}^{\prime}$ rule rather than the $\Box\mathsf{L}$ rule. However, the left premise of the $\Box\mathsf{L}^{\prime}$ rule is provable in $\mathsf{G3GL}$ using $\Box\mathsf{L}$ , $\Box\mathsf{R}$ , and $\mathsf{tr}$ [31]. We therefore opt to use the simpler $\Box\mathsf{L}$ rule in $\mathsf{G3GL}$ rather than the $\Box\mathsf{L}^{\prime}$ rule to simplify our work.

A derivation of a labeled sequent $\mathcal{R},\Gamma\vdash\Delta$ is defined to be a (potentially infinite) tree whose nodes are labeled with labeled sequents such that (1) $\mathcal{R},\Gamma\vdash\Delta$ is the root of the tree and (2) each parent node is the conclusion of a rule with its children the corresponding premises. A proof is a finite derivation such that every leaf is an instance of an initial sequent. We use $\pi$ (potentially annotated) to denote derivations and proofs throughout the remainder of the paper, and use this notation to denote derivations and proofs in other systems as well with the context determining the usage. The height of a proof is defined as usual to be equal to the length of a maximal path from the root of the proof to an initial sequent.

$\blacktriangleright$ Remark 5.

We assume w.l.o.g. that every fresh variable used in a proof is globally fresh, meaning there is a one-to-one correspondence between $\Box\mathsf{R}$ applications and their fresh variables. This assumption is helpful, yet benign (cf. [31]).

As shown by Negri [31], the various rules displayed in Figure 3 are admissible in $\mathsf{G3GL}$ . Note that the $(x/y)$ rule applies a label substitution to the premise which replaces every occurrence of the label $y$ in a relational atom or labeled formula by $x$ . We define a rule to be admissible (height-preserving admissible) iff if the premises of the rule have proofs (of height $h_{1},\ldots,h_{n}$ ), then the conclusion of the rule has a proof (of height $h\leq\max\{h_{1},\ldots,h_{n}\}$ ). We refer to a height-preserving admissible rule as hp-admissible. Moreover, the non-initial rules of $\mathsf{G3GL}$ are height-preserving invertible. If we let $\mathsf{r}^{-1}_{i}$ be the $i$ -inverse of the rule $\mathsf{r}$ whose conclusion is the $i^{th}$ premise of the $n$ -ary rule $\mathsf{r}$ and premise is the conclusion of $\mathsf{r}$ , then we say that $\mathsf{r}$ is (height-preserving) invertible iff $\mathsf{r}^{-1}_{i}$ is (height-preserving) admissible for each $1\leq i\leq n$ . We refer to height-preserving invertible rules as hp-invertible. The following theorem is due to Negri [31].

Theorem 6 ( $\mathsf{G3GL}$ Properties [31]).

The labeled sequent calculus $\mathsf{G3GL}$ satisfies the following:

(1)

Each labeled sequent of the form $\mathcal{R},\Gamma,x:\varphi\vdash x:\varphi,\Delta$ is provable in $\mathsf{G3GL}$ ;
(2)

All non-initial rules are hp-invertible in $\mathsf{G3GL}$ ;
(3)

The $(x/y)$ , $\mathsf{w}$ , $\mathsf{cL}$ , and $\mathsf{cR}$ rules are hp-admissible in $\mathsf{G3GL}$ ;
(4)

The $\mathsf{cut}$ rule is admissible in $\mathsf{G3GL}$ ;
(5)

$\varphi$ is valid iff $\vdash x:\varphi$ is provable in $\mathsf{G3GL}$ .

3.2 Labeled Tree Sequents

A set $\mathcal{T}$ of relational atoms is a tree iff the graph $G(\mathcal{T})=(V,E)$ forms a tree, where $V=\{x\ |\ x\in\mathrm{Lab}(\mathcal{T})\}$ and $E=\{(x,y)\ |\ xRy\in\mathcal{T}\}$ . A tree sequent is defined to be an expression of the form $\mathcal{T},\Gamma\vdash\Delta$ such that (1) $\mathcal{T}$ is a tree, (2) if $\mathcal{T}\neq\emptyset$ , then $\mathrm{Lab}(\Gamma,\Delta)\subseteq\mathrm{Lab}(\mathcal{T})$ , and (3) if $\mathcal{T}=\emptyset$ , then $|\mathrm{Lab}(\Gamma,\Delta)|=1$ , i.e. all labeled formulae in $\Gamma,\Delta$ share the same label. We note that conditions (1)–(3) ensure that each tree sequent forms a connected graph that is indeed of a tree shape. We use $T$ and annotated versions thereof to denote tree sequents. We define a flat sequent to be a tree sequent of the form $\Gamma\vdash\Delta$ , that is, a flat sequent is a sequent $\Gamma\vdash\Delta$ without relational atoms and where every labeled formula in $\Gamma,\Delta$ shares the same label. The root of a tree sequent $\mathcal{T},\Gamma\vdash\Delta$ is the label $x$ such that there exists a unique directed path of relational atoms in $\mathcal{T}$ from $x$ to every other label $y\in\mathrm{Lab}(\mathcal{T},\Gamma,\Delta)$ ; if $\mathcal{T}=\emptyset$ , then the root is the single label $x$ shared by all formulae in $\Gamma,\Delta$ .

Every tree sequent encodes a tree whose vertices are flat sequents. In other words, each tree sequent $T=\mathcal{T},xRy_{1},\ldots,xRy_{n},\Gamma\vdash\Delta$ such that $x$ is the root and $y_{1},\ldots,y_{n}$ are all children of $x$ can be graphically depicted as a tree $tr_{x}(T)$ of the form shown below:

Definition 7 (Tree Sequent Calculus $\mathsf{CSGL}$ ).

We define $\mathsf{CSGL}:=(\mathsf{G3GL}\setminus\{\mathsf{ir},\mathsf{tr}\})\cup\{% \mathsf{4L}\}$ , where the $\mathsf{4L}$ is shown below and the rules of the calculus only operate over tree sequents.

The system $\mathsf{CSGL}$ is a notational variant of Poggiolesi’s eponymous tree-hypersequent system [35], and thus, we identify the two systems with one another. The main difference between the two systems is notational: the system defined above uses tree sequents, which are tree-hypersequents “dressed” as labeled sequents [15]. We also note that Poggiolesi’s original tree-hypersequent system $\mathsf{CSGL}$ uses a notational variant of the binary rule $\Box\mathsf{L}^{\prime}$ discussed in Remark 4. However, as with the labeled system $\mathsf{G3GL}$ , the left premise of this rule is provable in $\mathsf{CSGL}$ . We have therefore opted to use the unary $\Box\mathsf{L}$ rule in $\mathsf{CSGL}$ to simplify our work and note that this change is benign.

$\blacktriangleright$ Remark 8.

Derivations, proofs, the height of a proof, (hp-)admissibility, the $i$ -inverse of a rule, and (hp-)invertibility are defined for $\mathsf{CSGL}$ analogous to how such notions are defined for $\mathsf{G3GL}$ . We will apply these terms and concepts in the expected way to other sequent systems as well to avoid repeating similar definitions.

The system $\mathsf{CSGL}$ differs from $\mathsf{G3GL}$ in that $\mathsf{CSGL}$ only allows for tree sequents in proofs, lacks the structural rules $\mathsf{ir}$ and $\mathsf{tr}$ , and includes the $\mathsf{4L}$ rule. We refer to $\mathsf{4L}$ and $\Box\mathsf{L}$ as propagation rules (cf. [12, 8]) since the rules bottom-up propagate data forward along relational atoms, and we refer to $\neg\mathsf{L}$ , $\neg\mathsf{R}$ , $\lor\mathsf{L}$ , and ${\lor}\mathsf{R}$ as local rules since they only affect formulae locally at a single label. For any rule, we call the label $x$ labeling the principal formula in the conclusion the principal label, for the $\mathsf{4L}$ , $\Box\mathsf{L}$ , and $\Box\mathsf{R}$ rules, we refer to the label $y$ labeling the auxiliary formula(e) in the premise(s) as the auxiliary label, and for local rules, the auxiliary label is taken to be the same as the principal label since they are identical. Note that we define a label $x$ in a tree sequent $\mathcal{T},\Gamma\vdash\Delta$ to be a leaf iff $x$ is a leaf in $\mathcal{T}$ , and we define a label $x$ to be a pre-leaf iff for all $y\in\mathrm{Lab}(\mathcal{T})$ , if $xRy\in\mathcal{T}$ , then $y$ is a leaf.

Since the tree sequent calculus $\mathsf{CSGL}$ is isomorphic to Poggiolesi’s tree-hypersequent system, the two systems share the same properties. We note that in the setting of tree sequents the $(x/y)$ and $\mathsf{w}$ rules are less general than for labeled sequents. In particular, such rules are assumed to preserve the “tree shape” of tree sequents when applied. Nevertheless, the restricted forms of these rules are still hp-admissible in $\mathsf{CSGL}$ .

Theorem 9 ( $\mathsf{CSGL}$ Properties [35]).

The tree sequent calculus $\mathsf{CSGL}$ satisfies the following:

(1)

Each tree sequent of the form $\mathcal{T},\Gamma,x:\varphi\vdash x:\varphi,\Delta$ is provable in $\mathsf{CSGL}$ ;
(2)

All non-initial rules are hp-invertible in $\mathsf{CSGL}$ ;
(3)

The $(x/y)$ , $\mathsf{w}$ , $\mathsf{cL}$ , and $\mathsf{cR}$ rules are hp-admissible in $\mathsf{CSGL}$ ;
(4)

The $\mathsf{cut}$ rule is admissible in $\mathsf{CSGL}$ ;
(5)

$\varphi$ is valid iff $\vdash x:\varphi$ is provable in $\mathsf{CSGL}$ .

Proofs in $\mathsf{G3GL}$ and $\mathsf{CSGL}$ are inter-translatable with one another. This correspondence was established by Goré and Ramanayake [15] and is based on a couple observations. First, the $\mathsf{ir}$ rule does not occur in $\mathsf{G3GL}$ proofs where the end sequent is a tree sequent. It is not difficult to see why this is the case: if one takes a proof of a tree sequent, then bottom-up applications of rules from $\mathsf{G3GL}$ will not allow for directed cycles to enter a sequent in a proof. This follows from the fact that the conclusion of the proof is a tree sequent, which is free of directed cycles, and each rule of $\mathsf{G3GL}$ either preserves relational atoms bottom-up, adds a single relational atom from a label $x$ to a fresh label $y$ in the case of the $\Box\mathsf{R}$ rule, or adds an undirected cycle in the case of $\mathsf{tr}$ . Since the conclusion of $\mathsf{ir}$ contains a directed cycle $x R x$ , such a sequent will never occur in such a proof.

Observation 10 ([15]).

The $\mathsf{ir}$ rule does not occur in any $\mathsf{G3GL}$ proof of a tree sequent.

Second, Goré and Ramanayake [15] show that instances of $\mathsf{tr}$ can be eliminated from $\mathsf{G3GL}$ proofs not containing $\mathsf{ir}$ and replaced by instances of $\mathsf{4L}$ . This elimination procedure can be used to map $\mathsf{G3GL}$ proofs such that the end sequent is a tree sequent to $\mathsf{CSGL}$ proofs. Conversely, if we let arbitrary labeled sequent appear in $\mathsf{CSGL}$ proofs, it can be shown that $\mathsf{4L}$ can be eliminated from $\mathsf{CSGL}$ proofs and replaced by instances of $\mathsf{tr}$ . These elimination results are proven syntactically, showing that proof transformations exist between $\mathsf{CSGL}$ and $\mathsf{G3GL}$ for proofs of tree sequents as summarized in the theorem below. We refer to the reader to [15] for the details.

Theorem 11 ([15]).

A tree sequent $T$ is provable in $\mathsf{G3GL}$ iff it is provable in $\mathsf{CSGL}$ .

4 Linearizing Tree Sequents in Proofs

We now show how to extract a linear nested sequent calculus from $\mathsf{CSGL}$ , dubbed $\mathsf{LNGL}$ (see Figure 4). To the best of the author’s knowledge, this is the first linear nested sequent calculus for Gödel-Löb provability logic. Linear nested sequents were introduced by Lellmann [21] and are a finite representation of Masini’s 2-sequents [29]. Such systems operate over lines of Gentzen sequents and have been used to provide cut-free systems for intermediate and modal logics [20, 21, 29, 30].

The extraction of linear nested sequent proofs from tree sequent proofs takes place in three phases. In the first phase, we show how to transform any $\mathsf{CSGL}$ proof into an end-active proof, i.e., a proof such that principal and auxiliary formulae only occur at (pre-)leaves in tree sequents (cf. [21]). In the second phase, we define our novel linearization technique, where we identify specific paths in tree sequents and “prune” sub-trees, yielding a linear nested sequent proof as the result. This technique is an additional contribution of this paper, and we conjecture that this technique can be used in other settings to extract linear nested sequent systems from tree sequent/nested sequent systems. In the third phase, we show how to “reshuffle” a linear nested sequent proof so that the proof proceeds in repetitive stages of local rules, propagation rules, and $\Box\mathsf{R}$ rules, which we refer to as a proof in normal form. This transformation is motivated by one provided in [33] for so-called basic nested systems, which transforms proofs in a similar manner to extract Gentzen sequent proofs. Our transformation is distinct however as it works within the context of linear nested sequents. The simpler data structure used in linear nested sequents and the “end-active” shape of the rules in $\mathsf{LNGL}$ simplifies the process of reshuffling proofs into normal form.

Figure 4: Linear Nested Sequent Calculus

\mathsf{LNGL}

for

\mathsf{GL}

.

A linear nested sequent is an expression of the form $\mathcal{G}:=\Gamma_{1}\vdash\Delta_{1}\sslash\cdots\sslash\Gamma_{n}\vdash% \Delta_{n}$ such that $\Gamma_{i}$ and $\Delta_{i}$ are multisets of formulae from $\mathcal{L}$ for $1\leq i\leq n$ . We use $\mathcal{G}$ , $\mathcal{H}$ , $\ldots$ to denote linear nested sequents and note that such sequents admit a formula interpretation:

f(\Gamma\vdash\Delta):=\bigwedge\Gamma\rightarrow\bigvee\Delta\qquad f(\Gamma% \vdash\Delta\sslash\mathcal{G}):=\bigwedge\Gamma\rightarrow(\bigvee\Delta\lor% \Box f(\mathcal{G}))

We define a linear nested sequent $\mathcal{G}$ to be (in)valid iff $f(\mathcal{G})$ is (in)valid. The linear nested sequent calculus $\mathsf{LNGL}$ consists of the rules shown in Figure 4. We take the $\neg\mathsf{L}$ , $\neg\mathsf{R}$ , $\lor\mathsf{L}$ , and ${\lor}\mathsf{R}$ rules to be local rules and the $\mathsf{4L}$ and $\Box\mathsf{L}$ rules to be propagation rules in $\mathsf{LNGL}$ . For $1\leq i\leq n$ , we refer to $\Gamma_{i}\vdash\Delta_{i}$ as the $i$ -component (or, as a component more generally) of the linear nested sequent $\mathcal{G}=\Gamma_{1}\vdash\Delta_{1}\sslash\cdots\sslash\Gamma_{n}\vdash% \Delta_{n}$ , we refer to $\Gamma_{n}\vdash\Delta_{n}$ as the end component, and we define the length of $\mathcal{G}$ to be $||\mathcal{G}||:=n$ , i.e., the length of a linear nested sequent is equal to the number of its components. Comparing $\mathsf{LNGL}$ to $\mathsf{CSGL}$ , one can see that $\mathsf{LNGL}$ is the calculus $\mathsf{CSGL}$ restricted to lines of Gentzen sequents and where rules only operate in the last two components. Making use of the formula translation, it is a basic exercise to show that if the conclusion of any rule is invalid, then at least one premise is invalid, i.e., $\mathsf{LNGL}$ is sound.

Theorem 12.

If $\mathcal{G}$ is provable in $\mathsf{LNGL}$ , then $\mathcal{G}$ is valid.

When transforming $\mathsf{CSGL}$ proofs into $\mathsf{LNGL}$ proofs later on, it will be helpful to use the weakening rule $\mathsf{w}$ shown in the lemma below. Observe that any application of $\mathsf{w}$ to $\mathsf{id_{1}}$ or $\mathsf{id_{2}}$ yields an initial sequent, and $\mathsf{w}$ permutes above every other rule of $\mathsf{LNGL}$ . As an immediate consequence, we have that $\mathsf{w}$ is hp-admissible in $\mathsf{LNGL}$ .

Lemma 13.

The following weakening rule $\mathsf{w}$ is hp-admissible in $\mathsf{LNGL}$ .

Furthermore, we have that the $\mathsf{4L}$ and $\Box\mathsf{L}$ rules are hp-invertible in $\mathsf{LNGL}$ since the premises of each rule may be obtained from the conclusion by $\mathsf{w}$ .

Lemma 14.

The $\mathsf{4L}$ and $\Box\mathsf{L}$ rules are hp-invertble in $\mathsf{LNGL}$ .

From Tree Sequents to Linear Nested Sequents

To extract $\mathsf{LNGL}$ from $\mathsf{CSGL}$ , we first establish a set of rule permutation results, i.e., we show that rules of a certain form in $\mathsf{CSGL}$ can always be permuted below other rules of a specific form. We note that a rule $\mathsf{r}$ permutes below a rule $\mathsf{r}^{\prime}$ whenever an application of $\mathsf{r}$ followed by $\mathsf{r}^{\prime}$ in a proof can be replaced by an application of $\mathsf{r}^{\prime}$ (potentially preceded by an application of an $i$ -inverse of $\mathsf{r}$ ) followed by an application of $\mathsf{r}$ to derive the same conclusion. To make this definition more concrete, we show (1) the permutation of a unary rule $\mathsf{r}$ below a binary rule $\mathsf{r}^{\prime}$ below top-left, (2) the permutation of a binary rule $\mathsf{r}$ below a unary rule $\mathsf{r}^{\prime}$ below top-right, (3) the permutation of a unary rule $\mathsf{r}$ below a unary rule $\mathsf{r}^{\prime}$ below bottom-left, and (4) the permutation of a binary rule $\mathsf{r}$ below a binary rule $\mathsf{r}^{\prime}$ below bottom-right. In (1) and (4), we note that the case where $\mathsf{r}$ is applied to the right premise of $\mathsf{r}^{\prime}$ is symmetric. Furthermore, recall that $\mathsf{r}^{-1}_{1}$ and $\mathsf{r}^{-1}_{2}$ are the $1$ - and $2$ -inverses of $\mathsf{r}$ , respectively. (NB. For the definition of the $i$ -inverse of a rule, see Section 3.1.) We use (annotated versions of) the symbol $S$ below to indicate not only tree sequents, but linear nested sequents since we consider permutations of rules in $\mathsf{LNGL}$ later on as well.

The various admissible rule permutations we describe are based on the notion of end-activity, which is a property of rule applications where principal and auxiliary formulae only occur at (pre-)leaves in sequents. End-activity was first discussed by Lellmann [21] in the context of mapping Gentzen sequent proofs into linear nested sequent proofs for non-classical logics.

Definition 15 (End Active).

A $\mathsf{CSGL}$ proof is end-active iff the following hold:

(1)

The principal label in every instance of $\mathsf{id_{1}}$ and $\mathsf{id_{2}}$ is a leaf;
(2)

The principal label of each local rule is a leaf;
(3)

The principal and auxiliary label of a propagation rule is a pre-leaf and leaf, respectively.

A rule $\mathsf{r}$ is end-active iff it satisfies its respective condition above; otherwise, the rule is non-end-active. We note that we always take the $\Box\mathsf{R}$ rule to be end-active.

As stated in the following lemma, the end-activity of sequential rule applications determines a set of permutation relationships between the rules of $\mathsf{CSGL}$ . The lemma is straightforward to prove, though tedious due to the number of cases; its proof can be found in the appendix.

Lemma 16.

The following permutations hold in $\mathsf{CSGL}$ :

(1)

If $\mathsf{r}$ is a non-end-active local rule and $\mathsf{r}^{\prime}$ is non-initial and end-active, then $\mathsf{r}$ permutes below $\mathsf{r}^{\prime}$ and $\mathsf{r}^{\prime}$ remains end-active after this permutation;
(2)

if $\mathsf{r}$ is a non-end-active propagation rule and $\mathsf{r}^{\prime}$ is non-initial and end-active, then $\mathsf{r}$ permutes below $\mathsf{r}^{\prime}$ and $\mathsf{r}^{\prime}$ remains end-active after this permutation.

Let us define a final-active proof in $\mathsf{CSGL}$ to be a proof such that the last inference is end-active. Using the above lemma, every final-active proof $\pi$ in $\mathsf{CSGL}$ can be transformed into an end-active proof as follows: first, observe that the last inference in $\pi$ is end-active by assumption. By successively considering bottom-most instances of non-end-active local and propagation rules $\mathsf{r}$ in $\pi$ , we can repeatedly apply Lemma 16 to permute $\mathsf{r}$ lower in the proof because all rules below $\mathsf{r}$ are guaranteed to be end-active. By inspecting the rules of $\mathsf{CSGL}$ , we know that the trees within the tree sequents in $\pi$ will never “grow” and tend to “shrink” as they get closer to the conclusion of the proof, meaning, each non-end-active rule $\mathsf{r}$ will eventually become end-active through successive downward permutations.²²2Observe that $\neg\mathsf{L}$ , $\neg\mathsf{R}$ , $\lor\mathsf{L}$ , ${\lor}\mathsf{R}$ , $\Box\mathsf{L}$ , and $\mathsf{4L}$ only affect the formulae associated with the label of a tree sequent, whereas $\Box\mathsf{R}$ top-down removes a relational atom from a tree sequent. Therefore, the number of relational atoms in tree sequents never increases as we move down paths in $\mathsf{CSGL}$ proofs from initial sequents to the conclusion. This process will eventually terminate and yield a proof where all non-initial rules are end-active for the following two reasons: (1) As stated in the lemma above, permuting a non-end-active local or propagation rule $\mathsf{r}^{\prime}$ below an end-active rule $\mathsf{r}$ preserves the end-activity of the rule $\mathsf{r}$ . (2) Although downward permutations may require the $i$ -inverse of a rule to be applied above the permuted inferences, the hp-invertibility of all non-initial rules in $\mathsf{CSGL}$ (see Theorem 9) ensures that the height of the proof does not grow after a downward rule permutation.

After all such downward permutations have been performed, the resulting proof is almost end-active with the exception that initial rules may not be end-active. For example, as shown below left, it may be the case that $\mathsf{id_{1}}$ is non-end-active and followed by a rule $\mathsf{r}$ . Since $\mathsf{r}$ is guaranteed to be end-active at this stage, we know that the auxiliary label of $\mathsf{r}$ is distinct from $y$ , meaning, the conclusion will be an instance of $\mathsf{id_{1}}$ as shown below right.

By replacing such rule applications $\mathsf{r}$ by $\mathsf{id_{1}}$ (or $\mathsf{id_{2}}$ ) instances, effectively “pushing” initial rules down in the proof, we will eventually obtain initial rules such that the label $y$ is auxiliary in the subsequent rule application, which will then be a leaf since all non-initial rules of the proof are end-active. Thus, every final-active proof in $\mathsf{CSGL}$ can be transformed into an end-active proof.

$\blacktriangleright$ Remark 17.

As a corollary, we note that every proof $\pi$ in $\mathsf{CSGL}$ of a sequent $\vdash x:\varphi$ can be transformed into an end-active proof as well. This is due to the fact that the last inference in $\pi$ must be end-active since the proof ends with $\vdash x:\varphi$ , i.e., $\pi$ is final-active in this case.

Theorem 18.

Each final-active proof in $\mathsf{CSGL}$ can be transformed into an end-active proof.

Theorem 19.

Each end-active proof in $\mathsf{CSGL}$ can be transformed into a proof in $\mathsf{LNGL}$ .

Proof.

We prove that if there exists an end-active proof in $\mathsf{CSGL}$ of a tree sequent $\mathcal{T},\Gamma\vdash\Delta$ , then there exists a path $x_{1},\ldots,x_{n}$ of labels from the root $x_{1}$ to a leaf $x_{n}$ in $\mathcal{T},\Gamma\vdash\Delta$ such that $\Gamma(x_{1})\vdash\Delta(x_{1})\sslash\cdots\sslash\Gamma(x_{n})\vdash\Delta(% x_{n})$ is provable in $\mathsf{LNGL}$ . We argue this by induction on the height of the end-active proof $\pi$ in $\mathsf{CSGL}$ .

Base case.

Suppose $\pi$ consists of a single application of $\mathsf{id_{1}}$ or $\mathsf{id_{2}}$ , as shown below:

We know that each initial sequent is end-active, i.e., the label $x$ is a leaf in both tree sequents. Therefore, since each sequent is a tree sequent, there exists a path $y_{1},\ldots,y_{n}=x$ of labels from the root $y_{1}$ to the leaf $x$ . By using this path, we obtain respective instances of $\mathsf{id_{1}}$ and $\mathsf{id_{2}}$ as shown below:

Inductive step.

For the inductive hypothesis (IH), we assume that the claim holds for every end-active proof in $\mathsf{CSGL}$ of height $h^{\prime}\leq h$ , and aim to show that the claim holds for proofs of height $h+1$ . We let $\pi$ be of height $h+1$ and argue the cases where $\pi$ ends with $\Box\mathsf{L}$ or $\Box\mathsf{R}$ as the remaining cases are shown similarly. Some additional cases are given in the appendix.

$\Box\mathsf{L}$ .

Let us suppose that $\pi$ ends with an instance of $\Box\mathsf{L}$ as shown below.

By IH, we know there exists a path $y_{1},\ldots,y_{n}$ of labels from the root $y_{1}$ to the leaf $y_{n}$ in the premise of $\Box\mathsf{L}$ such that $\mathcal{G}=\Gamma(y_{1})\vdash\Delta(y_{1})\sslash\cdots\sslash\Gamma(y_{n})% \vdash\Delta(y_{n})$ is provable in $\mathsf{LNGL}$ . Since $\Box\mathsf{L}$ is end-active, we have three cases to consider: (1) neither $x$ nor $y$ occur along the path in the premise, (2) only $x$ occurs along the path in the premise, or (3) both $x$ and $y$ occur along the path in the premise. In cases (1) and (2), we translate the entire $\Box\mathsf{L}$ inference as the linear nested sequent $\mathcal{G}$ . In case (3), $\mathcal{G}$ has the form of the premise shown below with $\Gamma(y_{n-1})=\Sigma_{1},\Box\varphi$ and $\Gamma(y_{n})=\Sigma_{2},\varphi$ . A single application of $\Box\mathsf{L}$ gives the desired result.

$\Box\mathsf{R}$ .

Let us suppose that $\pi$ ends with an instance of $\Box\mathsf{R}$ as shown below.

By IH, we know there exists a path $y_{1},\ldots,y_{n}$ of labels from the root $y_{1}$ to the leaf $y_{n}$ in the premise of $\Box\mathsf{R}$ such that $\Gamma(y_{1})\vdash\Delta(y_{1})\sslash\cdots\sslash\Gamma(y_{n})\vdash\Delta(% y_{n})$ is provable in $\mathsf{LNGL}$ . We have three cases to consider: either (1) neither $x$ nor $y$ occur along the path, (2) only $x$ occurs along the path, or (3) both $x$ and $y$ occur along the path. In case (1), we translate the entire $\Box\mathsf{R}$ instance as the single linear nested sequent $\mathcal{G}$ . In case (2), we know that $x=y_{i}$ for some $1\leq i\leq n$ . To obtain the desired conclusion, we apply the hp-admissible $\mathsf{w}$ rule as shown below. Observe that the conclusion of the $\mathsf{w}$ application below corresponds to the linear nested sequent obtained from the path $y_{1},\ldots,y_{n}$ in the conclusion of the $\Box\mathsf{R}$ instance above.

Last, in case (3), we know that $x=y_{n-1}$ and $y=y_{n}$ due to the freshness condition imposed on the $\Box\mathsf{R}$ rule. In this case, $\mathcal{G}$ has the form of the premise shown below, meaning, a single application of the $\Box\mathsf{R}$ rule gives the linear nested sequent corresponding to the path $y_{1},\ldots,y_{n}$ in the conclusion of the $\Box\mathsf{R}$ instance above.

$\hfill\blacktriangleleft$

The following is an immediate consequence of Theorems 12, 18, 19 and Remark 17.

Corollary 20 ( $\mathsf{LNGL}$ Soundness and Completeness).

$\varphi$ is valid iff $\vdash\varphi$ is provable in $\mathsf{LNGL}$ .

Last, we show that every $\mathsf{LNGL}$ proof can be put into a normal form (see Definition 21 and Theorem 18 below) such that (reading the proof bottom-up) $\Box\mathsf{R}$ instances are preceded by $\mathsf{4L}$ instances, which are preceded by $\Box\mathsf{L}$ instances, which are preceded by local rule instances (or, initial rules). We will utilize this normal form in the next section to show that every $\mathsf{LNGL}$ proof can be transformed into a Gentzen sequent proof (Theorem 24). We let $\mathrm{B}$ be a set of $\mathsf{LNGL}$ rules and define a block to be a derivation that only uses rules from $\mathrm{B}$ . We use the following notation to denote blocks, showing that the set $\mathrm{B}$ of rules derives $\mathcal{G}$ from $\mathcal{G}_{1},\ldots,\mathcal{G}_{n}$ , and refer to $\mathcal{G}_{1},\ldots,\mathcal{G}_{n}$ as the premises of the block $\mathrm{B}$ .

Definition 21 (Normal Form).

A proof in $\mathsf{LNGL}$ is in normal form iff each bottom-up $\Box\mathsf{R}$ application is derived from a block $\mathrm{B}$ of $\mathsf{4L}$ rules, whose premise is derived from a block $\mathrm{B}^{\prime}$ of $\Box\mathsf{L}$ rules, whose premise is derived from a block $\mathrm{B}^{\prime\prime}$ of local rules, as indicated below.

We refer to block of rules of the above form as a complete block, and refer to the portion of a complete block consisting of only $\Box\mathsf{R}$ , $\mathrm{B}$ , and $\mathrm{B}^{\prime}$ as a modal block.

As proven in the next section (Theorem 24), every normal form proof in $\mathsf{LNGL}$ can be transformed into a proof in Sambin and Valentini’s Gentzen calculus $\mathsf{GL_{seq}}$ . Therefore, we need to show that every proof in $\mathsf{LNGL}$ can be put into normal form. We prove this by making an observation about the structure of proofs in $\mathsf{LNGL}$ . Observe that local and propagation rules in $\mathsf{LNGL}$ only affect the end component of linear nested sequents and preserve the length of such sequents, whereas the $\Box\mathsf{R}$ rule increases the length of a linear nested sequent by 1 when applied bottom-up. This implies that any $\mathsf{LNGL}$ proof $\pi$ bottom-up proceeds in repetitive stages, as we now describe. Let $\pi$ be a proof in $\mathsf{LNGL}$ with conclusion $\mathcal{G}$ such that $||\mathcal{G}||=n$ . The conclusion $\mathcal{G}$ is derived with a block $\mathrm{B}$ of local and propagation rules that only affect the $n$ -component in inferences with the premises of the block $\mathrm{B}$ being initial rules or derived by applications of $\Box\mathsf{R}$ rules. These applications of $\Box\mathsf{R}$ rules will have premises of length $n+1$ and will be preceded by blocks $\mathrm{B}_{i}$ of local and propagation rules that only affect the $(n+1)$ -component in inferences. The premises of the $\mathrm{B}_{i}$ blocks will then either be initial rules or derived by applications of $\Box\mathsf{R}$ rules that have premises of length $n+2$ , which are preceded by blocks of local and propagation rules that only affect the $(n+2)$ -component in inferences, and so on. Every proof in $\mathsf{LNGL}$ will have this repetitive structure.

Let $\Box\mathsf{R}$ be applied in an $\mathsf{LNGL}$ proof $\pi$ with premise $\mathcal{G}\sslash\Gamma\vdash\Delta\sslash\Box\varphi\vdash\varphi$ of length $n$ . We say that an instance of a local or propagation rule $\mathsf{r}$ in $\pi$ is length-consistent with $\Box\mathsf{R}$ iff the length of the conclusion of $\mathsf{r}$ is equal to $n$ . Based on the discussion above, we can see that for any $\Box\mathsf{R}$ application in a proof $\pi$ , all length-consistent local and propagation rules will occur in a block $\mathrm{B}$ above the $\Box\mathsf{R}$ application with $\mathrm{B}$ free of other $\Box\mathsf{R}$ rules. It is not difficult to show that $\mathrm{B}$ can be transformed into a complete block by (1) successively permuting $\mathsf{4L}$ rules down into a block above $\Box\mathsf{R}$ , and (2) successively permuting $\Box\mathsf{L}$ rules down above the $\mathsf{4L}$ block. After the permutations from (1) and (2) have been carried out, the premise of the $\Box\mathsf{L}$ block will be derived by length-consistent local rule applications, showing that $\Box\mathsf{R}$ is preceded by a complete block. As these permutations can be performed for every $\Box\mathsf{R}$ rule in a proof, every proof can be put into normal form.

Theorem 22.

Every proof in $\mathsf{LNGL}$ can be transformed into a proof in normal form.

5 Sequent Systems and Correspondences

Figure 5: Sequent calculus rules.

5.1 Gentzen, Cyclic, and Non-Wellfounded Systems

We use $\Gamma$ , $\Delta$ , $\Sigma$ , $\ldots$ to denote finite multisets of formulae within the context of sequent systems. For a multiset $\Gamma:=\varphi_{1},\ldots,\varphi_{n}$ , we define $\Box\Gamma:=\Box\varphi_{1},\ldots,\Box\varphi_{n}$ . A sequent is defined to be an expression of the form $\Gamma\vdash\Delta$ . The sequent calculus $\mathsf{GL_{seq}}$ for $\mathsf{GL}$ consists of the rules $\mathsf{id}$ , $\neg\mathsf{L}$ , $\neg\mathsf{R}$ , $\lor\mathsf{L}$ , ${\lor}\mathsf{R}$ , and $\Box_{\mathsf{GL}}$ shown in Figure 5 and is an equivalent variant of the Gentzen calculi $\mathsf{GLSC}$ and $\mathsf{GLS}$ introduced by Sambin and Valentini for $\mathsf{GL}$ [36, 37].³³3 $\mathsf{GL_{seq}}$ differs from Sambin and Valentini’s original systems in that multisets are used instead of sets, rules for superfluous logical connectives (e.g., conjunction $\land$ and implication $\rightarrow$ ) have been omitted as these are definable in terms of other rules, and the weakening rules have been absorbed into $\mathsf{id}$ and $\Box_{\mathsf{GL}}$ . The system $\mathsf{GL_{seq}}$ is sound and complete for $\mathsf{GL}$ , admits syntactic cut-elimination, and the weakening and contraction rules $\mathsf{w}$ , $\mathsf{cL}$ , and $\mathsf{cR}$ (shown below) are admissible (cf. [16, 39]).

Shamkanov [39] showed that equivalent non-wellfounded and cyclic sequent systems could be obtained for $\mathsf{GL}$ by taking the sequent calculus for the modal logic $\mathsf{K4}$ and generalizing the notion of proof. The sequent calculus $\mathsf{K4_{seq}}$ is obtained by replacing the $\Box_{\mathsf{GL}}$ rule in $\mathsf{GL_{seq}}$ with the $\Box_{\mathsf{4}}$ rule shown in Figure 5. Let us now recall Shamkanov’s non-wellfounded sequent calculus $\mathsf{GL_{\infty}}$ and cyclic sequent calculus $\mathsf{GL_{circ}}$ for $\mathsf{GL}$ . We present Shamkanov’s systems in a two-sided format, i.e., using two-sided sequents $\Gamma\vdash\Delta$ rather than one-sided sequents of the form $\Gamma$ . This makes the correspondence between Shamkanov’s systems and $\mathsf{GL_{seq}}$ clearer as well as saves us from having to introduce a new language for $\mathsf{GL}$ since one-sided sequents use formulae in negation normal form. Translating proofs with two-sided sequents to proofs with one-sided sequents and vice-versa can be easily obtained by standard techniques, and so, this minor modification causes no problems.

A derivation of a sequent $\Gamma\vdash\Delta$ is defined to be a (potentially infinite) tree whose nodes are labeled with sequents such that (1) $\Gamma\vdash\Delta$ is the root of the tree, and (2) each parent node is taken to be the conclusion of a rule in $\mathsf{K4_{seq}}$ with its children the corresponding premises. A non-wellfounded proof is a derivation such that all leaves are initial sequents. $\mathsf{GL_{\infty}}$ is the non-wellfounded sequent system obtained by letting the set of provable sequents be determined by non-wellfounded proofs.

A cyclic derivation is a pair $\pi=(\kappa,c)$ such that $\kappa$ is a finite derivation in $\mathsf{K4_{seq}}$ and $c$ is a function with the following properties: (1) $c$ is defined on a subset of the leaves of $\kappa$ , (2) the image $c(x)$ lies on the path from the root of $\kappa$ to $x$ and does not coincide with $x$ , and (3) both $x$ and $c(x)$ are labeled by the same sequent. If the function $c$ is defined at a leaf $x$ , then we say that a back-link exists from $x$ to $c(x)$ . A cyclic proof is a cyclic derivation $\pi=(\kappa,c)$ such that every leaf $x$ is labeled by an instance of $\mathsf{id}$ or there exists a back-link from $x$ to the node $c(x)$ . $\mathsf{GL_{circ}}$ is the cyclic sequent system obtained by letting the set of provable sequents be determined by cyclic proofs.

Shamkanov established a three-way correspondence between $\mathsf{GL_{seq}}$ , $\mathsf{GL_{\infty}}$ , and $\mathsf{GL_{circ}}$ , providing syntactic transformations mapping proofs between the three systems.⁴⁴4We note that Shamkanov’s proof transformation from $\mathsf{GL_{seq}}$ to $\mathsf{GL_{\infty}}$ relies on the admissibility of the $\mathsf{cut}$ rule in $\mathsf{GL_{seq}}$ . This is not problematic however since $\mathsf{GL_{seq}}$ admits syntactic cut-elimination.

Theorem 23 ([39]).

$\Gamma\vdash\Delta$ is provable in $\mathsf{GL_{seq}}$ iff $\Gamma\vdash\Delta$ is provable in $\mathsf{GL_{\infty}}$ iff $\Gamma\vdash\Delta$ is provable in $\mathsf{GL_{circ}}$ .

5.2 Completing the Correspondences

Theorem 24.

If $\pi$ is a normal form proof of $\vdash\varphi$ in $\mathsf{LNGL}$ , then $\pi$ can be transformed into a proof of $\vdash\varphi$ in $\mathsf{GL_{seq}}$ .

Proof.

We show how to transform the normal form proof $\pi$ of $\vdash\varphi$ in $\mathsf{LNGL}$ into a proof $\pi^{\prime}$ of $\vdash\varphi$ in $\mathsf{GL_{seq}}$ in a bottom-up manner. For the conclusion $\vdash\varphi$ of the proof $\pi$ , we take $\vdash\varphi$ to be the conclusion of $\pi^{\prime}$ . We now make a case distinction on bottom-up applications of rules applied in $\pi$ . For each rule $\neg\mathsf{L}$ , $\neg\mathsf{R}$ , $\lor\mathsf{L}$ , or ${\lor}\mathsf{R}$ , we translate each premise of the rule as its end component. For example, the $\lor\mathsf{L}$ rule will be translated as shown below.

Suppose now that we encounter a $\Box\mathsf{R}$ rule while bottom-up translating the proof $\pi$ into a proof in $\mathsf{GL_{seq}}$ . Since $\pi$ is in normal form, we know that $\Box\mathsf{R}$ is preceded by a modal block (see Definition 21), that is, $\Box\mathsf{R}$ is (bottom-up) preceded by a block $\mathrm{B}_{\mathsf{4L}}$ of $\mathsf{4L}$ rules, which is preceded by a block $\mathrm{B}_{\Box\mathsf{L}}$ of $\Box\mathsf{L}$ rules, i.e., the modal block has the shape shown below. We suppose that $\Box\Sigma_{1}$ are the principal formulae of the $\mathsf{4L}$ applications, $\Box\Sigma_{2}$ are those formulae principal in both $\mathsf{4L}$ and $\Box\mathsf{L}$ applications, and $\Box\Sigma_{3}$ are those formulae principal only in $\Box\mathsf{L}$ applications.

We bottom-up translate the entire block as shown below, where the conclusion is obtained from the end component of the modal block’s conclusion. Note that we may apply the $\mathsf{w}$ rule because it is admissible in $\mathsf{GL_{seq}}$ .

Last, suppose an instance of $\mathsf{id_{1}}$ or $\mathsf{id_{2}}$ is reached in the translation as shown below left.

In each case, we translate the linear nested sequent as its end component, yielding the respective Gentzen sequents shown above right, both of which are instances of $\mathsf{id}$ . $\hfill\blacktriangleleft$

Last, the following theorem completes the circuit of proof transformations and establishes syntactic correspondences between $\mathsf{G3GL}$ , $\mathsf{CSGL}$ , $\mathsf{LNGL}$ , $\mathsf{GL_{seq}}$ , $\mathsf{GL_{\infty}}$ and $\mathsf{GL_{circ}}$ .

Theorem 25.

If $\Gamma\vdash\Delta$ is provable in $\mathsf{GL_{seq}}$ , then $x:\Gamma\vdash x:\Delta$ is provable in $\mathsf{G3GL}$ .

Proof.

By induction on the height of the proof $\pi$ in $\mathsf{GL_{seq}}$ . The base case immediately follows from Theorem 6-(1), and the $\neg\mathsf{L}$ , $\neg\mathsf{R}$ , $\lor\mathsf{L}$ , and ${\lor}\mathsf{R}$ cases of the inductive step straightforwardly follow by applying IH and then the corresponding rule in $\mathsf{G3GL}$ . Therefore, we need only show the case where $\pi$ ends with an application of $\Box_{\mathsf{GL}}$ , as shown below left.

To obtain the desired proof, we first apply the hp-admissible $\mathsf{w}$ rule (Theorem 6), followed by applications of the $\Box\mathsf{L}$ rule and admissible $\mathsf{4L}$ rule (cf. [15]). Applying the $\Box\mathsf{R}$ rule, followed by applications of the hp-admissible $(x/y)$ and $\mathsf{w}$ rules (Theorem 6), gives the desired conclusion. $\hfill\blacktriangleleft$

6 Concluding Remarks

There are various avenues for future research: first, it would be interesting to look into the properties of the new linear nested sequent calculus $\mathsf{LNGL}$ , investigating additional admissible structural rules, how the system can be amended to allow for the hp-invertibility of all rules, and also looking into syntactic cut-elimination. Second, by employing a methodology for extracting nested sequent systems from relational semantics [28], we can integrate this approach with the linearization technique to develop a general method for extracting (cut-free) linear nested systems from the semantics of various modal, intuitionistic, and related logics. Third, it seems worthwhile to see if the proof transformation techniques discussed in this paper can be applied to structural cyclic systems (e.g., cyclic labeled sequent systems for classical and intuitionistic Gödel-Löb logic [11]) to remove extraneous structure and extract simpler (cyclic) Gentzen systems.

References

[1] Bahareh Afshari and Graham E. Leigh. Cut-free completeness for modal mu-calculus. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–12, 2017. doi:10.1109/LICS.2017.8005088.
[2] Arnon Avron. On modal systems having arithmetical interpretations. Journal of Symbolic Logic, 49(3):935–942, 1984. doi:10.2307/2274147.
[3] James Brotherston. Cyclic proofs for first-order logic with inductive definitions. In Bernhard Beckert, editor, Automated Reasoning with Analytic Tableaux and Related Methods, pages 78–92, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. doi:10.1007/11554554_8.
[4] James Brotherston. Formalised inductive reasoning in the logic of bunched implications. In Hanne Riis Nielson and Gilberto Filé, editors, Static Analysis, pages 87–103, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. doi:10.1007/978-3-540-74061-2_6.
[5] James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177–1216, October 2010. doi:10.1093/logcom/exq052.
[6] Kai Brünnler. Deep sequent systems for modal logic. Archive for Mathematical Logic, 48(6):551–577, 2009. doi:10.1007/s00153-009-0137-3.
[7] Robert A. Bull. Cut elimination for propositional dynamic logic without *. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 38(2):85–100, 1992. doi:10.1002/MALQ.19920380107.
[8] Marcos A Castilho, Luis Farinas del Cerro, Olivier Gasquet, and Andreas Herzig. Modal tableaux with propagation rules and structural rules. Fundamenta Informaticae, 32(3, 4):281–297, 1997. doi:10.3233/FI-1997-323404.
[9] Agata Ciabattoni, Tim Lyon, Revantha Ramanayake, and Alwen Tiu. Display to labelled proofs and back again for tense logics. ACM Transactions on Computational Logic, 22(3):1–31, 2021. doi:10.1145/3460492.
[10] Anupam Das and Marianna Girlando. Cyclic hypersequent system for transitive closure logic. Journal of Automated Reasoning, 67(3):27, 2023. doi:10.1007/s10817-023-09675-1.
[11] Anupam Das, Iris van der Giessen, and Sonia Marin. Intuitionistic Gödel-Löb Logic, à la Simpson: Labelled Systems and Birelational Semantics. In Aniello Murano and Alexandra Silva, editors, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), volume 288 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1–22:18, Dagstuhl, Germany, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CSL.2024.22.
[12] Melvin Fitting. Tableau methods of proof for modal logics. Notre Dame Journal of Formal Logic, 13(2):237–247, 1972. doi:10.1305/NDJFL/1093894722.
[13] Melvin Fitting. Nested sequents for intuitionistic logics. Notre Dame Journal of Formal Logic, 55(1):41–61, 2014. doi:10.1215/00294527-2377869.
[14] Rajeev Goré, Linda Postniece, and Alwen Tiu. Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. In Carlos Areces and Robert Goldblatt, editors, Advances in Modal Logic 7, pages 43–66. College Publications, 2008. URL: http://www.aiml.net/volumes/volume7/Gore-Postniece-Tiu.pdf.
[15] Rajeev Goré and Revantha Ramanayake. Labelled tree sequents, tree hypersequents and nested (deep) sequents. In Thomas Bolander, Torben Braüner, Silvio Ghilardi, and Lawrence S. Moss, editors, Advances in Modal Logic 9, pages 279–299. College Publications, 2012. URL: http://www.aiml.net/volumes/volume9/Gore-Ramanayake.pdf.
[16] Rajeev Goré and Revantha Ramanayake. Valentini’s cut-elimination for provability logic resolved. The Review of Symbolic Logic, 5(2):212–238, 2012. doi:10.1017/S1755020311000323.
[17] Ryo Ishigaki and Kentaro Kikuchi. Tree-sequent methods for subintuitionistic predicate logics. In Nicola Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, volume 4548 of Lecture Notes in Computer Science, pages 149–164, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. doi:10.1007/978-3-540-73099-6_13.
[18] Stig Kanger. Provability in logic. Almqvist & Wiksell, 1957.
[19] Ryo Kashima. Cut-free sequent calculi for some tense logics. Studia Logica, 53(1):119–135, 1994. doi:10.1007/BF01053026.
[20] Roman Kuznets and Björn Lellmann. Interpolation for intermediate logics via hyper- and linear nested sequents. In Guram Bezhanishvili, Giovanna D’Agostino, George Metcalfe, and Thomas Studer, editors, Advances in Modal Logic 12, pages 473–492. College Publications, 2018. URL: http://www.aiml.net/volumes/volume12/Kuznets-Lellmann.pdf.
[21] Björn Lellmann. Linear nested sequents, 2-sequents and hypersequents. In Hans De Nivelle, editor, Automated Reasoning with Analytic Tableaux and Related Methods, volume 9323 of Lecture Notes in Computer Science, pages 135–150, Cham, 2015. Springer International Publishing. doi:10.1007/978-3-319-24312-2_10.
[22] Tim Lyon. On the correspondence between nested calculi and semantic systems for intuitionistic logics. Journal of Logic and Computation, 31(1):213–265, December 2020. doi:10.1093/logcom/exaa078.
[23] Tim Lyon. Refining labelled systems for modal and constructive logics with applications. PhD thesis, TU Wien, 2021. URL: https://arxiv.org/abs/2107.14487, arXiv:2107.14487.
[24] Tim Lyon, Alwen Tiu, Rajeev Goré, and Ranald Clouston. Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), volume 152 of Leibniz International Proceedings in Informatics (LIPIcs), pages 28:1–28:16, Dagstuhl, Germany, 2020. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CSL.2020.28.
[25] Tim S. Lyon. Nested sequents for intuitionistic modal logics via structural refinement. In Anupam Das and Sara Negri, editors, Automated Reasoning with Analytic Tableaux and Related Methods, pages 409–427, Cham, 2021. Springer International Publishing. doi:10.1007/978-3-030-86059-2_24.
[26] Tim S. Lyon, Agata Ciabattoni, Didier Galmiche, Dominique Larchey-Wendling, Daniel Méry, Nicola Olivetti, and Revantha Ramanayake. Internal and external calculi: Ordering the jungle without being lost in translations. Found on arXiv, 2023. URL: https://arxiv.org/abs/2312.03426, doi:10.48550/arXiv.2312.03426.
[27] Tim S. Lyon and Eugenio Orlandelli. Nested sequents for quantified modal logics. In Revantha Ramanayake and Josef Urban, editors, Automated Reasoning with Analytic Tableaux and Related Methods, pages 449–467, Cham, 2023. Springer Nature Switzerland. doi:10.1007/978-3-031-43513-3_24.
[28] Tim S. Lyon and Piotr Ostropolski-Nalewaja. Foundations for an abstract proof theory in the context of horn rules. Found on arXiv, 2024. URL: https://arxiv.org/abs/2304.05697, doi:10.48550/arXiv.2304.05697.
[29] Andrea Masini. 2-sequent calculus: A proof theory of modalities. Annals of Pure and Applied Logic, 58(3):229–246, 1992. doi:10.1016/0168-0072(92)90029-Y.
[30] Andrea Masini. 2-sequent calculus: Intuitionism and natural deduction. Journal of Logic and Computation, 3(5):533–562, 1993. doi:10.1093/LOGCOM/3.5.533.
[31] Sara Negri. Proof analysis in modal logic. Journal of Philosophical Logic, 34(5):507–544, 2005. doi:10.1007/s10992-005-2267-3.
[32] Damian Niwiński and Igor Walukiewicz. Games for the $\mu$ -calculus. Theoretical Computer Science, 163(1):99–116, 1996. doi:10.1016/0304-3975(95)00136-0.
[33] Elaine Pimentel, Revantha Ramanayake, and Björn Lellmann. Sequentialising nested systems. In Serenella Cerrito and Andrei Popescu, editors, Automated Reasoning with Analytic Tableaux and Related Methods, volume 11714 of Lecture Notes in Computer Science, pages 147–165, Cham, 2019. Springer International Publishing. doi:10.1007/978-3-030-29026-9_9.
[34] Francesca Poggiolesi. The method of tree-hypersequents for modal propositional logic. In David Makinson, Jacek Malinowski, and Heinrich Wansing, editors, Towards Mathematical Philosophy, volume 28 of Trends in logic, pages 31–51. Springer, 2009. doi:10.1007/978-1-4020-9084-4_3.
[35] Francesca Poggiolesi. A purely syntactic and cut-free sequent calculus for the modal logic of provability. The Review of Symbolic Logic, 2(4):593–611, 2009. doi:10.1017/S1755020309990244.
[36] G. Sambin and S. Valentini. A modal sequent calculus for a fragment of arithmetic. Studia Logica: An International Journal for Symbolic Logic, 39(2/3):245–256, 1980. URL: http://www.jstor.org/stable/20014984.
[37] Giovanni Sambin and Silvio Valentini. The modal logic of provability. the sequential approach. Journal of Philosophical Logic, 11(3):311–342, 1982. URL: http://www.jstor.org/stable/30226252, doi:10.1007/BF00293433.
[38] Krister Segerberg. An Essay in Classical Modal Logic. Uppsala: Filosofiska Föreningen och Filosofiska Institutionen vid Uppsala Universitet, 1971.
[39] D. S. Shamkanov. Circular proofs for the Gödel-Löb provability logic. Mathematical Notes, 96(3):575–585, 2014. doi:10.1134/S0001434614090326.
[40] Alex K Simpson. The proof theory and semantics of intuitionistic modal logic. PhD thesis, University of Edinburgh. College of Science and Engineering. School of Informatics, 1994.
[41] Robert M. Solovay. Provability interpretations of modal logic. Israel Journal of Mathematics, 25(3):287–304, 1976. doi:10.1007/BF02757006.
[42] Lutz Straßburger. Cut elimination in nested sequents for intuitionistic modal logics. In Frank Pfenning, editor, Foundations of Software Science and Computation Structures, volume 7794 of Lecture Notes in Computer Science, pages 209–224, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. doi:10.1007/978-3-642-37075-5_14.
[43] Luca Viganò. Labelled Non-Classical Logics. Springer Science & Business Media, 2000.

Appendix A Proofs for Section 4

Lemma 16.

The following permutations hold in $\mathsf{CSGL}$ :

(1)

If $\mathsf{r}$ is a non-end-active local rule and $\mathsf{r}^{\prime}$ is non-initial and end-active, then $\mathsf{r}$ permutes below $\mathsf{r}^{\prime}$ and $\mathsf{r}^{\prime}$ remains end-active after this permutation;
(2)

if $\mathsf{r}$ is a non-end-active propagation rule and $\mathsf{r}^{\prime}$ is non-initial and end-active, then $\mathsf{r}$ permutes below $\mathsf{r}^{\prime}$ and $\mathsf{r}^{\prime}$ remains end-active after this permutation.

Proof.

Follows from Lemmas 26 and 27 below. $\hfill\blacktriangleleft$

Lemma 26.

If $\mathsf{r}$ is a non-end-active local rule and $\mathsf{r}^{\prime}$ is non-initial and end-active, then $\mathsf{r}$ permutes below $\mathsf{r}^{\prime}$ and $\mathsf{r}^{\prime}$ remains end-active after this permutation.

Proof.

We let $\mathsf{r}$ be an instance of $\neg\mathsf{R}$ as the cases where $\mathsf{r}$ is either $\neg\mathsf{L}$ , $\lor\mathsf{L}$ , or ${\lor}\mathsf{R}$ are shown similarly. We show that $\mathsf{r}$ can be permuted down $\mathsf{r}^{\prime}$ and consider a representative number of cases when $\mathsf{r}^{\prime}$ is either ${\lor}\mathsf{R}$ , $\mathsf{4L}$ , or $\Box\mathsf{R}$ as the remaining cases are similar.

${\lor}\mathsf{R}$ .

By our assumption that $\neg\mathsf{R}$ is non-end-active and ${\lor}\mathsf{R}$ is end-active, we know that the labels $x$ and $y$ are distinct. Hence, we can permute the $\neg\mathsf{R}$ instance below the ${\lor}\mathsf{R}$ instance. Observe that ${\lor}\mathsf{R}$ remains end-active after the permutation.

$\mathsf{4L}$ .

By our assumption, we know that $z$ is distinct from $y$ in the inferences shown below left, meaning, we can permute $\neg\mathsf{R}$ below $\mathsf{4L}$ as shown below right. Observe that $\mathsf{4L}$ remains end-active after the permutation.

$\Box\mathsf{R}$ .

By our assumption, we know that $z$ is distinct from $y$ in the inferences shown below left, meaning, we can permute $\neg\mathsf{R}$ below $\Box\mathsf{R}$ as shown below right. Trivially, the $\Box\mathsf{R}$ rule remains end-active after the permutation.

$\hfill\blacktriangleleft$

Lemma 27.

If $\mathsf{r}$ is a non-end-active propagation rule and $\mathsf{r}^{\prime}$ is non-initial and end-active, then $\mathsf{r}$ permutes below $\mathsf{r}^{\prime}$ and $\mathsf{r}^{\prime}$ remains end-active after this permutation.

Proof.

We consider the case where $\mathsf{r}$ is an instance of $\Box\mathsf{L}$ as the $\mathsf{4L}$ case is similar. We show that $\mathsf{r}$ can be permuted down $\mathsf{r}^{\prime}$ and consider a representative number of cases when $\mathsf{r}^{\prime}$ is either $\neg\mathsf{L}$ , $\mathsf{4L}$ , or $\Box\mathsf{R}$ as the remaining cases are similar.

$\neg\mathsf{L}$ .

By our assumption, we know that $z$ is distinct from $y$ in the inferences below left. We can therefore permute $\Box\mathsf{L}$ below $\neg\mathsf{L}$ as shown below right and we observe that $\neg\mathsf{L}$ remains end-active.

$\mathsf{4L}$ .

Let us suppose we have a $\Box\mathsf{L}$ instance followed by a $\mathsf{4L}$ instance. There are two cases to consider: either the principal formula of $\Box\mathsf{L}$ is the same as for $\mathsf{4L}$ , or the principal formulae are distinct. We show the first case as the second case is similar. Then, our inferences are of the form shown below left, where $y$ and $z$ are distinct due to our assumption. We may permute $\Box\mathsf{L}$ below $\mathsf{4L}$ as shown below right and we observe that $\mathsf{4L}$ remains end-active.

$\Box\mathsf{R}$ .

Suppose we have an instance of $\Box\mathsf{L}$ followed by an application of $\Box\mathsf{R}$ as shown below.

By our assumption, the labels $y$ and $u$ are distinct, meaning, we can permute $\Box\mathsf{L}$ below $\Box\mathsf{R}$ as shown below. Trivially, $\Box\mathsf{R}$ remains end-active after the permutation is performed.

$\hfill\blacktriangleleft$

Theorem 19.

Each end-active proof in $\mathsf{CSGL}$ can be transformed into a proof in $\mathsf{LNGL}$ .

Proof.

We have included additional cases of the inductive step that are not included in the main text.

$\mathsf{4L}$ .

Let us suppose that $\pi$ ends with an application of $\mathsf{4L}$ as shown below.

By IH, we know there exists a path $y_{1},\ldots,y_{n}$ of labels from the root $y_{1}$ to the leaf $y_{n}$ in the premise of $\mathsf{4L}$ such that $\mathcal{G}=\Gamma(y_{1})\vdash\Delta(y_{1})\sslash\cdots\sslash\Gamma(y_{n})% \vdash\Delta(y_{n})$ is provable in $\mathsf{LNGL}$ . Since $\mathsf{4L}$ is end-active, there are three cases to consider: either (1) neither $x$ nor $y$ occur along the path, (2) only $x$ occurs along the path, or (3) both $x$ and $y$ occur along the path. In each case, the conclusion is obtained by taking the linear nested sequent corresponding to the path $y_{1},\ldots,y_{n}$ in the conclusion of the $\mathsf{4L}$ instance above. In the first and second cases, we translate the entire $\mathsf{4L}$ instance as the single linear nested sequent $\mathcal{G}$ . In the third case, we have that $x=y_{n-1}$ and $y=y_{n}$ , meaning, the premise of the $\mathsf{4L}$ instance shown below is provable in $\mathsf{LNGL}$ by IH, where $\Gamma(y_{n-1})=\Sigma_{1},\Box\varphi$ and $\Gamma(y_{n})=\Sigma_{2},\Box\varphi$ . As shown below, a single application of $\mathsf{4L}$ yields the desired conclusion.

$\lor\mathsf{L}$ .

Let us suppose that $\pi$ ends with an instance of $\lor\mathsf{L}$ as shown below.

By IH, we know there exist paths $v=y_{1},\ldots,y_{n}$ and $v=z_{1},\ldots,z_{k}$ of labels from the root $v$ to the leaves $y_{n}$ and $z_{k}$ in the premises of $\lor\mathsf{L}$ such that $\mathcal{G}=\Gamma(v)\vdash\Delta(v)\sslash\cdots\sslash\Gamma(y_{n})\vdash% \Delta(y_{n})$ and $\mathcal{H}=\Gamma(v)\vdash\Delta(v)\sslash\cdots\sslash\Gamma(z_{k})\vdash% \Delta(z_{k})$ are provable in $\mathsf{LNGL}$ . There are two cases to consider: either (1) $x\neq y_{n}$ or $x\neq z_{k}$ , or (2) $x=y_{n}=z_{k}$ . In the first case, if $x\neq y_{n}$ , then we translate the entire $\lor\mathsf{L}$ inference as the single linear nested sequent $\mathcal{G}$ , and if $x\neq z_{k}$ , then we translate the entire $\lor\mathsf{L}$ inference as $\mathcal{H}$ . In the second case, we know that the left premise $\mathcal{G}$ and right premise $\mathcal{H}$ of the $\lor\mathsf{L}$ inference below are provable with $\Gamma(y_{n})=\Sigma,\varphi$ and $\Gamma(z_{k})=\Sigma,\psi$ , and so, a single application of $\lor\mathsf{L}$ gives the desired result.

$\hfill\blacktriangleleft$

Theorem 22.

Every proof in $\mathsf{LNGL}$ can be transformed into a proof in normal form.

Proof.

Let $\pi$ be a proof in $\mathsf{LNGL}$ . We consider an arbitrary instance of a $\Box\mathsf{R}$ rule in $\pi$ and first show that every length-consistent $\mathsf{4L}$ rule above $\Box\mathsf{R}$ can be permuted down into a block $\mathrm{B}$ of $\mathsf{4L}$ rules above $\Box\mathsf{R}$ . Afterward, we will show that every length-consistent $\Box\mathsf{L}$ rule can be permuted down into a block $\mathrm{B}^{\prime}$ of $\Box\mathsf{L}$ rules above $\mathrm{B}$ . As a result, all length-consistent local rules will occurs in a block $\mathrm{B}^{\prime\prime}$ above the premise of the block $\mathrm{B}^{\prime}$ , showing that $\Box\mathsf{R}$ is preceded be a complete block. As these permutations can be performed for every $\Box\mathsf{R}$ instance in $\pi$ , we obtain a normal form proof as the result.

Let us choose an application of $\Box\mathsf{R}$ in $\pi$ , as shown below, proceeded by a (potentially empty) block $\mathrm{R}$ of $\mathsf{4L}$ rules.

We now select a bottom-most, length-consistent application of a $\mathsf{4L}$ rule above the chosen $\Box\mathsf{R}$ application that does not occur within the block $\mathrm{R}$ of $\mathsf{4L}$ rules. We show that $\mathsf{4L}$ can be permuted below every local rule and $\Box\mathsf{L}$ rule until it reaches and joins the $\mathrm{R}$ block. We show that $\mathsf{4L}$ can be permuted below $\neg\mathsf{R}$ , $\lor\mathsf{L}$ , and $\Box\mathsf{L}$ as the remaining cases are similar. Note that we are guaranteed that no other $\Box\mathsf{R}$ applications occur below $\mathsf{4L}$ and above $\mathrm{R}$ since then $\mathsf{4L}$ would not be length-consistent with the chosen $\Box\mathsf{R}$ application.

Suppose $\mathsf{4L}$ occurs above a $\neg\mathsf{R}$ application as shown below left. The rules can be permuted as shown below right.

Suppose that we have $\mathsf{4L}$ followed by an application of the $\lor\mathsf{L}$ rule.

Invoking the hp-invertibility of $\mathsf{4L}$ (Lemma 14), we can permute $\mathsf{4L}$ below $\lor\mathsf{L}$ as shown below.

Last, we show (below left) one of the cases where $\mathsf{4L}$ is applied above a $\Box\mathsf{L}$ rule. We can permute the rules as shown below right.

We can repeat the above downward permutations of bottom-most, length-consistent $\mathsf{4L}$ rules, so that all length-consistent $\mathsf{4L}$ rules occur in a block $\mathrm{B}$ above $\Box\mathsf{R}$ as shown below, where we let $\mathrm{R}^{\prime}$ be a (potentially empty) block of $\Box\mathsf{L}$ rules above the $\mathrm{B}$ block of $\mathsf{4L}$ rules.

Next we show that every length-consistent $\Box\mathsf{L}$ rule occurring above the block $\mathrm{R}^{\prime}$ can be permuted down to the block $\mathrm{R}^{\prime}$ . Let $\Box\mathsf{L}$ occur above the block $\mathrm{R}^{\prime}$ be length-consistent with the chosen $\Box\mathsf{R}$ rule. Notice that we need only consider downward permutations of $\Box\mathsf{L}$ rules with local rules as all $\mathsf{4L}$ rules have already been permuted downward and no other $\Box\mathsf{R}$ rule can occur between $\Box\mathsf{L}$ and $\mathrm{R}^{\prime}$ because then $\Box\mathsf{L}$ would not be length-consistent. We show how to permute the $\Box\mathsf{L}$ rule below a $\lor\mathsf{L}$ instance; the remaining cases are simple and similar.

By using the hp-invertibility of $\Box\mathsf{L}$ (Lemma 14), we can permute $\Box\mathsf{L}$ below the $\lor\mathsf{L}$ rule.

By successively permuting all $\Box\mathsf{L}$ rules down into a block above $\mathrm{B}$ , we have that $\Box\mathsf{R}$ is preceded by a complete block in the proof. As argued above, this implies that every proof in $\mathsf{LNGL}$ can be put into normal form. $\hfill\blacktriangleleft$

[bib.bib1] [1] Bahareh Afshari and Graham E. Leigh. Cut-free completeness for modal mu-calculus. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–12, 2017. doi:10.1109/LICS.2017.8005088.

[bib.bib2] [2] Arnon Avron. On modal systems having arithmetical interpretations. Journal of Symbolic Logic, 49(3):935–942, 1984. doi:10.2307/2274147.

[bib.bib3] [3] James Brotherston. Cyclic proofs for first-order logic with inductive definitions. In Bernhard Beckert, editor, Automated Reasoning with Analytic Tableaux and Related Methods, pages 78–92, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. doi:10.1007/11554554_8.

[bib.bib4] [4] James Brotherston. Formalised inductive reasoning in the logic of bunched implications. In Hanne Riis Nielson and Gilberto Filé, editors, Static Analysis, pages 87–103, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. doi:10.1007/978-3-540-74061-2_6.

[bib.bib5] [5] James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177–1216, October 2010. doi:10.1093/logcom/exq052.

[bib.bib6] [6] Kai Brünnler. Deep sequent systems for modal logic. Archive for Mathematical Logic, 48(6):551–577, 2009. doi:10.1007/s00153-009-0137-3.

[bib.bib7] [7] Robert A. Bull. Cut elimination for propositional dynamic logic without *. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 38(2):85–100, 1992. doi:10.1002/MALQ.19920380107.

[bib.bib8] [8] Marcos A Castilho, Luis Farinas del Cerro, Olivier Gasquet, and Andreas Herzig. Modal tableaux with propagation rules and structural rules. Fundamenta Informaticae, 32(3, 4):281–297, 1997. doi:10.3233/FI-1997-323404.

[bib.bib9] [9] Agata Ciabattoni, Tim Lyon, Revantha Ramanayake, and Alwen Tiu. Display to labelled proofs and back again for tense logics. ACM Transactions on Computational Logic, 22(3):1–31, 2021. doi:10.1145/3460492.

[bib.bib10] [10] Anupam Das and Marianna Girlando. Cyclic hypersequent system for transitive closure logic. Journal of Automated Reasoning, 67(3):27, 2023. doi:10.1007/s10817-023-09675-1.

[bib.bib11] [11] Anupam Das, Iris van der Giessen, and Sonia Marin. Intuitionistic Gödel-Löb Logic, à la Simpson: Labelled Systems and Birelational Semantics. In Aniello Murano and Alexandra Silva, editors, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), volume 288 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1–22:18, Dagstuhl, Germany, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CSL.2024.22.

[bib.bib12] [12] Melvin Fitting. Tableau methods of proof for modal logics. Notre Dame Journal of Formal Logic, 13(2):237–247, 1972. doi:10.1305/NDJFL/1093894722.

[bib.bib13] [13] Melvin Fitting. Nested sequents for intuitionistic logics. Notre Dame Journal of Formal Logic, 55(1):41–61, 2014. doi:10.1215/00294527-2377869.

[bib.bib14] [14] Rajeev Goré, Linda Postniece, and Alwen Tiu. Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. In Carlos Areces and Robert Goldblatt, editors, Advances in Modal Logic 7, pages 43–66. College Publications, 2008. URL: http://www.aiml.net/volumes/volume7/Gore-Postniece-Tiu.pdf.

[bib.bib15] [15] Rajeev Goré and Revantha Ramanayake. Labelled tree sequents, tree hypersequents and nested (deep) sequents. In Thomas Bolander, Torben Braüner, Silvio Ghilardi, and Lawrence S. Moss, editors, Advances in Modal Logic 9, pages 279–299. College Publications, 2012. URL: http://www.aiml.net/volumes/volume9/Gore-Ramanayake.pdf.

[bib.bib16] [16] Rajeev Goré and Revantha Ramanayake. Valentini’s cut-elimination for provability logic resolved. The Review of Symbolic Logic, 5(2):212–238, 2012. doi:10.1017/S1755020311000323.

[bib.bib17] [17] Ryo Ishigaki and Kentaro Kikuchi. Tree-sequent methods for subintuitionistic predicate logics. In Nicola Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, volume 4548 of Lecture Notes in Computer Science, pages 149–164, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. doi:10.1007/978-3-540-73099-6_13.

[bib.bib18] [18] Stig Kanger. Provability in logic. Almqvist & Wiksell, 1957.

[bib.bib19] [19] Ryo Kashima. Cut-free sequent calculi for some tense logics. Studia Logica, 53(1):119–135, 1994. doi:10.1007/BF01053026.

[bib.bib20] [20] Roman Kuznets and Björn Lellmann. Interpolation for intermediate logics via hyper- and linear nested sequents. In Guram Bezhanishvili, Giovanna D’Agostino, George Metcalfe, and Thomas Studer, editors, Advances in Modal Logic 12, pages 473–492. College Publications, 2018. URL: http://www.aiml.net/volumes/volume12/Kuznets-Lellmann.pdf.

[bib.bib21] [21] Björn Lellmann. Linear nested sequents, 2-sequents and hypersequents. In Hans De Nivelle, editor, Automated Reasoning with Analytic Tableaux and Related Methods, volume 9323 of Lecture Notes in Computer Science, pages 135–150, Cham, 2015. Springer International Publishing. doi:10.1007/978-3-319-24312-2_10.

[bib.bib22] [22] Tim Lyon. On the correspondence between nested calculi and semantic systems for intuitionistic logics. Journal of Logic and Computation, 31(1):213–265, December 2020. doi:10.1093/logcom/exaa078.

[bib.bib23] [23] Tim Lyon. Refining labelled systems for modal and constructive logics with applications. PhD thesis, TU Wien, 2021. URL: https://arxiv.org/abs/2107.14487, arXiv:2107.14487.

[bib.bib24] [24] Tim Lyon, Alwen Tiu, Rajeev Goré, and Ranald Clouston. Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), volume 152 of Leibniz International Proceedings in Informatics (LIPIcs), pages 28:1–28:16, Dagstuhl, Germany, 2020. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CSL.2020.28.

[bib.bib25] [25] Tim S. Lyon. Nested sequents for intuitionistic modal logics via structural refinement. In Anupam Das and Sara Negri, editors, Automated Reasoning with Analytic Tableaux and Related Methods, pages 409–427, Cham, 2021. Springer International Publishing. doi:10.1007/978-3-030-86059-2_24.

[bib.bib26] [26] Tim S. Lyon, Agata Ciabattoni, Didier Galmiche, Dominique Larchey-Wendling, Daniel Méry, Nicola Olivetti, and Revantha Ramanayake. Internal and external calculi: Ordering the jungle without being lost in translations. Found on arXiv, 2023. URL: https://arxiv.org/abs/2312.03426, doi:10.48550/arXiv.2312.03426.

[bib.bib27] [27] Tim S. Lyon and Eugenio Orlandelli. Nested sequents for quantified modal logics. In Revantha Ramanayake and Josef Urban, editors, Automated Reasoning with Analytic Tableaux and Related Methods, pages 449–467, Cham, 2023. Springer Nature Switzerland. doi:10.1007/978-3-031-43513-3_24.

[bib.bib28] [28] Tim S. Lyon and Piotr Ostropolski-Nalewaja. Foundations for an abstract proof theory in the context of horn rules. Found on arXiv, 2024. URL: https://arxiv.org/abs/2304.05697, doi:10.48550/arXiv.2304.05697.

[bib.bib29] [29] Andrea Masini. 2-sequent calculus: A proof theory of modalities. Annals of Pure and Applied Logic, 58(3):229–246, 1992. doi:10.1016/0168-0072(92)90029-Y.

[bib.bib30] [30] Andrea Masini. 2-sequent calculus: Intuitionism and natural deduction. Journal of Logic and Computation, 3(5):533–562, 1993. doi:10.1093/LOGCOM/3.5.533.

[bib.bib31] [31] Sara Negri. Proof analysis in modal logic. Journal of Philosophical Logic, 34(5):507–544, 2005. doi:10.1007/s10992-005-2267-3.

[bib.bib32] [32] Damian Niwiński and Igor Walukiewicz. Games for the $\mu$ -calculus. Theoretical Computer Science, 163(1):99–116, 1996. doi:10.1016/0304-3975(95)00136-0.

[bib.bib33] [33] Elaine Pimentel, Revantha Ramanayake, and Björn Lellmann. Sequentialising nested systems. In Serenella Cerrito and Andrei Popescu, editors, Automated Reasoning with Analytic Tableaux and Related Methods, volume 11714 of Lecture Notes in Computer Science, pages 147–165, Cham, 2019. Springer International Publishing. doi:10.1007/978-3-030-29026-9_9.

[bib.bib34] [34] Francesca Poggiolesi. The method of tree-hypersequents for modal propositional logic. In David Makinson, Jacek Malinowski, and Heinrich Wansing, editors, Towards Mathematical Philosophy, volume 28 of Trends in logic, pages 31–51. Springer, 2009. doi:10.1007/978-1-4020-9084-4_3.

[bib.bib35] [35] Francesca Poggiolesi. A purely syntactic and cut-free sequent calculus for the modal logic of provability. The Review of Symbolic Logic, 2(4):593–611, 2009. doi:10.1017/S1755020309990244.

[bib.bib36] [36] G. Sambin and S. Valentini. A modal sequent calculus for a fragment of arithmetic. Studia Logica: An International Journal for Symbolic Logic, 39(2/3):245–256, 1980. URL: http://www.jstor.org/stable/20014984.

[bib.bib37] [37] Giovanni Sambin and Silvio Valentini. The modal logic of provability. the sequential approach. Journal of Philosophical Logic, 11(3):311–342, 1982. URL: http://www.jstor.org/stable/30226252, doi:10.1007/BF00293433.

[bib.bib38] [38] Krister Segerberg. An Essay in Classical Modal Logic. Uppsala: Filosofiska Föreningen och Filosofiska Institutionen vid Uppsala Universitet, 1971.

[bib.bib39] [39] D. S. Shamkanov. Circular proofs for the Gödel-Löb provability logic. Mathematical Notes, 96(3):575–585, 2014. doi:10.1134/S0001434614090326.

[bib.bib40] [40] Alex K Simpson. The proof theory and semantics of intuitionistic modal logic. PhD thesis, University of Edinburgh. College of Science and Engineering. School of Informatics, 1994.

[bib.bib41] [41] Robert M. Solovay. Provability interpretations of modal logic. Israel Journal of Mathematics, 25(3):287–304, 1976. doi:10.1007/BF02757006.

[bib.bib42] [42] Lutz Straßburger. Cut elimination in nested sequents for intuitionistic modal logics. In Frank Pfenning, editor, Foundations of Software Science and Computation Structures, volume 7794 of Lecture Notes in Computer Science, pages 209–224, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. doi:10.1007/978-3-642-37075-5_14.

[bib.bib43] [43] Luca Viganò. Labelled Non-Classical Logics. Springer Science & Business Media, 2000.

Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Outline of Paper.

2 Gödel-Löb Provability Logic

Definition 1 (Model).

Definition 2 (Semantic Clauses).

3 Labeled and Tree Sequent Systems

3.1 Labeled Sequents

Definition 3 (Labeled Sequent Semantics).

▶ Remark 4.

▶ Remark 5.

Theorem 6 (𝖦𝟥𝖦𝖫 Properties [31]).

3.2 Labeled Tree Sequents

Definition 7 (Tree Sequent Calculus 𝖢𝖲𝖦𝖫).

▶ Remark 8.

Theorem 9 (𝖢𝖲𝖦𝖫 Properties [35]).

Observation 10 ([15]).

Theorem 11 ([15]).

4 Linearizing Tree Sequents in Proofs

Theorem 12.

Lemma 13.

Lemma 14.

From Tree Sequents to Linear Nested Sequents

Definition 15 (End Active).

Lemma 16.

▶ Remark 17.

Theorem 18.

Theorem 19.

Proof.

Base case.

Inductive step.

□⁢𝗟.

□⁢𝗥.

Corollary 20 (𝖫𝖭𝖦𝖫 Soundness and Completeness).

Definition 21 (Normal Form).

Theorem 22.

5 Sequent Systems and Correspondences

5.1 Gentzen, Cyclic, and Non-Wellfounded Systems

Theorem 23 ([39]).

5.2 Completing the Correspondences

Theorem 24.

Proof.

Theorem 25.

Proof.

6 Concluding Remarks

References

Appendix A Proofs for Section 4

Lemma 16.

Proof.

Lemma 26.

Proof.

∨𝗥.

𝟰⁢𝗟.

□⁢𝗥.

Lemma 27.

Proof.

¬𝗟.

𝟰⁢𝗟.

□⁢𝗥.

Theorem 19.

Proof.

𝟰⁢𝗟.

∨𝗟.

Theorem 22.

Proof.

$\blacktriangleright$ Remark 4.

$\blacktriangleright$ Remark 5.

Theorem 6 ( $\mathsf{G3GL}$ Properties [31]).

Definition 7 (Tree Sequent Calculus $\mathsf{CSGL}$ ).

$\blacktriangleright$ Remark 8.

Theorem 9 ( $\mathsf{CSGL}$ Properties [35]).

$\blacktriangleright$ Remark 17.

$\Box\mathsf{L}$ .

$\Box\mathsf{R}$ .

Corollary 20 ( $\mathsf{LNGL}$ Soundness and Completeness).

${\lor}\mathsf{R}$ .

$\mathsf{4L}$ .

$\Box\mathsf{R}$ .

$\neg\mathsf{L}$ .

$\mathsf{4L}$ .

$\Box\mathsf{R}$ .

$\mathsf{4L}$ .

$\lor\mathsf{L}$ .