Sequent calculi and interpolation for non-normal modal and deonticlogics
Eugenio Orlandelli


Advanced Digital Signal Processing Techniques for High-Speed Optical Communications Links
    Dario Pilori
    December 30, 2023
=========================================================================================



   G3-style sequent calculi for the logics in the cube of non-normal modal logics and for their deontic extensions are studied. For each calculus we prove that weakening and contraction are height-preserving admissible, and we give a syntactic proof of the admissibility of cut. This implies that the subformula property holds  and that derivability can be decided by a terminating proof search whose complexity is in Pspace. These calculi are shown to be equivalent to the axiomatic ones and, therefore,  they are sound and complete with respect to neighbourhood semantics.  Finally,  it is given a Maehara-style proof of Craig's interpolation theorem for most of the logics considered.

Keywords: Non-normal logics, deontic logics, sequent calculi,   structural proof theory, interpolation,  decidability.




§ INTRODUCTION


For many interpretations  of the modal operators – e.g., for deontic, epistemic,  game-theoretic, and high-probability interpretations – it is necessary to adopt logics that are weaker than the normal ones; e.g., deontic paradoxes, see <cit.>,  are one of the main motivations for adopting a non-normal  deontic logic. Non-normal  logics, see <cit.> for naming conventions,  are quite well understood from a semantic point of view  by means of neighbourhood semantics  <cit.>.
  Nevertheless, until recent years their proof theory has been rather limited  since it was mostly confined to Hilbert-style axiomatic systems. This situation seems to be rather unsatisfactory since it is difficult to find derivations in axiomatic systems. When the aim is to find derivations and to analyse their structural properties, sequent calculi are to be preferred to  axiomatic systems. Recently  different kinds of sequent calculi for non-normal logics have been proposed: Gentzen-style calculi  <cit.>; labelled <cit.> and display <cit.> calculi based on  translations into normal modal logics; labelled calculi based on the internalisation of neighbourhood  <cit.> and  bi-neighbourhood  <cit.> semantics;   and, finally, 
 
  
 This paper, which extends the results  presented in <cit.>,  concentrates on Gentzen-style calculi since they are better suited than labelled calculi, display calculi, and  nested sequents to give  decision procedures (computationally well-behaved) and constructive proofs of interpolation theorems. We consider cut- and contraction-free G3-style sequent calculi for all the logics in the cube of non-normal modalities and for their  extensions with the deontic axioms D^:=Ø A→ A and D^:=Ø.  The calculi we present have the subformula property and  allow for a straightforward decision procedure by a terminating loop-free proof search. Moreover, with the  exception of the calculi for EC(N) and its deontic extensions, they are standard <cit.> – i.e., each operator is handled by a finite number of rules with a finite number of premisses – and they admit of a Maehara-style constructive proof of Craig's interpolation  theorem.
 
 This work improves on previous ones  on Gentzen-style calculi for non-normal logics  in that we  prove cut admissibility   for non-normal modal and deontic logics, and not only for the modal ones  <cit.>. Moreover, we prove height-preserving admissibility of weakening and contraction, whereas neither weakening nor contraction is admissible in <cit.> and weakening but not contraction is admissible in <cit.>. The admissibility of contraction is a major improvement since, as it is well known, contraction can be as bad as cut for  proof search: we may continue to duplicate some formula forever  and, therefore,  we need a (computationally expensive) loop-checker to ensure termination.  Proof search  procedures based on contraction-free calculi terminate because the height of derivations is bounded by a number depending on the complexity of the end-sequent and, therefore, we avoid the need of  loop-checkers.  To illustrate, the introduction  of contraction-free calculi has allowed to give computationally optimal decision procedures for propositional intuitionistic logic  (𝐈𝐋_𝐩) <cit.> and for the normal modal  logics K and T <cit.>.   The existence of a loop-free terminating decision procedure has also allowed  to give a constructive proof of uniform interpolation for 𝐈𝐋_𝐩 <cit.> as well as for  K and T <cit.>.  The cut- and contraction-free calculi for non-normal logics considered here are such that the height of each derivation is bounded by the weight of its end-sequent and, therefore, we easily obtain a polynomial space upper complexity bound for proof search. This upper bound  is  optimal for the  logics  having C  as theorem (the satisfiability problem for non-normal modal logics without C   is in  NP, see <cit.>).
 
  Moreover,  the introduction of well-behaved calculi for non-normal deontic logics is interesting since  proof analysis can be applied to  the deontic paradoxes <cit.> that are one of the central topics of deontic reasoning. We illustrate this in Section  <ref> by considering Forrester's Paradox <cit.> and by showing that proof analysis cast  doubts on the widespread opinion <cit.> that Forrester's argument provides evidence against rule RM (see Table <ref>).
If   Forrester's argument  is formalized as in <cit.> then  it does not compel us to adopt a deontic logic weaker than KD. If, instead, it is formalised as in <cit.> then it forces the adoption of a logic where RM fails, but the formal derivation  differs substantially from Forrester's informal argument. 
 
 It is also given a constructive proof of interpolation for all logics having a standard calculus. To our knowledge in the literature there is no other constructive  study of interpolation in non-normal  logics.  In <cit.> a constructive proof of Craig's (and Lyndon's)  interpolation theorem is given for the modal logics K and R, and for some of their extensions, including the deontic ones, but the proof makes use of model-theoretic notions. A proof of interpolation by the  Maehara-technique for KD is given in <cit.>. For a thorough study of  interpolation in modal logics we refer the reader to <cit.>. A model-theoretic proof of interpolation for E is given in <cit.>, and a coalgebraic proof  of (uniform) interpolation for all the logics considered here, as well as all other rank-1 modal logics (see below), is given in <cit.>. As it is explained in Example <ref>, we have not been able to prove interpolation for calculi containing the non-standard rule LR-C (see Table <ref>) and, as far as we know, it is still an open problem whether it is possible to give a constructive proof of interpolation for these logics.
 
 

  
Related Work.
 The modal rules of inference  presented in Table <ref> are obtained from the rules presented in <cit.> by adding weakening contexts to the conclusion of the rules. This minor modification, used also in <cit.> for several modal rules, allows us to shift from set-based sequents to multiset-based ones  and to prove not only that cut is admissible, as it is done in <cit.>, but also that weakening and contraction are height-preserving admissible. Given that implicit contraction is not eliminable from set-based sequents, the decision procedure for non-normal logics given in <cit.> is based on  a model-theoretic inversion technique so that it is possible to define a  procedure that  outputs a derivation for all valid sequents and a finite   countermodel  for all invalid ones. One weakness of this decision  procedure is that  it does not respect the subformula property for logics without rule RM (the procedure  adds instances of the excluded middle).
 

 
The paper <cit.> considers multiset-based calculi for the non-normal logic  M(N) and for its extensions with axioms D^,T, 4, 5, and B. Nevertheless,  neither weakening nor contraction is eliminable  because there are no weakening contexts in the conclusion of the modal rules. In <cit.> multiset-based sequent calculi for the non-normal  logic E(N) and  for its extensions with  axioms D^,T, 4, 5, and B are given. The rules LR-E and R-N are  as in Table <ref>, but the deontic axiom  D^ is expressed  by the following  rule:


    [ D-2]Ø A,Ø B,A,B   ( A,B)

where the right premiss  is present when we are working over LR-E and  it has to be omitted when we work over LR-M. In the calculi in <cit.> weakening and contraction are taken as primitive rules and not as admissible ones as in the present approach. Even if it is easy to show that weakening is eliminable from the calculi in <cit.>, contraction cannot be eliminated because rule D-2 has exactly two principal formulas and, therefore, it is not possible to permute contraction up with respect to instances of  rule D-2 (see Theorem <ref>). 
The presence of a non-eliminable rule of contraction makes the elimination of cut more problematic: in most cases we cannot  eliminate the cut directly, but we have to consider the rule known as multicut <cit.>.  Moreover, cut is not eliminable from the calculus given in <cit.> for the deontic  logic END. The formula  D^:= Ø is a theorem of this logic, but it can be derived only with a non-eliminable instance of  cut  as in:


    [ R]Ø[ Cut]Ø[ RN]Ø⊤⊤   [ D2]Ø⊤,Ø,⊤   ,⊤
 

Finally, it is worth noticing that all the non-normal logics we consider here are  rank-1 logics in the sense of <cit.> – i.e., logics whose modal axioms are propositional combinations of formulas of shape ϕ, where  ϕ is purely propositional – and the calculi we give for the  modal logics E, M, K and KD are explicitly considered in <cit.>.  Thus, they are part of the family of modal coalgebraic logics  <cit.> and most of the results in this paper can be seen as  instances of general results that hold for rank-1 (coalgebraic) logics. If, in particular, we consider cut-elimination for coalgebraic logics <cit.> then all our calculi  absorb congruence  and Theorem <ref> and case 3 of Theorem <ref> show that they absorb  contraction and cut. Hence, <cit.> entails  that cut and contraction are   admissible in these calculi; moreover, <cit.> entail that they are one-step cut free complete w.r.t. coalgebraic semantics. This latter result gives a semantic proof of cut admissibility  in the calculi considered here. Analogously, if we consider decidability, the polynomial space upper bound we find in Section <ref> coincides with that found in <cit.> for rank-1 modal logics. 




  
Synopsis. 
Section <ref> summarizes the basic notions of axiomatic systems and of neighbourhood semantics for  non-normal  logics.  Section <ref> presents G3-style  sequent calculi for these logics and then shows that weakening and contraction are height-preserving admissible and that cut is (syntactically) admissible.  Section <ref> describes a  terminating proof-search decision procedure for all calculi, it shows that each calculus is equivalent to the  corresponding axiomatic system, and  it applies proof search to Forrester's paradox.  Finally, Section <ref> gives a Maehara-style    constructive proof of Craig's interpolation theorem for the logics having a standard calculus.


§ NON-NORMAL LOGICS




 §.§ Axiomatic Systems

We introduce, following <cit.>,  the basic notions  of non-normal  logics. Given a countable set of propositional variables {p_n | n∈ℕ}, the formulas of the modal language Ł  are generated by:


    A::=  p_n |  | A∧ A | A A | A→ A | Ø A

We remark that  is a 0-ary logical symbol. This will be extremely important in the proof of Craig's interpolation theorem. As usual A is a shorthand for A→, ⊤ for →, A ↔ B  for (A→ B)∧(B→ A), and A for Ø A. We follow the usual conventions for parentheses. 







Let L  be the logic containing  all Ł-instances of propositional tautologies as axioms, and   modus ponens (MP) as inference rule.  The minimal non-normal modal logic E is the logic L plus the rule RE of Table <ref>. We will consider all the logics that are obtained by extending E with some set of axioms from Table <ref>. We will denote the logics according to the axioms that define them, e.g. EC is the logic  E⊕ C, and EMD^ is E⊕  M⊕ D^.  By X we denote any of these logics and we  write  whenever A is a theorem of X. We will call modal the logics containing neither D^ nor D^, and deontic those containing at least one of them. We have followed the usual naming conventions for the modal axioms, but we have introduced new  conventions for the deontic ones: D^ is usually called either  CON or P and D^ is usually called D, cf. <cit.>.
 
 It is also possible to give an equivalent  rule-based axiomatization of some of these logics. In particular, the logic EM, also called M, can be axiomatixed as L plus the rule RM of Table <ref>.  The logic  EMC, also called R, can be axiomatized as L plus the rule  RR of Table <ref>. Finally,  the logic EMCN, i.e. the smallest normal modal logic K,  can be axiomatized as L plus the rule RK of Table <ref>. These rule-based axiomatizations will be useful later on since they simplify the proof of the equivalence between  axiomatic systems and  sequent calculi (Theorem <ref>).







The following proposition states the well-known relations between the theorems of non-normal modal  logics. For a proof  the reader is referred to <cit.>.


 For any formula A∈Ł we have that E ⊢ A implies M  ⊢ A; M ⊢ A   implies R ⊢ A; R ⊢ A  implies K ⊢ A. Analogously for the logics containing axiom N and/or axiom C.


Axiom D^ is K-equivalent to D^, but the correctness of D^ has been a big issue in the literature on deontic logic. This fact urges the study of  logics weaker than KD, where D^ and D^ are no more equivalent <cit.>. 
The deontic  formulas D^ and D^ have the following relations in the logics we are considering.
 D^ and D^ are  independent  in E; D^ is derivable from D^ in  non-normal logics containing at least one of the axioms  M  and N; D^ is derivable from D^ in non-normal logics containing  axiom C.

In Figure  <ref> the reader finds the lattice of non-normal modal logics, see <cit.>, and in Figure <ref>  the lattice of non-normal deontic logics. 

 


 





 §.§ Semantics


The most widely known semantics for non-normal logics is neighbourhood semantics. We sketch its main tenets following <cit.>, where neighbourhood models are called minimal models. 

A neighbourhood model is a triple :=⟨ W,  N, P⟩, where W is a non-empty set of possible worlds; N:W⟶ 2^2^W is a neighbourhood function that associates to each possible world w a set N(w) of subsets   of W; and P gives a truth value to each propositional variable at each world. 

The definition of truth of a formula A at a world w of a neighbourhood model ℳ – _w^ℳA – is the standard one for the classical connectives with the addition of


    _w^ℳØ A    iff     || A||^ℳ∈ N(w)

where ||A||^ℳ is the truth set of A – i.e., ||A||^ℳ={w | _w^ A}. We say that a formula A  is valid in a class 𝒞 of neighbourhood models iff it is true in every world of every ℳ∈𝒞.

In order to give  soundness and completeness results for non-normal modal and deontic  logics with respect to (classes of) neighbourhood models, we introduce the following definition.
 Let ℳ=⟨ W,  N, P⟩ be a neighbourhood model, X,Y ∈ 2^W, and w∈ W, we say that: 


  *  is supplemented    if X∩ Y∈ N(w) imples X∈ N(w) and Y∈ N(w);

  *  is closed under finite intersection  if X∈ N(w) and Y∈ N(w) imply X∩ Y∈ N(w);

  *  contains the unit if   W∈ N(w);

  *  is non-blind  if X∈ N(w) implies X≠∅; 

  *  is complement-free if X∈ N(w) implies W-X∉N(w).            




 We have the following correspondence results between Ł-formulas and the properties of the neighbourhood function defined above:


  * Axiom M corresponds to supplementation;

  * Axiom C corresponds to closure under finite intersection;

  * Axiom N corresponds to containment of the unit;

  * Axiom D^ corresponds to non-blindness;

  * Axiom D^ corresponds to complement-freeness.



 E is sound and complete with respect to the class of all neighbourhood models. Any logic X which is obtained by extending E with some axioms from Table <ref> is sound and complete with respect to the class of all neighbourhood models which satisfies all the properties corresponding to the axioms of X.


See <cit.> for the proof of Proposition <ref> and of Theorem <ref>.



§ SEQUENT CALCULI



 We introduce  sequent calculi for non-normal logics that extend the multiset-based  sequent calculus  G3cp <cit.> for classical propositional logic  – see Table <ref> – by adding some modal and deontic rules from Table <ref>.   In particular, we  consider the modal sequent calculi given in Table <ref>, which will be shown to capture the modal logics of Figure <ref>, and their deontic extensions given in Table <ref>, which will be shown to capture all deontic logics of Figure <ref>.
We adopt the following notational conventions: we use G3X to denote a generic calculus from either Table <ref> or Table <ref>, and we use G3Y(Z)  to denote both G3Y and GRYZ.  All the rules in Tables <ref> and  <ref> but  LR-C and L-D^_C are standard rules in the sense of <cit.>: each of them is a  single rule with a fixed number of premisses; LR-C and L-D^_C, instead, stand for a recursively enumerable set of rules with a variable number of premisses.   

 For an introduction to G3cp and  the relevant notions, the reader is referred to <cit.>.
   We sketch here the main notions that will be used in this paper.   A sequent is an expression  $̣, whereand$̣ are finite, possibly empty, multisets of formulas. If Π is the (possibly empty) multiset A_1,…,A_m then ØΠ is  the (possibly empty) multiset Ø A_1,…,Ø A_m. A derivation of a sequent $̣ in  G3X is an upward growing  tree of sequents having$̣ as root, initial sequents or instances of rule L as leaves, and such that each non-initial node is the conclusion of an instance of one  rule of G3X whose premisses are its children. In the rules in Tables <ref> and <ref>, the multisets  and $̣ are called contexts, the other formulas occurring in the conclusion (premiss(es), resp.) are called principal (active). In a sequent the antecedent (succedent) is the multiset occurring to the left (right) of the sequent arrow.  As for  G3cp, a sequent$̣ has the following  denotational interpretation: the conjunction of the formulas in  implies the disjunction of the formulas in $̣.
 
As measures for inductive proofs we  use the weight of a formula and the height of a derivation. The weight of a formulaA,w(A), is defined inductively as follows:w()=w(p_i)=0;w(ØA)=w(A)+1;w(A∘B)=w(A)+w(B)+1(where∘is one of the binary connectives∧, , →). The weight of a sequent is the sum of the weight of the formulas occurring in that sequent.  The height of a derivation is the length of its longest branch minus one. A rule of inference is said to be (height-preserving) admissible in  G3X if, whenever its premisses are derivable in  G3X, then also its conclusion is derivable (with at most the same derivation height) in  G3X. The modal depth of a formula (sequent) is the maximal number of nested modal operators occurring in it(s members).
  


 §.§ Structural rules of inference

We are now going to prove that the calculi  G3X have the same good structural properties of  G3cp: weakening and contraction are height-preserving admissible  and  cut is admissible. All proofs are extension of those for  G3cp, see  <cit.>; in most cases, the modal rules have to be treated differently from the propositional ones  because of the presence of empty contexts in the premiss(es) of the modal ones. We adopt the following notational convention: given a derivation tree_k, the derivation tree of then-th leftmost premiss of its last step is  denoted by_kn. We begin by showing that the restriction to atomic initial sequents, which is needed to have the propositional rules invertible, is not limitative in that initial  sequents with arbitrary principal  formula are derivable in  G3X.

 Every instance of A,,̣ A is derivable in  G3X. By induction on the weight of A. If w(A)=0– i.e., A is atomic or – then we have an instance of an initial sequent or of a conclusion of L and there is nothing to prove. If w(A)≥1,  we  argue by cases according to the construction of A. In each case we apply, root-first, the appropriate rule(s) in order to obtain sequents where some proper subformula of A occurs both in the antecedent and in the succedent. The claim then holds by the inductive hypothesis (IH). To illustrate, if A≡Ø B and we are in  G3M(ND), we have:

[ LRM]Ø B,,Ø B[ IH]B B The left and right rules of weakening are height-preserving admissible in  G3X[ LW]A,    [ RW],AThe proof is a straightforward induction on the height of the derivation  of $̣. 
 If the last step ofis by a propositional rule, we have to apply the same rule to the weakened premiss(es), which are derivable by IH, see <cit.>. If it is by a modal or deontic rule, we proceed by addingAto the appropriate weakening context of the conclusion of that rule  instance. To illustrate, if the last rule isLR-E, we transform[ LRE]Ø B,,Ø CB C⋮ _1   C B⋮ _2        [ LRE]Ø B,A,,Ø CB C⋮ _1   C B⋮ _2Before considering contraction, we recall some facts that will be useful later on. 
 In  G3X the rules[ L] A,,A





and[ R], AA,





are admissible.

We have the following derivations (the step by RW is admissible thanks to Theorem <ref>):

[ L→]A→,,A   [ L],        [ R→],A→[ RW]A,,A,All propositional rules are height-preserving invertible in  G3X, that is the derivability of (a possible instance of) a conclusion of a propositional rule entails the derivability, with at most the same derivation height, of its premiss(es). We have only to extend the proof  for  G3cp, see  <cit.>, with new cases for the modal and deontic rules. If A∘ B occurs in the antecedent (succedent) of the conclusion of an instance of a  modal or deontic rule then it must be a member of the weakening context  ($̣)  of this rule instance, and we have only to change the weakening context according to the rule we are inverting.The left and right rules of contraction are height-preserving admissible in  G3X
[ LC]A,A,A,    [ RC],A,A,A













  The proof is by simultaneous  induction on the height  of the derivation   of the  premiss for left and right  contraction. The base case is straightforward. For the inductive steps, we have different strategies according to whether the last step in  is by a propositional  rule or not. If the last step in  is  by a propositional rule, we have two subcases: if the contraction formula is not principal in that step, we apply the inductive hypothesis and then the rule. Else  we start by using the height-preserving invertibility –  Lemma <ref>– of that rule, and then we apply the inductive hypothesis and the rule, see <cit.> for details. 
 
 If the last step in  is by a modal or deontic rule, we have two subcases: either (the last step is by one  of LR-C, LR-R, LR-K, L-D^_E, L-D^_M, L-D^_C and L-D^* and) both occurrences of the contraction formula A of LC are principal in the last step or  some  instance of the contraction formula  is    introduced in the appropriate  weakening context of the conclusion. In the first subcase, we apply the inductive hypothesis to the premiss and then the rule. An interesting example is when the last step in  is by L-D^_E. We transform
 
[ LC]Ø B,[ LD^]Ø B,Ø B,B,B  ⋮ _1    B,B⋮ _2     into     [ LD^]Ø B,B    ⋮ IH(_1)    B    ⋮ IH(_2) where IH(_1) is obtained  by applying the inductive hypothesis for the left rule of contraction to _1 and IH(_2) is obtained by applying the inductive hypothesis for the right rule of contraction to _2. 

In the second subcase,  we apply an instance of the same   modal or deontic rule which introduces one less occurrence of A in the appropriate context of the conclusion. Let's consider RC.  If the last step is by LR-M and no  instance of A is principal in the last rule, we transform
[  RC]Ø B,''̣,A,Ø C[ LRM]Ø B,''̣,A,A,Ø CB C⋮ _1        [ LRM]Ø B,''̣,A,Ø CB C  ⋮ _1






















 The rule of cut is admissible in  G3X[ Cut],Π,̣Σ,D⋮ _1   D,ΠΣ⋮ _2















 We consider an uppermost application of Cut and we show that either it is eliminable, or it can be permuted upward in the derivation until we reach sequents where it is eliminable. The proofs, one for each calculus, are by induction on the weight of the cut formula D with a sub-induction on the sum of the heights of the derivations of the two premisses (cut-height for shortness). The proof can be organized in 3 exhaustive cases:
 
 
  *  At least one of the premisses of cut  is an initial sequent or a conclusion of L;

  *  The cut formula in not principal in the last step of at least one of the two premisses;
 
  *  The cut formula is principal in both premisses.
 
• Case (1). Same as for  G3cp, see <cit.> for the details.
 
 • Case (2). We have many subcases according to the last rule applied in the derivation  (^⋆)  of the  premiss where the cut formula is not principal. For the propositional rules, we refer the reader to <cit.>, where it is given a procedure that allows to reduce the cut-height. If the last rule applied in ^⋆ is a modal or deontic one, we  can transform the derivation into a cut-free one because the conclusion of  is derivable  by replacing the last step of  ^⋆ with  the appropriate instance of the same modal or deontic rule. We present explicitly only the cases where the last step of the left premiss is by LR-E and L-D^ and the cut formula is not principal in it, all other transformations being similar.
 𝐋𝐑-𝐄:  If the left premiss  is by rule LR-E  (and ≡ A,' and ≡̣'̣, B), we  transform [ Cut]Ø A,',Π'̣,Ø B,Σ[ LRE]Ø A,''̣,Ø B,DA B⋮ _11   B A⋮ _12   D,ΠΣ⋮ _2        [ LRE ]Ø A,',Π'̣,Ø B,ΣA B⋮ _11   B A⋮ _12

































𝐋-𝐃^:  If the left premiss  is by rule L-D^, we  transform [ Cut]Ø A,',Π,̣Σ[ LD^]Ø A,',̣DA⋮ _11   D,ΠΣ⋮ _2        [ LD^ ]Ø A,',Π,̣ΣA⋮ _11




























 


• Case (3). If the cut formula D  is principal in both premisses, we have cases according to the principal operator of D. In each case we have a procedure that allows to reduce the weight of the cut formula, possibly increasing the cut-height. For the propositional cases, which are the same for all the logics considered here, see <cit.>.

 If D≡Ø C, we consider the different logics one by one, without repeating the common cases. 
• G3E(ND). Both premisses are by rule LR-E, we have

[ Cut]Ø A,',Π,̣Σ',Ø B[ LRE]Ø A,',̣Ø CA C⋮ _11   C A⋮ _12   [ LRE]Ø C,ΠΣ',Ø BC B⋮ _21   B C⋮ _22


























 and we transform it into the following derivation that has two  cuts with cut formulas of lesser weight, which are admissible by IH.

[ LRE]Ø A,',Π,̣Σ',Ø B[ Cut] A BA C⋮ _11   C B⋮ _21   [ Cut]B AB C⋮ _22   C A⋮ _12




































































• G3EN(D). Left premiss by R-N and right one by LR-E. We transform[ Cut],Π,̣Σ',Ø A[ RN],Ø C C⋮ _11   [ LRE]Ø C,ΠΣ',Ø AC A⋮ _21   A C⋮ _22        [ RN ],Π,̣Σ',Ø A[ Cut] A C⋮ _11   C A⋮ _21• G3E(N)D^.
Left premiss is by LR-E, and  right one by L-D^. We transform 
[ Cut]Ø A,',Π,̣Σ[ LRE]Ø A,',̣Ø CA C⋮ _11   C A⋮ _12   [ LD^]Ø C,ΠΣC⋮ _21        [ LD^ ]Ø A,',Π,̣Σ[ Cut]AA C⋮ _11   C⋮ _21• G3E(N)D^.
Left premiss is by LR-E, and  right one by L-D^_E. We transform (|Ξ|≤ 1)[ Cut]Ø A,',ØΞ,Π',̣Σ[ LRE]Ø A,',̣Ø CA C⋮ _11   C A⋮ _12   [ LD^_E]Ø C,ØΞ,Π'ΣC,Ξ⋮ _21    C,Ξ⋮ _22


























into
[ LD^_E]Ø A,',ØΞ,Π',̣Σ[ Cut]Ξ,AΞ, C⋮ _22   C A⋮ _12   [ Cut]A,ΞA C⋮ _11   C,Ξ⋮ _21• G3E(N)D. Left premiss by LR-E and right one by   L-D^ or L-D^_E. Same as  above.



































































































• G3END^. Left premiss by R-N and right one by L-D^. We transform [ Cut],Π,̣Σ[ RN],Ø C C⋮ _11   [ LD^]Ø C,ΠΣC⋮ _21        =[ LWsRWs ],Π,̣Σ[ Cut]C^ C⋮ _11   C⋮ _21• G3END. Left premiss by R-N and right one by L-D^_E. We transform (|Ξ|≤ 1)

[ Cut]ØΞ,,Π',̣Σ[ RN],̣Ø C C⋮ _11   [ LD^]Ø C,ØΞ,Π'ΣC,Ξ⋮ _21   C,Ξ⋮ _22    into    [ (⋆)]ØΞ,,Π',̣Σ[ Cut]Ξ C⋮ _11   C,Ξ⋮ _21
where (⋆) is an instance of L-D^ if |Ξ|=1, else (|Ξ|=0 and) it is some instances






























• G3M(ND).
 Both premisses are by rule LR-M, we transform
 [ Cut]Ø A,',Π,̣Σ',Ø B[ LRM]Ø A,',̣Ø CA C⋮ _11   [ LRM]Ø C,ΠΣ',Ø BC B⋮ _21        [ LRM]Ø A,',Π,̣Σ',Ø B[ Cut]A B A C⋮ _11   C B⋮ _21

























































• G3MN(D). Left premiss by R-N and right one by LR-M. Similar to the case with left premiss by R-N and right one by LR-E.
• G3M(N)D^ and  G3M(N)D.
Left premiss is by LR-M, and  right one by  L-D^ or L-D^_M. Similar to the  case with left premiss by LR-E and right by L-D^ or L-D^_E, respectively.
































• G3MND^ and  G3MND. The cases with left premiss by R-N and right one by  a deontic rule are like the analogous ones we have already considered.


• G3C(ND). Both premisses are by rule LR-C. Let us agree to use Λ to denote the non-empty  multiset A_1,…,A_n, and Ξ for the (possibly empty) multiset B_2,… B_m.  The derivation

[ Cut]ØΛ,',ØΞ,Π',̣Σ', Ø E[ LRC]ØΛ,',̣Ø CΛ C⋮ _11   C A_1⋮ _A_1   ^…   C A_n⋮ _A_n   [ LRC]Ø C,ØΞ,Π'Σ',Ø EC,Ξ E⋮ _21    E C⋮ _C   ^…   E B_m⋮ _B_m is transformed into the following derivation having  n+1 cuts on formulas of lesser weight
0.8000[ LRC]ØΛ,',ØΞ,Π',̣Σ', Ø E[ Cut]Λ,Ξ EΛ C⋮ _11   C,Ξ E⋮ _21   [Cut …]E A_1E C⋮ _C   C A_1⋮ _A_n   
[ Cut]E A_nE C⋮ _C   C A_n⋮ _A_n   E B_1⋮ _B_1   ^…   E B_m⋮ _B_m
• G3CN(D). Left premiss by R-N and right premiss by LR-C. We have

[ Cut],Ø A_1,…,Ø A_n,Π',̣Σ', Ø B[ RN],Ø C C⋮ _11   [ LRC]Ø C,Ø A_1,…,Ø A_n,Π'Σ',Ø BC,A_1,…,A_n B⋮ _21    B C⋮ _C   ^…   B A_n⋮ _A_n






























 where A_1,…,A_n (and thus also Ø A_1,…,Ø A_n)  may or may not be the empty multiset. If A_1,…,A_n is not empty, we transform it  into the following derivation having one cut with cut formula of lesser weigh
 
[ LRC],Ø A_1,…Ø A_n,Π',̣Σ', Ø B[ Cut]A_1,…,A_n B C  ⋮ _11   C,A_1,…, A_n B⋮ _21   B A_1⋮ _A_1   ^…   B A_n⋮ _A_n
If, instead, A_1,…,A_n is empty, we transform it into

[ RN],Π',̣Σ',Ø B[ Cut] B C    ⋮ _11   C B⋮ _21
• G3CD^. Left premiss by LR-C and right premiss by L-D^_C. We transform  (we assume Ξ= A_1,… A_k, Θ= C, B_2,…, B_m and Λ= D_1,…, D_n) 

[ Cut ]ØΞ,Ø B_1,…, Ø B_m,ØΛ,',Π',̣Σ[LRC]ØΞ,',̣Ø CΞ C⋮ _11   { C A_i |  A_i∈Ξ}⋮ _1A_i   [ LD^_C]Ø C,Ø B_2,…,Ø B_m,ØΛ,Π'ΣΘ,Λ⋮ _21   { E,D_j |  E∈Θ and  D_j∈ Λ}⋮ _Θ_iΛ_j
into the following derivation having 1+(k× n) cuts on formulas of lesser weight

0.830[ LD^_C]ØΞ,Ø B_1,…, Ø B_m,ØΛ,',Π',̣Σ[ Cut]Ξ,B_2,…, B_m,ΛΞ C⋮ _11   C,B_2,…,B_m,Λ⋮ _21   [ Cut]{ A_i,D_j| A_i∈Ξ,  D_j∈Λ} D_j,C⋮ _Θ_1,Λ_j   C A_i⋮ _1A_i   { B_i,D_j| B_i∈Θ-C,  D_j∈Λ}⋮ _Θ_iΛ_j























































































































• G3C(N)D. Left premiss by LR-C and right one by L-D^*. It is straightforward to transform the derivation into another one having one cut with cut formula of lesser weight. • G3R(D). Both premisses are by rule LR-R, we transform

0.88000[ Cut]Ø A,ØΞ,',ØΨ,Π',̣Σ',Ø B[ LRR]Ø A,ØΞ,',̣Ø CA,Ξ C⋮ _11   [ LRR]Ø C,ØΨ,Π'Σ',Ø BC,Ψ B⋮ _21    [ LRR]Ø A,ØΞ,',ØΨ,Π',̣Σ',Ø B[ Cut]A,Ξ,Ψ B A,Ξ C⋮ _11   C,Ψ B⋮ _21




























• G3RD^⋆.Left premiss is by LR-R, and  right one by L-D^⋆, we transform [ Cut]Ø A,ØΞ,',ØΨ,Π',̣Σ[ LRR]Ø A,ØΞ,',̣Ø CA,Ξ C⋮ _11   [ LD^*]Ø C,ØΨ,Π'ΣC,Ψ⋮ _21    [ LD^*]Ø A,ØΞ,',ØΨ,Π',̣Σ[ Cut]A,Ξ,ΨA,Ξ C⋮ _11   C,Ψ⋮ _21


























• G3K(D).
The new cases with respect to  G3R(D) are those with left premiss by an instance of LR-K that has no principal formula in the antecedent. These cases can be treated like cases with left premiss by R-N.


















§ DECIDABILITY AND SYNTACTIC COMPLETENESS


 §.§ Decision procedure for  G3X

Each calculus  G3X has the strong subformula property since all  active formulas of  each rule  in Tables <ref> and <ref> are  proper subformulas of the the principal formulas and no formula  disappears in moving from premiss(es) to conclusion. As usual, this gives us a syntactic proof of consistency.

  *  Each  premiss of each rule of  G3X has smaller weight than its conclusion;

  *  Each premiss of each modal or deontic rule of  G3X has smaller modal depth than its conclusion;

  *  The calculus  G3X has the subformula property:  a  G3X-derivation of a sequent 𝒮 contains only sequents composed of subformulas of 𝒮;

  *  The empty sequent is not  G3X-derivable.
 
We also have an effective method to decide the derivability of a sequent in  G3X: we start from the desired sequent$̣ and we construct all possible  G3X-derivation trees until either we find a tree where each leaf is an initial sequent or a conclusion of L– we have found a  G3X-derivation of $̣– or we have checked all possible  G3X-derivations   and we have found none –$̣ is not  G3X-derivable.  

More in details, we present  a depth-first procedure that tests  G3X-derivability in polynomial space. As it is usual in decision procedures involving non-invertible rules, we have trees involving two kinds of branching. Application of a rule with more than one premiss produce an AND-branching point, where all branches have to be derivable to obtain a derivation. Application of a non-invertible rule to a sequent that can be the conclusion of different instances of non-invertible rules produces an OR-branching point, where only one branch need be derivable to obtain a derivation.
In the procedure below we will assume that, given a calculus  G3X and given a sequent ØΠ,^p^̣p,ØΣ (where ^p and ^̣p are multisets of propositional variables), there is some fixed way of ordering the finite (see below) set of instances of modal and deontic rules of  G3X ( X-instances, for shortness) having that sequent as conclusion. Moreover, we will represent the root of branches above an OR-branching point  by nodes of shape _i, where _i is the name of the i-th  X-instance applied (in the order of  all  X-instances having that conclusion).  To illustrate, if we are in  G3EN and we have to consider  Ø A,Ø B,^p^̣p,Ø C then we obtain (fixing one way of ordering the three  X-instances having that sequent as conclusion):
 
Ø A,Ø B,^p^̣p,Ø C[    ]LREA C    C A   [    ]LREB C   C B   RN B
where the lowermost sequent is an  OR-branching point  and the two nodes   LR-E_1 and LR-E_2 are AND-branching points. Finally, Given an AND(OR)-branching point 

𝒮𝒮_1   …   𝒮_n we say that the branch above 𝒮_i is an  unexplored AND(OR)-branch if no one  of its nodes has already been active. 
























  Stage 1. We write the one node tree $̣
and we label$̣ as active.

  Stage n+1. Let 𝒯_n be the tree constructed at stage n, let 𝒮≡ΠΣ be its active sequent, and let ℬ be the branch  going from   the root  of 𝒯_n to 𝒮. 

  Closed. If 𝒮 is such that p∈Π∩Σ (for some propositional variable p) or ∈Π, then we label 𝒮 as closed and

  Derivable. If ℬ contains no  unexplored AND-branch, the procedure ends and