# Universal Proof Theory: Feasible Admissibility in Intuitionistic Modal
Logics

Amirhossein Akbar Tabatabai111Support by the FWF project P 33548 is gratefully
acknowledged.
University of Groningen  Raheleh Jalali222Support by the Netherlands
Organisation for Scientific Research under grant 639.073.807 is gratefully
acknowledged.
Utrecht University

###### Abstract

In this paper, we introduce a general family of sequent-style calculi over the
modal language and its fragments to capture the essence of all constructively
acceptable systems. Calling these calculi _constructive_ , we show that any
strong enough constructive sequent calculus, satisfying a mild technical
condition, feasibly admits all Visser’s rules, i.e., there is a polynomial
time algorithm that reads a proof of the premise of a Visser’s rule and
provides a proof for its conclusion. As a positive application, we show the
feasible admissibility of Visser’s rules in several sequent calculi for
intuitionistic modal logics, including $\mathsf{CK}$, $\mathsf{IK}$ and their
extensions by the modal axioms $T$, $B$, $4$, $5$, the modal axioms of bounded
width and depth and the propositional lax logic. On the negative side, we show
that if a strong enough intuitionistic modal logic (satisfying a mild
technical condition) does not admit at least one of Visser’s rules, then it
cannot have a constructive sequent calculus. Consequently, no intermediate
logic other than $\mathsf{IPC}$ has a constructive sequent calculus.

_Keywords:_ admissible rules, feasible disjunction property, intuitionistic
modal logics

###### Contents

  1. 1 Introduction
  2. 2 Preliminaries
    1. 2.1 Intuitionistic Modal Logics
    2. 2.2 Sequent Calculi
  3. 3 Constructive Formulas and Rules
    1. 3.1 Constructive Formulas
    2. 3.2 Constructive Rules
    3. 3.3 General Rules and the Justification
  4. 4 Feasible Visser-Harrop Property
    1. 4.1 The Translations and their Properties
    2. 4.2 The Provability Preservation
    3. 4.3 The Unit Propagation
    4. 4.4 $T$-freeness and $T$-fullness
    5. 4.5 The Main Theorem
  5. 5 Fragments
    1. 5.1 $\Diamond$-free Fragment
    2. 5.2 $\Box$-free Fragment
    3. 5.3 Propositional Fragment
  6. 6 Conclusion and Future Work

##  1 Introduction

Universal proof theory [1, 2] is a recent research project whose aim is to
investigate the _generic_ behavior of proof systems, considered as independent
mathematical objects standing on their own feet. It opposes the usual attitude
in proof theory that sees a proof system as an auxiliary object by which we
investigate the logical system it captures. Similar to any other field in
mathematics (e.g. group theory), the goal in universal proof theory is to
provide a _classification_ of proof systems of a given form up to a given
equivalence. For that purpose, one must first address the following two
problems: first, the _existence problem_ that investigates the existence of
the proof systems of a given form and second, the _equivalence problem_ ,
focusing on the natural equivalence relations between the systems. So far, the
main focus of the project has been on its first and most accessible problem,
i.e., the existence problem. To attack this problem, as it is usual in
mathematics, one must invoke the _method of invariants_. Roughly speaking, the
main idea is to show that the special form of a proof system for a logic $L$
implies a pure logical property for $L$, depending only on $L$ and not its
proof systems. Therefore, the lack of the property can be used as a method to
show the non-existence of the proof system. As the first instance of
implementing this method, Iemhoff [23, 24] and then the authors [1, 2] studied
the relationship between a certain general form for the rules in a sequent
calculus and different flavours of the interpolation property for the
corresponding logic. In this paper, we continue this type of study by
employing the _admissibility of Visser’s rules_ as the logical property. To
explain how, let us first provide a historical context for the admissible
rules in general, Visser’s rules in particular, and the corresponding
complexity-theoretic issues.

A rule is called _admissible_ in a logic $L$ if the set of theorems of $L$ is
closed under that rule. Admissible rules have been studied from various
perspectives including decidability, decision and proof complexity, and their
explicit bases. As an early instance of such an interest, the decidability
problem for the admissible rules of the intuitionistic propositional logic,
$\mathsf{IPC}$, was posed by Friedman in [15] and answered positively in a
series of works by Rybakov gathered in [35]. He showed that admissibility is
decidable in many intermediate logics and various modal logics extending
$\mathsf{K4}$. Later, Ghilardi [16, 17] provided a characterization for the
admissible rules in some modal and intermediate logics using projective
formulas. Building on his results, Iemhoff [20] gave an explicit basis for
$\mathsf{IPC}$ and some other intermediate logics [21, 22]. The basis consists
of what is called Visser’s rules. Later, Jeřábek employed the techniques used
for $\mathsf{IPC}$ to provide a basis for a series of normal modal logics
extending $\mathsf{K4}$ [25], and investigated the admissible rules of
Lukasiewicz logic [28, 30]. Recently, van der Giessen studied the admissible
rules of some intuitionistic modal logics and provided a basis for them [14].

Admissible rules are also interesting from a complexity-theoretic lens. Two
instances of such interests are the decision and the proof complexity of the
admissible rules. As for the decision complexity, Jeřáebk [27] showed that
even in basic transitive modal logics such as $\mathsf{K4,S4,GL}$, and
$\mathsf{Grz}$, the decision procedure is coNEXP-complete and for Lukasiewicz
logic, it is PSPACE-complete [29]. As for the proof complexity of admissible
rules, some investigations have been done on the special case of the
disjunction property. Buss and Mints [6] and later Buss and Pudlák [7] showed
that the natural deduction system and the sequent calculus for $\mathsf{IPC}$,
_feasibly_ (i.e., in polynomial time) admit the disjunction property,
respectively. More precisely, they showed that given the proof systems for
$\mathsf{IPC}$, there exists a polynomial time algorithm that reads a proof of
the formula $A\vee B$ and outputs a proof of either $A$ or $B$. In both
papers, a form of normalization or cut elimination is required. Later, Ferrari
et al. [10, 11] provided a uniform framework to study the proof complexity of
the disjunction property in intuitionistic logic and some modal and
intuitionistic modal logics. The method they used is based on a calculus
called the extraction calculus. The benefit of their method, compared to the
previous ones, is that they do not take the structural properties of the
system in use into account and hence there is no need for normalization/cut
elimination. Moreover, there is a weaker version of the disjunction property
suitable for the classical modal logics. For this property, the feasibility
has been shown by Bílková [5] and for Frege systems for any extensible modal
logic, by Jeřábek [26]. For more on the disjunction property of intermediate
logics, see [8].

#### Our contribution

In this paper, we first identify a class of rules called the _constructive_
rules to provide a general enough family of constructively acceptable rules
for intuitionistic modal logics over the language
$\mathcal{L}=\\{\wedge,\vee,\to,\top,\bot,\Box,\Diamond\\}$ and its fragments.
To find such a family, we will use the well-known heuristic that the
constructive rules, whatever they are, must be careful in introducing any
disjunction-like connectives. Restricting all the direct and indirect ways to
produce such a connective, we will provide a tight and robust family of rules
to use. Then, as mentioned before, we set the admissibility of Visser’s rules
as the logical invariant property. In fact, we use a stronger property called
the _feasible Visser-Harrop property_. A calculus $G$ is called to have the
feasible Visser-Harrop property, if there is a polynomial time algorithm $f$
such that for any proof $\pi$ of $\Gamma,\\{A_{i}\to B_{i}\\}_{i\in
I}\Rightarrow C\vee D$ in $G$, $f(\pi)$ is a $G$-proof of either
$\Gamma,\\{A_{i}\to B_{i}\\}_{i\in I}\Rightarrow C$, or $\Gamma,\\{A_{i}\to
B_{i}\\}_{i\in I}\Rightarrow D$, or $\Gamma,\\{A_{i}\to B_{i}\\}_{i\in
I}\Rightarrow A_{i}$ for some $i\in I$, where $\Gamma$ consists of a modal
version of the Harrop formulas. Note that the feasible Visser-Harrop property
is a property of the calculus and not the logic. In this sense it deviates
from the basic setting of the invariant technique we discussed. However,
forgetting the feasibility condition, it is easy to rephrase the property as a
property of the logic which is a modest generalization of the admissibility of
Visser’s rules.

Having the two ingredients of form and property settled, we show that over
$\mathcal{L}$ and its fragments, any strong enough sequent calculus,
consisting only of constructive rules and some basic modal rules, and
satisfying a mild technical condition has the feasible Visser-Harrop property
and hence, its logic admits Visser’s rules. As an application, on the positive
side, we show that the sequent calculi for several intuitionistic modal logics
have the feasible Visser-Harrop property and consequently enjoy the feasible
disjunction property. It includes the usual sequent calculi for the
constructive modal logic $\mathsf{CK}$, intuitionistic modal logic
$\mathsf{IK}$, their extensions by the modal axioms $T$, $B$, $4$, $5$ or more
generally the modal axioms of bounded width and depth
$ga_{klmn}:\Diamond^{k}\Box^{l}p\to\Box^{m}\Diamond^{n}p$, unless $k=m=0$, and
many others. We also prove the same result for the fragments of the language,
where the system for the propositional lax logic, $\mathsf{PLL}$, is also
covered. On the negative side, we show that if an intuitionistic modal logic
extending $\mathsf{CK}$ does not admit Visser’s rules, then it cannot have a
sequent calculus as explained above. As there are many such intermediate modal
logics, we provide an interesting family of non-existence results. One
interesting example lives over the propositional fragment where we prove that
the only intermediate logic with a calculus consisting of constructive rules
is $\mathsf{IPC}$.

The method we use to prove the main result is also interesting by its own. It
is inspired by the technique that Hrubeš used in [18] to prove an exponential
lower bound on the lengths of proofs in the intuitionistic Frege system.
Usually, to prove the admissibility of an admissible rule in a logic, one
needs to design a sequent calculus for the logic and then eliminate the cut
rule to make the proof combinatorially controllable. Such a drastic change in
the proof structure is not possible in many cases if the logic has no cut-free
sequent calculi. Even in the cases that it does, the process of cut
elimination or the like is usually extremely costly. However, our method in
the present paper is based on using translations and as translations commute
with the cut rule, there is no need for any sort of cut elimination. As a
consequence of this liberal attitude towards cut, the extraction method
becomes feasible.

The paper is organized as follows. In Preliminaries, Section 2, we recall
several well-known constructive and intuitionistic modal logics and their
sequent calculi. In Section 3, we introduce the constructive rules and as a
witness to their generality, we present a wide range of its instances. In
Section 4, we present our main result, which is proving the feasible Visser-
Harrop property for any strong enough sequent calculus consisting of
constructive rules and some basic modal rules (up to a mild technical
property). Finally, the analogue of the main result is provided in Subsections
5.1, 5.2, and 5.3, for the $\Diamond$-free, $\Box$-free, and propositional
fragments, respectively.

Acknowledgements We are thankful to Rosalie Iemhoff for the interesting
discussions we had on the subject.

##  2 Preliminaries

Let $\mathcal{L}=\\{\wedge,\vee,\to,\top,\bot,\Box,\Diamond\\}$ be the
language of intuitionistic modal logic. In this paper, we mainly work over the
language $\mathcal{L}$. However, we are also interested in its fragments
$\mathcal{L}_{\Box}=\mathcal{L}\setminus\\{\Diamond\\}$,
$\mathcal{L}_{\Diamond}=\mathcal{L}\setminus\\{\Box\\}$ and
$\mathcal{L}_{p}=\mathcal{L}\setminus\\{\Box,\Diamond\\}$, addressed in
Subsections 5.1, 5.2, and 5.3, respectively. To refer to any of these
languages, we use the variable $\mathfrak{L}$ with the condition
$\mathfrak{L}\in\\{\mathcal{L},\mathcal{L}_{\Box},\mathcal{L}_{\Diamond},\mathcal{L}_{p}\\}$.
Fixing $\mathfrak{L}$, by _$\mathfrak{L}$ -formulas_, we mean the formulas
over the language $\mathfrak{L}$ in its usual sense. We use small Roman
letters $p,q,\dots$ for _atomic formulas (atoms)_. Small Greek letters
$\varphi,\psi,\dots$ and capital Roman letters $A,B,\dots$ denote
$\mathfrak{L}$-formulas. The bar notation, as in
$\overline{\varphi},\overline{\psi},\overline{A},\overline{B},\ldots$, is
reserved for finite multisets of $\mathfrak{L}$-formulas. Capital Greek
letters $\Gamma,\Delta,\dots$ denote finite multisets of
$\mathfrak{L}$-formulas as well as multiset variables (also called contexts).
The latter are the variables that can be substituted by finite multisets as it
is usual in the sequent-style rules. It will always be clear from the text
which one we are using. The set of _immediate subformulas_ of a formula $A$ is
defined recursively as follows. The immediate subformula of an atom is itself;
the immediate subformulas of $A\circ B$ are $A$ and $B$, for
$\circ\in\\{\wedge,\vee,\to\\}$ and the immediate subformula of $\bigcirc A$
is $A$, for $\bigcirc\in\\{\Box,\Diamond\\}$. For a formula $A$, define $\neg
A$ as $A\to\bot$ and $\bigcirc^{n}A$ recursively by $\bigcirc^{0}A=A$ and
$\bigcirc^{n+1}A=\bigcirc\bigcirc^{n}A$, where
$\bigcirc\in\\{\Box,\Diamond\\}$. For a multiset $\Gamma$, by
$\bigcirc\Gamma$, we mean $\\{\bigcirc\gamma\mid\gamma\in\Gamma\\}$. And, for
$\Gamma=\\{\gamma_{1},\dots,\gamma_{n}\\}$, by $\bigwedge\Gamma$ (resp.
$\bigvee\Gamma$), we mean $\gamma_{1}\wedge\ldots\wedge\gamma_{n}$ (resp.
$\gamma_{1}\vee\ldots\vee\gamma_{n}$). We use the convention
$\bigwedge\varnothing=\top$ and $\bigvee\varnothing=\bot$. By $\mathsf{IPC}$,
we mean the intuitionistic propositional logic and by $\mathsf{CPC}$, the
classical propositional logic.

###  2.1 Intuitionistic Modal Logics

We begin with a definition of logics over a given language
$\mathfrak{L}\in\\{\mathcal{L},\mathcal{L}_{\Box},\mathcal{L}_{\Diamond},\mathcal{L}_{p}\\}$.

######  Definition 2.1.

Let
$\mathfrak{L}\in\\{\mathcal{L},\mathcal{L}_{\Box},\mathcal{L}_{\Diamond},\mathcal{L}_{p}\\}$
be a language. A _logic $L$ over $\mathfrak{L}$ _is a set of
$\mathfrak{L}$-formulas closed under the substitution, modus ponens and

  * •

the necessitation rule, if $\mathfrak{L}=\mathcal{L}$ or
$\mathfrak{L}=\mathcal{L}_{\Box}$,

  * •

no other rule, if $\mathfrak{L}=\mathcal{L}_{\Diamond}$ or
$\mathfrak{L}=\mathcal{L}_{p}$, where

  * $\triangleright$

the _modus ponens_ rule means that if $\varphi,\varphi\to\psi\in L$ then
$\psi\in L$,

  * $\triangleright$

the _necessitation_ rule means that if $\varphi\in L$ then $\Box\varphi\in L$.

Let $L_{1}$ and $L_{2}$ be logics over the language $\mathfrak{L}$. Then,
$L_{2}$ _extends_ $L_{1}$, if $L_{1}\subseteq L_{2}$. Given a logic $L$
defined over $\mathfrak{L}$ and a set of $\mathfrak{L}$-formulas
$\\{A_{i}\\}_{i\in I}$, by $L+\\{A_{i}\\}_{i\in I}$, we mean the smallest
logic over $\mathfrak{L}$, extending $L$ and containing all the formulas in
$\\{A_{i}\\}_{i\in I}$.

To introduce intuitionistic modal logics, notice that over the language
$\mathcal{L}$, the modalities $\Box$ and $\Diamond$ are not supposed to be the
dual of each other, i.e, $\Diamond$ is not equivalent to $\neg\Box\neg$.
Consequently, there are many possibilities to define the intuitionistic
counterpart of a given classical modal logic (e.g., see [37]). In the
following, we introduce some intuitionistic modal logics starting from two
well-known intuitionistic counterparts of the classical modal logic
$\mathsf{K}$. First, consider the family of axioms in Table 1.

name | axiom | name | axiom
---|---|---|---
$K_{a}$ | $\Box(p\to q)\to(\Box p\to\Box q)$ | $K_{b}$ | $\Box(p\to q)\to(\Diamond p\to\Diamond q)$
$\Diamond\bot$ | $\neg\Diamond\bot$ | $\Diamond\vee$ | $\Diamond(p\vee q)\to\Diamond p\vee\Diamond q$
$\Box\to$ | $(\Diamond p\to\Box q)\to\Box(p\to q)$ | $D$ | $\Box p\to\Diamond p$
$D_{a}$ | $\Box\bot\to\bot$ | $D_{b}$ | $\top\to\Diamond\top$
$T_{a}$ | $\Box p\to p$ | $T_{b}$ | $p\to\Diamond p$
$4_{a}$ | $\Box p\to\Box\Box p$ | $4_{b}$ | $\Diamond\Diamond p\to\Diamond p$
$B_{a}$ | $\Diamond\Box p\to p$ | $B_{b}$ | $p\to\Box\Diamond p$
$5_{a}$ | $\Diamond\Box p\to\Box p$ | $5_{b}$ | $\Diamond p\to\Box\Diamond p$
$c_{a}$ | $p\to\Box p$ | $c_{b}$ | $\Diamond p\to p$
$den_{n,a}$ | $\Box^{n+1}p\to\Box^{n}p$ | $den_{n,b}$ | $\Diamond^{n}p\to\Diamond^{n+1}p$
$4_{n,m,a}$ | $\Box^{n}p\to\Box^{m}p$ | $4_{n,m,b}$ | $\Diamond^{m}p\to\Diamond^{n}p$
$tra_{n,a}$ | $\bigwedge_{i=1}^{n}\Box^{i}p\to\Box^{n+1}p$ | $tra_{n,b}$ | $\Diamond^{n+1}p\to\bigvee_{i=0}^{n}\Diamond^{i}p$
$ga$ | $\Diamond\Box p\to\Box\Diamond p$ | $ga_{klmn}$ | $\Diamond^{k}\Box^{l}p\to\Box^{m}\Diamond^{n}p$
$.2$ | $\Diamond(p\wedge\Box q)\to\Box(p\vee\Diamond q)$ | $d_{1}$ | $\neg\Diamond p\to\Box\neg p$
$d_{2}$ | $\Box\neg p\to\neg\Diamond p$ | $d_{3}$ | $\Diamond\neg p\to\neg\Box p$
$bw_{r}$ | $\bigwedge_{i=0}^{r}\Diamond p_{i}\to\bigvee_{0\leq i\neq j}^{r}\Diamond(p_{i}\wedge(p_{j}\vee\Diamond p_{j}))$ | $H$ | $p\to\Box(\Diamond p\to p)$
$bd_{n}$ | $\Diamond(\Box p_{n}\wedge bd_{n})\to p_{n}$ | $dir$ | $\Diamond(\Box p\wedge q)\to\Box(\Diamond p\vee q)$
$M^{\to}_{\Diamond}$ | $(p\to q)\to(\Diamond p\to\Diamond q)$ |  |
Table 1: Some modal axioms. Everywhere, we assume $n\geq 0$ and $r\geq 1$. In
$4_{n,m,a}$ and $4_{n,m,b}$ we assume $0\leq n<m$ and in $ga_{klmn}$ we have
$k,l,m,n\geq 0$. The formula $bd_{n}$ is defined recursively: $bd_{0}:=\bot$,
and $bd_{n+1}:=p_{n}\vee\Box(\Diamond\neg p_{n}\vee bd_{n})$.

Most of them are well-known for the properties they impose on the classical
Kripke frames that validate them: the axiom $(dir)$, when added to the logic
$\mathsf{K}$, is sound and complete with respect to directed Kripke frames.
Or, a Kripke frame $\mathcal{F}$ validates ($T_{a}$) if and only if
$\mathcal{F}$ is reflexive. Note that beside their classical importance, the
axioms $ga_{klmn}$, for $0\leq k,l,m,n$, have been studied both syntactically
and semantically in the realm of intuitionistic modal logics (e.g., see [37]).

Over the language $\mathcal{L}$, there are two basic modal logics considered
as the intuitionistic counterparts of the logic $\mathsf{K}$. The first, is
the _constructive_ $\mathsf{K}$, denoted by $\mathsf{CK}$, studied for
instance in [4], and the second is the _intuitionistic_ $\mathsf{K}$, denoted
by $\mathsf{IK}$, introduced in [12, 13] and studied in [36] in detail:

$\mathsf{CK}:=\mathsf{IPC}+\\{K_{a},K_{b}\\}\quad\quad\quad\mathsf{IK}:=\mathsf{IPC}+\\{K_{a},K_{b},\Diamond\vee,\Box\to,\Diamond\bot\\}$

$\mathsf{CK}$ is the weakest intuitionistic modal logic considered in this
paper. Using the axioms in Table 1, we can design constructive versions of
well-known classical modal logics. To name a few, let
$X\subseteq\\{T,B,4,5\\}$. By $\mathsf{CK}X$, we mean the smallest logic over
$\mathcal{L}$ extending $\mathsf{CK}$ and all the axioms in $X$ in both $(a)$
and $(b)$ versions. An interesting logic is the constructive counterpart of
$\mathsf{S4}$, introduced in [4] and defined as $\mathsf{CK}T4$, which is
$\mathsf{CK}+\\{T_{a},T_{b},4_{a},4_{b}\\}$.

Although $\mathsf{CK}$ is natural and interesting in some settings, including
the type theoretical approach to modality, the system $\mathsf{IK}$ is the one
that is claimed to be the _true_ intuitionistic analogue of the classical
modal logic $\mathsf{K}$. In [12, 13], Fischer-Servi provided two types of
evidence to support this claim. First, she mapped $\mathsf{IK}$ to an
extension of the fusion of $\mathsf{K}$ and $\mathsf{S4}$, using a natural
generalization of Gödel’s translation. Second, using the standard translation
of modal formulas to first order formulas, in the same manner that
$\mathsf{K}$ is mapped into the classical first order logic, $\mathsf{IK}$ is
mapped into the intuitionistic first order logic. Several extensions of
$\mathsf{IK}$ have been introduced and studied (e.g., see [3]), where the
intuitionistic version of several modal logics such as $\mathsf{KD,KT,KB,S4,}$
and $\mathsf{S5}$ are investigated. To be more precise, for any
$X\subseteq\\{T,B,4,5\\}$, define $\mathsf{IK}X$ as the smallest logic over
$\mathcal{L}$ extending $\mathsf{IK}$ and all the axioms in $X$ in both $(a)$
and $(b)$ versions. An important logic here is the logic $\mathsf{MIPC}$
defined as $\mathsf{MIPC}:=\mathsf{IK}T45.$

It is possible to introduce some intuitionistic modal logics over the
fragments of $\mathcal{L}$. Over the language $\mathcal{L}_{\Box}$, the basic
system we are interested in is $\mathsf{CK}_{\Box}:=\mathsf{IPC}+\\{K_{a}\\}$.
In [37], $\mathsf{CK}_{\Box}$ is introduced by the name $\mathsf{IntK_{\Box}}$
and $\Diamond\varphi$ is defined as $\neg\Box\neg\varphi$. Consequently,
$\Diamond$ is not distributed over disjunction. This relation between $\Box$
and $\Diamond$ is too binding from the intuitionistic perspective. Again, we
can extend $\mathsf{CK}_{\Box}$ by the $\Diamond$-free axioms in Table 1. More
precisely, let $X\subseteq\\{T,4\\}$. By $\mathsf{CK}_{\Box}X$, we mean the
smallest logic over $\mathcal{L}_{\Box}$ extending $\mathsf{CK}_{\Box}$ and
all the axioms in $X$ in their $(a)$ version. These logics, specially with the
$\mathsf{S4}$ and $\mathsf{S5}$ flavours, are studied in [34] by model
theoretical methods.

Finally, the most basic logic in this paper over $\mathcal{L}_{\Diamond}$ is
the _basic lax logic_ , $\mathsf{BLL}:=\mathsf{IPC}+\\{M^{\to}_{\Diamond}\\}$,
(see Table 1). If we add the axioms $(T_{b})$ and $(4_{b})$ to the logic
$\mathsf{BLL}$, we get the _propositional lax logic_ ,
$\mathsf{PLL}:=\mathsf{IPC}+\\{M^{\to}_{\Diamond},T_{b},4_{b}\\}$, see [9].
For a nice survey on intuitionistic modal logics, see [36].

So far, we have seen two approaches to design modal logics over the
intuitionistic base. We can also lift these approaches to the intermediate
base.

######  Definition 2.2.

Let $L$ be an intermediate logic, i.e., a logic over $\mathcal{L}_{p}$ such
that $\mathsf{IPC}\subseteq L\subseteq\mathsf{CPC}$. Then, by $L\mathsf{CK}$
(resp. $L\mathsf{IK}$), we mean the smallest logic over $\mathcal{L}$,
extending $L\cup\mathsf{CK}$ (resp. $L\cup\mathsf{IK}$). Similarly, we define
$L\mathsf{CK}_{\Box}$ as the smallest logic over $\mathcal{L}_{\Box}$,
extending $L\cup\mathsf{CK}_{\Box}$ and we set $L\mathsf{BLL}$ as the smallest
logic over $\mathcal{L}_{\Diamond}$, extending $L\cup\mathsf{BLL}$.

Moving to Kripke frames, there are also different proposals for their
intuitionistic counterparts. Here, we define the most general one that
captures our base logic $\mathsf{CK}$. However, as we will only use them when
they have one node, the choice of the model is immaterial in this paper.

######  Definition 2.3.

[32] A _constructive modal Kripke frame_ is a quadruple
$\mathcal{F}=(W,\leq,R,F)$, where $W$ is a non-empty set, $\leq$ is a preorder
(a reflexive and transitive binary relation) on $W$, $R$ is a binary relation
on $W$ and $F\subseteq W$, a set of fallible worlds, such that:

  * •

$F$ is closed under $\leq$: if $v\in F$ and $v\leq w$ then $w\in F$,

  * •

$F$ is closed under $R$: if $(v,w)\in R$ and $v\in F$ then $w\in F$,

  * •

$R$ is serial on $F$: if $v\in F$ then there exists $w\in F$ such that
$(v,w)\in R$.

A _constructive modal Kripke model_ based on the frame
$\mathcal{F}=(W,\leq,R,F)$ is a tuple $\mathcal{M}=(W,\leq,R,F,V)$, where $V$
is a valuation function mapping each world in $W$ to a set of atomic formulas
in $\mathcal{L}$ such that for every $v,w\in W$ if $v\leq w$ then
$V(v)\subseteq V(w)$, and if $w\in F$ then $V(w)$ has all the atomic formulas.
Define a formula $\varphi$ to be _true at the world $w$ in $\mathcal{M}$_,
denoted by $\mathcal{M},w\vDash\varphi$ (or $w\vDash\varphi$, for short), by
recursion on the construction of $\varphi$:

$\mathcal{M},w\vDash\top$ |  |
---|---|---
$\mathcal{M},w\vDash\bot$ | iff |  $w\in F$;
$\mathcal{M},w\vDash p$ | iff |  $p\in V(w)$, for an atomic formula $p$;
$\mathcal{M},w\vDash\varphi\wedge\psi$ | iff |  $\mathcal{M},w\vDash\varphi$ and $\mathcal{M},w\vDash\psi$;
$\mathcal{M},w\vDash\varphi\vee\psi$ | iff |  $\mathcal{M},w\vDash\varphi$ or $\mathcal{M},w\vDash\psi$;
$\mathcal{M},w\vDash\varphi\to\psi$ | iff |  $\forall v\geq w$, if $\mathcal{M},v\vDash\varphi$ then $\mathcal{M},v\vDash\psi$;
$\mathcal{M},w\vDash\Box\varphi$ | iff |  $\forall u\geq w,\forall v\in W$ (if $(u,v)\in R$, then $\mathcal{M},v\vDash\varphi\big{)}$;
$\mathcal{M},w\vDash\Diamond\varphi$ | iff |  $\forall u\geq w$, $\exists v\in W$ $\big{(}(u,v)\in R$ and $\mathcal{M},v\vDash\varphi$).

A formula $\varphi$ is _valid in $\mathcal{M}$_, denoted by
$\mathcal{M}\vDash\varphi$, when $\mathcal{M},w\vDash\varphi$ for all $w\in
W$, and it is _valid in $\mathcal{F}$_ when it is valid in all models based on
$\mathcal{F}$. A logic $L$ is _valid in_ $\mathcal{F}$ if
$\mathcal{F}\vDash\varphi$, for any $\varphi\in L$. By the _reflexive node
frame_ , we mean the frame
$\mathcal{K}_{r}=(\\{w\\},=,\\{(w,w)\\},\varnothing)$ and by the _irreflexive
node frame_ , we mean $\mathcal{K}_{i}=(\\{w\\},=,\varnothing,\varnothing)$.

###  2.2 Sequent Calculi

A _sequent_ $S$ over the language $\mathfrak{L}$ is an expression of the form
$\Sigma\Rightarrow\Lambda$, where $\Sigma$ and $\Lambda$ are finite multisets
of $\mathfrak{L}$-formulas. By the formula interpretation of the sequent
$S=\Sigma\Rightarrow\Lambda$, we mean $I(S)=\bigwedge\Sigma\to\bigvee\Lambda$.
The multiset $\Sigma$ is called the _antecedent_ and $\Lambda$ the _succedent_
of the sequent $S$. If the succedent of a sequent has at most one formula, the
sequent is called _single-conclusion_. A _meta-sequent_ $\mathcal{S}$ is
defined in the same way as sequents, except that here we are also allowed to
use multiset variables both in the antecedents and in the succedents and we
can also use the boxes of the multiset variables in the antecedents. More
precisely, a meta-sequent is in the form

$\\{\Box\Gamma_{i}\\}_{i\in I},\\{\Pi_{j}\\}_{j\in
J},\overline{A}\Rightarrow\Delta\quad$ or $\quad\\{\Box\Gamma_{i}\\}_{i\in
I},\\{\Pi_{j}\\}_{j\in J},\overline{A}\Rightarrow\overline{B}$

where $\Gamma_{i},\Pi_{j},$ and $\Delta$ are multiset variables and $I$ is a
(possibly empty) set of indices, and $\overline{A}$ and $\overline{B}$ are
(possibly empty) multisets of $\mathfrak{L}$-formulas. Notice that the meta-
sequents, as defined, are not in their most general form. For instance, it is
possible to allow more complex expressions such as $\Diamond\Box\Gamma$ in the
meta-sequents, where $\Gamma$ is a multiset variable. However, we use this
restricted form as it is the only form we need in the present paper.

A _rule_ is an expression of the form
$\mathcal{S}_{1},\;\;\ldots,\;\;\mathcal{S}_{n}$ $\mathcal{S}$ where
$\mathcal{S}$, called the _conclusion_ , and $\mathcal{S}_{i}$’s, called the
_premises_ , are meta-sequents. A rule with no premise is called an _axiom_.
By an _instance_ of a rule or an axiom over $\mathfrak{L}$, we mean the result
of substituting the multiset variables by multisets of $\mathfrak{L}$-formulas
and substituting the atomic formulas by $\mathfrak{L}$-formulas. A _sequent
calculus_ (_calculus_ , for short) over $\mathfrak{L}$ is defined as a finite
set of rules over $\mathfrak{L}$. A sequent calculus $H$ _extends_ the sequent
calculus $G$ when they are over the same language and $G\subseteq H$. For a
set of rules $\mathcal{R}$, by $G+\mathcal{R}$, we mean the calculus obtained
by adding every rule in $\mathcal{R}$ to $G$. For a set of formulas
$\mathcal{A}$, by $G+\mathcal{A}$, we mean the calculus obtained by adding the
meta-sequent $(\,\Rightarrow A)$, for every $A\in\mathcal{A}$ as an axiom to
$G$. A _proof_ $\pi$ in the calculus $G$ for a sequent $T$ from a finite set
of sequents $\\{T_{i}\\}_{i\in I}$ is a sequence of sequents
$\\{S_{j}\\}_{j=1}^{m}$ such that $S_{m}=T$ and each sequent $S_{j}$ is either
one of the sequents $T_{i}$, or an instance of an axiom in $G$, or derived
from an instance of a rule in $G$ from some $S_{j_{1}},\dots,S_{j_{k}}$, where
$j_{1},\dots,j_{k}<j$. When $\pi$ is a proof of $T$ from $\\{T_{i}\\}_{i\in
I}$ in $G$, we write $\\{T_{i}\\}_{i\in I}\vdash^{\pi}_{G}T$, and we call it a
_$G$ -proof_ of $T$ from the set of assumptions $\\{T_{i}\\}_{i\in I}$. If
$\pi$ is a proof of the sequent $S$ in $G$ from an empty set of assumptions,
we write $G\vdash^{\pi}S$ and we call $\pi$ a _$G$ -proof_ of $S$. We say the
formulas $A$ and $B$ are $G$-_equivalent_ or _equivalent in $G$_, denoted by
$G\vdash A\Leftrightarrow B$, when $G\vdash A\Rightarrow B$ and $G\vdash
B\Rightarrow A$. A rule $R$ is called _admissible_ in $G$, if for any instance
$S_{1},\;\;\ldots,\;\;S_{n}$ $S$ of $R$, the provability of all the premises
in $G$ implies the provability of the conclusion in $G$. Similarly, $R$ is
_admissible_ in a logic $L$, when for any instance
$S_{1},\;\;\ldots,\;\;S_{n}$ $S$ of $R$, if $I(S_{1}),\dots,I(S_{n})\in L$
then $I(S)\in L$. The rule $R$ is called _provable_ in $G$, if for any
instance  $S_{1},\;\;\ldots,\;\;S_{n}$ $S$ we have
$S_{1},\ldots,S_{n}\vdash_{G}S$. We say $L$ is the _logic of the sequent
calculus_ $G$ or equivalently $G$ is the _sequent calculus of the logic_ $L$,
when $\Sigma\Rightarrow\Lambda$ is provable in $G$ if and only if
$\bigwedge\Sigma\to\bigvee\Lambda\in L$, for any sequent
$\Sigma\Rightarrow\Lambda$. Usually, we prefer to use the same name for a
logic and its canonical sequent calculus. However, we use different fonts to
distinguish them. We use the boldface letters, as in $\mathbf{CK}$, for a
sequent calculus while the sans-serif font, as in $\mathsf{CK}$, is reserved
for the logic. Finally, if $\mathcal{M}$ is a constructive modal Kripke model
and $S=(\Sigma\Rightarrow\Lambda)$ a sequent, then _$S$ is valid in
$\mathcal{M}$_ if $I(S)=\bigwedge\Sigma\to\bigvee\Lambda$ is valid in
$\mathcal{M}$. A similar definition for frames is in place. Moreover, a
sequent calculus $G$ is _valid in the frame_ $\mathcal{F}$ (model
$\mathcal{M}$) if every $G$-provable sequent is valid in $\mathcal{F}$ (model
$\mathcal{M}$).

For $\mathsf{IPC}$ we use the single-conclusion Gentzen-style sequent
calculus, $\mathbf{LJ}$333The calculus mentioned here is almost identical to
Gentzen’s original calculus $\mathbf{LJ}$, where $\Gamma$ and $\Delta$ are
sequences of formulas, as opposed to finite multisets, and the axioms are
slightly different. However, it is easy to see that these two systems are
equivalent., presented in Table 2.

$\Gamma,p\Rightarrow p\;\;$ $(id)$ |  $\Gamma,\bot\Rightarrow\Delta\;\;$ $(L\bot)$ |  $\Gamma\Rightarrow\top\;\;$ $(R\top)$
---|---|---
$\Gamma,p,p\Rightarrow\Delta$ $(Lc)$ $\Gamma,p\Rightarrow\Delta$ |  $\Gamma\Rightarrow$ $(Rw)$ $\Gamma\Rightarrow p$ |  |
$\Gamma\Rightarrow p$ $\Gamma,p\Rightarrow\Delta$ $(cut)$ $\Gamma\Rightarrow\Delta$ |  |  |
$\Gamma\Rightarrow p$ $\Gamma\Rightarrow q$ $(R\wedge)$ $\Gamma\Rightarrow p\wedge q$ |  $\Gamma,q\Rightarrow\Delta$ $(L\wedge_{2})$ $\Gamma,p\wedge q\Rightarrow\Delta$ |  |
$\Gamma\Rightarrow q$ $(R\vee_{2})$ $\Gamma\Rightarrow p\vee q$ |  |  |
$\Gamma\Rightarrow p$ $\Gamma,q\Rightarrow\Delta$ $(L\to)$ $\Gamma,p\to q\Rightarrow\Delta$ |  $\Gamma,p\Rightarrow q$ $(R\to)$ $\Gamma\Rightarrow p\to q$ |  |

Table 2: Single-conclusion sequent calculus $\mathbf{LJ}$

Note that being single-conclusion means that in each rule, $\Delta$ has at
most one formula. In Table 1, several modal axioms are introduced. Adding them
to $\mathbf{LJ}$ will result in various sequent calculi for intuitionistic
modal logics. To present sequent calculi for the logics introduced in
Subsection 2.1, consider the following modal rules:

$\Gamma\Rightarrow p$ $(K_{\Box})$ $\Box\Gamma\Rightarrow\Box p$ |  $\Gamma,p\Rightarrow q$ $(\Diamond L)$ $\Gamma,\Diamond p\Rightarrow\Diamond q$
---|---

Over $\mathcal{L}$, the most basic intuitionistic modal calculus that we are
interested in is $\mathbf{CK}$ defined as
$\mathbf{LJ}+\\{K_{\Box},K_{\Diamond}\\}$. Note that the cut rule is
explicitly present in $\mathbf{LJ}$ and hence in $\mathbf{CK}$. For the logic
$\mathsf{CK}X$, where $X\subseteq\\{T,B,4,5\\}$, by $\mathbf{CK}X$, we mean
the calculus $\mathbf{CK}$ extended by the axioms in $X$ in both $(a)$ and
$(b)$ versions. Over $\mathcal{L}_{\Box}$, we denote the calculus
$\mathbf{LJ}+\\{K_{\Box}\\}$ by $\mathbf{CK}_{\Box}$. For the logic
$\mathsf{CK}_{\Box}X$, where $X\subseteq\\{T,4\\}$, by $\mathbf{CK}_{\Box}X$,
we mean the calculus $\mathbf{CK}_{\Box}$ extended by the axioms in $X$ in
their $(a)$ version. Over $\mathcal{L}_{\Diamond}$, the interesting systems
are the calculus $\mathbf{BLL}$ defined as $\mathbf{LJ}+\\{\Diamond L\\}$. If
we add the axioms $(T_{b})$ and $(4_{b})$ to the calculus $\mathbf{BLL}$, we
reach the calculus $\mathbf{PLL}=\mathbf{LJ}+\\{\Diamond L,T_{b},4_{b}\\}$. It
is easy to see that the systems introduced here are the sequent calculi for
their corresponding logics, introduced in Subsection 2.1.

######  Remark 2.4.

Unlike the usual situation where sequent calculi are assumed to be “well-
behaved”, here we are quite liberal to accept the problematic rules such as
cut, the unfamiliar rules such as  $\Gamma\Rightarrow p\wedge q$
$\Gamma\Rightarrow p$ and initial sequents like $\Gamma\Rightarrow\Box p\to
p$, in our systems. Therefore, one may read our sequent calculi as our
preferred way to represent the general proof systems and nothing more. For
instance, it is easy to represent the natural deduction systems using the
sequent calculi we allow. In this sense, our results about sequent calculi can
be safely applied on the natural deduction systems, as well.

######  Definition 2.5.

Let $L$ be a logic over the language
$\mathfrak{L}\in\\{\mathcal{L},\mathcal{L}_{\Box},\mathcal{L}_{\Diamond},\mathcal{L}_{p}\\}$.
We say that $L$ has the _disjunction property (DP)_ , if $A\vee B\in L$
implies either $A\in L$ or $B\in L$, for any $\mathfrak{L}$-formulas $A$ and
$B$. Define _Visser’s rules_ as

$V_{n}$ $\Rightarrow\left(\bigwedge_{i=1}^{n}\left(p_{i}\rightarrow
q_{i}\right)\rightarrow p_{n+1}\vee p_{n+2}\right)\vee r$
$\Rightarrow\bigvee_{j=1}^{n+2}\left(\bigwedge_{i=1}^{n}\left(p_{i}\rightarrow
q_{i}\right)\rightarrow p_{j}\right)\vee r$
---

for $n\geq 1$. By abuse of notation, if $L$ has DP, we say $L$ admits $V_{0}$
to consider DP as one of Visser’s rules. We say the logic $L$ _admits all
Visser’s rules_ when it admits all $V_{n}$ for $n\geq 0$.

######  Remark 2.6.

It is easy to see that a logic $L$ admits all Visser’s rules if and only if it
has the property that if $\bigwedge_{i\in I}(A_{i}\to B_{i})\to(C\vee D)\in
L$, for some (possibly empty) finite index set $I$, then one of the following
formulas:

$\bigwedge_{i\in I}(A_{i}\to B_{i})\to C\;$ or |  $\bigwedge_{i\in I}(A_{i}\to B_{i})\to D\;$ or |  $\bigwedge_{i\in I}(A_{i}\to B_{i})\to A_{i}\;$,
---|---|---

for some $i\in I$, is in $L$.

######  Lemma 2.7.

Let $G$ be a calculus over $\mathcal{L}$ for a logic $L$ over $\mathcal{L}$
such that $L\supseteq\mathsf{CK}$. Then, $G+\mathbf{CK}$ is also a calculus
for $L$. The same holds if we replace the triple
$(\mathcal{L},\mathsf{CK},\mathbf{CK})$ by
$(\mathcal{L}_{\Box},\mathsf{CK}_{\Box},\mathbf{CK}_{\Box})$,
$(\mathcal{L}_{\Diamond},\mathsf{BLL},\mathbf{BLL})$, or
$(\mathcal{L}_{p},\mathsf{IPC},\mathbf{LJ})$.

###### Proof.

We only prove the case for the language $\mathcal{L}$. The rest are similar.
For the case $\mathcal{L}$, we know that adding the admissible rules of $L$ to
$G$ does not change the theorems of $L$. Therefore, it is enough to show that
all the axioms and rules of $\mathbf{CK}$ are admissible in $L$. We only
investigate the crucial rules of cut and $(K_{\Box})$, as the other are
similar. First, as $L\supseteq\mathsf{CK}$, we have:

  1. 1.

$(C\to D)\to(C\to C\wedge D)\in L$,

  2. 2.

$(E\to F)\to[(F\to I)\to(E\to I)]\in L$.

  3. 3.

$\bigwedge\Box\Gamma\to\Box\bigwedge\Gamma\in L$

for any formulas $C,D,E,F$, $I$ and multiset $\Gamma$. The reason is that all
these formulas are in $\mathsf{CK}$ and hence in $L$. Now, for the
admissibility of the cut rule, suppose $\bigwedge\Gamma\to A\in L$ and
$(\bigwedge\Gamma\wedge A)\to B\in L$. By 1 and the former formula, as $L$ is
closed under modus ponens, we get $\bigwedge\Gamma\to(\bigwedge\Gamma\wedge
A)\in L$. By 2, we have

$(\bigwedge\Gamma\to(\bigwedge\Gamma\wedge A))\to[(\bigwedge\Gamma\wedge A)\to
B)\to(\bigwedge\Gamma\to B)]\in L.$

Therefore, as $L$ is closed under modus ponens, we have $\bigwedge\Gamma\to
B\in L$.
For the admissibility of the rule $(K_{\Box})$, suppose $\bigwedge\Gamma\to
A\in L$. By definition of a logic, $L$ is closed under necessitation. Hence,
$\Box(\bigwedge\Gamma\to A)\in L$. As $L\supseteq\mathsf{CK}$, we have
$\Box(\bigwedge\Gamma\to A)\to(\Box\bigwedge\Gamma\to\Box A)\in L$. Since $L$
is closed under modus ponens, we get $\Box\bigwedge\Gamma\to\Box A\in L$. By
3, $\bigwedge\Box\Gamma\to\Box\bigwedge\Gamma\in L$. Therefore, by 2 and modus
ponens, we get $\bigwedge\Box\Gamma\to\Box A\in L$. ∎

Finally, we set some basic conventions on the complexity-theoretic part of the
paper. The _size_ of a formula $A$, a multiset $\Gamma$, a sequent $S$ or a
proof $\pi$ is defined as the number of symbols in it, and denoted by $|A|$,
$|\Gamma|$, $|S|$, and $|\pi|$, respectively. For a multiset $\Gamma$, by
$\parallel\Gamma\parallel$, we mean the cardinality of $\Gamma$, i.e., the
number of the elements in $\Gamma$, counting their multiplicity. An algorithm
is called _feasible_ , if it runs in polynomial time in the size of the input.
We use feasible and polynomial time computable, interchangeably. A proof is
called _tree-like_ , if every sequent in the proof is used at most once as a
hypothesis of a rule in the proof. From the complexity theoretic point of
view, usually it makes a difference if we use tree-like proofs or _general
(dag-like)_ proofs. However, in the presence of the cut rule, conjunction and
implication in the language and their intuitionistic rules, it is possible to
feasibly simulate dag-like proofs by tree-like ones, see [33]. Therefore,
w.l.o.g., throughout this paper, whenever we write down a proof, we always
mean a tree-like proof. The reason for this preference is the inequality

$\sum_{i\in I}|\pi_{i}|+|S|\leq|\pi|,$

where $\pi$ is a tree-like proof with the conclusion $S$ and the immediate
sub-proofs $\\{\pi_{i}\\}_{i\in I}$, i.e., the proofs of the premises. This
inequality helps to bound the time of different constructions in which we will
use $\pi$ as an input.

######  Definition 2.8.

Let
$\mathfrak{L}\in\\{\mathcal{L},\mathcal{L}_{\Box},\mathcal{L}_{\Diamond},\mathcal{L}_{p}\\}$
be a language and $G$ be a sequent calculus over $\mathfrak{L}$. A rule $R$
over $\mathfrak{L}$ is called _feasibly provable_ in $G$, if there is a
polynomial time algorithm $f_{R}$ such that for any $\mathfrak{L}$-instance of
$R$ with the premises $\\{S_{i}\\}_{i\in I}$ and the consequence $S$,
$f(\\{S_{i}\\}_{i\in I},S)$ provides a $G$-proof of $S$ with the set of
assumptions $\\{S_{i}\\}_{i\in I}$, i.e., $\\{S_{i}\\}_{i\in
I}\vdash_{G}^{f(\\{S_{i}\\}_{i\in I},S)}S$. A sequent calculus $G$ is called
_strong_ over the language

  * •

$\mathcal{L}$, if every axiom and rule of $\mathbf{CK}$ is feasibly provable
in $G$;

  * •

$\mathcal{L}_{\Box}$, if every axiom and rule of $\mathbf{CK}_{\Box}$ is
feasibly provable in $G$;

  * •

$\mathcal{L}_{\Diamond}$, if every axiom and rule of $\mathbf{BLL}$ is
feasibly provable in $G$;

  * •

$\mathcal{L}_{p}$, if every axiom and rule of $\mathbf{LJ}$ is feasibly
provable in $G$.

######  Remark 2.9.

Clearly if a rule is in $G$, it is feasibly provable in $G$. Hence, if $G$ is
defined over $\mathcal{L}$ and has all the axioms and rules of $\mathbf{CK}$
as its axioms and rules, then $G$ is trivially strong over $\mathcal{L}$. A
corresponding claim also holds for the fragments of $\mathcal{L}$.

######  Definition 2.10.

Let $G$ and $H$ be two sequent calculi over the same language. A _polynomial
deduction simulation_ (_pd-simulation_) of $G$ in $H$ is a polynomial time
function $f$ such that for any proof $\pi$ of $S$ from $\\{S_{i}\\}_{i\in I}$
in $G$, $f(\pi)$ is a proof of $S$ from $\\{S_{i}\\}_{i\in I}$ in $H$. We say
$H$ _pd-simulates_ $G$, denoted by $G\leq_{pd}H$ when there is a pd-simulation
of $G$ in $H$. The calculi $G$ and $H$ are _pd-equivalent_ , when
$G\leq_{pd}H$ and $H\leq_{pd}G$. Sequent calculi $G$ and $H$ are _d-
equivalent_ if $\\{S_{i}\\}_{i\in I}\vdash_{G}S$ if and only if
$\\{S_{i}\\}_{i\in I}\vdash_{H}S$, for any family of sequents
$\\{S_{i}\\}_{i\in I}\cup\\{S\\}$.

######  Remark 2.11.

The well-known notion of p-simulation of one proof system by another is a
feasible machinery to simulate proofs without any assumptions. Our pd-
simulation strengthens this notion to also cover _deductions_ , i.e., proofs
where assumptions can also be present. For the specific systems we are
interested in, these two notions are equivalent. However, to avoid any
confusion, throughout this paper, we only use the pd-simulations.

######  Lemma 2.12.

Let $G$ and $H$ be two sequent calculi over
$\mathfrak{L}\in\\{\mathcal{L},\mathcal{L}_{\Box},\mathcal{L}_{\Diamond},\mathcal{L}_{p}\\}$.

  1. 1.

For any rule $R$ over $\mathfrak{L}$, if $G\leq_{pd}H$ and $R$ is feasibly
provable in $G$, then $R$ is feasibly provable in $H$.

  2. 2.

If each rule of $G$ is feasibly provable in $H$, then $G\leq_{pd}H$.

###### Proof.

Part 1 is easy. For 2, by the assumption, for each rule $R$ of $G$, there is a
feasible function $f_{R}$ such that for any instance $(\\{S_{k}\\}_{k\in
K},S)$ of $R$, $f_{R}(\\{S_{k}\\}_{k\in K},S)$ is an $H$-proof of $S$ from the
assumptions $\\{S_{k}\\}_{k\in K}$. Therefore, $f_{R}$ is computable in time
$O((\sum_{k\in K}|S_{k}|+|S|)^{c_{R}})$, for some constant $c_{R}$. As $G$ has
finitely many rules, we set $c$ as the maximum of all $c_{R}$’s. Hence, each
$f_{R}$ is computable in time $O((\sum_{k\in K}|S_{k}|+|S|)^{c})$. Now, to
simulate any $G$-proof $\pi$ in $H$, it is enough to replace the instance
$(\\{S_{k}\\}_{k\in K},S)$ of any rule $R$ used in $\pi$ by
$f_{R}(\\{S_{k}\\}_{k\in K},S)$. Call the result of this replacement $g(\pi)$
and notice that $g(\pi)$ is a proof in $H$. To compute the time that $g$
requires, note that any sequent in $\pi$ is bounded in size by $|\pi|$.
Therefore, for each $f_{R}(\\{S_{k}\\}_{k\in K},S)$ in $g(\pi)$, we need
$O(|\pi|^{c})$ steps for the computation and as the number of the rules in
$\pi$ is less than $|\pi|$, the whole time that $g(\pi)$ requires is
$O(|\pi|^{c+1})$. ∎

######  Remark 2.13.

Let $\mathcal{A}$ be a finite set of axioms and $G$ be a sequent calculus in
which the weakening rules are feasibly provable. Recall that we defined
$G+\mathcal{A}$ as a sequent calculus obtained by adding the meta-sequent
$(\,\Rightarrow A)$ as an axiom, for any $A\in\mathcal{A}$. It is also
possible to define $G+\mathcal{A}$ as the calculus obtained by adding the
meta-sequent $\Gamma\Rightarrow A$, for any $A\in\mathcal{A}$, where $\Gamma$
is a multiset variable. Call this new definition
$G+^{{}^{\prime}}\mathcal{A}$. We claim that $G+^{{}^{\prime}}\mathcal{A}$ and
$G+^{{}^{\prime}}\mathcal{A}$ are pd-equivalent. It is clear that
$G+^{{}^{\prime}}\mathcal{A}$ pd-simulates $G+\mathcal{A}$. For the converse,
as the weakening rule is feasibly provable in $G$, it is easy to see that the
axiom $\Gamma\Rightarrow A$ is feasibly provable in $G$ and hence by Lemma
2.12, $G+\mathcal{A}$ pd-simulates $G+^{{}^{\prime}}\mathcal{A}$. Using this
observation, from now on, as we only work with the calculi that feasibly prove
the weakening rules, we will use these two definitions interchangeably.

##  3 Constructive Formulas and Rules

One of the main goals of the present paper is to identify a general form for
constructive rules in the intuitionistic realm of modal logics. Informally
speaking, by a constructive rule, we mean a rule that its addition to the base
system $\mathbf{CK}$ respects the constructive character of the intuitionistic
ground. In this section, we first provide a formalization for these
constructive rules. Then, by presenting many examples, we see how general
these rules are and finally we provide a justification for our choice.

Our strategy to find a natural candidate for constructive rules consists of
two parts. First, by employing the least possible syntactical limit on
formulas, we introduce a class of constructive formulas as the simplest case
of the general form of the constructive rules. By a constructive formula, we
mean a formula $A$ such that if we extend $\mathbf{CK}$ with the axiom
$(\,\Rightarrow A)$, the calculus remains constructively acceptable. Second,
we exhaustively investigate a general form for rules and select the ones that
are equivalent to a constructive formula. To show that this syntactical limit
provides a _true_ constructive system, in Section 4 we show that any calculus
extending $\mathbf{CK}$ by some constructive rules and satisfying a mild
technical condition admits the feasible version of Visser’s rules and
specially has the feasible disjunction property. This provides a substantial
evidence for the claim that the introduced rules are constructive, as well as
a uniform machinery to prove the feasible version of Visser’s rules for a huge
family of intuitionistic modal logics.

###  3.1 Constructive Formulas

To identify the aforementioned class of constructive formulas, we employ the
well-known heuristic that constructive formulas, whatever they are, must be
careful with positive occurrences of the _disjunction-like_ connectives, i.e.,
$\\{\vee,\Diamond\\}$. For instance, the axioms444Although the sequent
$(\,\Rightarrow A)$ is the axiom, for simplicity, we also call $A$ an
axiom.$\neg(p\wedge q)\rightarrow\neg p\vee\neg q$ and $\neg\Box
p\rightarrow\Diamond\neg p$ are clearly non-constructive. The former proves
the axiom of the weak excluded middle, i.e., $\neg r\vee\neg\neg r$, that
breaks the disjunction property and hence is not constructively acceptable.
For the latter, using the Kripke-style first-order reading of a modal formula,
$\neg\Box p\rightarrow\Diamond\neg p$ is reminiscent of the first-order
formula $\neg\forall xP(x)\to\exists x\neg P(x)$, which is not constructively
acceptable.

Following this heuristic, one might naively demand that constructive formulas
must be defined as formulas that have no positive occurrences of the
connectives $\\{\vee,\Diamond\\}$. Here are two objections to this proposal.
First, note that this restriction is too strict and rejects even some
constructively accepted formulas with positive occurrences of
$\\{\vee,\Diamond\\}$ that are essential for a constructive reasoning. For
instance, consider the axioms $p\rightarrow p\vee q$ and $\Diamond
p\vee\Diamond q\rightarrow\Diamond(p\vee q)$, where the former is even an
axiom of the intuitionistic logic. Second, even in such a harsh form, the
restriction may not be sufficient to ensure the constructive character of the
resulting system. The reason is that the disjunction-like connectives are
sometimes introduced in an indirect manner via an occurrence of a nested
_implication-like_ connective, i.e., $\\{\Box,\to\\}$. For instance, the axiom
$\neg\neg p\rightarrow p$ indirectly proves $q\vee\neg q$ in a constructively
acceptable manner. Hence, to have a constructive axiom, we should also be
careful with nested implication-like connectives. Here, one might object that
what really is problematic is nested implications and boxes are harmless.
However, reading the box as what its first-order interpretation dictates, it
is clear that the box has the same character as the universal quantifier and
hence behaves similarly as the implication.

To solve these issues, we first extend the heuristic of avoiding the positive
occurrences of $\\{\vee,\Diamond\\}$, by also adding a limit on the depth of
the nested implication-like connectives. We limit this depth to two, as the
problematic formulas such as $\neg\neg p\rightarrow p$ have the depth three or
more.555By the depth function, we formally mean the function defined by:
$d(p)=d(\bot)=d(\top)=0$, $d(\varphi\circ\psi)=max\\{d(\varphi),d(\psi)\\}$,
for any $\circ\in\\{\wedge,\vee\\}$, $d(\Diamond\varphi)=d(\varphi)$,
$d(\varphi\to\psi)=max\\{d(\varphi)+1,d(\psi)\\}$ and
$d(\Box\varphi)=max\\{d(\varphi),1\\}$. For instance, the depth of $(p\to
q)\to r$ and $\Box\Box p\to q$ are two, while the depth of $p\to(q\to r)$ and
$p\to\Box q$ are one. However, for the sake of our informal discussion, what
we need is an informal notion of depth, counting the depth of the nested
implications appearing in the antecedents of the implications. This new limit
hopefully solves the second problem we encountered. For the first problem,
though, we need to observe that the real problem with the disjunction-like
connectives is not their positive occurrences but the mix of such occurrences
with the implication-like connectives. For instance, think about the formulas
$p\vee\neg p$ and $(p\to q)\vee(q\to p)$, where the disjunction-like
connectives are applied on the formulas with an implication-like connective
inside. Having this observation, it seems that if we confine the disjunction-
like connectives to some blocks that have no occurrence of the implication-
like connectives, then substituting the atoms of an acceptable formula with
these blocks may keep the formula unproblematic. Therefore, as the final
proposal, we define the class of all constructive formulas as the least class
of formulas containing the ones without any positive occurrence of
$\\{\vee,\Diamond\\}$ or any nested occurrence of $\\{\Box,\to\\}$ with depth
three or more, closed under the substitution by the formulas that only consist
of $\\{\wedge,\vee,\Diamond\\}$. Note that by excluding $\\{\Box,\to\\}$ from
the substituting formulas, we also avoid any increase in depth which has a
crucial role in our investigation. We will see that this weakening covers many
natural constructively acceptable axioms with positive occurrences of
disjunction-like connectives, while it is still constructively acceptable. To
justify the latter claim, we show that if we add any of these formulas to
$\mathbf{CK}$ as new axioms, if the result satisfies a mild technical
condition, the resulting system admits all Visser’s rules and specially enjoys
the disjunction property.

In the following, we see a more precise definition for constructive formulas.

######  Definition 3.1.

We define the following three sets of $\mathcal{L}$-formulas:

  * •

The set of _basic_ formulas is the smallest set containing the atomic formulas
and the constants $\top$ and $\bot$ and closed under
$\\{\wedge,\vee,\Diamond\\}$.

  * •

The set of _almost positive_ formulas is the smallest set containing the basic
formulas and closed under $\\{\wedge,\vee,\Box,\Diamond\\}$ and the
implications of the form $A\to B$, where $A$ is basic and $B$ is almost
positive.

  * •

The set of _constructive_ formulas is the smallest set containing the basic
formulas and closed under $\\{\wedge,\Box\\}$ and the implications of the form
$A\to B$, where $A$ is almost positive and $B$ is constructive.

A formula in the languages $\mathcal{L}_{\Box}$, $\mathcal{L}_{\Diamond}$ and
$\mathcal{L}_{p}$ is called basic, almost positive or constructive, if it is
basic, almost positive or constructive as a formula in the extended language
$\mathcal{L}$.

######  Remark 3.2.

Note that the basic formulas are exactly the ones used for the substitutions
in the opening discussion of Subsection 3.1. Another point is that it is
customary to call the formulas constructed from the atoms by the positive
operators $\\{\wedge,\vee,\Box,\Diamond\\}$, the positive formulas. Our almost
positive formulas deviate from this usual definition by allowing a very
limited form of implication, i.e., the ones with the basic antecedents.
Therefore, almost positive formulas provide a definition for the formulas that
avoid any nested application of the implication-like connectives. Finally,
notice that the constructive formulas are exactly the ones we motivated
before. First, by their structure, we see that they do not contain any
positive occurrence of the connectives $\\{\vee,\Diamond\\}$, except when the
occurrences are confined in the basic formulas. Second, the antecedent of any
implication in a constructive formula is almost positive which implies that
the depth of the nested implication-like connectives in a constructive formula
is at most two.

######  Example 3.3.

The following table provides some examples and non-examples for basic, almost
positive and constructive formulas

| is | is not
---|---|---
basic |  $p\wedge q$, $p\vee q$, $\Diamond^{n}p$ |  $\neg p$, $p\to q$, $\Box p$
almost positive |  $\neg p$, $(p\vee\neg p)$, $\Diamond^{m}\Box^{n}p$, $\Box^{m}\Diamond^{n}p$ |  $\neg\neg p$, $(p\to q)\to r$, $\Box p\to q$
constructive |  $\neg\neg p$, $(p\to q)\to r$, $\Box^{m}\Diamond^{n}p$ , $\Box(\Diamond p\vee q)$ |  $(p\vee\neg p)$, $\Diamond^{m+1}\Box^{n+1}p$

where $m,n\geq 0$. It is easy to see that the formulas $p$, $(p\wedge q)$,
$(p\vee q)$, $(p\to q)$, $\neg p$, $\Box p$, $\Diamond p$ as well as all the
basic formulas are both almost positive and constructive. For more
constructive formulas, see Table 1. To have some examples of the formulas that
are neither almost positive nor constructive, consider $((p\to q)\to r)\to s$
and $(\Box p\to q)\to r$.

###  3.2 Constructive Rules

In this subsection, we present our proposal for the promised constructive
rules and see some of their examples and non-examples. Then, in Subsection
3.3, to justify our proposal, we present a general form for the sequent-style
rules and show that the constructive rules are exactly the ones that are
equivalent to a constructive formula over $\mathbf{CK}$. This observation
provides a justification for our definition for the constructive rules and its
tightly chosen form.

######  Definition 3.4.

Let $I$ and $J$ be finite (possibly empty) index sets, $\Gamma$ and $\Delta$
multiset variables, $\overline{P},\overline{P_{i}}$ multisets of almost
positive formulas, $\overline{C},\overline{C_{j}}$ multisets of constructive
formulas, and $\overline{B_{i}}$ a multiset of basic formulas, for any $i\in
I$ and $j\in J$. A single-conclusion rule is called:

  * •

_left constructive_ , when it is of the form

$\\{\Gamma,\overline{B_{i}}\Rightarrow\overline{P_{i}}\\}_{i\in I}$
$\\{\Gamma,\overline{C_{j}}\Rightarrow\Delta\\}_{j\in J}$
$\Gamma,\overline{P}\Rightarrow\Delta$
---

and if $|J|>1$, then all the formulas in $\bigcup_{j\in J}(\overline{C_{j}})$
are basic. Note that by convention, we assume that even if $|J|=0$, the
multiset variable $\Delta$ appears in the succedent of the conclusion.

  * •

_right constructive_ , when it is of the form

$\\{\Gamma,\overline{B_{i}}\Rightarrow\overline{P_{i}}\\}_{i\in I}$
$\Gamma,\overline{P}\Rightarrow\overline{C}$
---

Note that as both types of the rules are single-conclusion, each of the
multisets $\overline{P_{i}},\overline{C}$, and $\Delta$ can have at most one
formula.

As a special case, an axiom is called _constructive_ if it is either of the
form $\Gamma,\overline{P}\Rightarrow\Delta$ or of the form
$\Gamma,\overline{P}\Rightarrow\overline{C}$.

######  Remark 3.5.

Here is a terminological remark. Note that the form we used for our left
constructive rules generalizes the usual form of the left rules in the single-
conclusion sequent-style systems. For instance, consider the left rules
$(L\to),(L\wedge)$ and $(L\vee)$ in the calculus $\mathbf{LJ}$. However, our
form is slightly more general, as in $\overline{P}$ in the antecedent of the
conclusion, we also allow the empty set or more than one formula to appear.
The form we use in our right constructive rules also generalizes the usual
form of the right rules such as $(R\to),(R\wedge)$ and $(R\vee)$. It is also
slightly more general, as it allows a multiset $\overline{P}$ in the
antecedent of the conclusion and the empty set in its succedent. One might
object that as the right rules have formulas both in the antecedent and
succedent of the conclusion, it is not reasonable to call them right, anymore.
However, in the presence of $\mathbf{CK}$, having formulas in the left hand
side in $\overline{P}$ is not a real extension, as one can safely change
$\overline{P}$ and $\overline{C}$ to $\bigwedge\overline{P}$ and
$\bigvee\overline{C}$, respectively and then move $\bigwedge\overline{P}$ to
the right, by $(R\to)$. Note that the formula
$\bigwedge\overline{P}\to\bigvee\overline{C}$ is still constructive. It is
also possible to reveres the changes. It is enough to use cut with the
$\mathbf{CK}$-provable sequent
$\bigwedge\overline{P}\to\bigvee\overline{C},\bigwedge\overline{P}\Rightarrow\bigvee\overline{C}$
and then cut with the $\mathbf{CK}$-provable sequents
$\overline{P}\Rightarrow\bigwedge\overline{P}$ and
$\bigvee\overline{C}\Rightarrow\overline{C}$. Therefore, one can argue that
the right constructive rule as introduced is still essentially a right rule.

######  Remark 3.6.

To avoid confusion, let us emphasize that if we accept a constructive rule in
a system, all of its substitutions are also allowed. However, it does not mean
that a substitution of a constructive rule is also constructive. For instance,
although the rule $(L\vee)$ is constructive, its substituted version

$\Gamma,p\Rightarrow\Delta$ $\Gamma,\neg p\Rightarrow\Delta$ $\Gamma,p\vee\neg
p\Rightarrow\Delta$
---

is not constructive, as the rule has two premises while $\neg p$ is not basic.

######  Definition 3.7.

Let
$\mathfrak{L}\in\\{\mathcal{L},\mathcal{L}_{\Box},\mathcal{L}_{\Diamond},\mathcal{L}_{p}\\}$
be a language. A rule $R$ over $\mathfrak{L}$ is called _constructive_ if it
is constructive as a rule over the extended language $\mathcal{L}$. A sequent
calculus over $\mathfrak{L}$ is called _constructive_ , when its axioms and
rules are all either constructive or

  * •

$(K_{\Box})$ or $(K_{\Diamond})$, if $\mathfrak{L}=\mathcal{L}$;

  * •

$(K_{\Box})$, if $\mathfrak{L}=\mathcal{L}_{\Box}$;

  * •

no other rules, if $\mathfrak{L}=\mathcal{L}_{\Diamond}$ or
$\mathfrak{L}=\mathcal{L}_{p}$.

$\Gamma\Rightarrow\Diamond\bot$ $\Gamma\Rightarrow\bot$ |  $\Gamma\Rightarrow\Box p$ $\Gamma\Rightarrow\Diamond p$
---|---
$\Gamma,\Diamond p\Rightarrow\Delta$ $\Gamma,\Diamond q\Rightarrow\Delta$ $\Gamma,\Diamond(p\vee q)\Rightarrow\Delta$ |  $\Gamma,\Box p\Rightarrow\Diamond p$
$\Gamma\Rightarrow\Box p$ $\Gamma\Rightarrow p$ |  $\Gamma\Rightarrow\Diamond\Diamond p$ $\Gamma\Rightarrow\Diamond p$
$\Gamma\Rightarrow\Diamond\Box p$ $\Gamma\Rightarrow p$ |  $\Gamma\Rightarrow\Diamond p$ $\Gamma\Rightarrow\Box\Diamond p$
$\Gamma\Rightarrow\Box^{n+1}p$ $\Gamma\Rightarrow\Box^{n}p$ |  $\Gamma\Rightarrow\Diamond^{m}p$ $\Gamma\Rightarrow\Diamond^{n}p$
$\\{\Gamma\Rightarrow\Box^{i}p\\}_{i=0}^{n}$ $\Gamma\Rightarrow\Box^{n+1}p$ |  $\Gamma\Rightarrow\Diamond^{k}\Box^{l}p$ $\Gamma\Rightarrow\Box^{m}\Diamond^{n}p$
$\Gamma,p\Rightarrow\Delta$ $\Gamma,\Box p\Rightarrow\Delta$ |  $\Gamma,\Box\bot\Rightarrow\Delta$ $\Gamma\Rightarrow\Diamond\top$
$\Gamma\Rightarrow\Diamond(p\wedge\Box q)$ $\Gamma\Rightarrow\Box(p\vee\Diamond q)$ |  $\Gamma\Rightarrow\Diamond\neg p$ $\Gamma\Rightarrow\neg\Box p$
$\\{\Gamma,\Diamond^{i}p\Rightarrow\Delta\\}_{i=0}^{n}$ $\Gamma,\Diamond^{n+1}p\Rightarrow\Delta$ |  $\Gamma\Rightarrow\Diamond\neg p$ $\Gamma,\Box p\Rightarrow\Delta$
$\\{\Gamma,\Diamond(p_{i}\wedge(p_{j}\vee\Diamond p_{j}))\Rightarrow\Delta\\}_{0\leq i\neq j\leq r}$ $\Gamma,\\{\Diamond p_{i}\\}_{i=0}^{r}\Rightarrow\Delta$ |  $\Gamma,p_{n}\Rightarrow\Delta$ $\Gamma,\Diamond(\Box p_{n}\wedge bd_{n})\Rightarrow\Delta$
$\Gamma\Rightarrow p$ $\Gamma\Rightarrow\Box(\Diamond p\to p)$ |  $\Gamma\Rightarrow\Diamond(\Box p\wedge q)$ $\Gamma\Rightarrow\Box(\Diamond p\vee q)$

Table 3: The numbers $n,m,l,k\geq 0$ and $r\geq 1$ are arbitrary natural
numbers. The formula $bd_{n}$ is defined recursively by $bd_{0}=\bot$, and
$bd_{n+1}=p_{n}\vee\Box(\Diamond\neg p_{n}\vee bd_{n})$.

######  Example 3.8.

The rules of Table 3 correspond to the axioms in Table 1. Some of them may
seem unfamiliar or even unnatural. However, as the presence of the cut rule in
the studied systems will be assumed, they are equivalent to the usual rules
used for the corresponding axioms. Moreover, notice that some of the rules in
Table 3 are equivalent. The point to mention the different versions is to
convey the different forms that a rule might have.
Now, referring to Example 3.3, we easily see that the rules of $\mathbf{LJ}$,
and the rules in Table 3 are all constructive. For instance, consider the
rules:

$\Gamma\Rightarrow p$ $\Gamma,p\Rightarrow\Delta$ $(cut)$ $\Gamma\Rightarrow\Delta$ |  $\Gamma,p\Rightarrow q$ $(R\to)$ $\Gamma\Rightarrow p\to q$
---|---

The cut rule is left constructive as $p$ is both almost positive and
constructive. The rules $(R\vee)$ and $(R\to)$ are right constructive as $p$
is basic, $q$ is almost positive and $p\to q$ and $p\vee q$ are both
constructive. To see a modal example, consider the following rule which
corresponds to the axiom $(ga_{klmn})$:

$\Gamma\Rightarrow\Diamond^{k}\Box^{l}p$
$\Gamma\Rightarrow\Box^{m}\Diamond^{n}p$
---

It is a right constructive rule as $\Diamond^{k}\Box^{l}p$ is almost positive
and $\Box^{m}\Diamond^{n}p$ is constructive. This implies that all the rules
in the third, fourth and fifth rows of Table 3 are also constructive, for they
are special cases of the rule we just mentioned. To have more complex
examples, consider:

$\Gamma\Rightarrow\Diamond(p\vee q)$ $\Gamma\Rightarrow\Diamond p\vee\Diamond q$ |  $\Gamma,\Diamond p\Rightarrow\Box q$ $\Gamma\Rightarrow\Box(p\to q)$
---|---

The left rule is a right constructive rule as $\Diamond(p\vee q)$ is almost
positive and $\Diamond p\vee\Diamond q$ is basic and hence constructive. The
right rule is also a right constructive rule as $\Diamond p$ is basic, $\Box
q$ is almost positive, and $\Box(p\to q)$ is a constructive formula. To have
an example that uses the full power of the definition of the basic formulas,
consider the rule:

$\\{\Gamma\Rightarrow\Diamond p_{i}\\}_{i=0}^{r}$
$\Gamma\Rightarrow\bigvee_{0\leq i\neq
j}^{r}\Diamond(p_{i}\wedge(p_{j}\vee\Diamond p_{j}))$
---

Despite its complicated form, the rule is also a right constructive rule as
the complex formula $\bigvee_{0\leq i\neq
j}^{r}\Diamond(p_{i}\wedge(p_{j}\vee\Diamond p_{j}))$ is basic and $\Diamond
p_{i}$ is almost positive.

######  Example 3.9.

To have some non-examples, consider the following rules:

$\Gamma\Rightarrow p\vee\neg p$ |  $\Gamma,p\Rightarrow\Delta$ $\Gamma,\neg p\Rightarrow\Delta$ $\Gamma\Rightarrow\Delta$
---|---

None of these rules are constructive. For instance, the leftmost rule is an
axiom, and to be a constructive axiom, the formula in the succedent of the
sequent must be a constructive formula. However, according to Definition 3.1
and as observed in Example 3.3, the formula $p\vee\neg p$ is not constructive.
For the other three, the reason is that the formula $\neg\neg p$ is not almost
positive and $\neg p$ is not basic as observed in Example 3.3. Another non-
example is

$\Gamma,\neg p\Rightarrow\bot$ $\Gamma,p\Rightarrow\Delta$
$\Gamma\Rightarrow\Delta$
---

Here, according to the side conditions in Definition 3.4, all the formulas in
the antecedent of $(\Gamma,\neg p\Rightarrow\bot)$ must be basic, which is not
the case, as $\neg p$ is not basic. Note that each of these rules implies an
equivalent version of the axiom of the excluded middle. (In the rightmost
rule, set $\Gamma=\\{\neg\neg p\\}$ and $\Delta=\\{p\\}$ to obtain $\neg\neg
p\Rightarrow p$). Hence, we see how the conditions in the definition of the
constructive rules are necessary to keep the system constructive.

To see some modal rules as the non-examples, first note that the rules
$(K_{\Box})$ and $(K_{\Diamond})$ are not constructive, as they change the
context $\Gamma$ to $\Box\Gamma$ and hence do not follow the enforced form. To
see some other types of non-examples, consider the following rules:

$\Gamma,\Box(\Box p\to q)\Rightarrow\Delta$ $\Gamma,\Box(\Box q\to p)\Rightarrow\Delta$ $(sc)$ $\Gamma\Rightarrow\Delta$ |  $\Gamma\Rightarrow\Box\Diamond p$ $(ma)$ $\Gamma\Rightarrow\Diamond\Box p$
---|---
$\Gamma\Rightarrow\Box(\Box p\to p)$ $(la)$ $\Gamma\Rightarrow\Box p$ |  $\Gamma\Rightarrow\neg\Box p$ $\Gamma\Rightarrow\Diamond\neg p$
---|---
$\Gamma\Rightarrow\Box\Diamond p$ $\Gamma\Rightarrow\Diamond p$ $(.1)$ $\Gamma\Rightarrow\Diamond\Box p\vee\Box p$ |  $\Gamma\Rightarrow\Diamond\top\vee\Box\bot$
---|---

None of these rules are constructive. The rule $(sc)$ is not constructive, as
otherwise, it must have been a left constructive rule, while it has two
premises, with $\Delta$ as the succedents, and the formulas $\Box(\Box p\to
q)$ and $\Box(\Box q\to p)$ in the antecedents are not basic. The rules $(ma)$
and $(la)$ are not constructive either, as otherwise, they must have been
right constructive rules, but the formulas $\Box(\Box p\to p)$ and
$\Diamond\Box p$ are not almost positive and constructive, respectively. The
other rules are not constructive, as the formula $\Box(\Box(p\to\Box p)\to p)$
is not almost positive and the formulas $\Diamond\neg p$, $\Diamond\Box
p\vee\Box p$ and $\Diamond\top\vee\Box\bot$ are not constructive. It is worth
mentioning that the rules $(ma)$, $(la)$ and $(grz)$ correspond to the
McKinsey axiom $\Box\Diamond p\to\Diamond\Box p$, the Löb axiom $\Box(\Box
p\to p)\to\Box p$, and the Grzegorczyk axiom $\Box(\Box(p\to\Box p)\to p)\to
p$, respectively. Note that none of these formulas are constructive.

###  3.3 General Rules and the Justification

To follow our strategy as explained in the opening discussion of Section 3,
let us first introduce a general form for the rules that we want to consider
and then select the ones that are equivalent to a constructive formula.

######  Definition 3.10.

Let $\mathfrak{R}$ be the set of all the rules in one of the forms:

$\\{\Gamma,\overline{\varphi}_{i}\Rightarrow\overline{\psi}_{i}\\}_{i\in I}$ $\\{\Gamma,\overline{\theta}_{j}\Rightarrow\Delta\\}_{j\in J}$ $\Gamma,\overline{\eta}\Rightarrow\Delta$ |  $\\{\Gamma,\overline{\varphi}_{i}\Rightarrow\overline{\psi}_{i}\\}_{i\in I}$ $\Gamma,\overline{\theta}\Rightarrow\overline{\eta}$
---|---

where $\Gamma$ and $\Delta$ are multiset variables, free to be substituted by
any multisets and $\overline{\varphi}_{i}$’s, $\overline{\psi}_{i}$’s,
$\overline{\theta}_{j}$’s, $\overline{\theta}$ and $\overline{\eta}$ are
multiset of formulas. We call any rule in the left form a _left_ rule and any
rule in the right form a _right_ rule.

These two forms capture a general common structure in the usual single-
conclusion rules covering all possible combinations of formulas and multiset
variables subject to two main restrictions. First, they must be single-
conclusion and hence in the succedent we do not allow to have both multisets
of formulas and $\Delta$. The second is the presence of the multiset variables
that are free for any multiset substitution. Note that they remain intact in
the rule application. These forms cover all the axioms and rules of the system
$\mathbf{LJ}$ including the cut rule. They also cover all possible axioms in
the form $\Gamma\Rightarrow\eta$. Note that in the presence of the cut rule,
many rules are equivalent to an axiom and hence the forms must be seen as
quite powerful and general. Having that said, we must also emphasize that
these forms unfortunately do not cover all possible interesting rules in the
literature. The reason is mostly the restriction on the context. For instance,
consider the following rules:

$\neg p\Rightarrow q\vee r$ $(KP)$ $\Rightarrow(\neg p\to q)\vee(\neg p\to r)$ |  $\Gamma\Rightarrow p$ $(K_{\Box})$ $\Box\Gamma\Rightarrow\Box p$
---|---

In $(KP)$, as typical for non-derivable admissible rules, the multiset
variable $\Gamma$ is missing. In $(RS4)$, there is a restriction on the form
of the antecedents of the meta-sequents (only boxed formulas are allowed). And
in $(K_{\Box})$, the multiset variable changes from $\Gamma$ in the premise to
$\Box\Gamma$ in the conclusion.

Having the forms fixed, in the second step (the following theorem), we prove
that over $\mathbf{CK}$, any rule $R\in\mathfrak{R}$ is equivalent to a
formula, denoted by $Ax_{R}$, and $R$ is constructive iff $Ax_{R}$ is
constructive. Therefore, we can argue that the constructive rules are all
constructively acceptable and as the forms of the rules in $\mathfrak{R}$ are
chosen to be quite general, the constructive rules are also sufficiently
general to capture the constructively acceptable rules.

######  Theorem 3.11.

For any rule $R\in\mathfrak{R}$, there is a formula $Ax_{R}$ such that:

  * $(i)$

$\mathbf{LJ}+R$ feasibly proves $(\Rightarrow Ax_{R})$.

  * $(ii)$

$\mathbf{LJ}+Ax_{R}$ feasibly proves the rule $R$.

Moreover, $R$ is constructive if and only if $Ax_{R}$ is a constructive
formula.

###### Proof.

For any right rule $R\in\mathfrak{R}$

$\\{\Gamma,\overline{\varphi}_{i}\Rightarrow\overline{\psi}_{i}\\}_{i\in I}$
$\Gamma,\overline{\theta}\Rightarrow\overline{\eta}$
---

define $Ax_{R}$ as $[\bigwedge_{i\in
I}[\bigwedge\overline{\varphi}_{i}\to\bigvee\overline{\psi}_{i}]\wedge\bigwedge\overline{\theta}]\to\bigvee\overline{\eta}$
and for any left rule $R\in\mathfrak{R}$

$\\{\Gamma,\overline{\varphi}_{i}\Rightarrow\overline{\psi}_{i}\\}_{i\in I}$
$\\{\Gamma,\overline{\theta}_{j}\Rightarrow\Delta\\}_{j\in J}$
$\Gamma,\overline{\eta}\Rightarrow\Delta$
---

define $Ax_{R}$ as $\bigwedge_{i\in
I}(\bigwedge\overline{\varphi}_{i}\to\bigvee\overline{\psi}_{i})\wedge\bigwedge\overline{\eta}\to\bigvee_{j\in
J}\bigwedge\overline{\theta}_{j}$. We only prove the claim for left rules. The
case for right rules is similar.

For $(i)$, we first show that $(\Rightarrow Ax_{R})$ is provable in
$\mathbf{LJ}+R$. The algorithm is as follows. Set
$\Gamma=\\{\bigwedge\overline{\varphi}_{i}\to\bigvee\overline{\psi}_{i}\\}_{i\in
I}$ and $\Delta=\bigvee_{j\in J}(\bigwedge\overline{\theta}_{j})$. Therefore,
we have
$\mathbf{LJ}\vdash\Gamma,\overline{\varphi}_{i}\Rightarrow\bigvee\overline{\psi}_{i}$
and $\mathbf{LJ}\vdash\Gamma,\overline{\theta}_{j}\Rightarrow\Delta$. By
applying the rule $R$, we reach
$\mathbf{LJ}+R\vdash\\{\bigwedge\overline{\varphi}_{i}\to\bigvee\overline{\psi}_{i}\\}_{i\in
I},\overline{\eta}\Rightarrow\bigvee_{j\in
J}(\bigwedge\overline{\theta}_{j})$. Then, by using the rules $(L\wedge)$,
$(Lc)$ and $(R\to)$ in $\mathbf{LJ}$, we get $\mathbf{LJ}+R\vdash(\Rightarrow
Ax_{R})$. The feasibility of the algorithm is clear.

For $(ii)$, denoting $\mathbf{LJ}+Ax_{R}$ by $H$, we have to provide a
polynomial time algorithm $f_{R}$ that reads the sequents in the multiset
$\\{\Gamma,\overline{\varphi}_{i}\Rightarrow\overline{\psi}_{i}\\}_{i\in
I}\cup\\{\Gamma,\overline{\theta}_{j}\Rightarrow\Delta\\}_{j\in J}$ and
$\Gamma,\overline{\eta}\Rightarrow\Delta$ and provides an $H$-proof witnessing

$\\{\Gamma,\overline{\varphi}_{i}\Rightarrow\overline{\psi}_{i}\\}_{i\in
I},\\{\Gamma,\overline{\theta}_{j}\Rightarrow\Delta\\}_{j\in
J}\vdash_{H}\Gamma,\overline{\eta}\Rightarrow\Delta$.

We only present the algorithm $f_{R}$. The fact that it is polynomial time is
trivial. First, observe that by a simple application of the cut rule on the
axiom $(\Rightarrow Ax_{R})$ and the $\mathbf{LJ}$-provable sequent

$Ax_{R},[\bigwedge_{i\in
I}(\bigwedge\overline{\varphi}_{i}\to\bigvee\overline{\psi}_{i})\wedge\bigwedge\overline{\eta}]\Rightarrow\bigvee_{j\in
J}(\bigwedge\overline{\theta}_{j}).$

we have

$H\vdash[\bigwedge_{i\in
I}(\bigwedge\overline{\varphi}_{i}\to\bigvee\overline{\psi}_{i})\wedge\bigwedge\overline{\eta}]\Rightarrow\bigvee_{j\in
J}(\bigwedge\overline{\theta}_{j})$

Then, notice that

$\\{\Gamma,\overline{\varphi}_{i}\Rightarrow\overline{\psi}_{i}\\}_{i\in
I}\vdash_{H}\Gamma\Rightarrow\bigwedge_{i\in
I}(\bigwedge\overline{\varphi}_{i}\to\bigvee\overline{\psi}_{i})$

and hence

$\\{\Gamma,\overline{\varphi}_{i}\Rightarrow\overline{\psi}_{i}\\}_{i\in
I}\vdash_{H}\Gamma,\overline{\eta}\Rightarrow\bigwedge_{i\in
I}(\bigwedge\overline{\varphi}_{i}\to\bigvee\overline{\psi}_{i})\wedge\bigwedge\overline{\eta}$.

By using the cut rule on the above sequent and the aforementioned $H$-provable
sequent $[\bigwedge_{i\in
I}(\bigwedge\overline{\varphi}_{i}\to\bigvee\overline{\psi}_{i})\wedge\bigwedge\overline{\eta}]\Rightarrow\bigvee_{j\in
J}(\bigwedge\overline{\theta}_{j})$, we have

$\\{\Gamma,\overline{\varphi}_{i}\Rightarrow\overline{\psi}_{i}\\}_{i\in
I}\vdash_{H}\Gamma,\overline{\eta}\Rightarrow\bigvee_{j\in
J}(\bigwedge\overline{\theta}_{j})$ (1)

On the other hand, we have

$\\{\Gamma,\overline{\theta}_{j}\Rightarrow\Delta\\}_{j\in
J}\vdash_{H}\Gamma,\bigvee_{j\in
J}(\bigwedge\overline{\theta}_{j})\Rightarrow\Delta$ (2)

Now, using the cut rule on (1) and (2) and several weakening rules we get

$\\{\Gamma,\overline{\varphi}_{i}\Rightarrow\overline{\psi}_{i}\\}_{i\in
I},\\{\Gamma,\overline{\theta}_{j}\Rightarrow\Delta\\}_{j\in
J}\vdash_{H}\Gamma,\overline{\eta}\Rightarrow\Delta$.

The above process of using some simple $H$-provable facts with their simple
$H$-proofs and then applying some cut rules clearly takes polynomial time in
the sum of the sizes of the sequents
$\\{\Gamma,\overline{\varphi}_{i}\Rightarrow\overline{\psi}_{i}\\}_{i\in
I}\cup\\{\Gamma,\overline{\theta}_{j}\Rightarrow\Delta\\}_{j\in J}$ and
$\Gamma,\overline{\eta}\Rightarrow\Delta$. The presence of the cut rule,
assumed to be a primitive rule in $\mathbf{LJ}$, is crucial to provide the
required short proofs and make $f_{R}$ feasible.

As the last part of the proof, we show that $R$ is constructive iff $Ax_{R}$
is constructive. For any left rule $R\in\mathfrak{R}$

$\\{\Gamma,\overline{\varphi}_{i}\Rightarrow\overline{\psi}_{i}\\}_{i\in I}$
$\\{\Gamma,\overline{\theta}_{j}\Rightarrow\Delta\\}_{j\in J}$
$\Gamma,\overline{\eta}\Rightarrow\Delta$
---

the formula $Ax_{R}$ defined as

$[\bigwedge_{i\in
I}(\bigwedge\overline{\varphi}_{i}\to\bigvee\overline{\psi}_{i})\wedge\bigwedge\overline{\eta}]\to\bigvee_{j\in
J}(\bigwedge\overline{\theta}_{j})$

is constructive iff the antecedent, i.e., $\bigwedge_{i\in
I}(\bigwedge\overline{\varphi}_{i}\to\bigvee\overline{\psi}_{i})\wedge\bigwedge\overline{\eta}$,
is almost positive and the succedent, i.e., $\bigvee_{j\in
J}(\bigwedge\overline{\theta}_{j})$ is constructive. To enforce that, there
are several cases to consider. For the succedent:

  * •

If $|J|>1$, then all the formulas in $\overline{\theta}_{j}$ must be basic as
the disjunction of at least two formulas is constructive iff all of them are
basic.

  * •

If $|J|=1$, then all the formulas in any of $\overline{\theta}_{j}$’s must be
constructive.

  * •

If $|J|=0$, then $\bigvee_{j\in J}(\bigwedge\overline{\theta}_{j})=\bot$,
hence it is constructive automatically.

For the antecedent of the formula,

  * •

If $|I|=0$, then the antecedent of the formula is defined as $\top$, which is
an almost positive formula automatically.

  * •

If $|I|\geq 1$, then all the formulas in $\overline{\varphi}_{i}$’s must be
basic while all the formulas in $\overline{\psi}_{i}$’s and $\overline{\eta}$
must be almost positive as this is the only way to make the antecedent almost
positive.

These conditions altogether are the ones to make the rule constructive.
For any right rule $R\in\mathfrak{R}$ of the form

$\\{\Gamma,\overline{\varphi}_{i}\Rightarrow\overline{\psi}_{i}\\}_{i\in I}$
$\Gamma,\overline{\theta}\Rightarrow\overline{\eta}$
---

the formula $Ax_{R}$ defined as $[\bigwedge_{i\in
I}[\bigwedge\overline{\varphi}_{i}\to\bigvee\overline{\psi}_{i}]\wedge\bigwedge\overline{\theta}]\to\bigvee\overline{\eta}$
is constructive iff $[\bigwedge_{i\in
I}[\bigwedge\overline{\varphi}_{i}\to\bigvee\overline{\psi}_{i}]$ and
$\bigwedge\overline{\theta}$ are almost positive and $\bigvee\overline{\eta}$
is constructive. This means that all
$\bigwedge\overline{\varphi}_{i}\to\bigvee\overline{\psi}_{i}$’s and all
formulas in $\overline{\theta}$ are almost positive and any formula in
$\overline{\eta}$ is constructive. Notice that as the rule is single-
conclusion, the disjunction in $\bigvee\overline{\eta}$ is over either one or
zero formulas and hence is not problematic. Finally,
$\bigwedge\overline{\varphi}_{i}\to\bigvee\overline{\psi}_{i}$ is almost
positive iff all the elements in $\bar{\varphi}_{i}$’s and
$\overline{\psi}_{i}$’s are basic and almost positive, respectively. These
conditions altogether are the ones to make the rule constructive. ∎

######  Corollary 3.12.

Let
$\mathfrak{L}\in\\{\mathcal{L},\mathcal{L}_{\Box},\mathcal{L}_{\Diamond},\mathcal{L}_{p}\\}$
be a language, $R\in\mathfrak{R}$ a rule over $\mathfrak{L}$ and $G$ a sequent
calculus over $\mathfrak{L}$ such that $G$ feasibly proves all the rules in
$\mathbf{LJ}$. Then, $R$ is provable in $G$ iff it is feasibly provable in
$G$.

###### Proof.

We prove the claim for $\mathcal{L}$, the others are similar. One direction is
clear. For the other, assume that $R$ is provable in $G$. As $G$ proves all
the rules in $\mathbf{LJ}$ and $\mathbf{LJ}+R$ proves $(\,\Rightarrow Ax_{R})$
by Theorem 3.11, then $G$ proves $(\,\Rightarrow Ax_{R})$. We claim that $G$
also feasibly proves $(\,\Rightarrow Ax_{R})$. Take a proof of $(\,\Rightarrow
Ax_{R})$ in $G$ and call it $\rho$. Then, for any instance of $(\,\Rightarrow
Ax_{R})$ resulting from the substitution $\sigma$, the application $\sigma$ on
$\rho$, denoted by $\sigma(\rho)$, is a proof for that instance. As $\rho$ is
fixed, clearly the process of reading the instance of $(\Rightarrow Ax_{R})$
and providing the $G$-proof $\sigma(\rho)$ is feasible. Hence, $G$ feasibly
proves $(\,\Rightarrow Ax_{R})$. By Theorem 3.11, $\mathbf{LJ}+Ax_{R}$
feasibly proves $R$ and as $G$ feasibly proves all the rules in
$\mathbf{LJ}+Ax_{R}$, by Lemma 2.12 we have $G$ pd-simulates
$\mathbf{LJ}+Ax_{R}$. Finally, by Lemma 2.12 part 1, $R$ is feasibly provable
in $G$. ∎

######  Corollary 3.13.

Let $G$ be a strong constructive sequent calculus over $\mathcal{L}$. Then,
there exists a finite set of constructive $\mathcal{L}$-formulas $\mathcal{C}$
such that $G$ is pd-equivalent to $\mathbf{CK}+\mathcal{C}$. A similar claim
holds, replacing the pair $(\mathcal{L},\mathbf{CK})$ by
$(\mathcal{L}_{\Box},\mathbf{CK}_{\Box})$,
$(\mathcal{L}_{\Diamond},\mathbf{BLL})$, or $(\mathcal{L}_{p},\mathbf{LJ})$.

###### Proof.

We only prove the case for $(\mathcal{L},\mathbf{CK})$. The proof for the
fragments is similar. Define $\mathcal{R}$ as the set of the constructive
rules of $G$ and set $\mathcal{C}=\\{Ax_{R}\mid R\in\mathcal{R}\\}$. As $G$ is
strong, it feasibly proves all the rules in $\mathbf{CK}$ and specifically all
the rules in $\mathbf{LJ}$. Hence, by Lemma 2.12 $G$ pd-simulates
$\mathbf{LJ}$. As $R$ is in $G$, by Remark 2.9, $G$ feasibly proves $R$. By
Theorem 3.11, $\mathbf{LJ}+R$ feasibly proves $(\Rightarrow Ax_{R})$.
Therefore, by Lemma 2.12 part 1, $G$ also feasibly proves $(\,\Rightarrow
Ax_{R})$. Hence, again by Lemma 2.12, $G$ pd-simulates
$\mathbf{CK}+\mathcal{C}$. For the other direction, notice that
$\mathbf{CK}+\mathcal{C}$ feasibly proves the rule $R\in\mathcal{R}$, by
Theorem 3.11 and Lemma 2.12. For the other rules of $G$, as they can only be
$(K_{\Box})$ or $(K_{\Diamond})$, they are feasibly provable in
$\mathbf{CK}+\mathcal{C}$. Therefore, by Lemma 2.12, $\mathbf{CK}+\mathcal{C}$
pd-simulates $G$. ∎

##  4 Feasible Visser-Harrop Property

In this section, we prove the main result of the paper stating that any strong
constructive sequent calculus over $\mathcal{L}$, satisfying a modest
technical condition, feasibly admits a generalization of Visser’s rules. For
the moment, let us ignore the generalization. By the feasible admissibility of
Visser’s rule, we mean there is a polynomial time algorithm that reads a
$G$-proof $\pi$ for

$\\{A_{i}\to B_{i}\\}_{i\in I}\Rightarrow C\vee D,$

where $I$ is an index set and outputs a $G$-proof for one of the following
sequents

$\\{A_{i}\to B_{i}\\}_{i\in I}\Rightarrow C\;$ or |  $\\{A_{i}\to B_{i}\\}_{i\in I}\Rightarrow D\;$ or |  $\\{A_{i}\to B_{i}\\}_{i\in I}\Rightarrow A_{i}$,
---|---|---

for some $i\in I$. Using Corollary 3.13, it is enough to prove the claim for
the systems $G=\mathbf{CK}+\mathcal{C}$, where $\mathcal{C}$ is a finite set
of constructive formulas. To prove this claim, we need to develop the
following two ingredients. First, a translation function to transform the
provable sequent $\\{A_{i}\to B_{i}\\}_{i\in I}\Rightarrow C\vee D$ to a
simpler provable sequent $\Sigma,\\{\neg p_{i}\\}_{i\in I}\Rightarrow q\vee
r$, where $p_{i}$’s, $q$ and $r$ are all atomic formulas and $\Sigma$ consists
of some sort of simple formulas. The second ingredient is a proof theoretical
version of the usual unit propagation algorithm to read the result of the
first part, i.e., $\Sigma,\\{\neg p_{i}\\}_{i\in I}\Rightarrow q\vee r$ and
find a proof for either $\Sigma,\\{\neg p_{i}\\}_{i\in I}\Rightarrow q$ or
$\Sigma,\\{\neg p_{i}\\}_{i\in I}\Rightarrow q$ or $\Sigma,\\{\neg
p_{i}\\}_{i\in I}\Rightarrow p_{i}$, for some $i\in I$. Finally, by applying
the converse of the transformation of the first part, we can provide a proof
for either $\\{A_{i}\to B_{i}\\}_{i\in I}\Rightarrow C$ or $\\{A_{i}\to
B_{i}\\}_{i\in I}\Rightarrow D$ or $\\{A_{i}\to B_{i}\\}_{i\in I}\Rightarrow
A_{i}$, for some $i\in I$. We will cover the first ingredient in Subsection
4.1 and Subsection 4.2 and the second ingredient will be explained in
Subsection 4.3 and Subsection 4.4. Finally, in Subsection 4.5, we will combine
these two ingredients to prove the theorem.

###  4.1 The Translations and their Properties

In this subsection, we introduce the two translations we mentioned before and
investigate their effects on basic, almost positive and constructive formulas.

######  Definition 4.1.

For any formula $\varphi\in\mathcal{L}$, set $\langle\varphi\rangle$ as a
fresh atomic formula, called an _angled atom_ , and add it to $\mathcal{L}$.
The new language is denoted by $\mathcal{L}^{+}$.

Note that an _atom_ in $\mathcal{L}^{+}$ is either an atom in $\mathcal{L}$ or
an angled atom, and these possibilities do not intersect. Moreover, notice
that in computing the size of the atom $\langle\varphi\rangle$, we consider
all the symbols in $\langle\varphi\rangle$. Hence,
$|\langle\varphi\rangle|=|\varphi|+2$.

######  Definition 4.2.

The translation function $t:\mathcal{L}\to\mathcal{L}^{+}$ is defined as:

  * $\bullet$

$\bot^{t}=\bot$, $\top^{t}=\langle\top\rangle$, and $p^{t}=\langle p\rangle$,
for any atomic formula $p$;

  * $\bullet$

$(A\circ B)^{t}=(A^{t}\circ B^{t})\wedge\langle A\circ B\rangle$, for any
$\circ\in\\{\wedge,\vee,\to\\}$;

  * $\bullet$

$(\bigcirc A)^{t}=(\bigcirc A^{t})\wedge\langle\bigcirc A\rangle$, for any
$\bigcirc\in\\{\Box,\Diamond\\}$.

For a multiset $\Gamma$, by $\Gamma^{t}$, we mean the multiset consisting of
the translation of all the elements of $\Gamma$, i.e.,
$\Gamma^{t}=\\{\gamma^{t}\mid\gamma\in\Gamma\\}$.

######  Definition 4.3.

The _standard_ substitution $s:{\mathcal{L}}^{+}\to\mathcal{L}$ is defined as:

  * $\bullet$

$\langle\varphi\rangle^{s}=\varphi$, $p^{s}=p$, for any formula
$\varphi\in\mathcal{L}$ and $p$ is an atom in $\mathcal{L}$, $\bot$ or $\top$;

  * $\bullet$

$(A\circ B)^{s}=A^{s}\circ B^{s}$, for any $\circ\in\\{\wedge,\vee,\to\\}$;

  * $\bullet$

$(\bigcirc A)^{s}=\bigcirc A^{s}$, for any $\bigcirc\in\\{\Box,\Diamond\\}$.

Define $\Gamma^{s}$ in the usual way, i.e.,
$\Gamma^{s}=\\{\gamma^{s}\mid\gamma\in\Gamma\\}$.

The standard substitution $s:{\mathcal{L}}^{+}\to\mathcal{L}$ is the map that
substitutes the angled atom $\langle\varphi\rangle$ by $\varphi$ and leaves
the non-angled atomic formulas intact. By induction, it is easy to see that
for any formula $A(p_{1},\cdots,p_{n})\in\mathcal{L}$, we have
$A(\langle\varphi_{1}\rangle,\dots,\langle\varphi_{n}\rangle)^{s}=A(\varphi_{1},\dots,\varphi_{n})$.
The substitution $s$ can be interpreted as a translation function, mapping
$\mathcal{L}^{+}$ into $\mathcal{L}$, cancelling all the changes made by the
translation $t$ and tracing back the original formula.

######  Lemma 4.4.

The functions $t$ and $s$ are polynomial time computable.

###### Proof.

First, we prove the claim for the function $t$. Consider the canonical
recursive algorithm that computes $A^{t}$ and denote the time of this
algorithm by $T_{t}(A)$. We show that $T_{t}(A)\leq O(|A|^{2})$, using the
following inequalities:

  * •

$T_{t}(A)\leq O(1)$, for the atomic $A$ (including $\bot$ and $\top$),

  * •

$T_{t}(B\circ C)\leq T_{t}(B)+T_{t}(C)+|B|+|C|+O(1)$,

  * •

$T_{t}(\bigcirc B)\leq T_{t}(B)+|B|+O(1)$.

for any $\circ\in\\{\wedge,\vee,\to\\}$ and $\bigcirc\in\\{\Box,\Diamond\\}$.
The atomic case is obvious. For the second case, to compute $(B\circ C)^{t}$
we have to first compute $B^{t}$ and $C^{t}$, put them together separated by
$\circ$ and finally add $\langle B\circ C\rangle$ to its end, separated by a
$\wedge$. Therefore, the bound is clear. The argument for the third case is
similar. By these inequalities and induction on the structure of $A$, it is
easy to see that $T_{t}(A)\leq O(|A|^{2})$. The case for the function $s$ is
similar and in fact easier. Consider the canonical recursive algorithm that
computes $A^{s}$ by first implementing the substitutions for the atoms and
then mimicking the structure of $A$. Denoting the time of this algorithm by
$T_{s}(A)$ and using a similar type of inequalities as before, we get
$T_{s}(A)\leq O(|A|^{2})$. ∎

######  Lemma 4.5.

$\mathbf{CK}\vdash A^{t}\Rightarrow\langle A\rangle$, for any formula
$A\in\mathcal{L}$.

###### Proof.

The case where $A$ is atomic, $\bot$, or $\top$ is trivial, as $A^{t}=\langle
A\rangle$ or $A^{t}=\bot$. If $A$ is of the form $B\circ C$ or $\bigcirc B$,
where $\circ\in\\{\wedge,\vee,\to\\}$ or $\bigcirc\in\\{\Box,\Diamond\\}$,
then by Definition 4.2, we have $(B\circ C)^{t}=(B^{t}\circ
C^{t})\wedge\langle B\circ C\rangle=(B^{t}\circ C^{t})\wedge\langle A\rangle$
and $(\bigcirc B)^{t}=\bigcirc B^{t}\wedge\langle\bigcirc B\rangle=\bigcirc
B^{t}\wedge\langle A\rangle$. In either case, the proof is clear. ∎

Recall that an atom $p\in\mathcal{L}^{+}$ is either an atomic formula in the
original language $\mathcal{L}$ or a new added angled atom.

######  Definition 4.6.

The set of _implicational Horn_ formulas is the smallest set of
$\mathcal{L}^{+}$-formulas containing $\bot$, atomic formulas, and closed
under implications of the form $\bigwedge Q\to r$, where
$Q=\\{q_{1},\dots,q_{n}\\}\subseteq\mathcal{L}^{+}$ is a non-empty multiset of
atoms and $r$ is either $\bot$ or an atom in $\mathcal{L}^{+}$. The set of
_modal Horn_ formulas is the smallest set of $\mathcal{L}^{+}$-formulas
containing $\bot$, atomic formulas, and closed under $\Box$ and implications
of the form $A\to B$, where $A$ is of the form
$\bigwedge_{i=1}^{k}\Diamond^{n_{i}}p_{i}$ for some $k\geq 1$ and $n_{i}\geq
0$ and $B$ is a modal Horn formula.

######  Remark 4.7.

Here are two remarks. First, as mentioned in Preliminaries, by
$\Diamond^{0}p$, we mean $p$. Therefore, it is easy to see that any
implicational Horn formula is also a modal Horn formula. Second, in the
literature usually Horn formulas are defined as formulas in the conjunctive
normal form (CNF) such that each conjunct contains at most one positive
literal. In the classical logic, our implicational Horn formulas are
equivalent to Horn formulas defined as CNF’s. However, this is not generally
the case for non-classical logics.

Our first aim, as it usually happens in translations, is to show that $t$
preserves the provability in $\mathbf{CK}+\mathcal{C}$, for any finite set
$\mathcal{C}$ of constructive formulas. Unfortunately, due to the addition of
the new atoms and their use in the translation, the preservation in general
does not hold. However, a slightly weaker form is true if we see the sequents
up to some “harmless” modal Horn formulas in the antecedents. More precisely,
if $\Gamma\Rightarrow\Delta$ is provable in $\mathbf{CK}+\mathcal{C}$, then
there is a multiset $\Sigma$ of modal Horn formulas such that
$\Sigma,\Gamma^{t}\Rightarrow\Delta^{t}$ is also provable in
$\mathbf{CK}+\mathcal{C}$, while the formulas in $\Sigma$ are harmless in the
sense that $\mathbf{CK}+\mathcal{C}\vdash\,\Rightarrow\bigwedge\Sigma^{s}$.
Roughly speaking, the translation preserves the provability, up to the modal
Horn formulas that $s$ sees as $(\mathbf{CK}+\mathcal{C})$-provable. To prove
this property, we need a machinery to commute the translation $t$ with the
constructive formulas, simply because we need to show that the translation of
an instance of an axiom is an instance of the axiom itself. The most desirable
such commutation would be the provability of both
$A(\overline{\varphi})^{t}\Rightarrow A(\overline{\varphi^{t}})$ and
$A(\overline{\varphi^{t}})\Rightarrow A(\overline{\varphi})^{t}$ in
$\mathbf{CK}$, for any constructive formula $A(\overline{p})$ and any formulas
$\overline{\varphi}$. Unfortunately, such a situation rarely takes place. To
solve the issue, again adding a harmless multiset $\Sigma^{\prime}$ of modal
Horn formulas helps. In fact, we show that for a basic, almost positive or
constructive formula $A(\overline{p})$ either
$\Sigma^{\prime},A(\overline{\varphi})^{t}\Rightarrow
A(\overline{\varphi^{t}})$ or
$\Sigma^{\prime},A(\overline{\varphi^{t}})\Rightarrow
A(\overline{\varphi})^{t}$ or both are provable in $\mathbf{CK}$. For basic
formulas $A(\overline{p})$, both directions are provable. However, for almost
positive and constructive formulas, only one direction can be proved, and in
the case of constructive formulas, even an additional formula is needed to
make the sequent provable in $\mathbf{CK}$. The following theorem is devoted
to these commutations. Note that although our main goal is the commutation
with the constructive formulas, we also need to address the other two families
as the steps to reach our goal.

######  Theorem 4.8.

We have the following commutations.

  * $(i)$

For any basic formula $A(\overline{p})\in\mathcal{L}$ and formulas
$\overline{\varphi}\in\mathcal{L}^{+}$, there is a multiset of modal Horn
formulas $\Phi_{A,\overline{\varphi}}$ constructed from angled atoms such that

$\mathbf{CK}\vdash\Phi_{A,\overline{\varphi}},(A(\overline{\varphi}))^{t}\Rightarrow
A(\overline{\varphi^{t}})\quad\text{and}\quad\mathbf{CK}\vdash\Phi_{A,\overline{\varphi}},A(\overline{\varphi^{t}})\Rightarrow(A(\overline{\varphi}))^{t}.$

  * $(ii)$

For any almost positive formula $A(\overline{p})\in\mathcal{L}$ and formulas
$\overline{\varphi}\in\mathcal{L}^{+}$, there is a multiset of modal Horn
formulas $\Pi_{A,\overline{\varphi}}$ constructed from angled atoms such that

$\mathbf{CK}\vdash\Pi_{A,\overline{\varphi}},(A(\overline{\varphi}))^{t}\Rightarrow
A(\overline{\varphi^{t}}).$

  * $(iii)$

For any constructive formula $A(\overline{p})\in\mathcal{L}$ and formulas
$\overline{\varphi}\in\mathcal{L}^{+}$, there is a multiset of modal Horn
formulas $\Upsilon_{A,\overline{\varphi}}$ constructed from angled atoms such
that

$\mathbf{CK}\vdash\Upsilon_{A,\overline{\varphi}},\langle
A(\overline{\varphi})\rangle,A(\overline{\varphi^{t}})\Rightarrow(A(\overline{\varphi}))^{t}.$

For any $\Theta\in\\{\Phi,\Pi,\Upsilon\\}$ and formulas
$A(\overline{p})\in\mathcal{L}$ and $\overline{\varphi}\in\mathcal{L}^{+}$,
there is a proof $\sigma_{\Theta,A,\overline{\varphi}}$ such that
$\mathbf{CK}\vdash^{\sigma_{\Theta,A,\overline{\varphi}}}(\,\Rightarrow\bigwedge\Theta_{A,\overline{\varphi}}^{s})$,
where $s$ is the standard substitution. Moreover, the processes of finding
$\Theta_{A,\overline{\varphi}}$ and $\sigma_{\Theta,A,\overline{\varphi}}$ are
polynomial time computable in the inputs $A(\overline{p})$ and
$\overline{\varphi}$.

###### Proof.

We first provide $\Theta_{A,\overline{\varphi}}$ and
$\sigma_{\Theta,A,\overline{\varphi}}$ in each case, ignoring the complexity
issues altogether. Then, we will address the feasibility of the algorithms in
the last part of the proof.

For $(i)$, we use recursion on the structure of the basic formula
$A(\overline{p})$ to define $\Phi_{A,\overline{\varphi}}$ and
$\sigma_{\Phi,A,\overline{\varphi}}$. If $A(\overline{p})$ is either an atom
or $\bot$, for any formulas $\overline{\varphi}$, we take
$\Phi_{A,\overline{\varphi}}$ to be the empty set. Therefore, both sequents
are trivially provable in $\mathbf{CK}$. Moreover, since $\bigwedge\emptyset$
is defined as $\top$, the sequent
$(\,\Rightarrow\bigwedge\Phi_{A,\overline{\varphi}}^{s})$ is an axiom an hence
provable in $\mathbf{CK}$. Define the proof
$\sigma_{\Phi,A,\overline{\varphi}}$ as $(\Rightarrow\top)$. If
$A(\overline{p})=\top$, we take $\Phi_{A,\overline{\varphi}}$ to be
$\\{\langle\top\rangle\\}$. The sequents in this case are
$\langle\top\rangle,\langle\top\rangle\Rightarrow\top$ and
$\langle\top\rangle,\top\Rightarrow\langle\top\rangle$, both provable in
$\mathbf{CK}$. Moreover, $\bigwedge\Phi_{A,\overline{\varphi}}^{s}$ is equal
to $\top$ and hence $(\,\Rightarrow\bigwedge\Phi_{A,\overline{\varphi}}^{s})$
is an instance of an axiom an provable in $\mathbf{CK}$. Define the proof
$\sigma_{\Phi,A,\overline{\varphi}}$ as this axiom.
For $A(\overline{p})=B(\overline{p})\wedge C(\overline{p})$, by Definition
4.2,
$(A(\overline{\varphi}))^{t}=(B(\overline{\varphi}))^{t}\wedge(C(\overline{\varphi}))^{t}\wedge\langle
B(\overline{\varphi})\wedge C(\overline{\varphi})\rangle$. By recursion, there
are multisets $\Phi_{B,\overline{\varphi}}$ and $\Phi_{C,\overline{\varphi}}$
such that

$\Phi_{B,\overline{\varphi}},(B(\overline{\varphi}))^{t}\Rightarrow
B(\overline{\varphi^{t}})\quad(1)\quad,\quad\Phi_{B,\overline{\varphi}},B(\overline{\varphi^{t}})\Rightarrow(B(\overline{\varphi}))^{t}\quad(2),$

$\Phi_{C,\overline{\varphi}},(C(\overline{\varphi}))^{t}\Rightarrow
C(\overline{\varphi^{t}})\quad(3)\quad,\quad\Phi_{C,\overline{\varphi}},C(\overline{\varphi^{t}})\Rightarrow(C(\overline{\varphi}))^{t}\quad(4),$

hold in $\mathbf{CK}$. Define $F_{\Phi,A,\overline{\varphi}}=\big{(}\langle
B(\overline{\varphi})\rangle\wedge\langle
C(\overline{\varphi})\rangle\big{)}\to\langle B(\overline{\varphi})\wedge
C(\overline{\varphi})\rangle$ and

$\Phi_{A,\overline{\varphi}}=\Phi_{B,\overline{\varphi}}\cup\Phi_{C,\overline{\varphi}}\cup\\{F_{\Phi,A,\overline{\varphi}}\\}$

Note that $\Phi_{A,\overline{\varphi}}$ only consists of modal Horn formulas
constructed from angled atoms. Now, let us first prove the trickier sequent,
namely
$\Phi_{A,\overline{\varphi}},A(\overline{\varphi^{t}})\Rightarrow(A(\overline{\varphi}))^{t}$.
Using the rules in $\mathbf{CK}$, we easily get from $(2)$ and $(4)$

$\mathbf{CK}\vdash\Phi_{B,\overline{\varphi}},\Phi_{C,\overline{\varphi}},B(\overline{\varphi^{t}})\wedge
C(\overline{\varphi^{t}})\Rightarrow(B(\overline{\varphi}))^{t}\wedge(C(\overline{\varphi}))^{t}\quad(5).$

By Lemma 4.5, both $(B(\overline{\varphi}))^{t}\Rightarrow\langle
B(\overline{\varphi})\rangle$ and
$(C(\overline{\varphi}))^{t}\Rightarrow\langle C(\overline{\varphi})\rangle$
are provable in $\mathbf{CK}$, hence so is

$(B(\overline{\varphi}))^{t}\wedge(C(\overline{\varphi}))^{t}\Rightarrow\langle
B(\overline{\varphi})\rangle\wedge\langle
C(\overline{\varphi})\rangle\quad(6).$

Applications of the cut rule on the $\mathbf{CK}$-provable sequent

$\big{(}\langle B(\overline{\varphi})\rangle\wedge\langle
C(\overline{\varphi})\rangle\big{)}\to\langle B(\overline{\varphi})\wedge
C(\overline{\varphi})\rangle,\langle B(\overline{\varphi})\rangle\wedge\langle
C(\overline{\varphi})\rangle\Rightarrow\langle B(\overline{\varphi})\wedge
C(\overline{\varphi})\rangle$

and $(5)$ and $(6)$, we get

$\mathbf{CK}\vdash\Phi_{A,\overline{\varphi}},A(\overline{\varphi^{t}})\Rightarrow\langle
B(\overline{\varphi})\wedge C(\overline{\varphi})\rangle.$

Moreover, using $(Lw)$ on $(5)$ we get

$\mathbf{CK}\vdash\Phi_{A,\overline{\varphi}},A(\overline{\varphi^{t}})\Rightarrow(B(\overline{\varphi}))^{t}\wedge(C(\overline{\varphi}))^{t}$

which together with the above sequent we finally obtain

$\mathbf{CK}\vdash\Phi_{A,\overline{\varphi}},A(\overline{\varphi^{t}})\Rightarrow(A(\overline{\varphi}))^{t}.$

The other sequent, i.e.,
$\Phi_{A,\overline{\varphi}},(A(\overline{\varphi}))^{t}\Rightarrow
A(\overline{\varphi^{t}})$, is easier. Using the rules in $\mathbf{CK}$, we
easily get from $(1)$ and $(3)$

$\mathbf{CK}\vdash\Phi_{B,\overline{\varphi}},\Phi_{C,\overline{\varphi}},(B(\overline{\varphi}))^{t}\wedge(C(\overline{\varphi}))^{t}\Rightarrow
B(\overline{\varphi^{t}})\wedge C(\overline{\varphi^{t}}).$

Then, using the weakening and the rule $(L\wedge)$, we have

$\mathbf{CK}\vdash\Phi_{A,\overline{\varphi}},(A(\overline{\varphi}))^{t}\Rightarrow
A(\overline{\varphi^{t}}).$

Finally, to provide $\sigma_{\Phi,A,\overline{\varphi}}$, first note that by
the axiom $(id)$ and then applying the rule $(R\to)$ in $\mathbf{CK}$, we have
$\mathbf{CK}\vdash\;\Rightarrow(F_{\Phi,A,\overline{\varphi}})^{s}$. Call this
proof $\rho_{\Phi,A,\overline{\varphi}}$. We have already the
$\mathbf{CK}$-proofs $\sigma_{\Phi,B,\overline{\varphi}}$ and
$\sigma_{\Phi,C,\overline{\varphi}}$ for
$(\,\Rightarrow\bigwedge\Phi_{B,\overline{\varphi}}^{s})$ and
$(\,\Rightarrow\bigwedge\Phi_{C,\overline{\varphi}}^{s})$, respectively.
Therefore, together with $\rho_{\Phi,A,\overline{\varphi}}$ and some
applications of $(R\wedge)$, they form a proof
$\sigma_{\Phi,A,\overline{\varphi}}$ for
$\mathbf{CK}\vdash(\,\Rightarrow\bigwedge\Phi_{A,\overline{\varphi}}^{s})$.
Similarly, we can prove that in the case $A(\overline{p})=B(\overline{p})\vee
C(\overline{p})$, setting

$\Phi_{A,\overline{\varphi}}=\Phi_{B,\overline{\varphi}}\cup\Phi_{C,\overline{\varphi}}\cup\\{F_{\Phi,A,\overline{\varphi}},F^{\prime}_{\Phi,A,\overline{\varphi}}\\}$

works, where $F_{\Phi,A,\overline{\varphi}}=\langle
B(\overline{\varphi})\rangle\to\langle B(\overline{\varphi})\vee
C(\overline{\varphi})\rangle$ and
$F^{\prime}_{\Phi,A,\overline{\varphi}}=\langle
C(\overline{\varphi})\rangle\to\langle B(\overline{\varphi})\vee
C(\overline{\varphi})\rangle$. Finding $\sigma_{\Phi,A,\overline{\varphi}}$ is
also similar.
For the case $A(\overline{p})=\Diamond B(\overline{p})$, by Definition 4.5, we
have
$(A(\overline{\varphi}))^{t}=\Diamond(B(\overline{\varphi}))^{t}\wedge\langle\Diamond
B(\overline{\varphi})\rangle$. We already know that

$\Phi_{B,\overline{\varphi}},(B(\overline{\varphi}))^{t}\Rightarrow
B(\overline{\varphi^{t}})\quad(7)\quad,\quad\Phi_{B,\overline{\varphi}},B(\overline{\varphi^{t}})\Rightarrow(B(\overline{\varphi}))^{t}\quad(8)$

are provable in $\mathbf{CK}$. Define

$\Phi_{A,\overline{\varphi}}=\Box\Phi_{B,\overline{\varphi}}\cup\\{F_{\Phi,A,\overline{\varphi}}\\}$,

where $F_{\Phi,A,\overline{\varphi}}=\Diamond\langle
B(\overline{\varphi})\rangle\to\langle\Diamond B(\overline{\varphi})\rangle$.
Note that $\Phi_{A,\overline{\varphi}}$ consists of modal Horn formulas
constructed from angled atoms. Let us investigate the more complicated case,
namely the provability of the sequent
$\Phi_{A,\overline{\varphi}},A(\overline{\varphi^{t}})\Rightarrow(A(\overline{\varphi}))^{t}$
in $\mathbf{CK}$. The other case is easier. Now, applying the rule
$(K_{\Diamond})$ on $(8)$, we get

$\mathbf{CK}\vdash\Box\Phi_{B,\overline{\varphi}},\Diamond
B(\overline{\varphi^{t}})\Rightarrow\Diamond(B(\overline{\varphi}))^{t}\quad(9).$

By Lemma 4.5, we have
$\mathbf{CK}\vdash(B(\overline{\varphi}))^{t}\Rightarrow\langle
B(\overline{\varphi})\rangle$ and by $(K_{\Diamond})$, we get
$\mathbf{CK}\vdash\Diamond(B(\overline{\varphi}))^{t}\Rightarrow\Diamond\langle
B(\overline{\varphi})\rangle$. Therefore, using cut and $(9)$, we get
$\mathbf{CK}\vdash\Box\Phi_{B,\overline{\varphi}},\Diamond
B(\overline{\varphi^{t}})\Rightarrow\Diamond\langle
B(\overline{\varphi})\rangle$. By cut on the latter sequent and the
$\mathbf{CK}$-provable sequent $\Diamond\langle
B(\overline{\varphi})\rangle,\Diamond\langle
B(\overline{\varphi})\rangle\to\langle\Diamond
B(\overline{\varphi})\rangle\Rightarrow\langle\Diamond
B(\overline{\varphi})\rangle$, we get

$\mathbf{CK}\vdash\Box\Phi_{B,\overline{\varphi}},\Diamond
B(\overline{\varphi^{t}}),\Diamond\langle
B(\overline{\varphi})\rangle\to\langle\Diamond
B(\overline{\varphi})\rangle\Rightarrow\langle\Diamond
B(\overline{\varphi})\rangle\quad(10).$

Using the rule $(Lw)$ on $(9)$ and then applying the rule $(R\wedge)$ on the
resulting sequent and $(10)$, we get
$\Phi_{A,\overline{\varphi}},A(\overline{\varphi^{t}})\Rightarrow(A(\overline{\varphi}))^{t}$
in $\mathbf{CK}$.
To provide $\sigma_{\Phi,A,\overline{\varphi}}$, note that by the axiom $(id)$
and then applying $(R\to)$, we have
$\mathbf{CK}\vdash\;\Rightarrow(F_{\Phi,A,\overline{\varphi}})^{s}$. Call this
proof $\rho_{\Phi,A,\overline{\varphi}}$. Applying $(K_{\Box})$ on the already
existing proof
$\mathbf{CK}\vdash^{\sigma_{\Phi,B,\overline{\varphi}}}\;\Rightarrow\bigwedge(\Phi_{B,\overline{\varphi}})^{s}$,
we get
$\mathbf{CK}\vdash\;\Rightarrow\Box\bigwedge(\Phi_{B,\overline{\varphi}})^{s}$.
To prove
$\mathbf{CK}\vdash\;\Rightarrow\bigwedge(\Box\Phi_{B,\overline{\varphi}})^{s}$,
we will provide a $\mathbf{CK}$-proof for
$\Box\bigwedge\Gamma\Rightarrow\bigwedge\Box\Gamma$ and investigate its
complexity, for any multiset $\Gamma$. First, notice that by the axiom $(id)$,
we have $\mathbf{CK}\vdash\gamma\Rightarrow\gamma$, for any $\gamma\in\Gamma$.
Applying the rule $(L\wedge)$ for $\parallel\Gamma\parallel-1$ many times, we
get $\mathbf{CK}\vdash\bigwedge\Gamma\Rightarrow\gamma$, where
$\parallel\Gamma\parallel$ is the cardinality of $\Gamma$. Applying the rule
$(K\Box)$, we get $\mathbf{CK}\vdash\Box\bigwedge\Gamma\Rightarrow\Box\gamma$,
for any $\gamma\in\Gamma$. Applying the rule $(R\wedge)$ for
$\parallel\Gamma\parallel-1$ many times, we finally get
$\mathbf{CK}\vdash\Box\bigwedge\Gamma\Rightarrow\bigwedge\Box\Gamma$. Notice
that producing the whole proof takes $|\Gamma|^{O(1)}$ many steps. Using this
proof for $\Gamma=(\Phi_{B,\overline{\varphi}})^{s}$, we get a
$\mathbf{CK}$-proof for
$\Box\bigwedge(\Phi_{B,\overline{\varphi}})^{s}\Rightarrow\bigwedge\Box(\Phi_{B,\overline{\varphi}})^{s}$,
in time $|\Phi_{B,\overline{\varphi}}|^{O(1)}$. Then, using the proof
$\rho_{\Phi,A,\overline{\varphi}}$, we can easily construct a proof
$\sigma_{\Phi,A,\overline{\varphi}}$ for
$\mathbf{CK}\vdash\;\Rightarrow\bigwedge(\Phi_{A,\overline{\varphi}})^{s}$.

For $(ii)$, again, we use recursion on the structure of the almost positive
formula $A(\overline{p})$. The base case, where $A(\overline{p})$ is a basic
formula, is covered in $(i)$. The cases $A(\overline{p})=B(\overline{p})\circ
C(\overline{p})$ or $A(\overline{p})=\bigcirc B(\overline{p})$, where
$\circ\in\\{\wedge,\vee\\}$ and $\bigcirc\in\\{\Box,\Diamond\\}$ are simple
and similar to the cases in $(i)$. It is easy to see that in the former cases
$\Pi_{A,\overline{\varphi}}=\Pi_{B,\overline{\varphi}}\cup\Pi_{C,\overline{\varphi}}$
and in the latter cases
$\Pi_{A,\overline{\varphi}}=\Box\Pi_{B,\overline{\varphi}}$ works. The
structure of $\sigma_{\Pi,A,\overline{\varphi}}$ is similar to that of the
case $(i)$. The only remaining case, which is also simple, is when
$A(\overline{p})=B(\overline{p})\to C(\overline{p})$, where $B(\overline{p})$
is a basic formula and $C(\overline{p})$ is almost positive. Here again
$\Pi_{A,\overline{\varphi}}=\Phi_{B,\overline{\varphi}}\cup\Pi_{C,\overline{\varphi}}$
works. It is clear that $\Pi_{A,\overline{\varphi}}$ is a multiset of modal
Horn formulas constructed from angled atoms. Using Definition 4.2, we have
$(A(\overline{\varphi}))^{t}=[(B(\overline{\varphi}))^{t}\to(C(\overline{\varphi}))^{t}]\wedge\langle
B(\overline{\varphi})\to C(\overline{\varphi})\rangle$. By $(i)$ and the
recursive step, we have the multisets $\Phi_{B,\overline{\varphi}}$ and
$\Pi_{C,\overline{\varphi}}$ such that

$\Phi_{B,\overline{\varphi}},B(\overline{\varphi^{t}})\Rightarrow(B(\overline{\varphi}))^{t}\quad(11)\quad,\quad\Pi_{C,\overline{\varphi}},(C(\overline{\varphi}))^{t}\Rightarrow
C(\overline{\varphi^{t}})\quad(12)$

are provable in $\mathbf{CK}$. Using the rule $(Lw)$ and then $(L\to)$ on
$(11)$ and $(12)$ and then the rule $(R\to)$, we get

$\mathbf{CK}\vdash\Phi_{B,\overline{\varphi}},\Pi_{C,\overline{\varphi}},(B(\overline{\varphi}))^{t}\to(C(\overline{\varphi}))^{t}\Rightarrow
B(\overline{\varphi^{t}})\to C(\overline{\varphi^{t}}).$

Now, using the rule $(L\wedge_{1})$ to introduce $\langle
B(\overline{\varphi})\to C(\overline{\varphi})\rangle$ in the antecedent of
the sequent, and setting
$\Pi_{A,\overline{\varphi}}=\Phi_{B,\overline{\varphi}}\cup\Pi_{C,\overline{\varphi}}$,
we get
$\mathbf{CK}\vdash\Pi_{A,\overline{\varphi}},(A(\overline{\varphi}))^{t}\Rightarrow
A(\overline{\varphi^{t}})$. Finally, similar to the case $(i)$, it is easy to
use $\sigma_{\Phi,B,\overline{\varphi}}$ and
$\sigma_{\Pi,C,\overline{\varphi}}$ to construct
$\sigma_{\Pi,A,\overline{\varphi}}$ such that
$\mathbf{CK}\vdash^{\sigma_{\Pi,A,\overline{\varphi}}}\;\Rightarrow\bigwedge\Theta_{A,\overline{\varphi}}^{s}$.

For $(iii)$, the proof again proceeds by recursion on the structure of the
constructive formula $A(\overline{p})$. The base case is covered in $(i)$. For
the case $A(\overline{p})=B(\overline{p})\wedge C(\overline{p})$, set
$\Upsilon_{A,\overline{\varphi}}$ as

$\Upsilon_{B,\overline{\varphi}}\cup\Upsilon_{C,\overline{\varphi}}\cup\\{F_{\Upsilon,A,\overline{\varphi}},F^{\prime}_{\Upsilon,A,\overline{\varphi}}\\},$

where $F_{\Upsilon,A,\overline{\varphi}}=\langle B(\overline{\varphi})\wedge
C(\overline{\varphi})\rangle\to\langle B(\overline{\varphi})\rangle$ and
$F^{\prime}_{\Upsilon,A,\overline{\varphi}}=\langle
B(\overline{\varphi})\wedge C(\overline{\varphi})\rangle\to\langle
C(\overline{\varphi})\rangle$, and for the case that $A(\overline{p})=\Box
B(\overline{p})$ take

$\Upsilon_{A,\overline{\varphi}}=\Box\Upsilon_{B,\overline{\varphi}}\cup\\{F_{\Upsilon,A,\overline{\varphi}}\\},$

where $F_{\Upsilon,A,\overline{\varphi}}=\langle\Box
B(\overline{\varphi})\rangle\to\Box\langle B(\overline{\varphi})\rangle$. It
is easy to see that in both cases $\Upsilon_{A,\overline{\varphi}}$ works, it
is a multiset of modal Horn formulas constructed from angled atoms, and
$\mathbf{CK}\vdash(\,\Rightarrow\bigwedge\Theta_{A,\overline{\varphi}}^{s})$
by a proof $\sigma_{\Upsilon,A,\overline{\varphi}}$, constructed in a similar
fashion as in $(i)$. The only case left is $A(\overline{p})=B(\overline{p})\to
C(\overline{p})$, where $B(\overline{p})$ is almost positive and
$C(\overline{p})$ is constructive. By Definition 4.5, we have
$(A(\overline{\varphi}))^{t}=[(B(\overline{\varphi}))^{t}\to(C(\overline{\varphi}))^{t}]\wedge\langle
B(\overline{\varphi})\to C(\overline{\varphi})\rangle$. By $(ii)$ and the
recursive step, we have the multisets $\Pi_{B,\overline{\varphi}}$ and
$\Upsilon_{C,\overline{\varphi}}$ such that

$\Pi_{B,\overline{\varphi}},(B(\overline{\varphi}))^{t}\Rightarrow
B(\overline{\varphi^{t}})\quad(13)\quad,\quad\Upsilon_{C,\overline{\varphi}},\langle
C(\overline{\varphi})\rangle,C(\overline{\varphi^{t}})\Rightarrow(C(\overline{\varphi}))^{t}\quad(14)$

are provable in $\mathbf{CK}$. We claim taking

$\Upsilon_{A,\overline{\varphi}}=\Pi_{B,\overline{\varphi}}\cup\Upsilon_{C,\overline{\varphi}}\cup\\{F_{\Upsilon,A,\overline{\varphi}}\\}$

where $F_{\Upsilon,A,\overline{\varphi}}=\big{(}\langle
B(\overline{\varphi})\to C(\overline{\varphi})\rangle\wedge\langle
B(\overline{\varphi})\rangle\big{)}\to\langle C(\overline{\varphi})\rangle$
works. Applying the rule $(Lw)$ and then $(L\to)$ on $(13)$ and $(14)$, we
have

$\mathbf{CK}\vdash\Pi_{B,\overline{\varphi}},\Upsilon_{C,\overline{\varphi}},(B(\overline{\varphi}))^{t},\langle
C(\overline{\varphi})\rangle,B(\overline{\varphi^{t}})\to
C(\overline{\varphi^{t}})\Rightarrow(C(\overline{\varphi}))^{t}.$

Using the cut rule on the above sequent and
$(B(\overline{\varphi}))^{t},(B(\overline{\varphi}))^{t}\to\langle
C(\overline{\varphi})\rangle\Rightarrow\langle C(\overline{\varphi})\rangle$
and then $(Lc)$ and $(R\to)$, we get

$\Pi_{B,\overline{\varphi}},\Upsilon_{C,\overline{\varphi}},(B(\overline{\varphi}))^{t}\to\langle
C(\overline{\varphi})\rangle,B(\overline{\varphi^{t}})\to
C(\overline{\varphi^{t}})\Rightarrow(B(\overline{\varphi}))^{t}\to(C(\overline{\varphi}))^{t}\;\;(15)$

is provable in $\mathbf{CK}$. Using the cut rule on the following
$\mathbf{CK}$-provable sequents

$\langle A(\overline{\varphi})\rangle,\langle
A(\overline{\varphi})\rangle\wedge\langle
B(\overline{\varphi})\rangle\to\langle
C(\overline{\varphi})\rangle\Rightarrow\langle
B(\overline{\varphi})\rangle\to\langle C(\overline{\varphi})\rangle\quad,$

$\langle B(\overline{\varphi})\rangle\to\langle
C(\overline{\varphi})\rangle\Rightarrow(B(\overline{\varphi}))^{t}\to\langle
C(\overline{\varphi})\rangle$

we get

$\mathbf{CK}\vdash\langle A(\overline{\varphi})\rangle,\langle
A(\overline{\varphi})\rangle\wedge\langle
B(\overline{\varphi})\rangle\to\langle
C(\overline{\varphi})\rangle\Rightarrow(B(\overline{\varphi}))^{t}\to\langle
C(\overline{\varphi})\rangle$.

Using the cut rule on the above sequent and $(15)$, we obtain

$\mathbf{CK}\vdash\Pi_{B,\overline{\varphi}},\Upsilon_{C,\overline{\varphi}},\langle
A(\overline{\varphi})\rangle,\langle A(\overline{\varphi})\rangle\wedge\langle
B(\overline{\varphi})\rangle\to\langle
C(\overline{\varphi})\rangle,B(\overline{\varphi^{t}})\to
C(\overline{\varphi^{t}})\Rightarrow(B(\overline{\varphi}))^{t}\to(C(\overline{\varphi}))^{t}.$

Using the left weakening rule on $\langle
A(\overline{\varphi})\rangle\Rightarrow\langle A(\overline{\varphi})\rangle$
we get

$\mathbf{CK}\vdash\Upsilon_{A,\overline{\varphi}},\langle
A(\overline{\varphi})\rangle,A(\overline{\varphi^{t}})\Rightarrow\langle
A(\overline{\varphi})\rangle.$

Applying the rule $(R\wedge)$ on the above two sequent, we get

$\mathbf{CK}\vdash\Upsilon_{A,\overline{\varphi}},\langle
A(\overline{\varphi})\rangle,A(\overline{\varphi^{t}})\Rightarrow(A(\overline{\varphi}))^{t},$

as required. Again, it is clear that $\Upsilon_{A,\overline{\varphi}}$ is a
multiset of modal Horn formulas constructed from angled atoms and
$\mathbf{CK}\vdash^{\sigma_{\Upsilon,A,\overline{\varphi}}}(\,\Rightarrow\bigwedge\Upsilon_{A,\overline{\varphi}}^{s})$,
where the structure of $\sigma_{\Upsilon,A,\overline{\varphi}}$ is similar to
that of the case $(i)$.

The only issue remained to investigate is the feasibility of the algorithms
for $\Theta_{A,\overline{\varphi}}$ and
$\sigma_{\Theta,A,\overline{\varphi}}$. From now on, for simplicity, we use
$A$ and $|A|$, when we want to refer to $A(\overline{p})$ and
$|A(\overline{p})|$. For $\Theta_{A,\overline{\varphi}}$, we use the above
algorithm that reads $A$ and $\overline{\varphi}$ and computes
$\Theta_{A,\overline{\varphi}}$, by recursion on the structure of $A$. Let
$\Theta\in\\{\Phi,\Pi,\Upsilon\\}$, $\circ\in\\{\wedge,\vee\\}$, and
$\bigcirc\in\\{\Box,\Diamond\\}$. First, we need an upper bound on
$\parallel\Theta_{A,\overline{\varphi}}\parallel$ and
$|\Theta_{A,\overline{\varphi}}|$. For the former, by a simple induction on
$A$, observe that $\parallel\Theta_{A,\overline{\varphi}}\parallel\leq
O(|A|)$. For the latter, we have the following inequalities:

  1. 1.

$|\Theta_{A,\overline{\varphi}}|\leq O(1)$, where $A(\overline{p})$ is an
atom, $\bot$, or $\top$,

  2. 2.

$|\Theta_{B\circ
C,\overline{\varphi}}|\leq|\Theta_{B,\overline{\varphi}}|+|\Theta_{C,\overline{\varphi}}|+O(|A||\overline{\varphi}|),$
except when $\\{\Theta=\Upsilon,\circ=\vee\\}$,

  3. 3.

$|\Pi_{B\to
C,\overline{\varphi}}|\leq|\Phi_{B,\overline{\varphi}}|+|\Pi_{C,\overline{\varphi}}|+O(|A||\overline{\varphi}|),$

  4. 4.

$|\Upsilon_{B\to
C,\overline{\varphi}}|\leq|\Pi_{B,\overline{\varphi}}|+|\Upsilon_{C,\overline{\varphi}}|+O(|A||\overline{\varphi}|),$

  5. 5.

$|\Theta_{\bigcirc
B,\overline{\varphi}}|\leq|\Theta_{B,\overline{\varphi}}|+O(|A||\overline{\varphi}|),$
except when $\\{\Theta=\Phi,\bigcirc=\Box\\}$ or
$\\{\Theta=\Upsilon,\bigcirc=\Diamond\\}$.

First, note that the cases which are excluded in $2$ and $5$, are the cases
where the theorem does not apply to. For instance, in $5$, we have excluded
the case where $\Theta=\Phi$ and $\bigcirc=\Box$. The reason is that the
multiset $\Phi_{A,\overline{\varphi}}$ corresponds to the case where $A$ is a
basic formula, and by Definition 3.1, $A$ cannot be of the form $\Box B$.
Similarly for the other excluded cases.

Now, to justify the inequalities, based on how the multisets were constructed,
the bounds are easy to compute. In each case, $\Theta_{A,\overline{\varphi}}$
is the union or the box of $\Phi$, $\Pi$ or $\Upsilon$ of the immediate
subformulas of $A$ and the formulas $F_{\Theta,A,\overline{\varphi}}$ and
$F^{\prime}_{\Theta,A,\overline{\varphi}}$. As the addend
$O(|A||\overline{\varphi}|)$ represents an upper bound for
$|F_{\Theta,A,\overline{\varphi}}|$ or
$|F_{\Theta,A,\overline{\varphi}}|+|F^{\prime}_{\Theta,A,\overline{\varphi}}|$,
depending on the case, the bounds are trivially in place. Now, using a simple
induction on the structure of $A$ (first starting with basic formulas, then
almost positive and finally constructive formulas) and the above inequalities,
we can show that
$|\Theta_{A,\overline{\varphi}}|\leq(|A|+|\overline{\varphi}|)^{O(1)}$.

Having the upper bounds on $\parallel\Theta_{A,\overline{\varphi}}\parallel$
and $|\Theta_{A,\overline{\varphi}}|$ established, we are now ready to address
the feasibility of the computation of $\Theta_{A,\overline{\varphi}}$. Denote
the time that the algorithm takes to compute $\Theta_{A,\overline{\varphi}}$
by $T_{\Theta}(A,\overline{\varphi})$. We have:

  1. 1.

$T_{\Theta}(A,\overline{\varphi})\leq O(1)$, where $A(\overline{p})$ is an
atom, $\bot$, or $\top$,

  2. 2.

$T_{\Theta}(B\circ C,\overline{\varphi})\leq
T_{\Theta}(B,\overline{\varphi})+T_{\Theta}(C,\overline{\varphi})+O(|A||\overline{\varphi}|),$
except when $\\{\Theta=\Upsilon,\circ=\vee\\}$,

  3. 3.

$T_{\Pi}(B\to C,\overline{\varphi})\leq
T_{\Phi}(B,\overline{\varphi})+T_{\Pi}(C,\overline{\varphi})+O(|A||\overline{\varphi}|),$

  4. 4.

$T_{\Upsilon}(B\to C,\overline{\varphi})\leq
T_{\Pi}(B,\overline{\varphi})+T_{\Upsilon}(C,\overline{\varphi})+O(|A||\overline{\varphi}|),$

  5. 5.

$T_{\Theta}(\bigcirc B,\overline{\varphi})\leq
T_{\Theta}(B,\overline{\varphi})+O(|\Theta_{B,\overline{\varphi}}|+\parallel\Theta_{B,\overline{\varphi}}\parallel)+O(|A||\overline{\varphi}|),$
except when $\\{\Theta=\Phi,\bigcirc=\Box\\}$ or
$\\{\Theta=\Upsilon,\bigcirc=\Diamond\\}$.

It is easy to see why these inequalities hold, based on how the multisets were
constructed. The reason simply is that in each case, we must first compute the
appropriate multiset among $\Phi$, $\Pi$ or $\Upsilon$ of the immediate
subformulas of $A$, and then possibly the formulas
$F_{\Theta,A,\overline{\varphi}}$ and
$F^{\prime}_{\Theta,A,\overline{\varphi}}$. Note that in the modal cases (the
last inequality), the algorithm also needs to add boxes to
$\Theta_{A,\overline{\varphi}}$ that takes
$O(|\Theta_{B,\overline{\varphi}}|+\parallel\Theta_{B,\overline{\varphi}}\parallel)$
steps. As the addend $O(|A||\overline{\varphi}|)$ represents an upper bound on
the time to compute $F_{\Theta,A,\overline{\varphi}}$ and
$F^{\prime}_{\Theta,A,\overline{\varphi}}$, the bounds are trivially in place.
Now, using a simple induction on the structure of $A$ (first starting with the
basic formulas, then the almost positive and finally the constructive
formulas), by the above inequalities together with the fact that
$\parallel\Theta_{A,\overline{\varphi}}\parallel\leq O(|A|)$ and
$|\Theta_{A,\overline{\varphi}}|\leq(|A|+|\overline{\varphi}|)^{O(1)}$, we can
show that
$T_{\Theta}(A,\overline{\varphi})\leq(|A|+|\overline{\varphi}|)^{O(1)}$.

Similarly, we follow the above algorithm to compute
$\sigma_{\Theta,A,\overline{\varphi}}$, where the time of the algorithm is
denoted by $T_{\sigma,\Theta}(A,\overline{\varphi})$. We have the
inequalities:

  * $1^{\prime}.$

$T_{\sigma,\Theta}(A,\overline{\varphi})\leq O(1),$ where $A(\overline{p})$ is
an atom, $\bot$, or $\top$,

  * $2^{\prime}.$

$T_{\sigma,\Theta}(B\circ C,\overline{\varphi})\leq
T_{\sigma,\Theta}(B,\overline{\varphi})+T_{\sigma,\Theta}(C,\overline{\varphi})+T_{\rho,\Theta}(A,\overline{\varphi})+O(|\Theta_{B,\overline{\varphi}}|+|\Theta_{C,\overline{\varphi}}|+|A||\overline{\varphi}|),$
except when $\\{\Theta=\Upsilon,\circ=\vee\\}$,

  * $3^{\prime}.$

$T_{\sigma,\Pi}(B\to C,\overline{\varphi})\leq
T_{\sigma,\Phi}(B,\overline{\varphi})+T_{\sigma,\Pi}(C,\overline{\varphi})+T_{\rho,\Pi}(A,\overline{\varphi})+O(|\Phi_{B,\overline{\varphi}}|+|\Pi_{C,\overline{\varphi}}|+|A||\overline{\varphi}|),$

  * $4^{\prime}.$

$T_{\sigma,\Upsilon}(B\to C,\overline{\varphi})\leq
T_{\sigma,\Pi}(B,\overline{\varphi})+T_{\sigma,\Upsilon}(C,\overline{\varphi})+T_{\rho,\Upsilon}(A,\overline{\varphi})+O(|\Pi_{B,\overline{\varphi}}|+|\Upsilon_{C,\overline{\varphi}}|+|A||\overline{\varphi}|),$

  * $5^{\prime}.$

$T_{\sigma,\Theta}(\bigcirc B,\overline{\varphi})\leq
T_{\sigma,\Theta}(B,\overline{\varphi})+T_{\rho,\Theta}(A,\overline{\varphi})+(|\Theta_{B,\overline{\varphi}}|)^{O(1)}+O(|A||\overline{\varphi}|),$
except when $\\{\Theta=\Phi,\bigcirc=\Box\\}$ or
$\\{\Theta=\Upsilon,\bigcirc=\Diamond\\}$.

where $T_{\rho,\Theta}(A,\varphi)$ is the time to compute
$\rho_{\Theta,A,\overline{\varphi}}$. To show why, as $1^{\prime}$ is trivial,
we split the bounds $2^{\prime}-5^{\prime}$ into two families: the
propositional and the modal cases. For the propositional cases,
$2^{\prime}-4^{\prime}$, the proof $\sigma_{\Theta,A,\overline{\varphi}}$ is
the combination of the corresponding proofs for $\Phi$, $\Pi$ or $\Upsilon$ of
the immediate subformulas of $A$, the proofs of the sequents
$(\,\Rightarrow(F_{\Theta,A,\overline{\varphi}})^{s})$ and
$(\,\Rightarrow(F^{\prime}_{\Theta,A,\overline{\varphi}})^{s})$, denoted by
$\rho_{\Theta,A,\overline{\varphi}}$ throughout the construction, and finally
some constant number of the applications of the rule $(R\wedge)$. Note that
the last part expands the time of the computation by a constant number of the
sum of the sizes of $\Phi$, $\Pi$ or $\Upsilon$ for the immediate subformulas
and the size of $F_{\Theta,A,\overline{\varphi}}$ and
$F^{\prime}_{\Theta,A,\overline{\varphi}}$. For instance, in the case
$4^{\prime}$, the proof $\sigma_{\Upsilon,B\to C,\overline{\varphi}}$ looks
like:

$\sigma_{\Pi,B,\overline{\varphi}}$
$\Rightarrow\bigwedge\Pi^{s}_{B,\overline{\varphi}}$
$\sigma_{\Upsilon,C,\overline{\varphi}}$
$\Rightarrow\bigwedge\Upsilon^{s}_{C,\overline{\varphi}}$
$\Rightarrow\bigwedge\Pi^{s}_{B,\overline{\varphi}}\wedge\bigwedge\Upsilon^{s}_{C,\overline{\varphi}}$
$\rho_{\Upsilon,A,\overline{\varphi}}$
$\Rightarrow(F_{\Upsilon,A,\overline{\varphi}})^{s}$
$\Rightarrow\bigwedge\Pi^{s}_{B,\overline{\varphi}}\wedge\bigwedge\Upsilon^{s}_{C,\overline{\varphi}}\wedge(F_{\Upsilon,A,\overline{\varphi}})^{s}$
---

For the modal case, i.e., $5^{\prime}$, we start with
$\sigma_{\Theta,B,\overline{\varphi}}$ to which we apply the rule
$(K_{\Box})$. Then, we prove
$\Box\bigwedge\Theta_{B,\overline{\varphi}}^{s}\Rightarrow\bigwedge\Box(\Theta_{B,\overline{\varphi}})^{s}$
and finally we add the proof $\rho_{\Theta,A,\overline{\varphi}}$ for
$F_{\Theta,A,\overline{\varphi}}$ together with some constant number of the
applications of $(R\wedge)$. The addend
$(|\Theta_{B,\overline{\varphi}}|)^{O(1)}$ in $5^{\prime}$ is a bound for the
time of the box distribution part, while $O(|A||\overline{\varphi}|)$ is a
bound for the size of $F_{\Theta,A,\overline{\varphi}}$.
Finally, having the inequalities established, by using the inequalities
$|\Theta_{A,\overline{\varphi}}|\leq(|A|+|\overline{\varphi}|)^{O(1)}$ and
$T_{\rho,\Theta}(A,\overline{\varphi})\leq(|A|+|\overline{\varphi}|)^{O(1)}$,
it is easy to use an induction on the structure of $A$ to prove
$T_{\sigma,\Theta}(A,\overline{\varphi})\leq(|A|+|\overline{\varphi}|)^{O(1)}$.
∎

######  Remark 4.9.

Here are two remarks. First, note that Theorem 4.8 holds for _any_ multiset of
formulas $\overline{\varphi}$, as long as the formula $A$ has the described
structure. Another point to make is that in the proof of Theorem 4.8, other
(sometimes simpler) choices exist for the set of modal Horn formulas such that
it makes the translated sequent provable in $\mathbf{CK}$. The crucial point
of our choices for these sets of modal Horn formulas is the condition that the
standard translation of each of their elements are provable in $\mathbf{CK}$.

The last part of this subsection is devoted to investigate the relationship
between the translation $t$ and the Harrop formulas as defined below.

######  Definition 4.10.

The set of _Harrop_ formulas in the language $\mathcal{L}$ is the smallest set
of formulas containing the atoms in $\mathcal{L}$ and $\bot$, $\top$, and is
closed under $\wedge,\Box$, and implications of the form $A\to B$, where $A$
is an arbitrary formula and $B$ a Harrop formula. A formula in the language
$\mathcal{L}_{\Box}$, $\mathcal{L}_{\Diamond}$ or $\mathcal{L}_{p}$ is called
Harrop, if it is Harrop as a formula in the extended language $\mathcal{L}$.

######  Lemma 4.11.

There is a feasible algorithm that reads a Harrop formula $A\in\mathcal{L}$
and outputs a multiset $\Gamma_{A}$ and a proof $\sigma_{A}$ such that:

  1. $(i)$

$\Gamma_{A}$ consists of modal Horn formulas, constructed only from $\bot$,
and angled atoms,

  2. $(ii)$

$\mathbf{CK}\vdash\Gamma_{A}\Rightarrow A^{t}$, and

  3. $(iii)$

$\mathbf{CK}\vdash^{\sigma_{A}}\bigwedge\Gamma_{A}^{s}\Leftrightarrow A$.

###### Proof.

We first explain the algorithm to compute $\Gamma_{A}$ and $\sigma_{A}$. The
feasibility part will be explained afterwards. To construct $\Gamma_{A}$ and
$\sigma_{A}$, we use recursion on the structure of $A$. If $A$ is atomic,
$\bot$, or $\top$, then it is easy to see that $\Gamma_{A}=\\{A^{t}\\}$
satisfies the Conditions $(i)$ and $(ii)$. Moreover, notice that
$\bigwedge\Gamma_{A}^{s}\Leftrightarrow A$ is an instance of the axiom $(id)$
in $\mathbf{CK}$. Therefore, it is enough to define $\sigma_{A}$ as that
instance. If $A=B\wedge C$, where $B$ and $C$ are Harrop formulas, define
$\Gamma_{A}$ as $\Gamma_{B}\cup\Gamma_{C}\cup\\{\langle B\wedge C\rangle\\}$.
From the recursion step, we know that the multisets $\Gamma_{B}$ and
$\Gamma_{C}$ only consist of modal Horn formulas,
$\mathbf{CK}\vdash\Gamma_{B}\Rightarrow B^{t}$,
$\mathbf{CK}\vdash\Gamma_{C}\Rightarrow C^{t}$, and $\sigma_{B}$ and
$\sigma_{C}$ satisfy
$\mathbf{CK}\vdash^{\sigma_{B}}\bigwedge\Gamma_{B}^{s}\Leftrightarrow B$ and
$\mathbf{CK}\vdash^{\sigma_{C}}\bigwedge\Gamma_{C}^{s}\Leftrightarrow C$.
Given this data, it is easy to see that Conditions $(i)$ and $(ii)$ are
satisfied for $\Gamma_{A}$. For $\sigma_{A}$, it is easy to use the proofs
$\sigma_{B}$ and $\sigma_{C}$ to construct the proof $\sigma_{A}$ for
$\bigwedge\Gamma_{B}^{s}\wedge\bigwedge\Gamma_{C}^{s}\wedge\langle B\wedge
C\rangle^{s}\Leftrightarrow A$.
For $A=B\to C$, where $C$ is Harrop, take

$\Gamma_{A}=\\{\langle B\to C\rangle\\}\cup\\{\langle
B\rangle\to\gamma\mid\gamma\in\Gamma_{C}\\}.$

Condition $(i)$ is satisfied for $\Gamma_{A}$: the formula $\langle B\to
C\rangle$ is an angled atom and as $\langle B\rangle$ is an atom, $\Gamma_{C}$
consists of modal Horn formulas, and by Definition 4.6 the set of modal Horn
formulas are closed under implications with atomic antecedent and modal Horn
succedents, the formula $\langle B\rangle\to\gamma$ is modal Horn.

For Condition $(ii)$, we know that $\mathbf{CK}\vdash\Gamma_{C}\Rightarrow
C^{t}$ and hence $\mathbf{CK}\vdash\bigwedge\Gamma_{C}\Rightarrow C^{t}$. By
Lemma 4.5 we have $\mathbf{CK}\vdash B^{t}\Rightarrow\langle B\rangle$ and by
$(L\to)$ we get $\mathbf{CK}\vdash B^{t},\langle
B\rangle\to\bigwedge\Gamma_{C}\Rightarrow C^{t}$. As
$\mathbf{CK}\vdash\\{\langle
B\rangle\to\gamma\mid\gamma\in\Gamma_{C}\\}\Rightarrow\langle
B\rangle\to\bigwedge\Gamma_{C}$, we finally get $\mathbf{CK}\vdash\\{\langle
B\to C\rangle\\}\cup\\{\langle
B\rangle\to\gamma\mid\gamma\in\Gamma_{C}\\}\Rightarrow(B\to C)^{t}$.

For $\sigma_{A}$, take the following derivable sequents in $\mathbf{CK}$:

$\bigwedge\Gamma_{C}^{s}\Leftrightarrow C$ , |  $\langle B\to C\rangle^{s}\Leftrightarrow B\to C$ , |  $\bigwedge_{\gamma\in\Gamma_{C}}(\langle B\rangle\to\gamma)^{s}\Leftrightarrow B\to\bigwedge\Gamma_{C}^{s}$,
---|---|---

where the leftmost sequent is provable by $\sigma_{C}$, the middle one is an
instance of the axiom $(id)$ and the left to right direction of the rightmost
sequent is a result of applying the rule $(R\wedge)$ for
$\parallel\Gamma_{C}\parallel-1$ many times on the canonical proof of
$\bigwedge_{\gamma\in\Gamma_{C}}(B\to\gamma^{s}),B\Rightarrow\gamma^{s}$ and
then using $(R\to)$, while the other direction is clear. Using these three
proofs, it is easy to construct the proof $\sigma_{A}$. It is noteworthy that
although the choice $\\{\langle B\rangle\to\bigwedge\Gamma_{C},\langle
A\rangle\\}$ for $\Gamma_{A}$ seems more reasonable, it is not a possibility,
as the formula $\langle B\rangle\to\bigwedge\Gamma_{C}$ is not necessarily in
the modal Horn form as the class of modal Horn formulas is not closed under
conjunctions.
For $A=\Box B$, where $B$ is Harrop, define
$\Gamma_{A}=\Box\Gamma_{B}\cup\\{\langle\Box B\rangle\\}$. First, as the set
of modal Horn formulas is closed under box, $\Gamma_{A}$ consists of modal
Horn formulas, built only from angled atoms and $\bot$. Second, as we already
have $\mathbf{CK}\vdash\Gamma_{B}\Rightarrow B^{t}$, using the rules
$(K_{\Box}),(Lw)$, and $(R\wedge)$, we have
$\mathbf{CK}\vdash\Box\Gamma_{B},\langle\Box B\rangle\Rightarrow(\Box B)^{t}$.
Third, using $\sigma_{B}$ followed by two applications of $(K_{\Box})$, we
have a proof for $\Box\bigwedge\Gamma_{B}^{s}\Leftrightarrow\Box B$. As
observed in the proof of Theorem 4.8, for any multiset $\Omega$ we have
$\mathbf{CK}\vdash\Box\bigwedge\Omega\Rightarrow\bigwedge\Box\Omega$ and the
proof takes $|\Omega|^{O(1)}$ many steps. Using this proof for
$\Omega=\Gamma_{B}^{s}$, we get a proof for
$\bigwedge(\Box\Gamma_{B}^{s})\Leftrightarrow\Box B$ which provides the proof
$\sigma_{A}$ for $\bigwedge\Gamma_{A}^{s}\Leftrightarrow A$ in $\mathbf{CK}$.