{'fraction_non_alphanumeric': 0.07024986914240061, 'fraction_numerical': 0.012975564065125761, 'mean_word_length': 3.9067315490673153, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 12, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Nested Sequents for First-Order Modal Logics via Reachability Rules

We introduce (cut-free) nested sequent systems for first-order modal logics that admit increasing, decreasing, constant, and empty domains along with so-called general path conditions and seriality. We obtain such systems by means two devices: 'reachability rules' and 'structural refinement.' Regarding the former device, we introduce reachability rules as special logical rules parameterized with formal grammars (viz. semi-Thue systems) that operate by propagating formulae and/or checking if data exists along certain paths within a nested sequent, where paths are encoded as strings generated by a parameterizing grammar. Regarding the latter device, structural refinement is a relatively new methodology used to extract nested sequent systems from labeled systems (which are ultimately obtained from a semantics) by means of eliminating structural/relational rules, introducing reachability rules, and then carrying out a notational translation. We therefore demonstrate how this method can be extended to the setting of first-order modal logics, and expose how reachability rules naturally arise from applying this method.


Introduction
Analytic proof systems consist of sets of inference rules that stepwise (de)compose logical theorems. Such proof systems not only facilitate reasoning within a given logic, but have proven useful for establishing (meta-)logical properties of logics as well as for developing automated reasoning tools. One of the most prominent formalisms for constructing analytic proof systems is Gentzen's sequent calculus [15,16], which utilizes (pairs of) multisets of formulae, called sequents, to carry out proofs of logical theorems. Since its introduction, Gentzen's formalism has been generalized to supply ever more expressive logics with analytic proof systems. Such extensions include display calculi [2], hypersequent calculi [1], labeled calculi [36,38], and nested calculi [5,22], all of which have been exploited to establish meaningful results such as decidability [4,37], interpolation [11,26], complexity hardness [29], and automated counter-model extraction [27,37]. In this paper, we will be primarily concerned with the labeled sequent and nested sequent formalisms. Labeled sequent calculi generalize Gentzen's formalism by integrating semantic elements of a logic into the the syntax of sequents (cf. [21]). As such, labeled sequents can typically be viewed as graphs of Gentzen-style sequents, that is, graphs of (pairs of) multisets of logical formulae. This idea of defining inference rules over graphs of sequents has proven fruitful for More recently, it was discovered that nested sequent calculi could be extracted from labeled sequent calculi with the properties of the former transferred to the latter [7,19,33]. This discovery led to the formulation of a methodology referred to as structural refinement [24,25,27,28], which consists of two parts: first, one leverages general results regarding the (automated) construction of labeled sequent calculi (in possession of favorable properties) for a class of logics based on their semantics. Second, one transforms the labeled calculi into nested calculi via the introduction of propagation or reachability rules (cf. [6,9,25]) and the elimination of structural rules, followed by a notational translation. This entire process yields a method of transforming the semantics of a logic into a (cut-free) nested sequent calculus for the logic, being used to provide new and previously unknown nested sequent calculi [28]. Although this method has been investigated and put to use for a variety of different propositional modal logics, it has yet to be applied to first-order modal logics. Thus, the first contribution of this paper is the application and study of structural refinement in the setting of first-order modal logics, being used to obtain (to the best of the author's knowledge) the first (cut-free) nested sequent systems for such logics.
As in the propositional setting, first-order modal logics admit a Kripke-style semantics, but unlike in the propositional setting, each world is associated with a domain of elements used to interpret quantificational formulae [23]. One may then characterize distinct first-order modal logics by either imposing frame conditions on the accessibility relation of the model (as with propositional modal logics), or by imposing conditions on the domains associated with worlds [3,12]. Regarding the latter, one obtains distinct first-order modal logics depending on if domains are permitted to be empty, if domains are permitted to increase or decrease along the accessibility relation, or if domains are required to be constant. In this paper, we consider a class of first-order modal logics that consists of extensions of a base logic QK [3] with seriality, general path conditions [7], and the aforementioned domain conditions.
In order to give this class of logics a uniform nested sequent presentation, we make use of so-called reachability rules-a class of rules identified in [25], which possess two kinds of functionality: such rules may (i) propagate formulae along certain paths, and/or (ii) search for data along certain paths, within a labeled or nested sequent. The first kind of functionality is exhibited by the well-known class of propagation rules [6,9,18], which have proven vital for the provision of nested sequent systems for propositional modal and constructive logics [7,17,18,27]. Rules exhibiting the second kind of functionality have only been defined more recently [10,24,25]. Thus, reachability rules subsume the class of propagation rules, allowing for either or both kinds of functionality [25].
Our second contribution in this paper is the formulation of reachability rules for managing the introduction of quantificational formulae in labeled sequent and nested sequent proofs. Motivated by the work in [18,27], we parameterize such rules with semi-Thue systems [35] (i.e. certain types of context-free grammars), which encode along what paths formulae may be propagated and along what paths a rule should search for data. Such rules endow our nested sequent systems with a high degree of modularity as one nested sequent calculus for a first-order modal logic may be straightforwardly converted into a nested sequent calculus for another first-order modal logic by simply parameterizing the reachability rules with alternative semi-Thue systems.
The paper is organized as follows: In Section 2, we define the considered class of first-order modal logics, as well as provide the grammar theoretical foundations for the formulation of our reachability rules. In Section 3, we present equivalent variants of the labeled sequent systems for first-order modal logics given by [32,Chapter 12.1] and [38,Chapter 6]. In the subsequent section (Section 4), we show how to define reachability rules in the context of labeled sequents (the first contribution of the paper), and apply the structural refinement methodology to derive nested sequent calculi from the given labeled calculi. In the penultimate section (Section 5), our nested sequent calculi for first-order modal logics are defined (the second contribution of the paper), and in the final section (Section 6) we conclude.

First-order Modal Logics
We let Var := {x, y, z, . . .} be a denumerable set of variables and Φ := {p, q, r, . . .} be a set of denumerably many predicates of each arity n ∈ N with propositional variables predicates of arity zero. Atomic formulae are of form p(x 1 , . . . , x n ), and we will often write them as p( x). Similarly, we often write a list of variables x 1 , . . . , x n as x. The first-order modal language L is the set of formulae generated via the following grammar in BNF: where p ranges over Φ, and the variables x = x 1 , . . . , x n and x range over the set Var. We refer to a formula in L as an L-formula, and define ϕ → ψ := ¬ϕ ∨ ψ, ϕ := ¬♦¬ϕ, and ∀xϕ := ¬∃x¬ϕ. As usual, we say that the occurrence of a variable x in ϕ is free given that x does not occur within the scope of a quantifier. Also, we let ϕ[y/x] denote the substitution of the variable y for each free occurrence of the variable x in ϕ.

23:4
Nested Sequents for First-Order Modal Logics via Reachability Rules non-empty domains iff for each w ∈ W , D(w) = ∅. We define a model M based on a frame F to be an ordered pair (F, V ) where F is a frame and V is a valuation function such that V (p, w) ⊆ D(w) n with n ∈ N. 1 We make the simplifying assumption that for each world w ∈ W , D(w) 0 = {()} with () the empty tuple, meaning  We define the base logic QK to be the set of all valid L-formulae over the class of all frames. We consider extensions of QK by imposing a set C of frame conditions (shown in Figure 1 with their corresponding axioms) on the class of all frames. Following the top-down order of Figure 1, such frame conditions include: (1) the seriality condition S, (2) generalized path conditions G(n, k) := ∀w, u, v(wR n u ∧ wR k v → uRv) with n, k ∈ N, (3) the increasing domain condition I d (with the Barcan formula as the corresponding axiom), (4) the decreasing domain condition D d (with the converse Barcan formula as the corresponding axiom), (5) the constant domain condition C d , and (6) the non-empty domain condition N d . 2 We use G(n, k) to denote a generalized path condition, use G to denote a set of such conditions, and note that such conditions cover well-known properties such as reflexivity (when n = k = 0), transitivity (when k = 2 and n = 0), symmetry (when n = 1 and k = 0), and Euclideanity (when n = k = 1). For a set C of frame conditions, we define F C to be the class of frames satisfying C, and we define the logic QK(C) to be the set of all valid L-formulae over the class F C (with QK(∅) = QK). We make the simplifying assumption that C d ∈ C iff I d , D d ∈ C so that we may discuss C d purely in terms of I d and D d throughout the remainder of the paper.

Grammar-theoretic Preliminaries
As will be seen in subsequent sections, a significant aspect of our nested calculi is the incorporation of inference (viz. reachability) rules whose applicability depends upon certain strings generated by a formal grammar. Therefore, the current section introduces the grammar-theoretic notions required to properly define such rules.
We define our alphabet Σ := {♦, } to be the set of characters ♦ and , and we let ? ∈ Σ. We make use of the symbols ♦ and to encode information in inference rules about worlds 1 We note that D(w) n is the n-ary Cartesian product D(w) × · · · × D(w) n . 2 For an introduction to first-order modal logics, frame conditions, and corresponding axioms, see Fitting and Mendelsohn [12].

Figure 1
Axioms and their related frame conditions. We note that when n = 0, the second frame condition is ∀w, v(wR k v → wRv), when k = 0, the frame condition is ∀w, u(wR n u → uRw), and when n = k = 0, the frame condition is ∀w(wRw).
in the future and past (resp.) of an accessibility relation R in a model. We note that these symbols were adapted from the work in [18], and their usage mirrors their analogous meaning in the context of tense logics [18,22]. Additionally, we say that ♦ and are converses, and define the converse operation · −1 (on characters) as ♦ −1 := and −1 := ♦.
We let · denote the typical concatenation operation with ε the empty string. The set Σ * of strings over Σ is defined to be the smallest set satisfying the following conditions: (i) Σ ∪ {ε} ⊆ Σ * , and (ii) If s ∈ Σ * and ? ∈ Σ, then s · ? ∈ Σ * . We use s, t, r, . . . (potentially annotated) to denote strings from Σ * . Also, we will often write the concatenation of two strings s and t as st as opposed to s · t, and for the empty string ε, we have sε = εs = s. The converse operation on strings (adapted from [37]) is defined on strings accordingly: (i) ε −1 := ε, and (ii) If s = ? 1 · · · ? n , then s −1 := ?
We now define Semi-Thue systems [35], which encode information about the conditions imposed on frames and models, and which will parameterize inference rules in our nested sequent systems.

Definition 3 (Semi-Thue System).
We define a Semi-Thue System to be a set S of production rules of the form ? −→ s, where ? ∈ Σ and s ∈ Σ * .
Specific Semi-Thue systems will be of use to us in this paper. In particular, for a set G of generalized path conditions, we define the Semi-Thue system S(G) as follows We also define the Semi-Thue systems S4 : and describe their significance shortly; first, we define the notion of a derivation and a language in the context of Semi-Thue systems.
Definition 4 (Derivation, Language). Let S be an Semi-Thue system. We write s −→ t and say that the string t may be derived from the string s in Σ * in one-step iff there are strings s , t ∈ Σ * and ? −→ r ∈ S such that s = s ? t and t = s rt . We define the derivation relation −→ * S to be the reflexive and transitive closure of −→. For s, t ∈ Σ * , we call s −→ * S t a derivation of t from s, and define the length of a derivation to be the minimal number of one-step derivations required to derive t from s in S. Last, we define the language As noted in [25, p. 143], S4 encodes a notion of directed reachability and S5 encodes a notion of undirected reachability. Given a frame, recognizing what worlds are reachable from one another along paths of the accessibility relation R is relevant in our context as frame C V I T 2 0 1 6

23:6
Nested Sequents for First-Order Modal Logics via Reachability Rules The labeled calculus G3QK. The side condition † 1 ( † 2 ) states that the rule is applicable only if u (y, resp.) is fresh, i.e. u (y, resp.) does not occur in the conclusion of the rule.
conditions such as G(n, k) connect initial and terminal worlds, and I d , D d , and C d require domains to contain certain elements along R-paths. To see how S4 and S5 encode notions of (un)directed reachability, let us think of ♦ as representing a forward move along the accessibility relation of a model, and as representing a backward move along the accessibility relation. Then, S4 defines the languages L S4 (♦) = {♦ n | n ∈ N} and L S4 ( ) = { n | n ∈ N}, where each string ♦ n and n (denoting a sequence of n ♦'s and n 's, respectively, with ♦ 0 = 0 = ε) 'connects' a world w and u if u can be reached in n forward moves or backward moves (resp.) along the accessibility relation from w. Similarly, S5 defines the language L S5 (♦) = L S5 ( ) = Σ * where each string ? 1 · · · ? n 'connects' a world w to u if u can be reached in n forward and/or backward moves along the accessibility relation from w.

Labeled Sequent Systems
We introduce equivalent variants (within our logical signature) of the labeled sequent systems given in [38,Chapter 6] and [32, Chapter 12.1] for first-order modal logics. These systems utilize a denumerable set Lab := {w, u, v, . . .} of labels (which are occasionally annotated) and are comprised of inference rules that encode the semantics of first-order modal logics. Moreover, such inference rules operate on labeled sequents, that is, formulae of the form Λ := R, Γ ∆, where R is a multiset containing both relational atoms of the form wRu and domain atoms of the form x ∈ D(w), and Γ and ∆ are multisets of labeled formulae of the form w : ϕ, where x ranges over Var, w and u range over Lab, and ϕ ranges over L. Given a multiset R of relational atoms, we let Lab(R) be the set all labels occurring in R.
In addition, we define the composition of two labeled sequents as 3 Last, to increase notational concision, we define a sequence of relational atoms wR n u := wRw 1 , w 1 Rw 2 , . . . , w n−1 Ru, for n ∈ N, and note that wR 0 u := (w = u).
The labeled calculus G3QK for the logic QK is given in Figure 2, and consists of the initial rules (ax) and (⊥ l ), and pairs of left and right logical rules for each logical connective. To obtain labeled systems for extensions of QK with a set C of frame conditions, i.e. for a logic QK(C), we extend G3QK with relational rules, presented in Figure 3, and which are types of geometric structural rules [36, p. 126]. Note that G3QK(∅) = G3QK. We refer to formulae that are explicitly presented in premise(s) and conclusion of a rule as active; e.g. y ∈ D(w), w : ϕ[y/x], and w : ♦ϕ are active in (∃ l ). Also, the height of a proof is defined in the usual way as the longest sequence of sequents from the conclusion of a proof to an initial sequent (cf. [32]). When extending G3QK with relational rules, we refer to the resulting calculus as G3QK(C), which is obtained in the following manner: Furthermore, when n = 0 or k = 0 in (g n,k ), i.e. when G(0, k) ∈ C, G(n, 0) ∈ C, or G(0, 0) ∈ C, the relational rules (g 0,k ), (g n,0 ), and (g 0,0 ) are defined accordingly: Proof. Proven in the same manner as the soundness theorem (Theorem 12.13) and completeness theorem (Theorem 12.14) of [32, Chapter 12.1].

Structural Refinement
We now structurally refine the labeled systems of the previous section, that is, we expand each calculus G3QK(C) with a set of reachability rules (generalized versions of the (♦ r ) and (∃ l ) rules) that permit the elimination of relational rules (viz. (g n,k ), (id), (dd), and (nd)) from any given derivation. This process is an instance of a methodology introduced in [25] to derive nested systems from labeled systems, and begets 'refined' labeled calculi (each dubbed QK(C)L), which only utilize labeled sequents of a 'treelike' structure in proofs. The reachability rules we introduce are based on those of [7,18,24,25], and possess a rather complex functionality that will be detailed in the first half of this section with an example given below. In particular, our reachability rules view labeled sequents as automata, and enable formulae to be (bottom-up) introduced to a labeled sequent given that certain paths of relational atoms (corresponding to strings generated by a Semi-Thue system) exist in a sequent. To make the functionality of such rules precise, we define propagation graphs and propagation paths-concepts initially defined in the context of display and nested calculi [18], and subsequently transported to the setting of labeled calculi [7,27].  Figure 4 Labeled reachability rules. The side condition † 1 (C) is defined in Definition 9, † 2 (C) is defined in Figure 5, and † 3 (C) is defined in Figure 6. Definition 6 (Propagation Graph). We define a propagation graph of a labeled sequent Λ := R, Γ ∆ to be a pair P G(R) := (V, E) such that (i) (w, Θ) ∈ V iff w ∈ Lab(R), Θ = {x 1 , . . . , x n } ⊂ Var, and x 1 ∈ D(w), . . . , x n ∈ D(w) are all domain atoms in R associated with the label w, and (ii) (w, ♦, u), (u, , w) ∈ E iff wRu ∈ R. We will often write w ∈ P G(R) to mean w ∈ V , and (w, ? , u) ∈ P G(R) to mean (w, ? , u) ∈ E.
Definition 7 (Propagation Path [28]). Let Λ := R, Γ ∆ be a labeled sequent. We define a propagation path from w 1 to w n in P G(R) := (V, E) to be a sequence of the following form: Given a propagation path as above, we define its converse as shown below top and its string as shown below bottom: We let ε(w, w) := w represent an empty path with its string defined as s ε (w, w) := ε.
With the above notions, we can now define the operation of our reachability rules (p ♦ ), (s 1 ∃ ), and (s 2 ∃ ) which are displayed in Figure 4. We remark that the side conditions dictating the operation of such rules are specified in Definition 9 below. As mentioned in the introduction, reachability rules incorporate two kinds of functionality: (i) the propagation of formulae along paths within a sequent, and (ii) the search of data along paths within a sequent. Reachability rules that only incorporate the first kind of functionality are wellknown in the literature, and constitute propagation rules [6,9,18,36]. In this regard, (p ♦ ) serves as a propagation rule proper, being an instance of the propagation rule (Prop) defined in [7, p. 24]. On the other hand, rules that incorporate the second kind of functionality have only been defined more recently [10,24,25]. In this regard, (s 1 ∃ ) and (s 2 ∃ ) serve as reachability rules; although such rules only exhibit the second kind of functionality, we do note that reachability rules mixing both kinds of functionality do exist, having been defined for first-order intuitionistic logics [25].
Each rule (p ♦ ), (s 1 ∃ ), and (s 2 ∃ ) relies on a side condition (see Definition 9 below) that checks to see if a propagation path of a certain shape exists within the propagation graph of a labeled sequent. For a labeled sequent Λ := R, Γ ∆ and a semi-Thue system S, such conditions typically involve a statement of the following form: There exists a propagation path π(w, u) from w to u in the propagation graph P G(R) such that the string s π (w, u) is in the language L S ( ? ). We will express this statement in a concise manner as shown below: In addition, (s 1 ∃ ) and (s 2 ∃ ) rely on an availability notion (cf. [10,25]), which employs statements of the above shape.

Figure 5
The side condition † 2 (C) for (s 1 ∃ ), which depends on the contents of C.
Let us now formally specify the side conditions † 1 (C) - † 3 (C) imposed on the (p ♦ ), (s 1 ∃ ), and (s 2 ∃ ) rules, which depend upon the frame conditions present in C.
For the (s 1 ∃ ) and (s 2 ∃ ) rules, the side condition depends on if I d and D d occur within C or not. The conditions for (s 1 ∃ ) and (s 2 ∃ ) are presented in Figure 5 and Figure 6, respectively.
Remark 11. The (♦ r ) and (∃ r ) rules are instances of (p ♦ ) and (s 1 ∃ ), respectively, and thus we may disregard such rules. Also, notice that if I d , D d , ∈ C (meaning, C d ∈ C as discussed at the end of Section 2.1), then (s 1 ∃ ) is identical to the (∃ r ) rule and (s 2 ∃ ) corresponds to an application of (∃ r ) followed by an application of (nd) (given that N d ∈ C). Definition 12 (Refined Labeled Calculus). Let G = {G(n, k) | G(n, k) ∈ C}. We define the refined labeled calculus QK(C)L := In other words, QK(C)L extends G3QK(C) with the (p ♦ ) and (s 1 ∃ ) rules regardless, but only includes (s 2 ∃ ) iff N d ∈ C, and excludes the (g n,k ), (id), (dd), and (nd) relational rules.
We now argue that each refined labeled calculus QK(C)L is complete by means of a proof transformation procedure. In particular, we show that through the elimination of relational rules and the introduction of reachability rules, any proof in G3QK(C) can be transformed into a proof in QK(C)L. To provide intuition, we begin by showing how a concrete proof in G3QK(C) can be transformed into a proof in QK(C)L, and afterward, we prove in general that such a transformation can always be performed. Moreover, suppose we are given the following derivation in G3QK(C). We will show how the relational rules (id) and (g 0,2 ) can be permuted upward until they are eliminated from a given derivation, yielding a proof in QK(C)L.
First, as shown in the derivation below, (id) can be permuted above (∃ r ). Observe that if (id) is applied to the initial sequent, then a propagation path v, , w exists in P G(R), where R = wRu, uRv, wRv, such that ∈ L S4∪S(G) ( ), showing that (s 1 ∃ ) can indeed be applied after (id).
We now observe that the conclusion of (id) in the proof above is an instance of (ax), and hence, the application of (id) may be eliminated and replaced by an instance of (ax) as shown below. Furthermore, as is also shown below, (g 0,2 ) may be permuted above (s 1 ∃ ), since if (g 0,2 ) is applied to the conclusion of (ax), then there exists a propagation path v, , u, , w in P G(R ), where R = wRu, uRv, such that ∈ L S4∪S(G) ( ). Hence, the side condition of (s 1 ∃ ) continues to hold after (g 0,2 ) is applied.
Last, we observe that the conclusion of (g 0,2 ) is an instance of (ax), meaning (g 0,2 ) can be eliminated from the proof and replaced by (ax), as shown below.
As seen in the above example, all relational rules have been eliminated from a G3QK(C) derivation, yielding a derivation in QK(C)L. Significantly, observe that the relational atoms wRu, uRv occurring in the two labeled sequents of the proof form an R-path of length two, which is a type of tree. This is a characteristic feature of proofs in QK(C)L (proven in Lemma 23 below), namely, that proofs only require labeled sequents of a treelike structure-a fact leveraged to derive nested systems for first-order modal logics in the next section.
Proof. We prove the case where (r) is (s 1 ∃ ) as the case where (r) is (s 2 ∃ ) is shown similarly, and the case where (r) is (p ♦ ) follows from [7,Lemma 5.8]. Therefore, suppose we are given the following: We assume that the relational atom uRv is active in the (s 1 ∃ ) inference, since the case where it is not active is easily resolved as (g n,k ) can be freely permuted above (s 1 ∃ ). Let R 1 := R, y ∈ D(u ), wR n u, wR k v, uRv and R 2 := R, y ∈ D(u ), wR n u, wR k v. We note that since the relational atom uRv is assumed active in (s 1 ∃ ), it follows that uRv occurs along a propagation path π(u , w ) such that (u , Θ) ∈ P G(R 1 ) with y ∈ Θ and ∃π(u , w ) ∈ P G(R 1 ) s π (u , w ) ∈ L S∪S(G) ( ? ) . We note that S ∈ {S4, S5} and ? ∈ {♦, }, with both being determined on the basis of if I d and/or D d occur in C. We assume that ? = ♦ for simplicity, noting that the proof is similar when ? = .
To complete the proof, we need to show that ∃π (u , w ) ∈ P G(R 2 )(s π (u , w ) ∈ L S∪S(G) (♦)). To do so, we build a propagation path π (u , w ) by replacing each occurrence of u, ♦, v in π(u , w ) by the propagation path u, , u 1 , . . . , u n−1 , , w, ♦, w 1 , . . . , w k−1 , ♦, v (corresponding to the relational atoms wR n u, wR k v ∈ R 2 ), and replacing each occurrence of v, , u in π(u , w ) by v, , w k−1 , . . . , w 1 , , w, ♦, u n−1 , . . . , u 1 , ♦, u (also corresponding to the relational atoms wR n u, wR k v ∈ R 2 ). We let π (u , w ) denote the propagation path obtained from π(u , w ) in the just described way. As the only difference between P G(R 1 ) and P G(R 2 ) is that the former is guaranteed to contain the edges (u, ♦, v) and (v, , u) corresponding to uRv, whereas the latter is not, we have that π (u , w ) is a propagation path in P G(R 2 ) as π (u , w ) omits u, ♦, v and v, , u.
Last, we additionally need to show that s π (u , w ) ∈ L S∪S(G) (♦). By assumption, s π (u , w ) ∈ L S∪S(G) (♦), implying that ♦ −→ * S∪S(G) s π (u , w ) by Definition 4. Also, due to the fact that (g n,k ) is a rule in G3QK(C), we know that ♦ −→ n ♦ k , −→ k ♦ n ∈ S ∪ S(G). Applying ♦ −→ n ♦ k to each occurrence of ♦ in s π (u , w ) corresponding to the edge (u, ♦, v), and applying −→ k ♦ n to each occurrence of in s π (u , w ) corresponding to the edge (v, , u) (with both edges corresponding to the relational atom uRv), we obtain the string s π (u , w ) ∈ L S∪S(G) (♦). Hence, we may permute (g n,k ) above (s 1 ∃ ), giving us: (1) Given that I d ∈ C, (id) can be permuted above (s 1 ∃ ), and (2) Given that D d ∈ C, (dd) can be permuted above (s 1 ∃ ).
C V I T 2 0 1 6

Figure 6
The side condition † 3 (C) for (s 2 ∃ ), which depends on the contents of C.
Proof. Let G = {G(n, k) | G(n, k) ∈ C}. We prove statement (2) as statement (1) is shown in a similar fashion. Suppose we are given the following: We assume that the domain atom y ∈ D(u) is active in (s 1 ∃ ) above, since the case where it is not active can be easily resolved by permuting (dd) above (s 1 ∃ ). Also, we let R 1 := R, y ∈ D(u), y ∈ D(v), uRv and R 2 := R, y ∈ D(v), uRv. By the side condition on (s 1 ∃ ), we know that there exists a propagation path π(w, u) such that (u, Θ) ∈ P G(R 1 ) with y ∈ Θ and ∃π(w, u) ∈ P G(R 1 ) s π (w, u) ∈ L S4∪S(G) (♦) . We assume w.l.o.g. that π(w, u) is a minimal propagation path between w and u, which either (i) traverses v before it reaches u, or (ii) does not traverse v before it reaches u. We prove each case in turn: (i). If π(w, u) traverses v before it reaches u, then the propagation path is of the form π (w, v), , u. We observe that π (w, v) is a propagation path from w to v in R 2 and that s π (w, u) = s π (w, v) · . Since −→ ε ∈ S4, it follows that s π (w, v) ∈ L S4∪S(G) (♦), which shows that (dd) can be permuted above (s 1 ∃ ) as the side condition of (s 1 ∃ ) continues to hold after (dd) is applied.

Theorem 16. Every derivation in G3QK(C) can be transformed into a derivation in
Proof. Suppose we are given a proof in G3QK(C), which is a proof in G3QK(C) ∪ QK(C)L, and so, we may consider it as such. Let us now consider a topmost occurrence of a relational rule (g n,k ), (id), (dd), or (nd) in our given derivation. By Lemma 14, (g n,k ) permutes above (p ♦ ), (s 1 ∃ ), and (s 2 ∃ ) (which covers the (♦ r ) and (∃ r ) rules as well by Remark 11), and since (g n,k ) freely permutes above every other rule of (G3QK(C) ∪ QK(C)L) \ {(id), (dd), (nd)}, the considered (g n,k ) instance can be eliminated from the given derivation. Similarly, by Lemma 15, a topmost occurrence of (id) or (dd) can be eliminated from the given derivation. Moreover, observe that (nd) freely permutes above all rules of G3QK(C) \ {(g n,k ) | G(n, k) ∈ C} ∪ {(id), (dd)} with the exception of (s 1 ∃ ). The only case in which (nd) does not freely permute above (s 1 ∃ ) is when the active domain atom of (s 1 ∃ ) is active in (nd) as well; however, such a case (as shown below left) can be resolved as shown below right: By repeatedly eliminating topmost occurrences of relational rules in the above described manner, we eventually obtain a proof in QK(C)L.
Proof. The forward direction (soundness) is shown by induction on the height of a given derivation in QK(C)L. In particular, one interprets labeled sequents on models over the class F C of frames, showing that (ax) and (⊥ l ) are F C -valid and that all inference rules of QK(C)L preserve validity (similar to [32,Theorem 12.13]). For the backward direction (completeness), we know that if ϕ ∈ QK(C), then w : ϕ is provable in G3QK(C); hence, by Theorem 16, we may transform the derivation in G3QK(C) into a derivation in QK(C)L, showing that w : ϕ is derivable in QK(C)L.

Nested Sequent Systems
Let Γ and ∆ be multisets of L-formulae, Θ ⊂ Var be a multiset of variables, and {w 1 , . . . , w m } ⊂ Lab be a set of labels. A nested sequent Φ is inductively defined as follows: 1. Each flat sequent of the form Γ; Θ ∆ is a nested sequent, and 2. any formula of the form Γ; Θ ∆, [Ψ 1 ] w1 , . . . , [Ψ m ] wm , where Ψ i are nested sequents for each 1 ≤ i ≤ m, is a nested sequent. In the context of nested sequents, we use Γ, ∆, Σ, and Π to denote multisets of L-formulae, Θ and Ξ to denote multisets of variables (which encode domains), and Φ and Ψ to denote nested sequents. We will often use w, u, v, . . . (occasionally annotated) to denote labels from Lab and we make the simplifying assumption that every occurrence of a label in a nested sequent is unique. Note that the incorporation of labels in our nested systems is useful as it simplifies the presentation of our reachability rules below.
Observe that every nested sequent of the above form encodes a tree whose nodes are flat sequents. In other words, each nested sequent Φ = Γ; Θ ∆, [Ψ 1 ] w1 , . . . , [Ψ m ] wm can be graphically depicted as a tree tr w0 (Φ) of the following form: We refer to a flat sequent Γ i ; Θ i ∆ i occurring as a node labeled with w i in (the tree of) a nested sequent as a w i -component, or as a component more generally if we do not wish to specify its label. We note that the root Γ; Θ ∆ is always assumed to be associated with the label w 0 , that is, Γ; Θ ∆ is the unique w 0 -component. We use the notation Φ{Ψ 1 } w1 · · · {Ψ m } wm to indicate that Ψ i is a w i -component, for 1 ≤ i ≤ m.
Since nested sequents encode trees and labeled sequents encode binary graphs (via relational atoms of the form wRu), it is natural to view nested sequents as types of labeled sequents. Indeed, correspondences between labeled tree sequents [20] (i.e. labeled sequents R, Γ ∆ such that R forms a (labeled) tree and every label of the sequent either occurs in R or is identical if the R = ∅) and nested sequents have been established in various settings [7,19,28,33]. As our nested systems are extracted from the refined labeled systems (viz. QK(C)L) of the previous section, we define translations between nested and labeled tree sequents. These translations will be used subsequently to transform each refined labeled calculus into a nested calculus.

Definition 19 (Translation N).
Let Λ := R, D, Γ ∆ be a labeled tree sequent with R containing only relational atoms of the form uRv, D containing only domain atoms of the form x ∈ D(u), and let w be the root of Λ. We define Λ 1 ⊆ Λ iff there exists a labeled tree sequent Λ 2 such that Λ = Λ 1 ⊗ Λ 2 and where if u is the root of Λ 1 , then Λ 2 contains no domain atoms or labeled formulae associated with u. Let us further define Λ u to be the unique labeled tree sequent rooted at the label u such that Λ u ⊆ Λ. We define N(Λ) := N u (Λ) recursively on the tree structure of Λ: Before we define our nested systems, we define propagation graphs and related concepts in the setting of nested sequents. Such notions easily transfer from the labeled setting since every nested sequent can be viewed as a labeled sequent under the L translation.
Definition 21 (Propagation Graph of a Nested Sequent). Let Φ be a nested sequent and let L(Φ) := R, Γ ∆. We define the propagation graph of Φ to be P G(Φ) := P G(R) and we note that propagation paths, their converses, and strings thereof are defined as in Definition 7.
A uniform presentation of all nested systems is provided in Figure 7. We remark that NQK := NQK(∅) and that (p ♦ ), (s 1 ∃ ), and (s 2 ∃ ) constitute our reachability rules. The side conditions for such rules are identical to the side conditions given in the previous section, i.e. to apply the rule top-down (or, bottom-up) one takes the premise (conclusion, resp.) Φ, obtains R via the translation L(Φ) = R, Γ ∆, and then checks to see if the side conditions hold relative to P G(R).  The nested system NQK(C), which includes (d) iff S ∈ C. The side condition † states that the rule is applicable only if y is fresh; see Definition 9 for the interpretation of the side conditions † 1 (C) − † 3 (C), which are functions of C. [28]). We define a labeled tree derivation to be a proof containing only labeled tree sequents. We say that a labeled tree derivation has the fixed root property iff every labeled sequent in the derivation has the same root.

Lemma 23. Every proof in QK(C)L of a labeled tree sequent is a labeled tree proof with the fixed root property.
Proof. The lemma follows from the fact that if any rule of QK(C)L is applied bottom-up to a labeled tree sequent, then each premise is a labeled tree sequent with the same root.
Proof. Follows from Theorem 17 and Lemma 23 using the L and N translations.

Conclusion
In this work, we unified first-order modal logics in a single nested sequent framework by means of reachability rules. These rules, which may propagate formulae and/or check for data along paths within a nested sequent, permit one to toggle between the various logics by parameterizing rules with distinct semi-Thue systems. We used such rules to define (to the best of the author's knowledge) the first nested sequent systems for first-order modal logics.
In future work, we aim to investigate how reachability rules can be leveraged to provide nested systems for broader classes of logics. This can be accomplished in multiple ways. For instance, we could investigate the effect of parameterizing reachability rules with alternative semi-Thue systems, or through the introduction of new logical connectives (e.g. converse modalities). Second, we aim to explore the formulation of reachability rules for alternative quantifiers; e.g. Miller and Tiu's nabla quantifier ∇ [30] or the Gabbay-Pitts N quantifier [14]. Moreover, we aim to investigate the properties of our nested systems such as cut-elimination, 4 invertibility of rules, and the admissibility of structural rules (e.g. contraction and weakening). Lastly, such systems may prove well-suited for identifying decidable fragments of first-order modal (and related) logics by means of proof-search algorithms.