11institutetext: Computational Logic Group, Institute of Artificial Intelligence, Technische Universität Dresden, Germany
11email: [email protected]
Realizing the Maximal Analytic Display Fragment of Labeled Sequent Calculi for Tense Logics††thanks: This research was supported by the European Research Council European Research Council (Grant Agreement no. 771779, DeciGUT).
We define and study translations between the maximal class of analytic display calculi for tense logics and labeled sequent calculi, thus solving an open problem about the translatability of proofs between the two formalisms. In particular, we provide translations that map cut-free display proofs to and from special cut-free labeled proofs, which we dub ‘strict’ labeled proofs. This identifies the space of cut-free display proofs with a polynomially equivalent subspace of labeled proofs, showing how calculi within the two formalisms polynomially simulate one another. We analyze the relative sizes of proofs under this translation, finding that display proofs become polynomially shorter when translated to strict labeled proofs, though with a potential increase in the length of sequents; in the reverse translation, strict labeled proofs may become polynomially larger when translated into display proofs. In order to achieve our results, we formulate labeled sequent calculi in a new way that views rules as ‘templates’, which are instantiated with substitutions to obtain rule applications; we also provide the first definition of primitive tense structural rules within the labeled sequent formalism. Therefore, our formulation of labeled calculi more closely resembles how display calculi are defined for tense logics, which permits a more fine-grained analysis of rules, substitutions, and translations. This work establishes that every analytic display calculus for a tense logic can be viewed as a labeled sequent calculus, showing conclusively that the labeled formalism subsumes and extends the display formalism in the setting of primitive tense logics.
Logical methods are at the forefront of research in computer science, artificial intelligence, and formal philosophy, giving rise to a diverse number of logics capable of executing reasoning fine-tuned for specific application scenarios. Logics have found extensive, meaningful applications in various domains such as the verification of software [28], in ontology mediated querying [2], and in explainable AI [37]. Analytic proof systems are of chief importance to logics, being used to facilitate reasoning with logics, to establish non-trivial properties, and to design automated reasoning methods.
An analytic calculus is a collection of inference rules that generates proofs satisfying the subformula property, i.e. every formula occurring in a proof is a subformula of the conclusion of the proof. This is a powerful constraint on the shape of proofs that has been exploited in various ways, e.g. in writing decision procedures [12, 15, 16] and in computing interpolants [26, 27]. One of the dominant formalisms (alongside tableaux [13, 35]) for constructing analytic calculi is Gentzen’s sequent formalism. Typically, sequent systems include a cut rule, which, although helpful for establishing completeness (among other uses), deletes formulae from the premises to the conclusion when applied. This has the effect that proofs in a sequent calculus with cut do not exhibit the desirable subformula property, though, this property can be reclaimed by establishing cut-elimination. That is, one shows that the cut rule can be eliminated from any derivation without affecting the conclusion derived, and therefore, is superfluous in the underlying sequent system.
Calculi built within the sequent formalism consist of rules that operate over sequents, i.e. formulae of the form , where and are sequences or (multi)sets of formulae. Despite the success of sequent systems in discovering new logics [17], in automated reasoning [34, 12], and in confirming non-trivial logical properties [27], it was discovered that the structure of the sequent is insufficient to capture more expressive logics in an analytic or cut-free manner (e.g. the modal logic and bi-intuitionistic logic [7]). In an attempt to recapture analyticity for more expressive logics of interest, various generalization of Gentzen’s sequent formalism have been proposed; e.g. hypersequents [1, 30], linear nested sequents [25], nested sequents [8, 22], display sequents [3, 39], and labeled sequents [33, 38]. We will focus on the relationship between the latter two formalisms in this paper in the context of tense logics.
A prominent generalization of Gentzen’s sequent formalism is the display framework, originally defined by Belnap in 1982 under the name display logic [3]. Belnap’s display calculi generalize Gentzen’s calculi by expanding sequents with a host of new structural connectives—corresponding to pairs of dual connectives—along with rules for manipulating them. Incorporating structural connectives for pairs of dual connectives has proven fruitful in the design of analytic systems for large classes of logics [3, 6, 18, 23, 39, 40]. This is in part due to a general cut-elimination theorem proved by Belnap, which states that a display calculus admits cut-elimination if eight (checkable) syntactic conditions are satisfied [3]. We remark that Belnap’s display formalism is among one of the most expressive generalizations of Gentzen’s sequent formalism, providing a uniform and modular proof theory for substantial classes of logics.
Another rich extension of Gentzen’s sequent formalism is the labeled formalism. Whereas display calculi are obtained via algebraic considerations, labeled sequent calculi are normally extracted from a logic’s relational semantics. The labeled sequent formalism was initiated by Kanger in the 1950’s [21], though it was arguably the work of Simpson [33] that provided the contemporary, general form of labeled sequents and their encompassing systems. Labeled sequents extend Gentzen sequents by prefixing formulae with labels (e.g. ) and incorporating relational atoms (e.g. ) into the syntax of sequents. A labeled formulae encodes that a formula holds at a world in a Kripke model and a relational atom encodes the accessibility relation. Like the display formalism, the labeled formalism has been used to provide analytic calculi for extensive classes of logics. Moreover, fundamental properties hold generally for such systems, e.g. labeled sequent systems admit the height-preserving admissibility of important structural rules (e.g. weakenings and contractions), have height-preserving invertible rules, and cut-elimination holds [5, 19, 33, 38].
There are a number of key differences between the display and labeled formalisms, e.g. display sequents are composed of structural connectives whereas labeled sequents encode graphs, display calculi are based on an algebraic semantics whereas labeled calculi are based on a relational semantics, display calculi employ structural rules and display rules while such rules are admissible or redundant in labeled calculi, etc. Despite these notional, motivational, and operational distinctions, both formalisms permit the definition of analytic calculi for wide classes of overlap** logics, implying the existence of an underlying relationship between the two formalisms. Normally, relationships between calculi are studied via translations, i.e. functions that stepwise translate a proof from one calculus into a proof in another, and it is informative to provide the computational complexity of the translations as well as compare the relative sizes of the input and output proofs.
Preliminary studies relating display and labeled calculi for some normal modal logics were undertaken by Mints [29] and Restall [32]. A more intensive investigation studying the relationship between shallow-nested calculi (which are close relatives of display calculi) and labeled calculi for extensions of the tense logic with path axioms (encoding Horn properties on Kripke frames) was given more recently in [10]. Nevertheless, the renowned ‘Display Theorem I’ by Kracht tells us that a substantially larger class of logics (subsuming the aforementioned logics), namely, primitive tense logics admit analytic display calculi [23]. Moreover, this result also tells us that if a tense logic has an analytic display calculus, then it is a primitive tense logic, meaning the set of display calculi for primitive tense logics forms the maximal analytic set of display calculi for tense logics. Therefore, the aforementioned studies fall short of characterizing the relationship between all analytic display calculi for tense (and modal) logics and their labeled counterparts. Indeed, this problem was explicitly left open in Restall’s 2006 paper [32] as well as in [10], and all aforementioned studies left the complexity of such translations unaddressed. In this paper, we develop and apply new techniques to solve this open problem and provide complexity bounds for our translations. In particular, we accomplish the following:
•
We provide the first characterization of primitive tense rules in the setting of labeled sequent calculi.
•
We provide a new formulation of labeled sequent calculi that matches the standard formulation of display calculi, namely, we take inference rules to be templates with variables that are instantiated to produce rule applications. This new formulation is crucial in defining translations between display and labeled proofs.
•
We establish a correspondence between the space of all analytic display proofs and a special subspace of labeled proofs, which we dub strict labeled proofs. We show that translations exist between every analytic display proof and each corresponding strict labeled proof. Furthermore, our translations are direct and do not take any detours through other systems as in other approaches (cf. [10]).
•
We find that translating a display proof into a strict labeled proof yields a proof with the same number of sequents or less, but may quadratically increase the length of sequents appearing in the output proof; therefore, there is a trade-off between the number of sequents and their lengths when translating from display to labeled, which is a previously unrecognized finding. Conversely, translating a strict labeled proof into a display proof may polynomially increase the number of sequents in the output proof.
•
We observe that display structures (which only form part of a display seqeuent) are labelled sequents, and that all display equivalent sequents translate to the same labeled sequent. This demonstrates a higher degree of syntactic bureaucracy in the display formalism and also shows that labeled sequents are canonical representations of display sequents since they do away with bureaucracy that obfuscates identities.
This paper is organized as follows: In Section 2, we define and give the preliminaries for primitive tense logics. We then present Kracht’s display calculi for primitive tense logics in Section 3. In Section 4, we reformulate and extend Boretti’s labeled calculi for tense logics [5] to capture primitive tense logics in a manner suitable for translations with display systems. In Section 5, we define labeled polytree sequents and strict proofs, which will be invaluable in translating labeled and display proofs. We then show how to translate between display and labeled notation in Section 6, and put our translations to use in Sections 7 and 8, showing how to translate display proofs into strict labeled proofs and vice versa, respectively, as well as analyze the complexity of our translations. In Section 9, we re-emphasize our findings and discuss future work.
2 Tense Logics and Primitive Axioms
In this section, we introduce and define the class of logics our proof systems consider, namely, tense logics. Tense logics were invented by Prior in the 1950’s [31] and extend classical propositional logic with modalities making reference to both future and past states of affairs. More concretely, tense logics employ the and modalities, which apply to a proposition that holds at every next moment, or at some next moment, respectively, and the and modalities, which apply to a proposition that holds at all prior moments, or at some prior moment, respectively. In other words, is read as ‘in all future moments’, is read as ‘in some future moment’, is read as ‘in all past moments’, and is read as ‘in some past moment’. The remaining logical operators employed in our language are the familiar classical operators , , , , , and , that is, the language we use is an extension of the language of classical propositional logic.
Definition 1 (The Language )
We define our language to consist of the formulae generated via the following grammar in BNF:
where ranges over a denumerable set of propositional atoms, which we call atoms for short. We use , , , (occasionally annotated) to denote atoms and , , , (occasionally annotated) to denote formulae from . The bi-conditional operator is defined in the usual way as .
We define the length of a formula , denoted , recursively as , for , and for . Our language is interpreted over standard relational (i.e. Kripke) models for normal modal logics [24].
Definition 2 (Relational Frame/Model)
We define a relational frame to be a tuple such that is a non-empty set of worlds and is the accessibility relation. A relational model is defined to be a tuple such that is a relational frame and is a valuation function map** atoms to sets of worlds.
We may think of the worlds in a relational model as possible moments in time with the accessibility relation holding between a moment and a (possible) future moment. Formulae are then interpreted at a specific moment in time (i.e. a world) and express a proposition concerning a present, past, or future state of affairs. The following definition makes the interpretation of formulae precise.
Definition 3 (Semantic Clauses)
Let be a relational model with . We define the satisfaction of a formula in at , written , recursively on the structure of as follows:
•
iff ;
•
;
•
;
•
iff ;
•
iff or ;
•
iff and ;
•
iff or ;
•
iff for all , if , then ;
•
iff for some , and ;
•
iff for all , if , then ;
•
iff for some , and .
A formula is globally true in a relational model iff for all , and a formula is -validiff it is globally true on all relational models.
We note that the set of all -valid formulae is axiomatizable (see [4]), i.e. the following axiomatization is sound and complete relative to our relational semantics.
Definition 4 (, )
The axiomatization consists of all classical propositional tautologies along with the following axioms and inference rules:
A1
A2
A3
A4
R0
\AxiomC
\AxiomC\BinaryInfC\DisplayProof
A5
A6
R1
\AxiomC
\UnaryInfC\DisplayProof
R2
\AxiomC
\UnaryInfC\DisplayProof
The logic is defined to be the smallest set of formulae closed under substitutions of the axioms A1–A6 and applications of the inference rules R0–R2.
The logic serves as the base logic in the class of tense logics we consider. All other logics considered can be characterized as extensions of with primitive tense axioms [23].
A primitive tense axiom is a formula of the form
, where and are generated via the following grammar in BNF:
and contains each atom at most once.
We will use to denote the primitive tense logic axiomatized by extended with a set of primitive tense axioms , and will use to denote the logic’s axiomatization. The set of primitive tense axioms covers a wide array of well-known axioms such as the axiom (), the axiom (), and the axiom (). Beyond capturing a diverse class of logics, the proof-theoretic significance of primitive tense logics was first identified by Kracht [23], who was able to show that the largest set of display calculi for tense logics satisfying a certain set of desirable properties (discussed in the subsequent section) is characterizable as those calculi that are sound and complete relative to primitive tense logics.
As remarked by Kracht [23], by making use of associativity, commutativity, and idempotency properties of and , along with standard equivalences, one can transform any primitive tense axiom into an equivalent normal form, defined below.
Proposition 1 (Primitive Tense Normal Form)
We define the language to be the smallest set of formulae generated by the following grammar:
Let , each , and each be in with and each containing at most one occurrence of each atom. Every primitive tense axiom can be put into a normal form, shown below left. We define a simplified primitive tense axiom to be a formula of the form shown below right.
Since every primitive tense axiom is equivalent to a conjunction of simplified primitive tense axioms (by proposition1 above), each primitive tense logic admits an axiomatization where contains simplified primitive tense axioms only. We therefore assume w.l.o.g. that any set of primitive tense axioms contains only simplified primitive tense axioms, unless specified otherwise.
3 Display Calculi for Tense Logics
In this section, we describe the display calculi for primitive tense logics introduced by Wansing [39] and Kracht [23]. One of the central ideas behind the construction of display systems is the use of structural connectives (also called Gentzen toggles [23]) which stand for different logical connectives depending on their position within a sequent. The use of structural connectives dates back to the inception of sequents, where Gentzen employed the comma connective representing a conjunction on the left and a disjunction on the right of a sequent [15, 16]; for example, is interpretd as whereas is interpreted as .
Although Belnap discusses display systems for modal logics in his seminal paper introducing display calculi [3], their formulation was improved upon and simplified in the work of Wansing [39]. While Belnap had formulated the structural connectives standing for modalities as binary connectives, Wansing formulated them as unary connectives. In particular, the bullet was used to represent a in the antecedent of a sequent and to represent a in the consequent; e.g. is interpreted as and is interpreted as [39].
The use of structural connectives in building sequents has proven beneficial. In the first place, the inclusion or exclusion of rules governing the behavior of structural connectives permits the supplementation of display calculi for diverse families of logics; e.g. bunched-implication logics [6], substructural logics [18], bi-intuitionistic logic [40], tense/temporal logics [23, 39], and relevance logics [3]. In the second place, the use of structural connectives supports the shifting of data within a sequent while at the same time preserving the subformula property. For instance, in the context of tense logics the sequents and are mutually derivable from one another; observe that the may be shifted to the antecedent or consequent, either displaying as the entire consequent or as the entire antecedent, respectively, without changing the logical formulae that occur. The capacity to display data within a display sequent (i.e. to shuffle data around) is what gives rise to the name of Belnap’s formalism.
Another significant feature of the display formalism is the existence of a general cut-elimination theorem. As shown by Belnap in [3], so long as a display calculus satisfies eight syntactic conditions (C1)–(C8), the calculus admits cut-elimination (see Definition 12 and Theorem 3.1 below). Thus, the display formalism is well-suited for supplying a variety of logics with cut-free calculi in a uniform and modular fashion.
The combination of data by means of structural connectives gives rise to structures, which serve as the entire antecedent or consequent of a display sequent. In the context of tense logics, we define a structure to be an object generated from the following grammar in BNF:
where ranges over the formulae in . We use , , , (occasionally annotated) to denote structures. A display sequent is defined to be a formula of the form where and are structures. We use , , , (or, just ) to denote display sequents. We recursively define the length of a structure as follows: , , , . The length of a display sequent is defined to be .
As mentioned above, structural connectives act as a proxy for certain logical connectives dependent upon where they occur within a display sequent. This gives rise to structures and display sequents being translatable into logical formulae.
We define the translations and from structures to formulae as follows:
•
•
•
•
•
•
•
•
•
•
We define the translation of a display sequent as .
We note that the structure is taken to stand for the empty structure, which functions as the identity element with respect to the operator, that is, , , and are taken to be equivalent. This property of is formalized as rules in our display calculus (viz. and ; see Figure 3) and corresponds to the fact that in the antecedent (or, consequent) a structure of the form or is equivalent to and (or, and , respectively), which is equivalent to (or, , respectively) by the formula translation above. We now define the notion of a substructure, which will be used in the sequel.
Definition 7 (Substructure)
We define to be a substructure of iff where is defined recursively:
•
•
•
•
•
We present Kracht’s display calculus for the minimal tense logic , consisting of three sets of rules: logical rules (see Figure 1), display rules (see Figure 2), and structural rules (see Figure 3), which we introduce in turn. After introducing , we define extensions of with rules corresponding to primitive tense axioms (cf. [23]). Before we proceed however, let us comment on the types of symbols that occur within rules and their instances.
We let the symbols , , , (occasionally annotated) be atomic variables, which are instantiated with atoms in rule applications, the symbols , , , (occasionally annotated) be formula variables, which are instantiated with formulae from in rule applications, and the symbols , , , (occasionally annotated) be structure variables, which are instantiated with structures in rule applications. (NB. Observe that atoms are formulae and formulae are structures, meaning formula variables can be instantiated with atoms and structure variables can be instantiated with formulae.) A schematic structure is defined to be a combination of atomic variables, formula variables, and structure variables with logical and structural connectives, i.e. it is a formula generated via the following grammar in BNF:
where and . We use , , , (occasionally annotated) to denote schematic structures and define a schematic display sequent to be a formula of the form .
Definition 8 (Substitution )
A substitution is defined to be a function that maps atomic variables to atoms, formula variables to formulae, and structure variables to structures. We use postfix notation when applying substitutions, viz. we let be the atom obtained by applying to , be the formula obtained from applying to , and be the structure obtained from applying to . We extend substitutions to schematic structures and schematic display sequents in the expected way by applying them to each atomic variable, formula variable, and structure variable therein (cf. [3, 23]). It immediately follows from the definition that for any substitution , .
We always assume that if a substitution is applied to a set of schematic structures or schematic display sequents, then all atomic variables, formula variables, and structure variables contained therein are within the domain of the substitution. If we want to indicate what variables are mapped to which atoms, formulae, or structures, then we write a substitution as
indicating that , , and for , , and .
A rule or inference rule (as shown below left) is a schema utilizing schematic display sequents that through the application of a substitution produces a rule instance or rule application (as shown below right). We always assume that if a substitution is applied to a rule that all structure, formula, and atomic variables are within the domain of the substitution.
\AxiomC\AxiomC\AxiomC\TrinaryInfC\DisplayProof
\AxiomC\AxiomC\AxiomC\TrinaryInfC\DisplayProof
The display calculus for the minimal tense logic consists of the logical rules given in Figure 1, the display rules given in Figure 2, and the structural rules given in Figure 3. Certain logical rules, viz. , , and , serve as axioms and are called initial rules; we refer to a display sequent generated by an initial rule as an initial sequent. The remaining logical rules either introduce a logical connective to a formula, or between formulae, which occur in the premise(s). As usual, we refer to the explicitly presented formula(e) in the premise(s) of a rule as auxiliary and refer to the explicitly presented formula in the conclusion of a rule as principal. A notable feature of the display formalism is that in each logical rule the principal formula is either the entire antecedent or consequent of the concluding display sequent.111This fact is utilized in the general cut-elimination theorem [3], stated as Theorem 3.1 below.Proofs in display calculi are defined in the usual inductive way, where each instance of an initial rule is a proof, and further proofs may be obtained by successively applying inference rules [23].
We use and annotated versions thereof to denote display proofs. There are various metrics that may be used to quantify aspects of proofs; we define a few notions below that will be helpful in relating display proofs to labeled proofs later on.
Definition 9 (Quantity, Width, Size)
We define the quantity of a proof to be the number of sequents it contains, i.e.
•
if is an initial rule of the form \AxiomC\RightLabel\UnaryInfC\DisplayProof, then ;
•
if \AxiomC\RightLabel\UnaryInfC\DisplayProof, then .
We define the width of a proof to be equal to the maximum length among all display sequents occurring in the proof, i.e. Last, we define the size of a proof to be .
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\AxiomC\RightLabel\BinaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\AxiomC\RightLabel\BinaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\AxiomC\RightLabel\BinaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
Figure 1: The logical rules for the display calculus [23].
The display rules (Figure 2) describe what display sequents may be mutually derived from one another (indicated by the use of a double line); e.g. one may derive from , or vice-versa. We refer to rules that can be applied top-down and bottom-up as reversible rules and indicate them by using a double line. Display rules are the defining characteristic of display calculi and permit data to be shuffled within a display sequent, letting structures be displayed as the entire antecedent or consequent. This gives rise to an equivalence relation defined on sequents called display equivalence and a property of display systems called the display property. The former relation holds between two display sequents if they can be derived from one another by means of the display rules, and the meaning of the latter property is that one can always pick a substructure within a display sequent and transform the sequent into a display equivalent version of the form or . Both of these notions are formally defined below.
Two display sequents and are display equivalent, written , iff they are mutually derivable from one another by means of the display rules. We also define two display sequents and to be deductively equivalent, written , iff they are mutually derivable from one another.
A display calculus has the display propertyiff the calculus includes a set of rules (called display rules) such that for any display sequent , if is a substructure of or , then either or are derivable for some structure using only the display rules. We note that in our setting the rules of Figure 2 are taken to be the display rules.
The capacity to display a substructure as the entire antecedent or consequent of a sequent gives rise to two separate types of substructures, namely, antecedent parts (a-parts) and consequent parts (c-parts). An a-part is a substructure that can be displayed as the entire antecedent, and a c-part is a substructure that can be displayed as the entire consequent. Formally, they are defined as follows.
A substructure of or is an antecedent part (a-part)iff for some structure , is derivable from using only the display rules. A substructure is defined to be a consequent part (c-part)iff for some structure , is derivable from using only the display rules.
Figure 2: The display rules for the display calculus [23].
Example 1
We give an example of the substructures of the structures and , as well as consider an example of a-parts and c-parts in a given display sequent.
•
•
All display sequents below are display equivalent to one another since all are mutually derivable by means of the rules in Figure 2. Moreover, we can see in the left derivation that the structures , , and are a-parts, and in the right derivation , , and are c-parts.
The structural rules for (Figure 3) ensure the proper behavior of our logical connectives; e.g. encodes the fact that is associative (since by Definition 6 the structural connective represents in the antecedent) and encodes the fact that is commutative (since by Definition 6 the structural connective represents in the consequent). Additionally, by the work of Belnap [3], we know that the rule is eliminable in since the calculus satisfies eight sufficient conditions necessitating the elimination of .
Definition 12 (Conditions (C1)–(C8))
Belnap’s eight sufficient conditions ensuring the elimination of are as follows:
(C1)
Each formula occurring in the premise of a rule instance is a subformula of some formula in the conclusion of the inference.
(C2)
We say that a structure variable in the premise of an inference is congruent to a structure variable in the conclusion iff the two structure variables are identical.
(C3)
Each structure variable in the premise of an inference is congruent to at most one structure variable in the conclusion.
(C4)
Congruent structure variables in an inference are either both a-parts or both c-parts.
(C5)
For each rule, if a formula variable is in the conclusion of the rule, then it is either the entire antecedent or consequent.
(C6)
Each rule is closed under the uniform substitution of arbitrary structures in c-parts for congruent structure variables.
(C7)
Each rule is closed under the uniform substitution of arbitrary structures in a-parts for congruent structure variables.
(C8)
Suppose there is an inference ending with and an inference ending with with principal in both inferences. Then, (1) is identical to or , or (2) there exists a proof of from the premises of each inference where is only used on proper subformulae of .
Any display calculus satisfying conditions (C1)–(C8) has the subformula property and admits elimination.
Although we have been discussing Kracht’s display calculus for the minimal tense logic , the above cut-elimination theorem applies equally to extensions of with rules corresponding to (simplified) primitive tense axioms. In order to define the rules capturing these axioms (referred to as primitive tense structural rules), we first define a translation from logical formulae to schematic structures. The reason being, we obtain primitive tense structural rules by translating simplified primitive tense axioms into such rules, and the translation of logical formulae into schematic structures is a crucial component of this process.
We define the translation function from formulae to schematic structures as follows:
•
•
•
•
•
In the above definition, each atom is transformed into a unique structure variable . Following Kracht [23], we make use of the translation to define primitive tense structural rules.
Definition 14 ()
Each simplified primitive tense axiom of the form shown below left corresponds to a primitive tense structural rule of the form shown below right.
If is a set of simplified primitive tense axioms, then we define to be the extension of with all primitive tense structural rules corresponding to the axioms in . We indicate that a display sequent is provable in with a display proof by writing . Note that is equal to where .
Each display calculus possesses the display property.
The proof-theoretic significance of primitive tense axioms was identified by Kracht in [23]. As discussed and proven there, primitive tense extensions of form the largest class of tense logics whose corresponding display calculus satisfies conditions (C1)–(C8), and—conversely—if a display calculus satisfies Belnap’s conditions, then it is sound and complete relative to a primitive tense extension of . This result is stated in Theorem 3.3 below, and relies on the notion of a tense logic being properly displayed.
Let be a set of structural rules such that satisfies conditions (C1)—(C8) and let be the logic obtained from extending the Hilbert calculus with the axioms in . Then, we say that a display calculus properly displaysiff it satisfies conditions (C1)–(C8) along with conditions (1) and (2) below.
(1) For every rule instance of the form shown below left in the rule instance of the form shown below right is derivable in :
\AxiomC
\AxiomC\AxiomC\TrinaryInfC\DisplayProof
\AxiomC
\AxiomC\AxiomC\TrinaryInfC\DisplayProof
(2) For every rule instance of the form shown below left (where we assume that an axiom is a rule instance with zero premises) in , the rule instance shown below right is derivable in .
\AxiomC\AxiomC\AxiomC\TrinaryInfC\DisplayProof
\AxiomC\AxiomC\AxiomC\TrinaryInfC\DisplayProof
As a consequence of the above definition, if a display calculus properly displays a logic, then it is sound and complete relative to that logic.
Let be a set of structural rules such that satisfies conditions (C1)—(C8) and let be the logic obtained from extending the Hilbert calculus with the axioms in . The display calculus properly displays iff is axiomatizable with primitive tense axioms.
Figure 4 shows some derivable rules in , which will be of use in our translation work later on. All rules are derivable by means of display and/or structural rules.
Last, we note that throughout the remainder of the paper we use distinct types of inference lines to indicate distinct types of inferences. In particular, a solid line ‘ ’ (as shown first below) is used to indicate a rule application, a dashed line ‘ ’ (as shown second below) is used to indicate the application of a derivable or admissible rule, a double line ‘ ’ (as shown third below) is used to indicate a reversible rule application, and a dotted line ‘ ’ (as shown fourth below) is used to indicate that the premise and conclusion are identical or isomorphic. (NB. We define isomorphisms between sequents in the next section.) In the notation below, each and denote a premise and each is the conclusion; these may be display or labeled sequents (defined in the next section).
Labeled sequents generalize the syntax of Gentzen-style sequents through the incorporation of labels and semantic elements. This idea is rooted in the work of Kanger [21], who employed spotted formulae in the construction of sequent systems for modal logics. Since then, large classes of modal and constructive logics have been supplemented with labeled sequent systems [9, 14, 29, 33, 38]. The labeled formalism has been successful in generating modular systems that cover extensive classes of logics in a uniform manner, i.e. through the inclusion or exclusion of structural rules, one labeled system for a logic may be transformed into a labeled system for another logic [33, 38]. Moreover, general results exist (e.g. [5, 19]) which show that labeled systems commonly possess favorable properties such as admissible structural rules, invertible logical rules, and cut-admissibility (we formally define these properties below). In this section, we introduce labeled calculi with primitive tense structural rules. The base calculus for the logic is a notational variant of Boretti’s [5] labeled calculus , though the primitive tense structural rules we define are entirely new.222We employ a schematic representation of labeled calculi whereby rules are instantiated by means of substitutions to better match the display formalism.
We let be a denumerable set of labels. A labeled sequent is defined to be a formula of the form , where is a (potentially empty) set of relational atoms of the form , and and are (potentially empty) multisets of labeled formulae of the form , where and range over , and ranges over .333Usually labeled calculi employ multisets of relational atoms. However, since weakenings and contractions are admissible over relational atoms in our setting, it is well-known that sets can be used instead of multisets. We use to denote sets of relational atoms, and to denote multisets of labeled formulae, and to denote labeled sequents, as well as use annotated versions of these symbols. We let , , and indicate the set of all labels in a set , a multiset , or a labeled sequent , respectively. We define the length of a labeled sequent to be , where , , and denote the cardinality of each (multi)set.
Given two labeled sequents and , we define the sequent composition . It follows by definition that sequent compositions are (1) associative, i.e. , and (2) commutative, i.e. . Due to the associative property, we will often omit parentheses when writing successive sequent compositions. If , we define .
As in the display setting, we utilize variables in the formulation of our inference rules and calculi. In particular, we let denote label variables, which will be instantiated with labels, we define schematic relational atoms to be formulae of the form with and label variables, and we define schematic labeled formulae to be formulae of the form where is a label variable and is generated by the following grammar in BNF:
with , , an atomic variable, and formula variables. We use and annotated versions thereof to denote labeled sequent variables, which will be instantiated with labeled sequents. Last, we define schematic labeled sequents to be formulae of the form
where, for each and , is a (potentially empty) set of schematic relational atoms, and are (potentially empty) multisets of schematic labeled formulae, and is a labeled sequent variable. We sometimes denote schematic labeled sequents by and annotated versions thereof. As can be seen in Figures 5–7, schematic labeled sequents are used to define inference rules, instances of which, are obtained via applications of substitutions.
Definition 16 (Substitution )
A substitution is defined to be a function (written in postfix notation) that satisfies the following: , , , and is a labeled sequent. We extend a substitution to sets of schematic relational atoms, multisets of schematic labeled formulae, and schematic labeled sequents in the expected way by applying to each label variable, atomic variable, formula variable, and labeled sequent variable occurring therein.
If we want to indicate what variables are mapped to which labeled sequents, formulae, atoms, or labels then we write a substitution as
indicating that , , , and for , , , and .
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\AxiomC\RightLabel\BinaryInfC\DisplayProof
\AxiomC\AxiomC\RightLabel\BinaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\AxiomC\RightLabel\BinaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
Figure 5: Initial and logical rules of .
It follows from the above definition that applying a substitution to a schematic labeled sequent yields a labeled sequent as the result. We define a rule or inference rule to be a schema utilizing schematic labeled sequents, which produces a rule instance or rule application when a substitution is applied to each schematic labeled sequent occurring in the rule (see Example 2 below). When a substitution is applied to a rule, we assume that every label variable, atomic variable, formula variable, and labeled sequent variable occurring in the rule is within the domain of .
The labeled calculus is defined to be set of the inference rules presented in Figures 5 and 6. contains the initial rules , , and , as well as logical rules for , , , and , all of which are shown in Figure 5. We refer to each rule , , and as an initial rule and refer to any labeled sequent generated by an initial rule as an initial sequent. The rules governing the introduction of modal formulae are provided in Figure 6, and we note that , , , and have a side condition, namely, for any application of the rule with a substitution , must be fresh, i.e must not occur in the conclusion of the rule application. As in the display setting, the explicitly presented formula(e) in the premise(s) of a rule is (are) referred to as auxiliary and the explicitly presented formula(e) in the conclusion is (are) called principal. We also note that the labeled sequent variable in each inference rule provides the context of the rule when instantiated. This formulation of labeled sequent rules is new and will be helpful in studying and defining translations with display calculi later on since substitutions may be explicitly taken into account in translations.
Example 2
To provide the reader with intuition concerning the application of rules, we give two examples. First, let and . Applying to the rule (shown below left) yields the rule instance below right.
Proofs are defined in the usual, inductive way: each instance of an initial rule is a proof, and applying a rule to the conclusion of a proof, or between conclusions of proofs, yields a proof. We use and annotated versions thereof to denote labeled proofs. A labeled sequent is derivableiff it is the conclusion of a proof. As with display proofs, we use various metrics to quantify the size of, or certain aspects of, proofs. We define the quantity, width, and size of a proof just as in Definition 9 (though relative to labeled proofs), i.e. the quantity of a proof is equal to the number of sequents it contains, the width is defined to be the maximal length among all labeled sequents occurring in the proof, and the size is defined to be the product of the quantity and the width of the proof. For a labeled proof , we let denote the quantity, denote the width, and denote the size.
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
Figure 6: Modal rules. The side condition stipulates that in a rule application under a substitution , the label must be fresh, i.e. it cannot occur in the conclusion of the rule application.
A rule is (quantity-preserving) admissible in a calculus iff for any instance of the rule, if each premise with is derivable with a proof , then the conclusion is derivable with a proof (such that ). To simplify terminology, we write qp-admissible rather than quantity-preserving admissible. The (qp-)admissible structural rules for are shown in Figure 7. More specifically, the rules , , , and rules are qp-admissible in and is admissible [5]. The rule is called the labeled substitution rule because it applies a label substitution to any instance of the premise to obtain the conclusion. As usual, a label substitution replaces each label occurring in a labeled sequent by a label (see [38]). For example, .
Example 3
To provide the reader with intuition, we give two examples of applications of structural rules. First, let and . Applying to the rule (shown below left) yields the rule instance below right.
As in the display setting, we not only want to provide a calculus for the minimal tense logic , but also for extensions of with (simplified) primitive tense axioms, i.e. for any tense logic . To accomplish this goal, we define labeled versions of primitive tense structural rules, which have hitherto been undefined for labeled sequent calculi. Such rules are obtained in a similar fashion as in the display setting by means of transforming a simplified primitive tense axiom into a rule. This transformation is carried out via a translation function .
Definition 17 (Translation )
We recursively define the translation function that maps formulae to schematic labeled sequents.
•
•
•
•
with a new label variable
•
with a new label variable
We note that each occurrence of is taken to be a unique labeled sequent variable; e.g. both occurrences of in are taken to be unique labeled sequent variables.
Labeled sequent variables obtained from the translation are annotated with label variables and atoms. This information is crucial for defining primitive tense structural rules in the labeled setting. First, the label variables tell us which labels must be fresh in a rule instance. Second, the atoms annotating labeled sequent variables tell us what substitutions are applicable, viz. labeled sequent variables annotated with the same atom must be instantiated with isomorphic labeled sequents (see Definition 18 below). These are restrictions on what substitutions may be applied to a primitive tense structural rule and they ensure the soundness of rule applications.
Definition 18 (Isomorphic)
Let and be two labeled sequent. They are isomorphic, written , iff there exists a function such that
(1)
is bijective,
(2)
iff ,
(3)
iff ,
(4)
iff .
Let us now define primitive tense structural rules in the labeled setting. Every simplified primitive tense axiom can be transformed into a primitive tense structural rule, dubbed . By extending with the set of rules corresponding to a set of (simplified) primitive tense axioms, we obtain a labeled calculus for a primitive tense logic .
Definition 19 (Primitive Tense Structural Rule)
Each simplified primitive tense axiom of the form shown below left corresponds to a primitive tense structural rule of the following form shown below right:
The side condition stipulates that for any instance of the rule under a substitution , the following conditions must be satisfied:
for each , if the label variable occurs in , but does not occur in some labeled sequent variable, then must be fresh.
for any two labeled sequent variables of the form and (i.e. for any two labeled sequent variables annotated with the same atom) occurring in the rule, .
for any labeled sequent variable , if , then .
Contrary to the display setting, each rule retains a copy of in its premises, that is, the principal formulae are bottom-up preserved in rule applications. Formulating rules in this manner permits the qp-admissibility of contractions, so long as our calculus abides by the so-called ‘closure condition’ (cf. [5, p. 29]). To define the closure condition, let us take a rule as in Definition 19 above and suppose that we substitute certain label variables occurring in by other label variables occurring in . If, after this substitution, all premises and the conclusion mutually contain (1) at least two copies of a schematic relational atom of the form or (2) at least two copies of a labeled sequent variable of the form , then we define a contraction of to be the rule obtained by deleting one of the duplicate copies, respectively. We then say that an extension of with a set of primitive tense structural rules and contractions thereof satisfies the closure conditioniff the calculus is closed under the contraction of every primitive tense structural rule and every contraction thereof.
We note that if we close the primitive tense structural rules of an extension of under contractions, then the resulting calculus is still finite. This follows from the fact that (1) we only consider extensions of with finitely many primitive tense structural rules, and (2) because each primitive tense structural rule has only finitely many contractions as only a finite number of label variable substitutions (as described above) are possible.
To make the closure condition clearer, we provide an example of a primitive tense structural rule and a contraction of the rule.
Example 4
Let us consider the Euclidean axiom (which is a simplified primitive tense axiom). The axiom’s corresponding primitive tense structural rule is as follows:
\AxiomC
\RightLabel\UnaryInfC\DisplayProof
If we substitute the label for and , then we obtain the following:
\AxiomC
\UnaryInfC\DisplayProof
Since the schematic labeled sequent occurs twice, a contraction of can be obtained by deleting the additional copy, yielding the following:
\AxiomC
\RightLabel\UnaryInfC\DisplayProof
We note that no contractions exist of the rule as no substitution of label variables can produce duplications. As specified above, contractions are only possible when all premises and the conclusion share duplicate formulae of the form or , yet, the conclusion of is of a form that precludes this possibility.
Definition 20 ()
Let be a primitive tense logic. We define to be extended with a rule and all contractions thereof, for each simplified primitive tense axiom in . We indicate that a labeled sequent is provable in with a labeled proof by writing .
Theorem 4.1
The , , , and rules are qp-admissible in and is admissible.
Proof
Follows from Lemma 2.3.4, Theorem 2.3.6, Theorem 2.3.8, and Theorem 2.3.10 of [5].
Remark 1
The qp-admissibility of , , , and is proven in by showing that each rule can be permuted upward in any proof and deleted at initial rules (while preserving the quantity of the proof). Therefore, this method of proof, which relies on rule permutations, shows the existence of an algorithm that takes a proof with structural rules as input and returns a proof without such rules as output. Such proof transformations are computable in in the size of the input proof. This is because if our input proof is , then there are most occurrences of structural rules in , and for each such occurrence at most many permutations need to be made, showing that the algorithm performs at most many permutations. Moreover, the width of the output proof will always be bounded by . This is straightforward to verify in the , , and cases, which may reduce the length of labeled sequents when permuted upward; in the case of , which weakens in a labeled sequent , , so permuting numerous instances of upward may increase the length of the ‘longest’ labeled sequent occurring in , and thus, the width of the output proof will be at most . Since , , , and are qp-admissible, this shows that the size of the output proof is polynomial in the size of the input proof and that the proof transformations eliminating , , , and instances are computable in .
5 Labeled Polytrees
In this section, we discuss special graphs, referred to as polytrees. Intuitively, a polytree is a directed graph such that the underlying graph (i.e. the graph obtained by replacing each directed edge by an undirected edge) is a tree (i.e. is a connected, cycle-free graph). This notion is important because labeled sequents with a polytree structure are notational variants of display sequents. The importance of polytrees was first observed in works on translations between labeled and shallow-nested calculi for tense logics with general path axioms [10], which form a small sub-class of the primitive tense logics and calculi we consider. In contrast, this paper considers translations between more expressive labeled and display calculi, which requires novel methods of translation, greatly generalizing the work in [10], and leading to new insights (discussed throughout Sections 6–9).
Let us now define important terminology that will be of use throughout the remainder of the paper. We define a -flat sequent to be a labeled sequent of the form i.e. a labeled sequent without relational atoms and where all labeled formulae share the same label. When the label is not important, we sometimes refer to a -flat sequent as a flat sequent. We define the graph of a labeled sequent to be such that
In other words, the graph of a labeled sequent is a graph where each node is a label decorated with -flat sequent (obtained from the formulae labeled with in ) and each edge is obtained from a relational atom.
Definition 21 (Labeled Polytree)
Let be a labeled sequent and be its graph. We define to be a labeled polytree sequentiff (1) if , then is a -flat sequent for some , (2) if , then , and (3) forms a polytree, that is, is connected and free of (un)directed cycles. We define a labeled polytree proof to be a proof containing only labeled polytree sequents.
Example 5
To provide intuition on labeled polytree sequents, we give an example. Suppose is a -flat sequent for . The labeled polytree sequent
can be pictured as shown on the left in Figure 8. (NB. Please ignore the dashed box for the time being; this is discussed below.)
Moreover, Figure 8 also demonstrates the concept of a -partition, whereby a labeled polytree sequent may be split into two labeled polytree sequents and such that . For instance, in Figure 8, if is the left-most labeled polytree sequent, then may be partitioned into (shown in the middle) and (shown on the right) so long as .
Definition 22 (-partition)
Let and be labeled sequents. We say that and are -disjointiff . We define to be a -partition of iff (1) , (2) and are labeled polytree sequents, and (3) and are -disjoint.
Figure 8: Examples of labeled polytree sequents , , and (read from left to right). If , then and serve as a -partition of , i.e. (see Definition 22). The dashed region contains the labeled polytree sequent that serves as a subpolytree sequent of (see Definition 23).
The concept of a subpolytree sequent will also be of use to us; in particular, to define certain recursive operations on the structure of a given labeled polytree sequent. For example, let us consider the labeled sequent shown in the left of Figure 8. The subpolytree sequent rooted at relative to , denoted , is the labeled sequent within the dashed region.
Definition 23 (Subpolytree Sequent)
If is a labeled polytree sequent with (or, ), then is defined to be the unique labeled polytree sequent, referred to as a subpolytree sequent, such that there exists a labeled polytree sequent and (respectively, ).
Let us now prove a few useful facts about the relationship between labeled polytree sequents and provability in . It will be useful to identify what proofs in are labeled polytree proofs since—as shown in Sections 7 and 8—such proofs translate to and from display proofs in . Toward this end, it will be helpful to consider rules in that preserve the polytree structure of labeled sequents when applied.
First, one can verify that for any rule in , the conclusion of is a labeled polytree sequent iff every premise is a labeled polytree sequent, i.e. the property of being a labeled polytree sequent is both top-down and bottom-up preserved in . For instance, if we consider the , , , and rules, then we notice that every rule bottom-up introduces a relational atom from a label already occurring in the labeled sequent to a fresh label, and thus, the conclusion is a labeled polytree sequent iff the premise is a labeled polytree sequent, albeit, the premise has an additional protruding edge/relational atom. Regarding the remaining rules of , each rule both top-down and bottom-up preserves the relational atoms of the premises and conclusion, respectively, meaning each premise will be a labeled polytree sequent iff the conclusion is. Therefore, we have the following:
Proposition 3
Let be a non-initial rule in . The premises of are labeled polytree sequents iff the conclusion is.
By the above proposition, we know that every rule in preserves the property of being a labeled polytree sequent. Yet, the question remains: is this also true for primitive tense structural rules? In general, the answer is ‘no’ as primitive tense structural rules can introduce disconnectedness and (un)directed cycles when applied. For instance, the primitive tense structural rule corresponding to the reflexivity axiom is shown below left. As shown below right, by applying the substitution such that , , , and , we obtain a valid instance of the rule which contains the loop .
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
Nevertheless, observe that if we apply a different substitution to such that , , , , and , then we obtain the following instance of the rule containing only labeled polytree sequents.
\AxiomC
\RightLabel\UnaryInfC\DisplayProof
This observation suggests that certain instances of primitive tense structural rules bottom-up preserve the polytree structure of the conclusion while others do not. In general, we find that if a certain set of conditions are satisfied, then each premise of a primitive tense structural rule will be labeled polytree sequent so long as the conclusion is. We list these conditions below and define the corresponding notion of a strict application.
Definition 24 (Strict)
Let be of the form shown in Definition 19 with . We say that an application of under a substitution is strictiff it satisfies conditions – as well as the following conditions:
for any two label variables and , if , then .
for any two occurrences of labeled sequent variables and , if , then ; otherwise, .
if , then .
for any occurrence of a labeled sequent variable , is a labeled polytree sequent.
A strict proof in is a proof such that every instance of is strict.
We aim to show that if a proof in is strict, then it is a labeled polytree proof. Let us therefore analyze the structures present in a primitive tense structural rule. Observe that the function takes a formula from the language and returns a schematic labeled sequent that forms a polytree. This follows from the fact that every time a or modality is encountered, the function adds a schematic relational atom to or from a fresh label variable (see Definition 17 above). For instance, if we consider the formula , then
which can be pictured as the polytree shown top left in Figure 9.
We define the graph of a schematic labeled sequent to be such that (1) iff occurs in and and (2) iff occurs in . A schematic labeled sequent forms a polytreeiff its graph is a polytree, i.e. is connected and free of (un)directed cycles. The following lemma is straightforward to prove:
Figure 9: A graphical depiction of the schematic labeled sequent , which forms a polytree, is shown top left. The top right graph and the three bottom graphs demonstrate how strict labeled substitutions can be applied to merge two isomorphic subpolytree sequents and so that every labeled sequent generated is a labeled polytree sequent.
Lemma 1
If , then the schematic labeled sequent forms a polytree.
Lemma 2
The premises and conclusion of a strict instance are labeled polytree sequents.
Proof
Let be a primitive tense structural rule of the form shown below. We consider a strict instance of under the substitution are argue that (for ) and are labeled polytree sequents.
First, by Lemma 1, we know that the schematic relational atoms of all schematic labeled sequents occurring in form a polytree. Let be the set of all labels in the range of . Also, let and . By condition , we know that is injective over the set of label variables occurring in its domain, meaning that and form polytrees. By condition , all labeled sequent variables will be instantiated with labeled polytree sequents, and by conditions and , we know that all such label polytree sequents (if not the empty sequent) will only intersect at a single label occurring in either or . As ‘fusing’ a single node of a polytree to a single node of another polytree forms a polytree, we are ensured that (for ) and will be labeled polytree sequents.
Theorem 5.1
If is a strict proof in of a labeled polytree sequent , then is a labeled polytree proof.
We end this section by discussing qp-admissible structural rules that preserve the polytree structure of labeled sequents when applied. One can see that the conclusion of a and application is a labeled polytree sequent if the premise is; however, this is not generally true for and (shown in Figure 7). We therefore define strict versions of these rules that preserve polytree structure.
Definition 25
We define to be an instance of under that satisfies the following condition: there exists a such that either or with . Effectively, either identifies two children nodes of a single parent node or two parent nodes of a single child node in , that is, it takes one of two forms shown below.
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
We define to be an instance of under that satisfies the following conditions: (1) is a label polytree sequent and (2) if , then . Effectively, introduces a labeled polytree sequent that intersects a single node (if one occurs) in .
Example 6
It is simple to verify that if the premise of a application is a labeled polytree sequent, then its conclusion is as well. We therefore show that always yields a labeled polytree sequent when applied to one. Moreover, as it will be important for our work in Section 7, we also show how can be repeatedly applied to ‘merge’ two isomorphic subpolytree sequents. Suppose we are given a labeled polytree sequent of the form:
where and for , . Also, suppose , , , , , and is a -flat, -flat, -flat, -flat, -flat, -flat, -flat sequent, respectively. Then, can be pictured as the top right polytree in Figure 9. By applying the label substitutions , , and , we obtain the bottom left, bottom middle, and bottom right graphs, respectively, where , , and . Observe that each graph is a polytree, exemplifying that strict label substitutions can always be applied to preserve the labeled polytree property.
Theorem 5.2
Let . (1) If is applied to a labeled polytree sequent, then the conclusion is a labeled polytree sequent. (2) Eliminating from a strict proof via upward permutations yields a strict proof.
Proof
We prove claim (2) since claim (1) is straightforward. We consider a representative number of cases in our proof of claim (2); the remaining cases and sub-cases are tedious, but go through. We argue that any strict application of followed by an application of can be replaced by applications of to the premises of followed by a strict application of , yielding the same conclusion. We only consider cases when is either or as the and cases are similar.
. Suppose we have an instance of followed by an instance of , as shown below, such that .
Either occurs in , occurs in , or one occurs in and the other occurs in . We argue the first case as the last two cases are similar. Since is a schematic labeled sequent that consists of schematic relational atoms and labeled sequent variables, it must be the case that either (1) there is some labeled sequent variable in such that occurs within , or (2) there are two labeled sequent variables and in such that one occurs in and the other occurs in . In case (1), we know that is of the form . We resolve the case by defining a new substitution such that and for any other label, atomic, formula, or labeled sequent variable occurring in , . In the case (2), we know that is of the form and is of the form . We resolve the case by defining a new substitution such that , , and for any other label, atomic, formula, or labeled sequent variable such that occurring in , . In both cases, we define the substitution such that , , and for .
We can now permute above as shown below. One can confirm that is strict under as all conditions – (see Definition 24) still hold after the permutation; in particular, will hold because we assume that any atom occurs at most once in by Definition 5.
We let , , and assume w.l.o.g. that takes the form shown above. Either occurs in , occurs in , or occurs in and occurs in (or, vice versa). We argue the first case as the remaining cases are similar. If occurs in , then there are four possibilities: (1) there exist schematic relational atoms and in such that and , (2) there exists a schematic relational atom and labeled sequent variable in such that and occurs in (or, vice versa), (3) there exists a labeled sequent variable in such that both and occur in , or (4) there exist labeled sequent variables and such that occurs in and occurs in . We consider case (1) and note that cases (2)–(4) can be argued in a similar manner.
By assumption, is of the form . We assume that the labeled sequent variables and occur in and note that the remaining cases (where no labeled sequent variable annotated with the label variable or occurs) are similar. Therefore, is of the form .
By the closure condition (see p. 19) and Definition 20, we know that contains a contraction of the rule , which we dub , that contains rather than . Let and for and . We define such that
and for all remaining atomic, formula, and labeled sequent variables occurring in , . In essence, the substitution ‘shifts’ all of the labeled polytree sequents rooted at to . We now define the substitution such that and for . We can permute upward to derive the same conclusion, if we apply under to the premise of under , and then apply under . Moreover, it can be checked that under is strict.
6 Translating Display and Labeled Notation
In this section, we define functions that translate display sequents into labeled polytree sequents and vice versa, which will be employed in translating display and labeled proofs in the following two sections. Our translations provide new insights into the relationship between the display and labeled formalisms. Interestingly, we find that display structures are inter-translatable with labeled polytree sequents, and display sequents likewise inter-translate with (compositions of) labeled polytree sequents. Moreover, display equivalent sequents translate to isomorphic labeled sequents (Lemma 4). All of this suggests that the labeled formalism is more compact and exhibits far less bureaucracy than the display formalism since seemingly distinct objects in the display formalism are easily recognized as identical in the labeled formalism.444The excessive bureaucracy of display calculi, which obfuscates identities on proofs, has been discussed in prior works [10, 36].
The first half of this section is dedicated to defining the translation of display sequents into labeled polytree sequents and proving certain properties thereof. The latter half of the section considers the reverse translation.
Definition 26 (Translation )
Let be a display sequent. We define the translation , where and translate display structures into labeled (polytree) sequents recursively as follows:
•
•
•
•
•
•
•
•
•
•
We note that and are fresh labels in the above translations.
Example 7
We provide an example of translating a display sequent into a labeled sequent.
Observe that when encounters a connective, it adds a relational atom to or from a fresh label, thus ensuring that the resulting labeled sequent is free of (un)directed cycles. In addition, as translates both the antecedent and consequent from the same label , the resulting labeled sequent will be connected. Hence, the above translation will always yield a labeled polytree sequent (as seen in the example above). We also find that for two reasons: first, there is a one-to-one correspondence between each bullet and formula occurrence in and each relational atom and labeled formula in . Second, the length of a labeled sequent is defined by the number of relational atoms and labeled formulae it contains, though may still contain other connectives (e.g. and ) that contribute to its length. (NB. Recall that the length of a display sequent was defined at the beginning of Section 3 and the length of a labeled sequent was defined at the beginning of Section 4.)
Lemma 3
Let be a display sequent. Then,
1.
is a labeled polytree sequent;
2.
;
3.
for , .
The translation also sheds light on which display calculus rules are rendered redundant in the labeled setting, as stated in the lemma below.
Lemma 4
Suppose that is derivable from by applying a display rule, , , , , , , , or . Then, .
Proof
We show the , , , and cases; the remaining cases are similar.
We note that the last step in the derivation follows from Lemma 3. All remaining steps in each derivation either follow from the definition of or by the properties of sequent composition.
Let us now discuss the reverse translation, i.e. translating labeled sequents to display sequents. Our translation relies on a couple operations, which we now define. First, given that are structures, we define
Second, if is a multiset of labeled formulae, then we define . If is not a label in , then , which includes the case when . Utilizing these two operations, we define the function as follows.
Definition 27 (Translation )
Let be a labeled polytree sequent with , , and . We define .
In the cases where , we assume that are all relational atoms occurring in of the form and that are all relational atoms occurring in of the form .
Example 8
Let us take the labeled sequent , which admits the following -partition:
We translate this into a display sequent (as shown below) by applying Definition 27.
With minor effort, the deductively equivalent display sequent can be derived from , which was the display sequent that translated to in the previous example.
Remark 2
For any labeled polytree sequent and label , there exists a polynomial such that .
The above translation is defined relative to a given -partition of the input labeled polytree sequent , and so, the question naturally arises if the choice of partition affects the result of the translation. As it so happens, each partition of the input may yield a distinct display sequent as the output, yet, all such display sequents are mutually derivable from one another using only polynomially many inferences in . We prove this fact in Lemma 7 below, but first prove two helpful lemmata.
Lemma 5
Let be a labeled polytree sequent with . For any two partitions and of , .
Proof
Let be a labeled polytree sequent with . Furthermore, let and be -partitions of with , , , and . It follows that and . In the translations and , we let and be as follows.
Let us now prove that . We note that the and rules are applied a sufficient number of times below to re-write as and as .
Let be a labeled polytree sequent. The following rules are derivable in :
\AxiomC\doubleLine\UnaryInfC\DisplayProof
\AxiomC\doubleLine\UnaryInfC\DisplayProof
\AxiomC\doubleLine\UnaryInfC\DisplayProof
\AxiomC\doubleLine\UnaryInfC\DisplayProof
Proof
We prove the lemma by induction on the number of labels in , and prove the claim for the first rule; the remaining cases are similar.
Base case. If , then the claim follows trivially by the rule. Let us suppose that , where every labeled formula in and has the same label . Then, the rule is derived as shown below, where and .
Inductive step. Let us suppose that contains labels. By Definition 27, is equal to the following display sequent.
Observe that each and is an a-part. Hence, we can invoke the display theorem (Theorem 3.2) to display each such structure; then, by applying IH (which is permitted since each labeled sequent and has a fewer number of labels), we obtain the following equivalent display sequent.
Using display and reversible structural rules, we may derive the following display sequent.
The above display sequent is equal to , thus giving us our desired conclusion. Also, we note that all of the rules used to derive the conclusion are reversible, implying that the premise may be derived from the conclusion as well.
Lemma 7
Let be a labeled polytree sequent with . Then, there exists a polynomial such that and are mutually derivable from one another with at most many reversible rule applications.
Proof
Let . We first argue that by induction on the length of the minimal path of relational atoms in from to . After, we argue that only polynomially many reversible rules were applied to derive from . Let us consider two partitions of , namely, (i) with and , and (ii) . By Lemma 5, and may be any arbitrary -partition and -partition of .
Base case. We assume that length of the minimal path between and is is one as the case when the length of the minimal path is zero (i.e. ) follows from Lemma 5 above. We prove that and have four cases to consider: either , , , or . We argue the first case as the others are proven in a similar fashion.
The display sequent is of the form shown below top, and we let for convenience.
We may now apply the following sequence of rules to the display sequent above to derive the conclusion shown below.
from the former display sequent above. By Lemma 5, since is a -partition of , we know that , and so, we have shown that since only display and reversible structural rules were used above.
Inductive step. Suppose that the length of the minimal path of relational atoms between and is . Then, there exists a label such that the length of the minimal path from to is at most length and length of the minimal path from to is . Hence, by IH , and , which implies the desired result and concludes the inductive step.
Last, observe that only reversible rules were used in the proofs of
Lemma 5, Lemma 6, and in the derivation of from above. Furthermore, the number of rules applied only depends on the length of the path from to in along with the number of incoming and outgoing edges (i.e. relational atoms) from nodes (i.e. labels) along this path. The above proof describes an algorithm that takes this path with incoming and outgoing edges as input and computes successive rule applications by processing ever smaller terminal segments of this path until is reached. Since the length of the path , one can verify that for a polynomial , -many reversible inferences occur in the derivation of from .
7 From Display to Labeled Proofs
We show how to translate each display proof in into a strict labeled polytree proof in . Moreover, we argue that this translation is computable in and does not increase the size of the proof. This result is significant for the following reasons: first, we establish that each labeled calculus can polynomially simulate each display calculus , showing that display calculi cannot outperform (in terms of complexity) labeled calculi. Second, we identify what subspace of labeled proofs correspond to display proofs, and in the following section, we show that each labeled proof within this space can be translated in into a display proof as well, giving a characterization result. In essence, we find that display calculi are a restriction of labeled calculi and that the space of display proofs is a fragment of the space of labeled proofs.
Let us first show how to translate proofs from the base system into . In the sequel, we explain how this translation can be augmented to translate primitive tense structural rules as well, giving the main result of the section (Theorem 7.2).
Theorem 7.1
If , then there exists a function in such that , , and is a labeled polytree proof.
Proof
Suppose . We show by induction on the quantity of that it can be translated in into a labeled polytree proof of in such that . By Lemma 4, we need not translate instances of , , , , , , , , or the display rules, as all such rules produce isomorphic or identical labeled polytree sequents under the translation. Below, when we invoke the qp-admissibility of (Theorem 4.1), we note that will always be an instance of , which ensures that the polytree structure of labeled sequents in the target proof will be preserved (Theorem 5.2).
Base case. We show how the initial rules , , and are translated from to initial rules in . Observe that each initial sequent is a labeled polytree sequent.
Inductive step. For the inductive step, we give a few interesting cases of translating inferences from the given display proof into the target labeled proof. The remaining cases can be found in the appendix as they are either simple or similar. In each case, it can be checked that the result is a labeled polytree proof.
When translating the rule below, observe that we invoke the qp-admissibility of (Lemma 4.1) to ensure that the contexts of the premises in the labeled proof match.
As can be seen below, relies on the qp-admissibility of , , and in . After is obtained, we apply to identify the two isomorphic copies of , making both copies identical, and then the contraction rules and are applied to contract identical labeled formulae, yielding the desired conclusion. We note that these operations can be applied in a manner to produce a labeled polytree proof as the output (see Example 6).
It is straightforward to check that the above translation is in relative to since each display sequent in is translated in and each qp-admissible rule application transforms the target proof in (Remark 1). Also, since each inference translated derives a labeled polytree sequent, will be a labeled polytree proof by Proposition 3. One can confirm in each case that since either a single inference is performed in the target proof, an qp-admissible rule (that does not appear in the target proof) is applied, or a redundant, ineffectual inference occurs (see Lemma 4). By Lemma 3, we know that for each in the input proof . Nevertheless, it is possible for the length of a labeled polytree sequent to increase in the target proof if the qp-admissibility of is applied. However, the length can only increase by at most since applying the qp-admissibility of in the target proof runs an algorithm (see Remark 1) that permutes upward and ‘deposits’ at most amount of syntactic material in each labeled sequent (increasing its length) at most many times. Putting all of the above together, we have that
showing that .
Let us now consider translating display proofs to labeled (polytree) proofs in the presence of primitive tense structural rules. We carry out this translation by considering an instance of a primitive tense structural rule under a substitution , and show that the instance can be translated via to an instance of under a related substitution, denoted . This is sufficient to prove the main result of this section (Theorem 7.2), which states that each proof in can be translated in into a strict labeled polytree proof in such that the quantity of the proof does not grow.
Let us consider an instance of a primitive tense structural rule under a substitution , as shown below.
Let us assume that are all of the structure variables occurring in the rule above with a substitution of the following form:
To translate the above instance of to an instance of under , we define the substitution accordingly:
In the definition of above, we let all labels in , , , and be fresh with the exception of , , , and , respectively. We note that if for , then for each labeled sequent variable in annotated with , we have and for . In other words, the substitution of a structure for a single structure variable in may give rise to multiple substitutions of labeled polytree sequents for multiple labeled sequent variables in .
Example 9
We give an example of translating an instance of into an instance of . The rule (shown below left) corresponds to the simple primitive tense axiom , where we let and . An instance of the rule under the substitution is shown below right.
\AxiomC\RightLabel\UnaryInfC\DisplayProof
\AxiomC\RightLabel\UnaryInfC\DisplayProof
If we transform into , we obtain the rule shown below.
\AxiomC
\RightLabel\UnaryInfC\DisplayProof
To obtain the corresponding instance of , we apply the following substitution
where , , , and . Applying to gives the following strict instance of the rule.
\AxiomC
\RightLabel\UnaryInfC\DisplayProof
It is interesting to observe that under translates via into under . Since retains a copy of in its premise, we must include a copy of when translating the premise of under as shown below.
Alternatively, the conclusion of under translates to the conclusion of under without modification: .
As demonstrated in the example above, instances of translate to strict instances of . We use this fact below to prove the main result of the section (Theorem 7.2), however, it will be helpful to first prove the following lemma.
Lemma 8
Let us consider an instance of a primitive tense structural rule as shown below.
We first prove claim 1 by induction on the complexity of .
Base case. If is an atom , then and the proof shown below left demonstrates the claim. If is the logical constant , so that , then the proof shown below right demonstrates the claim.
Inductive step. We consider the cases where , , and in turn. First, if , so that , then the following proof establishes the case.
If , so that , then the proof shown below left establishes the case, and if , so that , then the proof shown below right establishes the case.
The following establishes claim 2 and invokes claim 1 in the third to fourth line.
Theorem 7.2
If , then there exists a function in such that , , and is a strict labeled polytree proof.
Proof
The proof is obtained by extending the inductive step of Theorem 7.1 with the case. Therefore, let us consider an instance of as shown below top. We translate it into the instance shown below bottom, where each equality step is obtained from Lemma 8.
By the definition of and , it is straightforward to confirm that the conditions – hold, showing that the application of is strict. Since our proof extends the proof of Theorem 7.1, only introduces strict instances, and the target proof derives a labeled polytree sequent, we know will be a strict labeled polytree proof by Theorem 5.1. Moreover, as seen above, each instance of translates to a single instance of and may invoke the qp-admissibility of . By an argument similar to the one at the end of Theorem 7.1, one can confirm that the translation is computed in and .
8 From Labeled to Display Proofs
We now study the reverse translation, showing how to transform strict labeled polytree proofs into display proofs. We find that translating a strict labeled polytree proof gives a display proof with a higher quantity due to the introduction and use of display rules and structural rules in . Nevertheless, the translation occurs within , and so we definitively confirm that the largest class of analytic (i.e. cut-free) display calculi for tense logics can be polynomially simulated by analytic labeled sequent calculi. This result solves an open problem first discussed by Restall in 2006 [32], which was also left as an open problem in [10], concerning the existence of embeddings between labeled and display proofs.555In [10], it was shown how to translate labeled proofs into ‘one-sided’ display calculus (i.e. shallow nested calculus) proofs for a small subclass of primitive tense logics, namely, extension of with path axioms of the form with for .
Theorem 8.1
If and is a labeled polytree proof, then there exists a function in and polynomial such that and .
Proof
We prove the result by induction on the quantity of and make a case distinction on the last rule applied. We consider a representative number of cases and remark that the remaining cases are similar. In each case, we translate a suitable -partition of the input labeled polytree sequent. By Lemma 5 we are permitted to select any -partition to translate.
Base case. We show the case below and let , , and .
. In the second to third step in the target proof, we apply the definition of and let . By Proposition 2 we are allowed to apply the and rules in the target proof. Also, in the ninth and tenth lines, we let and .
This concludes the proof of the inductive step. Let us now analyze the complexity of the translation and the relative sizes of the input and target proofs.
Observe that each (logical) rule application in is considered once and adds a single logical rule application in the target proof. Furthermore, each application of Lemma 7 adds only polynomially many inferences to the target proof and only a constant number of display and structural rules are added to the target proof beyond these inferences, meaning for some polynomial , . Also, each display sequent in the target proof is polynomial in by Remark 2. Therefore, the translation takes place in and , for some polynomial .
We now show how to extend the above translation to cover strict primitive tense structural rules. To carry out this translation, we suppose that we have a strict instance of under a substitution , and show that this rule instance can be translated via to an instance of under a substitution . Therefore, let the following be a strict instance of :
To translate the above instance of to an instance of under , we define the substitution accordingly:
We note that multiple labeled sequent variables annotated with the same propositional atom may occur in , while in only a single structure variable annotated with will occur. By condition (see Definition 19), we know that .
Therefore, , meaning we can arbitrarily choose any labeled sequent with to use to substitute for in . As shown above, we simply choose the first labeled sequent mentioned in in defining the substitution . The interested reader should consult Example 9 in the previous section to see how an instance of is obtained from an instance of by reversing the example and viewing in the example as .
Lemma 9
Let us consider a strict instance of a primitive tense structural rule as shown below.
We prove claim 1 by induction on the complexity of . Claim 2 follows from claim 1.
Base case. If is an atom , so that and , then the proof shown below right proves the case. If is the logical constant , so that , then the proof shown below right establishes the case.
Inductive step. We consider the cases where , , and in turn. In the first case, we have that , and the proof below establishes the claim in this case. The third to fourth step below follows from the fact that is strict; in particular, satisfies conditions , , and (see Definition 24).
The proof of the second case is shown below left, where , and the proof of the final case is shown below right, where .
Theorem 8.2
If and is a strict labeled polytree proof, then there exists a function in and polynomial such that and .
Proof
We prove the result by extending the inductive step of Theorem 8.1 with the case. Let us suppose we are translating a strict labeled polytree proof , and let us consider a strict instance of as shown below top. The desired translation is obtained as shown below bottom, where the steps follow from Lemma 7 and the equality steps are obtained by Lemma 9.
By an argument similar to the one at the end of Theorem 8.1, it follows that is computable in and , for some polynomial .
9 Concluding Remarks
We have established a correspondence between the maximal analytic class of display calculi for tense logics (namely, all display calculi for primitive tense logics) and labeled sequent systems, thus solving an open problem posed in [10, 32]. Our translations show that the space of cut-free display proofs is polynomially equivalent to the space of strict labeled proofs. We also find that translating from display to labeled preserves (or decreases) the quantity of the proof, while potentially increasing the width; the reverse translation brings about a polynomial increase in the size of the proof. Moreover, we made the interesting observation that display structures translate to labeled polytree sequents and that all display equivalent sequents translate to the same labeled sequent (up to isomorphism), showing that labeled sequents are a canonical representation of display sequents that enjoy less bureaucracy.
A fascinating avenue of future research would be to study translations and the computational relationship between strict labeled proofs and non-strict labeled proofs (which might include labeled sequents not in a polytree form). Composing such translations with the translations in this paper would confirm if it is possible or not to translate any analytic display proof into any analytic labeled proof, or vice versa, in . Transforming a strict labeled proof into a non-strict one, where labeled sequents may include disconnectivity or (un)directed cycles, is simple to obtain by applying (1) the hp-admissibility of to add disjoint regions to labeled sequents in the proof, and (2) by applying the hp-admissibility of to identify labels, bringing about the formation of cycles. Showing the converse, i.e. that any non-strict labeled proof can be obtained from a strict proof via applications of and (up to admissible permutations of rules in a proof), appears far more challenging and may require new proof-theoretic techniques (or, operations beyond weakenings, label substitutions, and permutations).
Nevertheless, the above suggested correspondence between strict and non-strict labeled proofs would imply that every non-strict labeled proof is essentially a homomorphic image of a strict proof. This would tell us that display calculi are a special fragment of labeled calculi that generate proofs homomorphically mappable into any other proof of the same conclusion (up to admissible permutations of rules). It is not clear if transforming non-strict proofs into strict proofs is possible in however (assuming ) as finding the correct ‘homomorphic map**’ from a strict to a non-strict proof may require an algorithm (cf. [20]).
References
[1]
A. Avron.
The method of hypersequents in the proof theory of propositional
non-classical logics.
In W. Hodges, M. Hyland, C. Steinhorn, and J. Truss, editors, Logic: From Foundations to Applications: European Logic Colloquium, page
1–32. Clarendon Press, USA, 1996.
[2]
F. Baader, I. Horrocks, C. Lutz, and U. Sattler.
Introduction to Description Logic.
Cambridge University Press, 2017.
[3]
N. D. Belnap.
Display logic.
Journal of philosophical logic, 11(4):375–417, 1982.
[4]
P. Blackburn, M. de Rijke, and Y. Venema.
Modal Logic, volume 53 of Cambridge Tracts in Theoretical
Computer Science.
Cambridge University Press, 2001.
[5]
B. Boretti.
Proof Analysis in Temporal Logic.
PhD thesis, University of Milan, 2008.
[7]
L. Buisman and R. Goré.
A cut-free sequent calculus for bi-intuitionistic logic.
In N. Olivetti, editor, Automated Reasoning with Analytic
Tableaux and Related Methods, pages 90–106, Berlin, Heidelberg, 2007.
Springer Berlin Heidelberg.
[8]
R. A. Bull.
Cut elimination for propositional dynamic logic without *.
Z. Math. Logik Grundlag. Math., 38(2):85–100, 1992.
[9]
C. Castellini and A. Smaill.
A systematic presentation of quantified modal logics.
Logic Journal of the IGPL, 10(6):571–599, 2002.
[10]
A. Ciabattoni, T. S. Lyon, R. Ramanayake, and A. Tiu.
Display to labeled proofs and back again for tense logics.
ACM Trans. Comput. Logic, 22(3), July 2021.
[11]
A. Deutsch, A. Nash, and J. B. Remmel.
The chase revisited.
In M. Lenzerini and D. Lembo, editors, Proceedings of the 27th
ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems
(PODS’08), pages 149–158. ACM, 2008.
[12]
R. Dyckhoff.
Contraction-free sequent calculi for intuitionistic logic.
The Journal of Symbolic Logic, 57(3):795–807, 1992.
[13]
M. Fitting.
Tableau methods of proof for modal logics.
Notre Dame Journal of Formal Logic, 13(2):237–247, 1972.
[14]
D. M. Gabbay.
Labelled deductive systems, volume 33 of Oxford Logic
guides.
Clarendon Press/Oxford Science Publications, 1996.
[15]
G. Gentzen.
Untersuchungen über das logische schließen. i.
Mathematische zeitschrift, 39(1):176–210, 1935.
[16]
G. Gentzen.
Untersuchungen über das logische schließen. ii.
Mathematische Zeitschrift, 39(1):405–431, 1935.
[17]
J.-Y. Girard.
Linear logic.
Theoretical computer science, 50(1):1–101, 1987.
[18]
R. Goré.
Substructural logics on display.
Logic Journal of the IGPL, 6(3):451–504, 05 1998.
[19]
R. Hein.
Geometric theories and proof theory of modal logic.
Master’s thesis, Technische Universität Dresden, 2005.
[20]
P. Hell and J. Nesetril.
Graphs and Homomorphisms.
Oxford University Press, 07 2004.
[21]
S. Kanger.
Provability in logic.
Almqvist & Wiksell, 1957.
[22]
R. Kashima.
Cut-free sequent calculi for some tense logics.
Studia Logica, 53(1):119–135, 1994.
[23]
M. Kracht.
Power and weakness of the modal display calculus.
In H. Wansing, editor, Proof Theory of Modal Logic, pages
93–121. Springer Netherlands, Dordrecht, 1996.
[24]
S. A. Kripke.
Semantical considerations on modal logic.
Acta Philosophica Fennica, 16:83–94, 1963.
[25]
B. Lellmann.
Linear nested sequents, 2-sequents and hypersequents.
In H. 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.
[26]
T. Lyon, A. Tiu, R. Goré, and R. Clouston.
Syntactic interpolation for tense logics and bi-intuitionistic logic
via nested sequents.
In M. Fernández and A. Muscholl, editors, 28th EACSL
Annual Conference on Computer Science Logic (CSL), volume 152 of LIPIcs, pages 28:1–28:16. Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2020.
[27]
S. Maehara.
On the interpolation theorem of craig.
Sûgaku, 12(4):235–237, 1960.
[28]
K. L. McMillan.
Interpolation and model checking.
In E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, editors,
Handbook of Model Checking, pages 421–446. Springer International
Publishing, Cham, 2018.
[29]
G. Mints.
Indexed systems of sequents and cut-elimination.
Journal of Philosophical Logic, 26(6):671–696, 1997.
[30]
G. Pottinger.
Uniform, cut-free formulations of t, s4 and s5.
Journal of Symbolic Logic, 48(3):900, 1983.
[31]
A. N. Prior.
Time and Modality.
Oxford University Press, 1957.
[33]
A. 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.
[34]
J. K. Slaney.
Minlog: A minimal logic theorem prover.
In W. McCune, editor, Automated Deduction - CADE-14,
Proceedings, volume 1249 of Lecture Notes in Computer Science, pages
268–271. Springer, 1997.
[35]
R. M. Smullyan.
First-Order Logic.
Springer-Verlag, 1968.
[36]
P. Stouppa.
The design of modal proof theories: The case of s5.
Master’s thesis, Technische Universität Dresden, 2004.
[37]
K. van Berkel and C. Straßer.
Reasoning with and about norms in logical argumentation.
In F. Toni, S. Polberg, R. Booth, M. Caminada, and H. Kido, editors,
Computational Models of Argument - Proceedings of COMMA 2022, volume
353 of Frontiers in Artificial Intelligence and Applications, pages
332–343. IOS Press, 2022.
[38]
L. Viganò.
Labelled Non-Classical Logics.
Springer Science & Business Media, 2000.
[39]
H. Wansing.
Sequent calculi for normal modal propositional logics.
Journal of Logic and Computation, 4(2):125–142, 1994.
[40]
F. Wolter.
On logics with coimplication.
Journal of Philosophical Logic, 27(4):353–387, 1998.