11institutetext: Department of Philosophy (Zhuhai), Sun Yat-sen University
11email<EMAIL_ADDRESS>
# Deciding some displayable modal logics

Jinsheng Chen

###### Abstract

In this paper we use display calculus to show the decidability for normal
modal logic $\mathrm{K}$ and some of its extensions.

##  1 Introduction

Proof theory for modal logics aims at developing ‘good’ calculi for modal
logics. Though there is not a formal definition of ‘good’ calculi, it is
agreed that Gentzen-style calculi for normal modal logics like $\mathrm{K}$,
$\mathrm{T}$, $\mathrm{S4}$ (see e.g. [10]) are representatives of good
calculi. These calculi have the following properties:

(1) Cut-elimination. The following _cut_ rule, which is the proof-theoretic
analogue of _modus ponds_ in Hilbert-style axiomatization,

$\frac{\Gamma\Rightarrow\Delta,\varphi\quad\varphi,\Gamma’\Rightarrow\Delta’}{\Gamma,\Gamma’\Rightarrow\Delta,\Delta’}$

is eliminable from the calculus without affecting what are provable. From the
bottom up, the cut rule introduces a new formula. The elimination of the cut
rule paves the way to prove the subfromula property introduced below and hence
decidability.

(2) Subformula property. If sequent $\mathcal{S}$ is provable, then there is a
proof for $\mathcal{S}$ consisting only of subformulas in $\mathcal{S}$.

(3) Decidability. There is a root-first algorithm to decide whether a sequent
is provable in the calculus. ‘Root-first’ means to consider the main
connective of a formula in the sequent and try applicable rules.

Until now, Gentzen-style sequent calculi satisfying these properties
simultaneously has only been developed for a limited number of modal logics.
Even worse, it seems difficult to develop such calculi for some simple logics.
Take the Gentzen-style calculus for modal logic $\mathrm{S5}$ as an example
(see [10]). It has the subformula property and is decidable, but not cut-
eliminable. A restricted version of cut elimination is proved: [14] showed
that every application of cut can be transformed into one where the cut
formula is a subformula in the endsequent.

To endow more modal logics with good calculi, generalizations and variations
of Gentzen-style sequent calculi introduced in the literature which includes
hypersequent calculus[1], labelled sequent calculus [9], deep sequent system
[3], and display calculus [2] and so on. Back to the example of $\mathrm{S5}$,
[11] introduced a hypersequent calculus for $\mathrm{S5}$, which is cut-
admissible, decidable and has the subformula property.

This paper contributes to display calculus. It was introduced in [2], and
further developed in papers like [12, 8, 6, 13, 15, 5, 7, 4]. According to
[8], display calculus is a proof-system aiming to explore in depth the
strategy to replace logical connectives by structural operators. This is
called _Gentzenization_. In a proof of a Gentzenized calculus, structural
operators representing logical connectives are manipulated and transformed
into the corresponding connectives at a certain stage and this process is not
reversible. The rules for manipulating structural operators are called
_structural rules_ , which typically includes _weakening_ , _contraction_ and
the cut rule. The rules that transforms a structural operator to a logical
connective are called _connective rules_. A standard Gentzen sequent can be
written as
$\varphi_{1},\ldots,\varphi_{m}\Rightarrow\psi_{1},\ldots,\psi_{n}$, where the
comma is a structural operator and $\varphi_{1},\ldots,\varphi_{m}$ and
$\psi_{1},\ldots,\psi_{n}$ are two structures. The comma means different
things depending on the place it occupies in the sequent: it is interpreted as
_and_ when to the left of the double arrow and as _or_ when to the right,
which is witnessed by the connective rules for $\land$ and $\lor$. An example
of structural rules is the left contraction rule: from
$\varphi,\varphi,\Gamma\Rightarrow\Delta$ imply
$\varphi,\Gamma\Rightarrow\Delta$.

Display calculus for modal logic has more than one structural operator. [15]
uses binary structural operator $\circ$ which is interpreted as conjuction
when it is to the left of $\Rightarrow$ and disjunction when to the right.
Furthermore, it uses a unary operator $\ast$ for negation and a binary
operator $\bullet$ for modalities, which means the backward-looking diamond
$\blacklozenge$ when it is to the left of $\Rightarrow$ and the forward-
looking box $\Box$ when to the right. In the display calculus for modal logic
$\mathrm{K}$, sequents $\bullet X\Rightarrow Y$ and $X\Rightarrow\bullet Y$
are inter-provable, which reflects the fact that $\blacklozenge$ and $\Box$
are a residuated pair from an algebraic perspective.

The main advantages of display calculus are as follows:

(1) A general cut-elimination theorem111This was proposed in [2]. [8] and [15]
provides rephrased proofs.. For any display calculus, if it satisfies certain
syntactic criterion, then it is cut-eliminable. The corollary of this theorem
is as follows: given a cut-eliminable display calculus for $\mathrm{K}$ and
add rules of a specified form, then the new display calculus is also cut-
eliminable and has the subformula property.

(2) Given a display calculus for normal modal logic $\mathrm{K}$, there is an
algorithm to transform some axioms into rules of the specified form mentioned
in the last paragraph such that the display calculus plus these rules is sound
and complete with $\mathrm{K}$ plus these axioms.222The formulas with an
effective algorithm are called _primitive axioms_ in [8] and called _analytic
inductive axioms_ in [7]. An influential result for modal logics in [8] is
such that an axiomatic extension of the basic temporal logic is displayable
iff it is axiomatized by a set of primitive axioms. The logics studied in [7]
is algebraized by bounded distributive lattices with operators, which is more
general than the algebraic semantics for modal logics As a result, for some
extensions of $\mathrm{K}$, we can easily have display calculus for these
logics with cut elimination and subformula property.

However, it is unclear whether decidability of displayable modal logics can be
extracted from their display calculi333[13] proved the decidability of some
displayable substructural logics through their display calculi. The display
calculi for modal logics are more complex than those for substructural logics
and hence more techniques are needed to prove the results in our paper. . We
try to fill in this gap in this paper. We show that the display calculus for
normal modal logic $\mathrm{K}$ and a class of its extensions, called _normal
extension_ is decidable. Normal extensions of $\mathrm{K}$ includes logics
axiomatized by some Soctt-Lemmon axioms and primitive axioms (See Section
8.2). These results pertain to some displayable temporal logics and some
logics algebraized by bounded distributive lattices with operators.

The canonical method to prove that a calculus $\mathrm{D}$ is decidable is to
prove that (1) each provable sequent in $\mathrm{D}$ has a proof of a
particular form, and that (2) the search space for proofs of that form for any
sequent is finite. For instance, in Gentenze-style calculus for modal logic
$\mathrm{K}$, it is required to show that each provable sequent has a
irredundant, _$3$ -reduced_ proof with subformula property and that the search
space for such proofs is finite (see [10]). In this paper, we follow the same
method. Due to the complexity caused by the number of structural operators in
display calculus and by the bidirectional _display rules_ , it is not
straightforward to apply this method. See Section 3 for a description of our
proof strategy.

The rest of the paper is structured as follows. Section 2 introduces basic
notions for display calculus and the display calculi for normal modal logic
$\mathrm{K}$ and the basic temporal logic $\mathrm{Kt}$. Section 3 describes
the strategy for proving decidability. Each of Sections 4, 5 and 6 proves a
property mentioned in the strategy. Section 7 proves the decidability of
display calculus $\mathrm{D.K}$. Section 8 proves the decidability of some
extensions of $\mathrm{D.K}$. Section 9 concludes the paper.

##  2 Preliminareis

Modal logics and temporal logics are the main objects in this paper. The
language for modal logics is an extension of that for propositional logic with
modalities $\Box$ and $\Diamond$ and the language for temporal logics builds
on this by adding $\blacksquare$ and $\blacklozenge$. It is _structures_ , not
formulas, that are manipulated in display calculus. Therefore, structural
operators are needed. Following [8], we use $\mathrm{I}$ for $\top$ and
$\bot$, $\circ$ for conjunction and disjunction and $\bullet$ for modalities.
Here, ‘a structural operator (like $\mathrm{I}$) for a logical connective
(like $\top$ and $\bot$)’ means that there are rules in the display calculi
that transforms the structural operator to the logical connectives. This
sections gives the basic notions relating to language, structures and
sequents.

###  2.1 Language, structures, and sequents

_Language._ Given a set $\mathrm{Prop}$ of propositional letters, language
$\mathcal{L}$ is defined recursively as follows:

$\mathcal{L}::=p\mid\top\mid\bot\mid\neg\varphi\mid(\varphi\land\varphi)\mid(\varphi\lor\varphi)\mid(\varphi\to\varphi)\mid\Box\varphi\mid\blacksquare\varphi\mid\Diamond\varphi\mid\blacklozenge\varphi$

where $p\in\mathrm{Prop}$.

_Structures._ The set $\mathrm{Str}$ of structures is defined recursively as
follows:

$\mathrm{Str}::=\varphi\mid\mathrm{I}\mid(X\circ X)\mid\ast X\mid\bullet X$

where $\varphi\in\mathcal{L}$.

The outset parentheses may be omitted when no confusion arises.

If structure $X$ is a formula or $\mathrm{I}$, then $X$ is called an _atomic
structure_. For any sequent $\mathcal{S}$, denote by $At(\mathcal{S})$ the set
of atomic substructures in $\mathcal{S}$.

For a structure $X$, the set $Sub(X)$ of _substructures_ of $X$ is defined
recursively as follows:

$\displaystyle Sub(\mathrm{I})=\\{\mathrm{I}\\}$ $\displaystyle
Sub(\varphi)=\\{\varphi\\}$ $\displaystyle Sub(X\circ Y)=Sub(X)\cup Sub(Y)$
$\displaystyle Sub(\ast X)=\\{\ast X\\}\cup Sub(X)$ $\displaystyle Sub(\bullet
X)=\\{\bullet X\\}\cup Sub(X)$

_Sequents._ A _sequent_ is of the form $X\Rightarrow Y$, where
$X,Y\in\mathrm{Str}$. $X$ is called the _antecedent_ and $Y$ is called the
_succedent_ of $X\Rightarrow Y$. We call $Z$ a _substructure_ of $X\Rightarrow
Y$ if $Z\in Sub(X)\cup Sub(Y)$.

A substructure $Z$ of $X\Rightarrow Y$ is called an _antecedent part_ of
$X\Rightarrow Y$ if it is in the scope of an even number of $\ast$ and a
_succedent part_ of $X\Rightarrow Y$ if it is in the scope of an odd number of
$\ast$.

For any structure, the _length_ $l(X)$ of a structure $X$ is defined
recursively as follows:

$\displaystyle l(p)=l(\top)=l(\bot)=1$ $\displaystyle
l(\varphi\land\psi)=l(\varphi\lor\psi)=l(\varphi\to\psi)=l(\varphi)+l(\psi)$
$\displaystyle
l(\neg\varphi)=l(\Box\varphi)=l(\blacksquare\varphi)=l(\Diamond\varphi)=l(\blacklozenge\varphi)=l(\varphi)+1$
$\displaystyle l(\mathrm{I})=1$ $\displaystyle l(X\circ Y)=l(X)+l(Y)$
$\displaystyle l(\ast X)=l(\bullet X)=l(X)+1$

For any sequent $X\Rightarrow Y$, the _length_ $l(X\Rightarrow Y)$ of
$X\Rightarrow Y$ is $l(X)+l(Y)$.

The following proposition about the possibilities of being a substructure is
straightforward.

###### Proposition 1

Let $X\Rightarrow Y$ be a sequent and $Z$ a substructure of $X\Rightarrow Y$.
Then one of the following conditions hold:

  1. (1)

$X\Rightarrow Y$ contains $W\circ\star Z$ or $\star Z\circ W$ as a
substructure.

  2. (2)

$X\Rightarrow Y$ is $\star Z\Rightarrow Y$ or $X\Rightarrow\star Z$.

where $W$ is a structure and $\star$ is a sequence of $\ast$ and $\bullet$.

For a substructure $Z$ of $X\Rightarrow Y$, if item (1) in Proposition 1
holds, then we call $Z$ a _dependent substructure_ of $X\Rightarrow Y$.
Otherwise, we call it an _independent substructure_ of $X\Rightarrow Y$. For
example, if $Z$ is a dependent substructure of $X\Rightarrow Y$, then
$X\Rightarrow Y$ is $(X\Rightarrow Y)[\star Z\circ W]$ or $(X\Rightarrow
Y)[W\circ\star Z]$, where $W$ is a structure and $\star$ is sequence of $\ast$
and $\bullet$.

Substructures $Z_{1}$ and $Z_{2}$ of $X$ are called _distinct_ if neither
$Z_{1}$ is a substructure of $Z_{2}$ nor $Z_{2}$ is a substructure of $Z_{1}$.

Given a structure $X$, the notation $X[Z]$ means that $Z$ is a substructure of
$X$. Similarly, given a sequent $X\Rightarrow Y$, the notation $(X\Rightarrow
Y)[Z]$ means that $Z$ is a substructure of $X$ or $Y$. We denote by
$(X\Rightarrow Y)[W\backslash Z]$ the sequent obtained by substituting the
exhibited occurrence of $Z$ by $W$444Therefore, $(X\Rightarrow Y)[W\backslash
Z]$ means a single substitution and is different from the common uniform
substitution in logic.. More generally, notation $X[Z_{1},\ldots,Z_{n}]$ means
that $Z_{1},\ldots,Z_{n}$ are distinct substructures of $X$ and
$X[Z_{1},\ldots,W\backslash Z_{i},\ldots,Z_{n}]$ denotes the sequent obtained
by substituting the exhibited $Z_{i}$ with $W$.

_Display calculi._ A _sequent rule_ is of the form

$(\mathcal{R})\frac{X_{1}\Rightarrow Y_{1}\ldots X_{m}\Rightarrow
Y_{m}}{X\Rightarrow Y}$

where $m\geq 0$. $X_{1}\Rightarrow Y_{1},\ldots,X_{m}\Rightarrow Y_{m}$ are
called the _premises_ of this rule and $X\Rightarrow Y$ is called the
conclusion. If $m=0$, we simply write $X\Rightarrow Y$ and call it an _initial
sequent_.

A display calculus is a set of sequent rules. A _proof_ in a display calculus
$\mathrm{D}$ is a tree of sequents such that each leaf is an initial sequent
and that for each node $X\Rightarrow Y$ and its children nodes
$X_{1}\Rightarrow Y_{1},\ldots,X_{m}\Rightarrow Y_{m}$,
$\frac{X_{1}\Rightarrow Y_{1},\ldots,X_{m}\Rightarrow Y_{m}}{X\Rightarrow Y}$
is an instance of a rule in $\mathrm{D}$.

We use

$X\Rightarrow Y$ $X^{\prime}\Rightarrow Y^{\prime}$

as a shorthand for

$\frac{X\Rightarrow Y}{X^{\prime}\Rightarrow
Y^{\prime}}\quad\text{~{}and~{}}\quad\frac{X^{\prime}\Rightarrow
Y^{\prime}}{X\Rightarrow Y}$

The notation $\mathrm{D}\vdash X\Rightarrow Y$ means that there is a proof for
$X\Rightarrow Y$ in $\mathrm{D}$.

A sequent rule $\mathcal{R}$ is _admissible_ in $\mathrm{D}$ if
$\mathrm{D}\vdash X_{i}\Rightarrow Y_{i}$ for $1\leq i\leq m$ implies
$\mathrm{D}\vdash X\Rightarrow Y$.

A display calculus $\mathrm{D}$ is said to be _cut eliminable_ if the cut rule
is admissible in the calculus obtained by removing the cut rule from
$\mathrm{D}$.

###  2.2 Display calculus $\mathrm{D.K}$ and $\mathrm{D.Kt}$

This subsection introduces the display calculus $\mathrm{D.K}$ for the
smallest normal modal logic $\mathrm{K}$. It is taken from [8], but the
notation is a bit different. We refer the reader to that paper for a detailed
discussion.

The display calculus $\mathrm{D.K}$ consists of $(Id)$, $(Cut)$, _display
rules_ , _connective rules_ and _structural rules_.

$(Id)$ and $(Cut)$ are as follows:

$(Id)~{}p\Rightarrow
p\quad(Cut)\frac{X\Rightarrow\varphi\quad\varphi\Rightarrow Y}{X\Rightarrow
Y}$

The display rules are as follows:

$X\circ Y\Rightarrow Z$ $(\Rightarrow\ast 1)$ $X\Rightarrow Z\circ\ast Y$ |  $X\circ Y\Rightarrow Z$ $(\Rightarrow\ast 2)$ $Y\Rightarrow\ast X\circ Z$
---|---
$X\Rightarrow Y\circ Z$ $(\ast\Rightarrow 1)$ $X\circ\ast Z\Rightarrow Y$ |  $X\Rightarrow Y\circ Z$ $(\ast\Rightarrow 2)$ $\ast Y\circ X\Rightarrow Z$
$\ast X\Rightarrow Y$ $(\ast\Rightarrow)$ $\ast Y\Rightarrow X$ |  $X\Rightarrow\ast Y$ $(\Rightarrow\ast)$ $Y\Rightarrow\ast X$
$\ast\ast X\Rightarrow Y$ $(\ast\ast\Rightarrow)$ $X\Rightarrow Y$ |  $X\Rightarrow\ast\ast Y$ $(\Rightarrow\ast\ast)$ $X\Rightarrow Y$
$X\Rightarrow\bullet Y$ $(\Rightarrow\bullet)$ $\bullet X\Rightarrow Y$ |

The connective rules are the following:

$(\Rightarrow\top)$ $\mathrm{I}\Rightarrow\top$ |  $(\top\Rightarrow)$ $\mathrm{I}\Rightarrow X$ $\top\Rightarrow X$
---|---
$(\Rightarrow\bot)$ $X\Rightarrow\mathrm{I}$ $X\Rightarrow\bot$ |  $(\bot\Rightarrow)$ $\bot\Rightarrow\mathrm{I}$
$(\Rightarrow\neg)$ $X\Rightarrow\ast\varphi$ $X\Rightarrow\neg\varphi$ |  $(\neg\Rightarrow)$ $\ast\varphi\Rightarrow X$ $\neg\varphi\Rightarrow X$
$(\Rightarrow\land)$ $X\Rightarrow\varphi$ $Y\Rightarrow\psi$ $X\circ Y\Rightarrow\varphi\land\psi$ |  $(\land\Rightarrow)$ $\varphi\circ\psi\Rightarrow X$ $\varphi\land\psi\Rightarrow X$
$(\Rightarrow\lor)$ $X\Rightarrow\varphi\circ\psi$ $X\Rightarrow\varphi\lor\psi$ |  $(\lor\Rightarrow)$ $\varphi\Rightarrow X$ $\psi\Rightarrow Y$ $\varphi\lor\psi\Rightarrow X\circ Y$
$(\Rightarrow\to)$ $X\circ\varphi\Rightarrow\psi$ $X\Rightarrow\varphi\to\psi$ |  $(\to\Rightarrow)$ $X\Rightarrow\varphi$ $\psi\Rightarrow Y$ $\varphi\to\psi\Rightarrow\ast X\circ Y$
$(\Rightarrow\Box)$ $\bullet X\Rightarrow\varphi$ $X\Rightarrow\Box\varphi$ |  $(\Box\Rightarrow)$ $\varphi\Rightarrow X$ $\Box\varphi\Rightarrow\bullet X$
$(\Rightarrow\Diamond)$ $X\Rightarrow\varphi$ $\ast\bullet\ast X\Rightarrow\Diamond\varphi$ |  $(\Diamond\Rightarrow)$ $\ast\bullet\ast\varphi\Rightarrow X$ $\Diamond\varphi\Rightarrow X$

The structural rules in $\mathrm{D.K}$ are in Figure 1. The display calculus
$\mathrm{D.Kt}$ for the minimal temporal logic $\mathrm{Kt}$ is obtained by
adding to $\mathrm{D.K}$ the following rules:

$(\blacksquare\Rightarrow)$ $\varphi\Rightarrow X$ $\blacksquare\varphi\Rightarrow\ast\bullet\ast X$ |  $(\Rightarrow\blacksquare)$ $X\Rightarrow\ast\bullet\ast\varphi$ $X\Rightarrow\blacksquare\varphi$
---|---
$(\blacklozenge\Rightarrow)$ $\varphi\Rightarrow\bullet X$ $\blacklozenge\varphi\Rightarrow X$ |  $(\Rightarrow\blacklozenge)$ $X\Rightarrow\varphi$ $\bullet X\Rightarrow\blacklozenge\varphi$

$(Al)$ $X_{1}\circ(X_{2}\circ X_{3})\Rightarrow Z$ $(X_{1}\circ X_{2})\circ X_{3}\Rightarrow Z$ |  $(Ar)$ $Z\Rightarrow X_{1}\circ(X_{2}\circ X_{3})$ $Z\Rightarrow(X_{1}\circ X_{2})\circ X_{3}$
---|---
$(Pl)$ $X\circ Y\Rightarrow Z$ $Y\circ X\Rightarrow Z$ |  $(Pr)$ $Z\Rightarrow X\circ Y$ $Z\Rightarrow Y\circ X$
$(Ql)$ $\mathrm{I}\Rightarrow Y$ $\ast\mathrm{I}\Rightarrow Y$ |  $(Qr)$ $X\Rightarrow\mathrm{I}$ $X\Rightarrow\ast\mathrm{I}$
$(\mathrm{I}l)$ $X\Rightarrow Z$ $\mathrm{I}\circ X\Rightarrow Z$ |  $(\mathrm{I}r)$ $X\Rightarrow Z$ $X\Rightarrow\mathrm{I}\circ Z$
$(Wl)$ $X\Rightarrow Z$ $Y\circ X\Rightarrow Z$ |  $(Wr)$ $X\Rightarrow Z$ $X\Rightarrow Z\circ Y$
$(Cl)$ $X\circ X\Rightarrow Z$ $X\Rightarrow Z$ |  $(Cr)$ $Z\Rightarrow X\circ X$ $Z\Rightarrow X$
$(Ml)$ $\mathrm{I}\Rightarrow Y$ $\bullet\mathrm{I}\Rightarrow Y$ |  $(Mr)$ $X\Rightarrow\mathrm{I}$ $X\Rightarrow\bullet\mathrm{I}$
Figure 1: The structural rules in $\mathrm{D.K}$

For sequents $\mathcal{S}$ and $\mathcal{S}^{\prime}$, $\mathcal{S}$ and
$\mathcal{S}^{\prime}$ are said to be _displayablely equivalent_ in
$\mathrm{D.K}$ if $\mathcal{S}$ and $\mathcal{S}^{\prime}$ are inter-provable
with only display rules in $\mathrm{D.K}$.

######  Theorem 2.1 (Display Theorem)

For every sequent $\mathcal{S}$ and every antecedent (succedent) part $W$ of
$\mathcal{S}$, there is a displayablely equivalent $\mathcal{S}^{\prime}$ such
that $W$ is the antecedent (succedent) of $\mathcal{S}^{\prime}$ in
$\mathrm{D.K}$ and $\mathrm{D.Kt}$.

###### Proof

See Theorem 1 in [8]. Note that only display rules are needed to prove the
theorem.

Denote by $\mathrm{D.K}^{-}$ the calculus obtained by removing the cut rule
from $\mathrm{D.K}$.

######  Theorem 2.2 (Cut Elimination)

$\mathrm{D.K}$ and $\mathrm{D.Kt}$ are cut eliminable.

###### Proof

See Theorem 11 in [8].

##  3 Poof strategy

A display calculus $\mathrm{D}$ is said to be _decidable_ , if for any formula
$\varphi$, there exists an algorithm that can decide whether $\varphi$ is
provable in $\mathrm{D}$ or not. The following sections show that
$\mathrm{D.K}$ is decidable.

To this aim, by Theorem 2.2, it suffices to show that $\mathrm{D.K}^{-}$ is
decidable. The proof strategy is as follows:

  1. (1)

First, we show that in an ‘equivalent’ variant $\mathrm{D.K}^{-}_{\ast}$
(defined in the next section) of $\mathrm{D.K}^{-}$, any provable sequent in
$\mathrm{D.K}^{-}_{\ast}$ has an _$\ast$ -reduced_, _$3$ -reduced_,
_irredundant_ , _r-complexity-increasing_ proof satisfying the _subformula
property_.

  2. (2)

Then we show that for any sequent, the search space for possible such proofs
in $\mathrm{D.K}^{-}_{\ast}$ is finite. Therefore, $\mathrm{D.K}^{-}_{\ast}$
is decidable. Since $\mathrm{D.K}^{-}$ is ‘equivalent’ to
$\mathrm{D.K}^{-}_{\ast}$, $\mathrm{D.K}^{-}$ is decidable.

The idea behind $\ast$-reduced proofs is to avoid the infinite searching
caused by $(\ast\ast\Rightarrow)$ and $(\Rightarrow\ast\ast)$ which requires
that no consecutive occurrences of $\ast$ should appear in such proofs.

The notion of $3$-reduced proofs requires that the same structures occurs at
most $3$ times in a sequent. It deals with $(Cl)$, $(Cr)$, $(Il)$ and $(Ir)$
and restricts the number of applications of these rules in proof searching.
Readers familiar with Gentzen’s sequent calculi will soon realize that the
same problem also occurs in proving the decidability of Gentzen’s sequent
calculi: the contraction rules delete repetitive information when they are
applied, and lead to infinite searching when they are applied bottom-up to
search for possible proofs. For sequent calculi, it is easy to recognize
repetitive information because one just needs to check whether there are
occurrences of the same formula separated by the only structural operator, the
comma. Display calculi have one binary structural operator $\circ$, and two
unary structural operators $\ast$ and $\bullet$ and contain bi-directional
rules which allow us to transform sequents equivalently. As a result, some
repetitive occurrences of information no longer appear side-by-side and this
makes it more difficult to recognize them. The key idea to restricting the
applications of contractions rules is the same in sequent calculi and display
calculi, but more work needs to done in the latter.

Irredundant proofs are those do not contain repetitive occurrences of a
sequent. Any redundant proof can be transformed into an irredundant one by
deleting the sequents between the repetitive occurrences.

The property of being r-complexity-increasing captures what increases from
leaves to the root in a proof. Such a quantitative property can help us know
when to stop in proof searching.

A proof with subformula property is one such that each sequent in the proof is
contains only subformulas in the endsequent.

Now come back to our proof strategy. For any sequent $\mathcal{S}$, denote by
$\Gamma^{3}_{\mathcal{S}}$ the set of $\ast$-reduced and $3$-reduced sequents
made of subformuals in $\mathcal{S}$, and with $r$-complexity less than or
equal to $\mathcal{S}$. To show that $\mathrm{D.K}^{-}_{\ast}$ is decidable,
it suffices to show that $\Gamma^{3}_{\mathcal{S}}$ is finite. And this is
proved by showing that $\Gamma^{3}_{\mathcal{S}}$ is a subset of another
finite set (see Definition 13).

##  4 $\mathrm{D.K}^{-}_{\ast}$ and $\ast$-reduced proofs

This section introduces display calculus $\mathrm{D.K}^{-}_{\ast}$. For any
sequent $\mathcal{S}$, its provability in $\mathrm{D.K}$ is the same as its
_$\ast$ -reduced_ conterpart in $\mathrm{D.K}^{-}_{\ast}$. Before proving this
result, we introduce the notion of $\ast$-reduced sequents and proofs.

###### Definition 1

A structure is called _$\ast$ -reduced_ if it does not contain $\ast\ast$. A
sequent is called _$\ast$ -reduced_ if every substructure in it is
$\ast$-reduced. A proof is called _$\ast$ -reduced_ if each sequent in it is
$\ast$-reduced.

For any structure $X$, denote by $\tau_{\ast}(X)$ the structure obtained by
deleting each occurrence of $\ast\ast$ in $X$. Equivalently, $\tau_{\ast}(X)$
can be defined inductively as follows:

$\displaystyle\tau_{\ast}(\varphi)=\varphi$ $\displaystyle\tau_{\ast}(\bullet
X)=\bullet\tau_{\ast}(X)$ $\displaystyle\tau_{\ast}(X\circ
Y)=\tau_{\ast}(X)\circ\tau_{\ast}(Y)$ $\displaystyle\tau_{\ast}(\ast\ast
X)=\tau_{\ast}(X)$ $\displaystyle\tau_{\ast}(\ast\bullet
X)=\ast\bullet\tau_{\ast}(X)$ $\displaystyle\tau_{\ast}(\ast(X\circ
Y))=\ast(\tau_{\ast}(X)\circ\tau_{\ast}(Y))$

For any sequent $\mathcal{S}$, denote by $\tau_{\ast}(\mathcal{S})$ the
sequent obtained by deleting each occurrence of $\ast\ast$ in $\mathcal{S}$.

###### Definition 2

Display calculus $\mathrm{D.K}^{-}_{\ast}$ is obtained from $\mathrm{D.K}^{-}$
by deleting $(\ast\ast\Rightarrow)$ and $(\Rightarrow\ast\ast)$, restricting
$(Wl)$ and $(Wr)$ to adding $\ast$-reduced structures, and replacing
$(\to\Rightarrow)$, $(\Rightarrow\ast 1)$, $(\Rightarrow\ast 2)$,
$(\ast\Rightarrow 1)$ and $(\ast\Rightarrow 2)$ in $\mathrm{D.K}^{-}$ with the
following rules, respectively:

$(\to\Rightarrow^{\prime})\frac{X\Rightarrow\varphi\quad\psi\Rightarrow Y}{\varphi\to\psi\Rightarrow\overline{X}\circ Y}$ $X\circ Y\Rightarrow Z$ $(\Rightarrow\ast 1^{\prime})$ $X\Rightarrow Z\circ\overline{Y}$ |  $X\circ Y\Rightarrow Z$ $(\Rightarrow\ast 2^{\prime})$ $Y\Rightarrow\overline{X}\circ Z$
---|---
$X\Rightarrow Y\circ Z$ $(\ast\Rightarrow 1^{\prime})$ $X\circ\overline{Z}\Rightarrow Y$ |  $X\Rightarrow Y\circ Z$ $(\ast\Rightarrow 2^{\prime})$ $\overline{Y}\circ X\Rightarrow Z$

where $\overline{X}$ is $X^{\prime}$ if $X$ is of the form $\ast X^{\prime}$
and is $\ast X$ otherwise.

Being $\ast$-reduced is the first requirement for sequents in finite proof
searching. This concept and the new display rules in $\mathrm{D.K}^{-}_{\ast}$
aim to deal with the infinite search space caused by display rules concerning
$\ast$ in $\mathrm{D.K}^{-}$.

The following result follows immediately from the forms of rules in
$\mathrm{D.K}^{-}_{\ast}$:

###### Lemma 1

Each proof in $\mathrm{D.K}^{-}_{\ast}$ is a $\ast$-reduced proof.

Next we prove two lemmas and then the key result of this section: the
provability of a sequent in $\mathrm{D.K}^{-}$ is the same as its
$\ast$-reduced counterpart in $\mathrm{D.K}^{-}_{\ast}$

###### Lemma 2

For any sequent $\mathcal{S}$, if $\mathrm{D.K}^{-}_{\ast}\vdash\mathcal{S}$,
then $\mathrm{D.K}^{-}\vdash\mathcal{S}$.

###### Proof

It suffices to show that $(\to\Rightarrow^{\prime})$, $(\Rightarrow\ast
1^{\prime})$, $(\Rightarrow\ast 2^{\prime})$, $(\ast\Rightarrow 1^{\prime})$
and $(\ast\Rightarrow 2^{\prime})$ are admissible in $\mathrm{D.K}^{-}$. We
only show the top-to-bottom direction of $(\to\Rightarrow^{\prime})$ is
admissible in $\mathrm{D.K}^{-}$. Other cases can be proved in a similar way.

Assume that $\mathrm{D.K}^{-}_{\ast}\vdash X\Rightarrow\varphi$ and
$\mathrm{D.K}^{-}_{\ast}\vdash\psi\Rightarrow Y$. If $X$ is of the form $\ast
X^{\prime}$, then $\overline{X}=X^{\prime}$. A proof of
$\varphi\to\psi\Rightarrow X^{\prime}\circ Y$ in $\mathrm{D.K}^{-}$ is as
follows:

$\ast X^{\prime}\Rightarrow\varphi$ $\psi\Rightarrow Y$ $(\to\Rightarrow)$
$\varphi\to\psi\Rightarrow\ast\ast X^{\prime}\circ Y$ $(\ast\Rightarrow 1)$
$(\varphi\to\psi)\circ\ast Y\Rightarrow\ast\ast X^{\prime}$
$(\Rightarrow\ast\ast)$ $(\varphi\to\psi)\circ\ast Y\Rightarrow X^{\prime}$
$(\ast\Rightarrow 1)$ $\varphi\to\psi\Rightarrow X^{\prime}\circ Y$

If $X$ is not of the form $\ast X^{\prime}$, then $\overline{X}=\ast X$. Then
$\varphi\to\psi\Rightarrow\ast X\circ Y$ can be obtained by an application of
$(\to\Rightarrow)$.

###### Lemma 3

For any sequent $X\Rightarrow Y$,

  1. (1)

$\mathrm{D.K}^{-}\vdash X\Rightarrow Y$ iff
$\mathrm{D.K}^{-}\vdash\tau_{\ast}(X)\Rightarrow Y$.

  2. (2)

$\mathrm{D.K}^{-}\vdash Y\Rightarrow X$ iff $\mathrm{D.K}^{-}\vdash
Y\Rightarrow\tau_{\ast}(X)$.

###### Proof

We prove these claims simultaneously by induction on the length
$l(\tau_{\ast}(X))$ of $\tau_{\ast}(X)$.

If $l(\tau_{\ast}(X))=1$, then $\tau_{\ast}(X)=p$ for some propositional
letter $p$ and $X=\star p$, where $\star$ is an even number of $\ast$. The
claims follow from applications of $(\ast\ast\Rightarrow)$ and
$(\Rightarrow\ast\ast)$.

If $l(\tau_{\ast}(X))>1$, we use display rules to display the direct
substructure $\tau_{\ast}(X)$ and apply the induction hypothesis. For example,
Iif $\tau_{\ast}(X)=\tau_{\ast}(X_{1})\circ\tau_{\ast}(X_{2})$, then we use
$(\Rightarrow\ast 1)$ and $(\Rightarrow\ast 2)$ and the induction hypothesis.

$X_{1}\circ X_{2}\Rightarrow Y$ $(\Rightarrow\ast 1)$ $X_{1}\Rightarrow
Y\circ\ast X_{2}$ $(I.H.)$ $\tau_{\ast}(X_{1})\Rightarrow Y\circ\ast X_{2}$
$(\Rightarrow\ast 1)$ $\tau_{\ast}(X_{1})\circ X_{2}\Rightarrow Y$
$(\Rightarrow\ast 2)$ $X_{2}\Rightarrow\ast\tau_{\ast}(X_{1})\circ Y$ $(I.H.)$
$\tau_{\ast}(X_{2})\Rightarrow\ast\tau_{\ast}(X_{1})\circ Y$ $(\Rightarrow\ast
2)$ $\tau_{\ast}(X_{1})\circ\tau_{\ast}(X_{2})\Rightarrow Y$

A proof from $\tau_{\ast}(X_{1})\circ\tau_{\ast}(X_{2})\Rightarrow Y$ to
$X_{1}\circ X_{2}\Rightarrow Y$ is obtained by reversing the above proof.

###### Proposition 2

For any sequent $\mathcal{S}$, $\mathrm{D.K}^{-}\vdash\mathcal{S}$ iff
$\mathrm{D.K}^{-}_{\ast}\vdash\tau_{\ast}(\mathcal{S})$.

###### Proof

For the left-to-right direction, assume that $\mathcal{S}$ is derivable in
$\mathrm{D.K}^{-}$ with a proof of height $h$. We prove by induction on $h$.

If $h=1$, $\mathcal{S}$ is an instance of $(Id)$. So is
$\tau_{\ast}(\mathcal{S})$.

If $h>1$, let the last rule applied be $\mathcal{R}$.

If $\mathcal{R}$ is not $(\ast\ast\Rightarrow)$, $(\Rightarrow\ast\ast)$,
$(Wl)$, $(Wr)$, $(\to\Rightarrow)$, $(\Rightarrow\ast 1)$, $(\Rightarrow\ast
2)$, $(\ast\Rightarrow 1)$ or $(\ast\Rightarrow 2)$, then we apply the
induction hypothesis to the premise(s) of $\mathcal{R}$ and then apply
$\mathcal{R}$.

If $\mathcal{R}$ is $(\to\Rightarrow)$, $(\Rightarrow\ast 1)$,
$(\Rightarrow\ast 2)$, $(\ast\Rightarrow 1)$ or $(\ast\Rightarrow 2)$, then
$\mathcal{R}$ is not a rule in $\mathrm{D.K}^{-}_{\ast}$. But we can use
$\mathcal{R}^{\prime}$ in $\mathrm{D.K}^{-}_{\ast}$. For example, if
$\mathcal{R}$ is $(\to\Rightarrow)$, then the proof ends with

$\frac{X\Rightarrow\varphi\quad\psi\Rightarrow
Y}{\varphi\to\psi\Rightarrow\ast{X}\circ Y}(\to\Rightarrow)$

By the induction hypothesis,
$\mathrm{D.K}^{-}_{\ast}\vdash\tau_{\ast}(X)\Rightarrow\varphi$ and
$\mathrm{D.K}^{-}_{\ast}\vdash\psi\Rightarrow\tau_{\ast}(Y)$. Then by
$(\to\Rightarrow^{\prime})$,
$\mathrm{D.K}^{-}_{\ast}\vdash\varphi\to\psi\Rightarrow\overline{\tau_{\ast}(X)}\circ\tau_{\ast}(Y)$.
Since $\overline{\tau_{\ast}(X)}=\tau_{\ast}(\ast X)$,
$\mathrm{D.K}^{-}_{\ast}\vdash\varphi\to\psi\Rightarrow\tau_{\ast}(\ast
X)\circ\tau_{\ast}(Y)$, as required. Note that the proof uses equation
$\overline{\tau_{\ast}(X)}=\tau_{\ast}(\ast X)$.

If $\mathcal{R}$ is $(Wl)$ or $(Wr)$, let the newly added structure be $W$.
Then we add $\tau_{\ast}(W)$ instead, where $\tau_{\ast}(W)$ is the structure
obtained by deleting $\ast\ast$ in $W$.

If $\mathcal{R}$ is $(\ast\ast\Rightarrow)$ or $(\Rightarrow\ast\ast)$, then
the sequent obtained by applying the induction hypothesis to the premise is
the required sequent.

For the right-to-left direction, assume that
$\mathrm{D.K}^{-}_{\ast}\vdash\tau_{\ast}(\mathcal{S})$. By Lemma 2,
$\mathrm{D.K}^{-}\vdash\tau_{\ast}(\mathcal{S})$. By Lemma 3,
$\mathrm{D.K}^{-}\vdash\mathcal{S}$.

##  5 $n$-reduced proofs in $\mathrm{D.K}^{-}_{\ast}$

This section shows that the provability of a sequent is the same as its
_3-reduced_ counterpart in $\mathrm{D.K}^{-}_{\ast}$, in which the number of
repetitive substructures and $\mathrm{I}$ is restricted. Being 3-reduced is
the second requirement for sequents in finite proof searching. This concept
aims to deal with the infinite search space caused by ($\mathrm{I}$l),
($\mathrm{I}$r), (Cl) and (Cr) in $\mathrm{D.K}^{-}_{\ast}$.

Repetitive substructures also occur in Gentzen’s sequent. Take
$\varphi,\varphi,\Gamma\Rightarrow\Delta$ as an example, in which $\varphi$
occurs twice. Situations in display calculi are more complicated because
display rules allow certain structures and structural operators to move freely
from one side of $\Rightarrow$ to the other which may make repetitive
substructures difficult to be recognized. Therefore, a notion of _equivalence_
dissolving such movements is important for repetitive substructures
recognition.

###  5.1 Equivalent sequents

First let us analyze a set of rules in $\mathrm{D.K}^{-}_{\ast}$. Let $\Omega$
be the set of display rules, (Al), (Ar), (Pl) and (Pr) in
$\mathrm{D.K}^{-}_{\ast}$. $\Omega$ satisfies the following properties: each
rule in $\Omega$ has one premise; if
$\frac{\mathcal{S}}{\mathcal{S}^{\prime}}$ is an instance of a rule in
$\Omega$, so is $\frac{\mathcal{S}^{\prime}}{\mathcal{S}}$. It follows that if
$\mathcal{D}$ is a proof from $\mathcal{S}$ to $\mathcal{S}^{\prime}$ with
only rules in $\Omega$, then the proof obtained by reversing $\mathcal{D}$ is
a proof from $\mathcal{S}^{\prime}$ to $\mathcal{S}$ with only rules in
$\Omega$.

In addition, each rule in $\Omega$ is _atomicity-preserving_ , defined as
follows:

###### Definition 3

Let $\mathcal{R}=\frac{\mathcal{S}_{1},\ldots,\mathcal{S}_{n}}{\mathcal{S}}$
be a sequent rule. $\mathcal{R}$ is called _atomicity-preserving_ if

  1. (1)

For any instance of $\mathcal{R}$, $At(\mathcal{S}_{1})\cup\ldots\cup
At(\mathcal{S}_{n})=At(\mathcal{S})$, where $At(\mathcal{S}^{\prime})$ is the
set of atomic substructures in $\mathcal{S}^{\prime}$ for any sequent
$\mathcal{S}^{\prime}$.

  2. (2)

$\mathcal{R}$ is closed under _single atomic substitution_. That is, For any
instance
$\frac{\mathcal{S}_{1}\ldots\mathcal{S}_{i}[Z]\ldots\mathcal{S}_{n}}{\mathcal{S}[Z]}$
of $\mathcal{R}$, any atomic substructure $Z$ of $\mathcal{S}_{i}(1\leq i\leq
n)$ and any structure $W$,

$\frac{\mathcal{S}_{1}\ldots\mathcal{S}_{i}[W\backslash
Z]\ldots\mathcal{S}_{n}}{\mathcal{S}[W\backslash Z]}$

is also an instance of $\mathcal{R}$.

Condition (1) means that no atomic structure is introduced or removed an by
application of $\mathcal{R}$.

The rules in $\mathrm{D.K}^{-}_{\ast}$ other than the rules in $\Omega$ are
not atomicity-preserving.

By the above properties of $\Omega$, we define the notion of _sequent
equivalence_ :

###### Definition 4

Sequents $\mathcal{S}$ and $\mathcal{S}^{\prime}$ are called _equivalent_ if
$\mathcal{S}^{\prime}$ can be derived from $\mathcal{S}$ with only rules in
$\Omega$, which consists of display rules, ($Al$), ($Ar$), ($Pl$) and ($Pr$).

Equivalent sequents can be thought of as one sentences said in different ways.
For example, “Today is sunny” is another way of saying “It is sunny today”.
They expresses the same information.

The notion of sequent equivalence is different from the notion of inter-
provability in our setting. Since the intuition we want to characterize is the
free movement of certain structures and structural operators, the requirement
of being atomicity-preserving is added. This is the reason why $(\mathrm{I}l)$
and $(\mathrm{I}r)$ are excluded from $\Omega$.

The following proposition is straightforward:

###### Proposition 3

For any sequents
$\mathcal{S},\mathcal{S}^{\prime},\mathcal{S}^{\prime\prime}$,

  1. (1)

$\mathcal{S}$ is equivalent to itself.

  2. (2)

If $\mathcal{S}$ is equivalent to $\mathcal{S}^{\prime}$, then
$\mathcal{S}^{\prime}$ is equivalent to $\mathcal{S}$.

  3. (3)

If $\mathcal{S}$ is equivalent to $\mathcal{S}^{\prime}$ and
$\mathcal{S}^{\prime}$ is equivalent to $\mathcal{S^{\prime\prime}}$, then
$\mathcal{S}$ is equivalent to $\mathcal{S}^{\prime\prime}$.

Equivalent sequents has the following property: if the same substitution of an
atomic substructure is applied to equivalent sequents, then the resulting
sequents are still equivalent .

###### Proposition 4

Let $\mathcal{S}$ and $\mathcal{S}^{\prime}$ be equivalent sequents and $Z$ an
atomic substructure of $\mathcal{S}$. Then $Z$ is an atomic substructure of
$\mathcal{S}^{\prime}$ and $\mathcal{S}[W\backslash Z]$ and
$\mathcal{S}^{\prime}[W\backslash Z]$ are equivalent for any structure $W$.

###### Proof

It follows from the fact that each rule in $\Omega$ is atomicity-preserving.

###  5.2 Superfluous substructures, superfluous $\mathrm{I}$ and reduced
sequents

A substructure may appear more than once in a sequent. In a proof, the
repetition of some substructures may be redundant. The idea is captured by the
following definition, which is based on the notion of sequent equivalence.

######  Definition 5 (Superfluous substructures)

In any sequent $X\Rightarrow Y$, two occurrences $Z_{(1)}$ and $Z_{(2)}$ of
substructure $Z$ are said to be _matching_ if $X\Rightarrow Y$ is equivalent
to $Z_{(1)}\circ Z_{(2)}\Rightarrow W$ or $W\Rightarrow Z_{(1)}\circ Z_{(2)}$,
where $W$ is a structure. If $X\Rightarrow Y$ contains at least two matching
occurrences of $Z$, we say that $Z$ is _superfluous_ in $X\Rightarrow Y$.

The following lemma tells us that if $Z$ is a superfluous substructure in
$X\Rightarrow Y$, then the matching occurrences of $Z$ are not ‘separated’ by
$\bullet$.

###### Lemma 4

Let $Z$ be a superfluous substructure in $X\Rightarrow Y$ and $Z_{(i)}$ one of
the matching occurrences of $Z$ in $X\Rightarrow Y$. Then the any substructure
in $X\Rightarrow Y$ which contains $Z_{(i)}$ and does not contain another
occurrence of $Z$ is of the form $\ast^{n}W[Z_{(i)}]$, where $\ast^{n}$ is a
sequence of $n$ $\bullet$’s for some $n\in\mathbb{N}$.

###### Proof

We prove by contradiction and assume that there is a substructure in
$X\Rightarrow Y$ which contains $Z_{(i)}$ and does not contain another
occurrence of $Z$ is of the form $\star_{1}\bullet\star_{2}W[Z_{(i)}]$ where
$\star_{1}$ and $\star_{2}$ are sequences of $\ast$ and $\bullet$.

Since $Z_{(i)}$ one of the matching occurrences of $Z$ in $X\Rightarrow Y$,
there is another $Z_{(i^{\prime})}$ in $X\Rightarrow Y$ such that
$X\Rightarrow Y$ is equivalent to $Z_{(i)}\circ Z_{(i^{\prime})}\Rightarrow U$
or $U\Rightarrow Z_{(i)}\circ Z_{(i^{\prime})}$ for some structure $U$. This
contradicts the fact that no matter which rules of display rules, (Al), (Ar),
(Pl) and (Pr) are used, either $Z_{(i)}$ or $Z_{(i^{\prime})}$ is in the scope
of the exhibited $\bullet$ in $\star_{1}\bullet\star_{2}W[Z_{(i)}]$, but not
both.

The following lemma says that matching occurrences of a structure remains
matching when unrelated structure is changed.

###### Lemma 5

(1) Let $X$ be a structure containing matching occurrences $Z_{(1)},Z_{(2)}$
of a substructure $Z$ in $X\Rightarrow Y$. Then $Z_{(1)}$ and $Z_{(2)}$ are
matching in $X\Rightarrow U$ for any structure $U$.

(2) Let $X$ be a structure containing matching occurrences $Z_{(1)},Z_{(2)}$
of a substructure $Z$ in $Y\Rightarrow X$. Then $Z_{(1)}$ and $Z_{(2)}$ are
matching in $U\Rightarrow X$ for any structure $U$.

###### Proof

We prove these claims simultaneously by induction on the length $l(X)$ of $X$.
By assumption, $l(X)>1$.

Consider the case that $l(X)=2$. For item (1), $X\Rightarrow Y$ is of the form
$p\circ p\Rightarrow Y$. Then for any $U$, the two occurrences of $p$ are
matching in $p\circ p\Rightarrow U$. The proof for item (2) is similar.

Assume that $l(X)>2$. First consider the case that $X$ is of the form $\ast
X^{\prime}$. For item (1), $\ast X^{\prime}\Rightarrow Y$ is equivalent to
$\overline{Y}\Rightarrow X^{\prime}$. By assumption, $Z_{(1)}$ and $Z_{(2)}$
are matching occurrences of a substructure $Z$ in $\ast X^{\prime}\Rightarrow
Y$. Since $\ast X^{\prime}\Rightarrow Y$ is equivalent to
$\overline{Y}\Rightarrow X^{\prime}$, $Z_{(1)}$ and $Z_{(2)}$ are matching in
$\overline{Y}\Rightarrow X^{\prime}$. Then by the induction hypothesis of item
(2), $Z_{(1)}$ and $Z_{(2)}$ are matching in $U^{\prime}\Rightarrow
X^{\prime}$ for any structure $U^{\prime}$. Since $U^{\prime}\Rightarrow
X^{\prime}$ is equivalent to $\ast
X^{\prime}\Rightarrow\overline{U^{\prime}}$, $Z_{(1)}$ and $Z_{(2)}$ are
matching in $\ast X^{\prime}\Rightarrow\overline{U^{\prime}}$. This is
equivalent to say that $Z_{(1)}$ and $Z_{(2)}$ are matching in $\ast
X^{\prime}\Rightarrow U$ for any structure $U$. The proof for item (2) is
similar.

The case that $X$ is of the form $\bullet X^{\prime}$ is similar because
$\bullet X^{\prime}\Rightarrow Y$ is equivalent to
$X^{\prime}\Rightarrow\bullet Y$ and $Y\Rightarrow\bullet X^{\prime}$ is
equivalent to $\bullet Y\Rightarrow X^{\prime}$.

Now consider the case that $X$ is of the form $X_{1}\circ X_{2}$. For item
(1), If the two occurrences $Z_{(1)},Z_{(2)}$ of $Z$ are in $X_{1}$, the claim
follows from the fact that $X_{1}\circ X_{2}\Rightarrow Y$ is equivalent to
$X_{1}\Rightarrow Y\circ\overline{X_{2}}$ and the induction hypothesis. The
proof is the same for the case that $Z_{(1)},Z_{(2)}$ are in $X_{2}$.

If $X$ is of the form $X_{1}[Z_{(1)}]\circ X_{2}[Z_{(2)}]$, either the length
of $X_{1}[Z_{(1)}]$ or the length of $X_{2}[Z_{(2)}]$ is larger than $1$.
Without loss of generality, assume that $l(X_{1}[Z_{(1)}])>1$.

Consider the case that $X_{1}[Z_{(1)}]$ is of the form $\ast
X_{1}^{\prime}[Z_{(1)}]$.

If $X_{2}[Z_{(2)}]$ is of the form $X_{2}^{\prime}[Z_{(2)}]\circ
X_{2}^{\prime\prime}$ or $X_{2}^{\prime\prime}\circ X_{2}^{\prime}[Z_{(2)}]$,
then $X\Rightarrow Y$ is equivalent to $\ast X_{1}^{\prime}[Z_{(1)}]\circ
X_{2}^{\prime}[Z_{(2)}]\Rightarrow Y\circ\overline{X_{2}^{\prime\prime}}$. The
claim follows from the induction hypothesis and the fact that $X\Rightarrow Y$
is equivalent to $\ast X_{1}^{\prime}[Z_{(1)}]\circ
X_{2}^{\prime}[Z_{(2)}]\Rightarrow Y\circ\overline{X_{2}^{\prime\prime}}$.

If $X_{2}[Z_{(2)}]$ is of the form $\ast X_{2}^{\prime}[Z_{(2)}]$, then
$X\Rightarrow Y$ is equivalent to $\overline{Y}\Rightarrow
X_{1}^{\prime}[Z_{(1)}]\circ X_{2}^{\prime}[Z_{(2)}]$. The claim follows from
the induction hypothesis and the fact that $X\Rightarrow Y$ is equivalent to
$\overline{Y}\Rightarrow X_{1}^{\prime}[Z_{(1)}]\circ
X_{2}^{\prime}[Z_{(2)}]$.

The possibility that $X_{2}[Z_{(2)}]$ is of the form $\bullet
X_{2}^{\prime}[Z_{(2)}]$ is excluded by Lemma 4.

For the same reason, $X_{1}[Z_{(1)}]$ is not of the form $\bullet
X_{1}^{\prime}[Z_{(1)}]$. This completes the proof for item (1). The proof for
item (2) is similar.

$(\mathrm{I}l)$ and $(\mathrm{I}r)$ mean that certain occurrences of
$\mathrm{I}$ are redundant. This is captured by the notion of _superfluous
occurrences of $\mathrm{I}$_.

######  Definition 6 (Superfluous occurrences of $\mathrm{I}$)

An occurrence of $\mathrm{I}$ in $X\Rightarrow Y$ is said to be _superfluous_
if it is a dependent substructure of $X\Rightarrow Y$ and $X\Rightarrow Y$ is
equivalent to $Z\circ\mathrm{I}\Rightarrow U$ or $U\Rightarrow
Z\circ\mathrm{I}$ for some structures $Z$ and $U$.

If $X\Rightarrow Y$ contains a superfluous occurrence of $\mathrm{I}$, we say
that $\mathrm{I}$ is _superfluous_ in $X\Rightarrow Y$.

By a proof similar to that of Lemma 4, it follows that if $\mathrm{I}$ is a
superfluous occurrence in $\mathcal{S}$, then $\mathcal{S}$ is of the form
$\mathcal{S}[\ast^{n}\mathrm{I}\circ W]$ or
$\mathcal{S}[W\circ\ast^{n}\mathrm{I}]$, for some $n\in\mathbb{N}$.

Now we define the notion of reduced sequents. They are sequents that contain
no superfluous substructure or superfluous $\mathrm{I}$.

###### Definition 7

A sequent is called _reduced_ if it does not contain any superfluous
substructure or superfluous $\mathrm{I}$.

We will show that each provable sequent has a _$3$ -reduced proof_ in
$\mathrm{D.K}^{-}_{\ast}$. The notions of $n$-reduced sequents and proofs for
$n\in\mathbb{N}$ are as follows.

###### Definition 8

For a sequent $\mathcal{S}$ and a superfluous substructure $Z$ in
$\mathcal{S}$, let $\rho(Z)$ be the number of matching occurrences of $Z$ in
$\mathcal{S}$.

For a natural number $n$, a sequent $\mathcal{S}$ is called _$n$ -reduced_ if

  1. (1)

for any superfluous substructure $Z$ in $\mathcal{S}$, $\rho(Z)\leq n$;

  2. (2)

$\mathcal{S}$ contains at most $n$ superfluous occurrences of $\mathrm{I}$.

A proof is called _n-reduced_ if each sequent occurring in it is n-reduced.

In order to make a sequent reduced or $n$-reduced, we need to remove (some)
superfluous occurrences of substructures and $\mathrm{I}$. The definition of
deletion is given next.

######  Definition 9 (Deletion of superfluous substructures)

Let $\mathcal{S}$ be a sequent and $Z$ a superfluous substructure of
$\mathcal{S}$. The _deletion of $Z$ from $\mathcal{S}$_, denoted
$d(Z)(\mathcal{S})$, is defined as follows:

  1. (1)

$Z$ is a dependent substructure. Then $\mathcal{S}$ is of the form
$\mathcal{S}[\ast^{n}Z\circ W]$ or $\mathcal{S}[W\circ\ast^{n}Z]$, where
$\ast^{n}$ is a sequence of $n$ $\ast$’s for $n\in\mathbb{N}$ (by Lemma 4).
Let

$d(Z)(\mathcal{S})=\left\\{\begin{aligned}
&\mathcal{S}[W\backslash\ast^{n}Z\circ
W]&&\text{~{}if~{}}\mathcal{S}=\mathcal{S}[\ast^{n}Z\circ W]\\\
&\mathcal{S}[W\backslash
W\circ\ast^{n}Z]&&\text{~{}if~{}}\mathcal{S}=\mathcal{S}[W\circ\ast^{n}Z]\end{aligned}\right.$

  2. (2)

$Z$ is an independent substructure. Then $\mathcal{S}$ is of the form
$\ast^{n}Z\Rightarrow Y$ or $X\Rightarrow\ast^{n}Z$, where $\ast^{n}$ is a
sequence of $n$ $\ast$’s for $n\in\mathbb{N}$ (by Lemma 4). We substitute
$\ast^{n}Z$ with $\mathrm{I}$, i.e.,

$d(Z)(\mathcal{S})=S[\mathrm{I}\backslash\ast^{n}Z]=\left\\{\begin{aligned}
&\mathrm{I}\Rightarrow Y&&\text{~{}if~{}}\mathcal{S}=\ast^{n}Z\Rightarrow Y\\\
&X\Rightarrow\mathrm{I}&&\text{~{}if~{}}\mathcal{S}=X\Rightarrow\ast^{n}Z\end{aligned}\right.$

######  Definition 10 (Deletion of superfluous $\mathrm{I}$)

Let $\mathcal{S}$ be a sequent and $\mathrm{I}$ a superfluous occurrence in
$\mathcal{S}$. Then $\mathcal{S}$ is of the form
$\mathcal{S}[\ast^{n}\mathrm{I}\circ W]$ or
$\mathcal{S}[W\circ\ast^{n}\mathrm{I}]$ for some $n\in\mathbb{N}$ (see
discussion after Definition 6).

The _deletion of $\mathrm{I}$ from $\mathcal{S}$_, denoted
$d(\mathrm{I})(\mathcal{S})$, is defined as follows:

$d(\mathrm{I})(\mathcal{S})=\left\\{\begin{aligned}
&\mathcal{S}[W\backslash\ast^{n}\mathrm{I}\circ
W]&&\text{~{}if~{}}\mathcal{S}=\mathcal{S}[\ast^{n}\mathrm{I}\circ W]\\\
&\mathcal{S}[W\backslash
W\circ\ast^{n}\mathrm{I}]&&\text{~{}if~{}}\mathcal{S}=\mathcal{S}[W\circ\ast^{n}\mathrm{I}]\end{aligned}\right.$

It is straightforward that operations in Definitions 9 and 10 are enough to
make a sequent reduced. If a sequent $\mathcal{S}^{\prime}$ is obtained from
$\mathcal{S}$ by applying these operations until $\mathcal{S}^{\prime}$ is
reduced, then we call $\mathcal{S^{\prime}}$ a _reduced sequent from
$\mathcal{S}$_.

###  5.3 Uniqueness up to inter-provability

There may be more than one reduced sequent from a sequent. We will show that
all reduced sequents obtained from a sequent are inter-provable with display
rules and $(\mathrm{I}r)$ in $\mathrm{D.K}^{-}_{\ast}$.

For equivalent sequents $\mathcal{S}_{1}$ and $\mathcal{S}_{2}$, by the
atomicity-preserving property of display rules, $(Al)$, $(Ar)$, $(Pl)$ and
$(Pr)$, we can say that $\mathcal{S}_{1}$ and $\mathcal{S}_{2}$ contains the
same substructure $W$, though $W$ may occur at different positions in
$\mathcal{S}_{1}$ and $\mathcal{S}_{2}$. Let $\mathcal{S}_{1}^{\prime}$ and
$\mathcal{S}_{2}^{\prime}$ be the sequents obtained by deleting the same
substructure $W$ in $\mathcal{S}_{1}$ and $\mathcal{S}_{2}$, respectively. We
can show that $\mathcal{S}_{1}^{\prime}$ and $\mathcal{S}_{2}^{\prime}$ are
equivalent.

###### Lemma 6

Let $\mathcal{S}_{1}$ and $\mathcal{S}_{2}$ be equivalent sequents such that
$\mathcal{S}_{1}$ and $\mathcal{S}_{2}$ contains the same substructure $W$.
Then $d(W)(\mathcal{S}_{1})$ is equivalent to $d(W)(\mathcal{S}_{2})$.

###### Proof

Since $\mathcal{S}_{1}$ and $\mathcal{S}_{2}$ are equivalent, there is a proof
$\mathcal{D}$ from $\mathcal{S}_{1}$ to $\mathcal{S}_{2}$ with only display
rules, $(Al)$, $(Ar)$, $(Pl)$ and $(Pr)$. We prove by induction on the height
$h$ of this proof.

If $h=0$, then $\mathcal{S}_{1}$ and $\mathcal{S}_{2}$ are the same. The claim
follow directly.

If $h>0$, consider the last rule $\mathcal{R}$ applied. Consider the case that
$\mathcal{R}$ is the top-to-bottom direction of $(\Rightarrow\ast
2^{\prime})$. Then $\mathcal{S}_{2}$ is $Y\Rightarrow\overline{X}\circ Z$ and
$\mathcal{D}$ ends with

$\frac{X\circ Y\Rightarrow Z}{Y\Rightarrow\overline{X}\circ Z}$

By the induction hypothesis, $d(W)(\mathcal{S}_{1})$ is equivalent to
$d(W)(X\circ Y\Rightarrow Z)$. Now we show that $d(W)(X\circ Y\Rightarrow Z)$
is equivalent to $d(W)(Y\Rightarrow\overline{X}\circ Z)$. If $W$ is a
substructure of $X$, then $X\circ Y\Rightarrow Z$ is $X[U\circ\ast W]\circ
Y\Rightarrow Z$ or $X[\ast W\circ U]\circ Y\Rightarrow Z$ for some structure
$U$. Without loss of generality, assume the former case holds. Then
$d(W)(X\circ Y\Rightarrow Z)=X[U\backslash U\circ\ast W]\circ Y\Rightarrow Z$.
By an application of $(\Rightarrow\ast 2^{\prime})$, we have
$Y\Rightarrow\overline{X[U\backslash U\circ\ast W]}\circ Z$, which is
$d(W)(Y\Rightarrow\overline{X}\circ Z)$. Therefore, $d(W)(X\circ Y\Rightarrow
Z)$ is equivalent to $d(W)(Y\Rightarrow\overline{X}\circ Z)$. The case that
$W$ is a substructure of $Y$ and the case that $W$ is a substructure of $Z$
can be proved similarly.

Since $d(W)(\mathcal{S}_{1})$ is equivalent to $d(W)(X\circ Y\Rightarrow Z)$
and $d(W)(X\circ Y\Rightarrow Z)$ is equivalent to
$d(W)(Y\Rightarrow\overline{X}\circ Z)$, $d(W)(\mathcal{S}_{1})$ is equivalent
to $d(W)(Y\Rightarrow\overline{X}\circ Z)$, which is $d(W)(\mathcal{S}_{2})$.

Other cases of $\mathcal{R}$ are similar.

Then we have the following result about how reduced sequents preserve
equivalence.

###### Proposition 5

Let $\mathcal{S}_{1}^{\prime}$ be a reduced sequent from $\mathcal{S}_{1}$,
and $\mathcal{S}_{2}^{\prime}$ a reduced sequent from $\mathcal{S}_{2}$. If
$\mathcal{S}_{1}$ and $\mathcal{S}_{2}$ are equivalent, then
$\mathcal{S}_{1}^{\prime}$ and $\mathcal{S}_{2}^{\prime}$ are equivalent.

###### Proof

It follows directly from Lemma 6.

Next we show that it does not matter which of the matching occurrences of a
substructure is deleted.

###### Lemma 7

(1) Let $X$ be a structure containing matching occurrences $Z_{(1)},Z_{(2)}$
of a substructure $Z$ in $X\Rightarrow Y$. Then $d(Z_{(1)})(X\Rightarrow Y)$
is equivalent to $d(Z_{(2)})(X\Rightarrow Y)$.

(2) Let $X$ be a structure containing matching occurrences $Z_{(1)},Z_{(2)}$
of a substructure $Z$ in $Y\Rightarrow X$. Then $d(Z_{(1)})(Y\Rightarrow X)$
is equivalent to $d(Z_{(2)})(Y\Rightarrow X)$.

###### Proof

We prove these claims simultaneously by induction on the length $l(X)$ of $X$.
By assumption, $l(X)>1$.

Consider the case that $l(X)=2$. For item (1), $X\Rightarrow Y$ is of the form
$p\circ p\Rightarrow Y$. Then $d(p_{(1)})(p\circ p\Rightarrow
Y)=d(p_{(2)})(p\circ p\Rightarrow Y)$. It follows that they are equivalent.
Item (2) can be proved in a similar way.

Assume that $l(X)>2$. First consider the case that $X$ is of the form $\ast
X^{\prime}$. For item (1), $\ast X^{\prime}\Rightarrow Y$ is equivalent to
$\overline{Y}\Rightarrow X^{\prime}$. Then by the induction hypothesis of item
(2), $d(Z_{(1)})(\overline{Y}\Rightarrow X^{\prime})$ is equivalent to
$d(Z_{(2)})(\overline{Y}\Rightarrow X^{\prime})$. By Lemma 6, $d(Z_{(1)})(\ast
X^{\prime}\Rightarrow Y)$ is equivalent to $d(Z_{(1)})(\overline{Y}\Rightarrow
X^{\prime})$ and $d(Z_{(2)})(\ast X^{\prime}\Rightarrow Y)$ is equivalent to
$d(Z_{(2)})(\overline{Y}\Rightarrow X^{\prime})$. By the transitivity of
sequent equivalence (Proposition 3), it follows that $d(Z_{(1)})(\ast
X^{\prime}\Rightarrow Y)$ is equivalent to $d(Z_{(2)})(\ast
X^{\prime}\Rightarrow Y)$. Item (2) can be proved in a similar way.

The case that $X$ is of the form $\bullet X^{\prime}$ is similar because
$\bullet X^{\prime}\Rightarrow Y$ is equivalent to
$X^{\prime}\Rightarrow\bullet Y$ and $Y\Rightarrow\bullet X^{\prime}$ is
equivalent to $\bullet Y\Rightarrow X^{\prime}$.

Now consider the case that $X$ is of the form $X_{1}\circ X_{2}$. For item
(1), If the two occurrences $Z_{(1)},Z_{(2)}$ of $Z$ are in $X_{1}$, the claim
follows from the fact that $X_{1}\circ X_{2}\Rightarrow Y$ is equivalent to
$X_{1}\Rightarrow Y\circ\overline{X_{2}}$ and the induction hypothesis. The
proof is the same for the case that $Z_{(1)},Z_{(2)}$ are in $X_{2}$.

If $X$ is of the form $X_{1}[Z_{(1)}]\circ X_{2}[Z_{(2)}]$, since $l(X)>2$,
either the length of $X_{1}[Z_{(1)}]$ or the length of $X_{2}[Z_{(2)}]$ is
larger than 1. Without loss of generality, assume that $l(X_{1}[Z_{(1)}])>1$.

Consider the case that $X_{1}[Z_{(1)}]$ is of the form $\ast
X_{1}^{\prime}[Z_{(1)}]$.

If $X_{2}[Z_{(2)}]$ is of the form $X_{2}^{\prime}[Z_{(2)}]\circ
X_{2}^{\prime\prime}$ or $X_{2}^{\prime\prime}\circ X_{2}^{\prime}[Z_{(2)}]$,
then $X\Rightarrow Y$ is equivalent to $\ast X_{1}^{\prime}[Z_{(1)}]\circ
X_{2}^{\prime}[Z_{(2)}]\Rightarrow Y\circ\overline{X_{2}^{\prime\prime}}$. By
the induction hypothesis, $d(Z_{(1)})(\ast X_{1}^{\prime}[Z_{(1)}]\circ
X_{2}^{\prime}[Z_{(2)}]\Rightarrow Y\circ\overline{X_{2}^{\prime\prime}})$ is
equivalent to $d(Z_{(2)})(\ast X_{1}^{\prime}[Z_{(1)}]\circ
X_{2}^{\prime}[Z_{(2)}]\Rightarrow Y\circ\overline{X_{2}^{\prime\prime}})$. By
Lemma 6, $d(Z_{(1)})(X\Rightarrow Y)$ is equivalent to $d(Z_{(1)})(\ast
X_{1}^{\prime}$ $[Z_{(1)}]$ $\circ X_{2}^{\prime}[Z_{(2)}]\Rightarrow
Y\circ\overline{X_{2}^{\prime\prime}})$ and $d(Z_{(2)})(X\Rightarrow Y)$ is
equivalent to $d(Z_{(2)})(\ast X_{1}^{\prime}[Z_{(1)}]$ $\circ
X_{2}^{\prime}[Z_{(2)}]\Rightarrow Y\circ\overline{X_{2}^{\prime\prime}})$. By
the transitivity of sequent equivalence (Proposition 3),
$d(Z_{(1)})(X\Rightarrow Y)$ is equivalent to $d(Z_{(2)})(X\Rightarrow Y)$.

If $X_{2}[Z_{(2)}]$ is of the form $\ast X_{2}^{\prime}[Z_{(2)}]$, then
$X\Rightarrow Y$ is equivalent to $\overline{Y}\Rightarrow
X_{1}^{\prime}[Z_{(1)}]\circ X_{2}^{\prime}[Z_{(2)}]$. Then we can use the
induction hypothesis of item (2) and proceed as above to show that
$d(Z_{(1)})(X\Rightarrow Y)$ is equivalent to $d(Z_{(2)})(X\Rightarrow Y)$.

The possibility that $X_{2}[Z_{(2)}]$ is of the form $\bullet
X_{2}^{\prime}[Z_{(2)}]$ is excluded by Lemma 4.

For the same reason, $X_{1}[Z_{(1)}]$ is not of the form $\bullet
X_{1}^{\prime}[Z_{(1)}]$. This completes the proof for item (1). The proof for
item (2) is similar.

Next is the key result of this subsection: the reduced sequent from a sequent
is unique up to inter-provability.

###### Proposition 6

Let $\mathcal{S}_{1}$ and $\mathcal{S}_{2}$ be reduced sequents from
$\mathcal{S}$. Then $\mathcal{S}_{1}$ and $\mathcal{S}_{2}$ are inter-provable
with display rules and $(\mathrm{I}r)$ in $\mathrm{D.K}^{-}_{\ast}$.

###### Proof

This follows from the fact that for any sequent $X\Rightarrow Y$,
$X\Rightarrow Y$ and $X\circ\overline{Y}\Rightarrow\mathrm{I}$ are inter-
provable with display rules and $(\mathrm{I}r)$ and Lemma 7.

By this proposition, though there may be more than one reduced sequent from
$\mathcal{S}$, they are inter-provable. Therefore, it does not cause confusion
when we speak of ‘the’ reduced sequent from $\mathcal{S}$. For any sequent
$\mathcal{S}$, we use $r(\mathcal{S})$ to denote the reduced sequent from
$\mathcal{S}$.

_Reducing a substructure in a sequent_ is important in subsequent sections and
this is its definition.

###### Definition 11

Let $\mathcal{S}$ be a sequent and $W$ a substructure in $\mathcal{S}$.
_Reducing $W$ in $\mathcal{S}$_ means to delete all superfluous substructures
and superfluous $\mathrm{I}$ in $W$. We use $\mathfrak{r}(W)$ to denote the
substructure of $W$ after reducing $W$ in $\mathcal{S}$. Hence, the result of
reducing $W$ in $\mathcal{S}$ is $\mathcal{S}[\mathfrak{r}(W)\backslash W]$.

By Lemma 5, matching occurrences of a substructure remains matching when
unrelated structure is changed. Therefore, we can use one symbol
$\mathfrak{r}$ for reducing $W$ in $X[W]\Rightarrow Y$ and in $X[W]\Rightarrow
Y^{\prime}$ and denote the results by $X[\mathfrak{r}(W)\backslash
W]\Rightarrow Y$ and $X[\mathfrak{r}(W)\backslash W]\Rightarrow Y^{\prime}$,
respectively.

###  5.4 The existence of 3-reduced proofs in $\mathrm{D.K}^{-}_{\ast}$

This subsection shows that for any reduced and provable $\mathcal{S}$ in
$\mathrm{D.K}^{-}_{\ast}$, there is a 3-reduced proof for $\mathcal{S}$.

For sequent $X\Rightarrow Y$ and $X^{\prime}\Rightarrow Y^{\prime}$, the
notation $X\Rightarrow Y\vdash^{n}X^{\prime}\Rightarrow Y^{\prime}$ means that
there exists a $n$-reduced proof from $X\Rightarrow Y$ to
$X^{\prime}\Rightarrow Y^{\prime}$ in $\mathrm{D.K}^{-}_{\ast}$; the notation
$X\Rightarrow Y\dashv\vdash^{n}X^{\prime}\Rightarrow Y^{\prime}$ means that
$X\Rightarrow Y\vdash^{n}X^{\prime}\Rightarrow Y^{\prime}$ and
$X^{\prime}\Rightarrow Y^{\prime}\vdash^{n}X\Rightarrow Y$.

The following lemma says that we can go back and forth in
$\mathrm{D.K}^{-}_{\ast}$ with a $n$-reduced proof between a sequent
$\mathcal{S}$ and the sequent obtained by deleting a superfluous occurrence of
a substructure or $\mathrm{I}$ from $\mathcal{S}$.

######  Lemma 8 (Deleting and adding superfluous substructures)

Let $\mathcal{S}$ be a n-reduced sequent and $\mathcal{S}^{\prime}$ the
sequent obtained from $\mathcal{S}$ by deleting a superfluous occurrence of a
substructure or $\mathrm{I}$. Then
$\mathcal{S}\dashv\vdash^{n}\mathcal{S}^{\prime}$ in
$\mathrm{D.K}^{-}_{\ast}$.

###### Proof

We have three subcases to consider. The deleted structure is (1) a superfluous
occurrence of $\mathrm{I}$, (2) a dependent substructure or (3) an independent
substructure.

(1) If the deleted structure is a superfluous $\mathrm{I}$, then $\mathcal{S}$
contains $\ast^{n}\mathrm{I}\circ W$ or $W\circ\ast^{n}\mathrm{I}$ as a
substructure, where $W$ is a structure and $n\in\mathbb{N}$. Without loss of
generality, assume that $\mathcal{S}$ contains $W\circ\ast^{n}\mathrm{I}$ as a
substructure. By the definition of deletion, the $W$ in
$W\circ\ast^{n}\mathrm{I}$ remains in $\mathcal{S}^{\prime}$ and $\mathcal{S}$
is $\mathcal{S}^{\prime}[(W\circ\ast^{n}\mathrm{I})\backslash W]$.

Since $\mathrm{I}$ is superfluous in $\mathcal{S}$, there exists a proof from
$\mathcal{S}^{\prime}[(W\circ\ast^{n}\mathrm{I})\backslash W]$ to
$Z\circ\mathrm{I}\Rightarrow U$ or $U\Rightarrow Z\circ\mathrm{I}$ for some
structures $Z$ and $U$ using only display rules, $(Al)$, $(Ar)$, $(Pl)$ and
$(Pr)$. Let $\mathcal{D}$ be the shortest of such proofs and $h$ the height of
$\mathcal{D}$. We prove by induction on $h$.

First, consider the case that $h=0$. It follows that $W$ is $Z$ and $\ast^{n}$
is an empty string.

If $\mathcal{S}^{\prime}[(W\circ\ast^{n}\mathrm{I})\backslash W]$ is
equivalent to $Z\circ\mathrm{I}\Rightarrow U$, then
$\mathcal{S}^{\prime}[(W\circ\ast^{n}\mathrm{I})\backslash W]$ is
$Z\circ\mathrm{I}\Rightarrow U$ and $\mathcal{S}^{\prime}$ is $Z\Rightarrow
U$. Use $(\mathrm{I}l)$ and $(Pl)$ to derive the latter from the former and
use the other rule in $(\mathrm{I}l)$ and $(Pl)$ for the other direction.

If $\mathcal{S}^{\prime}[(W\circ\ast^{n}\mathrm{I})\backslash W]$ equivalent
to $U\Rightarrow Z\circ\mathrm{I}$, then
$\mathcal{S}^{\prime}[(W\circ\ast^{n}\mathrm{I})\backslash W]$ is
$U\Rightarrow Z\circ\mathrm{I}$ and $\mathcal{S}^{\prime}$ is $U\Rightarrow
Z$. Use $(\mathrm{I}r)$ and $(Pr)$ to derive the latter from the former and
use the other rule in $(\mathrm{I}r)$ and $(Pr)$ for the other direction.

If $h>0$, consider the first rule $\mathcal{R}$ applied in $\mathcal{D}$.

Assume that $\mathcal{D}$ starts with:

$\mathcal{S}^{\prime}[(W\circ\ast^{n}\mathrm{I})\backslash W]$ $(\mathcal{R})$
$\mathcal{S}^{\prime\prime}$

Since $\mathcal{R}$ is a display rule, $(Al)$, $(Ar)$, $(Pl)$ or $(Pr)$,
$\mathcal{R}$ is atomicity-preserving. Since $\mathcal{S}$ is n-reduced and
$\mathcal{S}$ is $\mathcal{S}^{\prime}[(W\circ\ast^{n}\mathrm{I})\backslash
W]$, $\mathcal{S}^{\prime}[(W\circ\ast^{n}\mathrm{I})\backslash W]$ is
n-reduced and $\mathcal{R}$ is atomicity-preserving,
$\mathcal{S}^{\prime\prime}$ is n-reduced.

Note that $\mathcal{S}^{\prime\prime}$ is equivalent to
$Z\circ\mathrm{I}\Rightarrow U$ or $U\Rightarrow Z\circ\mathrm{I}$ but the
shortest proof is of height $h-1$. Therefore, by the induction hypothesis,
$\mathcal{S}^{\prime}\dashv\vdash^{n}\mathcal{S}^{\prime\prime}$.

Since each of display rules, $(Al)$, $(Ar)$, $(Pl)$ and $(Pr)$ contains two
opposite rules and $\mathcal{R}$ is one of the rules in display rules, $(Al)$,
$(Ar)$, $(Pl)$ and $(Pr)$, its opposite $\mathcal{R}^{-1}$ exists. We have the
following proof:

$\mathcal{S}^{\prime\prime}$ $(\mathcal{R}^{-1})$
$\mathcal{S}^{\prime}[(W\circ\ast^{n}\mathrm{I})\backslash W]$

Since $\mathcal{S}^{\prime}\dashv\vdash^{n}\mathcal{S}^{\prime\prime}$ and
$\mathcal{S}$ is $\mathcal{S}^{\prime}[(W\circ\ast^{n}\mathrm{I})\backslash
W]$, $\mathcal{S}\dashv\vdash^{n}\mathcal{S}^{\prime}$.

(2) If the deleted structure $Z$ is a dependent substructure, then
$\mathcal{S}$ contains $\ast^{n}Z\circ W$ or $W\circ\ast^{n}Z$ as a
substructure, where $W$ is a structure and $n\in\mathbb{N}$. Without loss of
generality, assume that $\mathcal{S}$ contains $W\circ\ast^{n}Z$ as a
substructure. By the definition of deletion, the $W$ in $W\circ\ast^{n}Z$
remains in $\mathcal{S}^{\prime}$ and $\mathcal{S}$ is
$\mathcal{S}^{\prime}[(W\circ\ast^{n}Z)\backslash W]$.

Since $Z$ is superfluous in $\mathcal{S}$, there exists a proof from
$\mathcal{S}^{\prime}[(W\circ\ast^{n}Z)\backslash W]$ to $Z\circ Z\Rightarrow
U$ or $U\Rightarrow Z\circ Z$ for some structure $U$ using only display rules,
$(Al)$, $(Ar)$, $(Pl)$ and $(Pr)$. Let $\mathcal{D}$ be the shortest of such
proofs and $h$ the height of $\mathcal{D}$. We prove by induction on $h$.

First, consider the case that $h=0$. It follows that $W$ is $Z$.

If $\mathcal{S}^{\prime}[(W\circ\ast^{n}Z)\backslash W]$ is equivalent to
$Z\circ Z\Rightarrow U$, then
$\mathcal{S}^{\prime}[(W\circ\ast^{n}Z)\backslash W]$ is $Z\circ Z\Rightarrow
U$ and $\mathcal{S}^{\prime}$ is $Z\Rightarrow U$. Use $(Cl)$ to derive the
latter from the former and use $(Wl)$ for the other direction.

If $\mathcal{S}^{\prime}[(W\circ\ast^{n}Z)\backslash W]$ is equivalent to
$U\Rightarrow Z\circ Z$, $\mathcal{S}^{\prime}[(W\circ\ast^{n}Z)\backslash W]$
is $U\Rightarrow Z\circ Z$ and $\mathcal{S}^{\prime}$ is $U\Rightarrow Z$. Use
$(Cr)$ to derive the latter from the former and use $(Wr)$ for the other
direction.

If $h>0$, consider the first rule $\mathcal{R}$ applied in $\mathcal{D}$.

Assume that $\mathcal{D}$ starts with:

$\mathcal{S}^{\prime}[(W\circ\ast^{n}Z)\backslash W]$ $(\mathcal{R})$
$\mathcal{S}^{\prime\prime}$

Since $\mathcal{R}$ is a display rule, $(Al)$, $(Ar)$, $(Pl)$ or $(Pr)$,
$\mathcal{R}$ is atomicity-preserving. Since $\mathcal{S}$ is n-reduced and
$\mathcal{S}$ is $\mathcal{S}^{\prime}[(W\circ\ast^{n}Z)\backslash W]$,
$\mathcal{S}^{\prime}[(W\circ\ast^{n}Z)\backslash W]$ is n-reduced and
$\mathcal{R}$ is atomicity-preserving, $\mathcal{S}^{\prime\prime}$ is
n-reduced.

Note that $\mathcal{S}^{\prime\prime}$ is equivalent to $Z\circ Z\Rightarrow
U$ or $U\Rightarrow Z\circ Z$ but the shortest proof is of height $h-1$.
Therefore, by the induction hypothesis,
$\mathcal{S}^{\prime}\dashv\vdash^{n}\mathcal{S}^{\prime\prime}$.

Since each of display rules, $(Al)$, $(Ar)$, $(Pl)$ and $(Pr)$ contains two
opposite rules and $\mathcal{R}$ is one of the rules in display rules, $(Al)$,
$(Ar)$, $(Pl)$ and $(Pr)$, its opposite $\mathcal{R}^{-1}$ exists. We have the
following proof:

$\mathcal{S}^{\prime\prime}$ $(\mathcal{R}^{-1})$
$\mathcal{S}^{\prime}[(W\circ\ast^{n}Z)\backslash W]$

Since $\mathcal{S}^{\prime}\dashv\vdash^{n}\mathcal{S}^{\prime\prime}$ and
$\mathcal{S}$ is $\mathcal{S}^{\prime}[(W\circ\ast^{n}Z)\backslash W]$,
$\mathcal{S}\dashv\vdash^{n}\mathcal{S}^{\prime}$.

(3) If the deleted structure $Z$ is an independent substructure, then
$\mathcal{S}$ is $\ast^{n}Z\Rightarrow Y$ or $X\Rightarrow\ast^{n}Z$. Without
loss of generality, assume that $\mathcal{S}$ is $\ast^{n}Z\Rightarrow Y$.
Then $\mathcal{S}^{\prime}$ is $\mathrm{I}\Rightarrow Y$. We have to show
$\mathrm{I}\Rightarrow Y\dashv\vdash^{n}\ast^{n}Z\Rightarrow Y$.

This is a n-reduced proof from $\mathrm{I}\Rightarrow Y$ to
$\ast^{n}Z\Rightarrow Y$:

$\mathrm{I}\Rightarrow Y$ $(Wl)$ $\ast^{n}Z\circ\mathrm{I}\Rightarrow Y$
$(Pl)$ $\mathrm{I}\circ\ast^{n}Z\Rightarrow Y$ $(Il)$ $\ast^{n}Z\Rightarrow Y$

Now we prove $\ast^{n}Z\Rightarrow Y\vdash^{n}\mathrm{I}\Rightarrow Y$.

Since the $Z$ in $\ast^{n}Z\Rightarrow Y$ is independently superfluous, $Y$
contains an occurrence of $Z$ and $\ast^{n}Z\Rightarrow Y$ is equivalent to
$Z\circ Z\Rightarrow U$ or $U\Rightarrow Z\circ Z$ for some structure $U$. In
other words, there are two occurrences of $Z$ in $\ast^{n}Z\Rightarrow Y$,
each on one side of $\Rightarrow$ and they can be moved to the same side of
$\Rightarrow$ with only display rules, $(Al)$, $(Ar)$, $(Pl)$ and $(Pr)$. By
observation, $Y$ must be of the form $Y_{1}\circ Y_{2}$, otherwise the two
occurrences of $Z$ can not be gathered together. Without loss generality,
assume that the other occurrence of $Z$ is a substructure of $Y_{1}$.

By $(\ast\Rightarrow 2^{\prime})$, we have $\overline{Y_{1}}\circ Z\Rightarrow
Y_{2}$. It follows that the $Z$ in $\overline{Y_{1}}\circ Z\Rightarrow Y_{2}$
is dependently superfluous. By item (2) in this proof,
$\overline{Y_{1}}\circ\ast^{n}Z\Rightarrow
Y_{2}\dashv\vdash^{n}\overline{Y_{1}}\vdash Y_{2}$. It remains to show that
$\overline{Y_{1}}\Rightarrow Y_{2}\vdash^{n}\mathrm{I}\vdash Y_{1}\circ
Y_{2}$. An n-reduced proof is as follows:

$\overline{Y_{1}}\Rightarrow Y_{2}$ $(Il)$
$\mathrm{I}\circ\overline{Y_{1}}\Rightarrow Y_{2}$ $(Pl)$
$\overline{Y_{1}}\circ\mathrm{I}\Rightarrow Y_{2}$ $(\ast\Rightarrow
2^{\prime})$ $\mathrm{I}\Rightarrow Y_{1}\circ Y_{2}$

Next is the main result of this section.

###### Lemma 9

If $\mathcal{S}$ is reduced and is provable in $\mathrm{D.K}^{-}_{\ast}$, then
there is a 3-reduced proof for $r(\mathcal{S})$ in $\mathrm{D.K}^{-}_{\ast}$.

###### Proof

Since $\mathcal{S}$ is derivable in $\mathrm{D.K}^{-}_{\ast}$, there exists a
proof $\mathcal{D}$ of height $h$ for $\mathcal{S}$.

We prove by induction on $1\leq i\leq h$ that for each sub-proof
$\mathcal{D}^{\prime}$ of $\mathcal{D}$ of height $i$ with the last sequent
being $\mathcal{S}^{\prime}$, there is a 3-reduced proof for
$r(\mathcal{S}^{\prime})$. Recall that $r(\mathcal{S}^{\prime})$ denotes the
reduced sequent from $\mathcal{S}^{\prime}$.

If $i=1$, then $\mathcal{S}^{\prime}$ is an instance of $(Id)$,
$(\Rightarrow\top)$, $(\bot\Rightarrow)$. So is $r(\mathcal{S}^{\prime})$.
Instances of $(Id)$, $(\Rightarrow\top)$, $(\bot\Rightarrow)$ are 3-reduced.

If $i>1$, then we consider the last rule $\mathcal{R}$ applied in
$\mathcal{D}^{\prime}$.

_General idea._ Let $\mathcal{R}$ be

$\frac{\mathcal{S}_{1},\ldots,\mathcal{S}_{n}}{\mathcal{S}}$

By induction hypothesis, there are 3-reduced proofs $\mathcal{D}_{1},\ldots,$
$\mathcal{D}_{n}$ for $r(\mathcal{S}_{1}),\ldots,$ $r(\mathcal{S}_{n})$,
respectively. To show that there is a 3-reduced proof for $r(\mathcal{S})$, we
have to derive $r(\mathcal{S})$ from
$r(\mathcal{S}_{1}),\ldots,r(\mathcal{S}_{n})$. Definition 11 is important
here, because the sequents obtained by reducing certain substructures serve as
middle sequents from $r(\mathcal{S}_{1}),\ldots,r(\mathcal{S}_{n})$ to
$r(\mathcal{S})$.

In this process, we need to add or delete some superfluous substructures and
this is where Lemma 8 comes into play.

We divide the rules in $\mathrm{D.K}^{-}_{\ast}$ into three groups:

  1. (1)

Atomicity-preserving rules, which are display rules, (Al), (Ar), (Pl) and
(Pr);

  2. (2)

Connective rules;

  3. (3)

(Ql), (Qr), ($\mathrm{I}$l), ($\mathrm{I}$r), (Wl), (Wr), (Cl), (Cr), (Ml) and
(Mr).

(1) We only give the proof for the case that $\mathcal{R}$ is the top-to-
bottom rule of $(\Rightarrow\ast 1^{\prime})$. The proof for other cases is
similar.

In this case, $\mathcal{S}^{\prime}$ is $X\Rightarrow Z\circ\overline{W}$.
Then $\mathcal{D}^{\prime}$ ends with

$X\circ W\Rightarrow Z$ $(\Rightarrow\ast 1^{\prime})$ $X\Rightarrow
Z\circ\overline{W}$

By the induction hypothesis, there is a 3-reduced proof for $r(X\circ
W\Rightarrow Z)$. By Definition 11,
$\mathfrak{r}(X)\circ\mathfrak{r}(W)\Rightarrow\mathfrak{r}(Z)$ is 3-reduced
(the worst case is that each of $\mathfrak{r}(X)$, $\mathfrak{r}(W)$ and
$\mathfrak{r}(Z)$ contains a matching occurrence of a substructure or is an
occurrence of $\mathrm{I}$). By Lemma 8, $r(X\circ W\Rightarrow
Z)\vdash^{3}\mathfrak{r}(X)\circ\mathfrak{r}(W)\Rightarrow\mathfrak{r}(Z)$.
Then by $(\Rightarrow\ast 1^{\prime})$, we have
$\mathfrak{r}(X)\Rightarrow\mathfrak{r}(Z)\circ\overline{\mathfrak{r}(W)}$.
Note that $r(X\Rightarrow Z\circ\overline{W})$ can be obtained from
$\mathfrak{r}(X)\Rightarrow\mathfrak{r}(Z)\circ\overline{\mathfrak{r}(W)}$ by
deleting superfluous substructures and $\mathrm{I}$. Therefore, by Lemma 8,
$\mathfrak{r}(X)\Rightarrow\mathfrak{r}(Z)\circ\overline{\mathfrak{r}(W)}\vdash^{3}r(X\Rightarrow
Z\circ\overline{W})$. Since there is a 3-reduced proof for $r(X\circ
W\Rightarrow Z)$, there is a 3-reduced proof for $r(X\Rightarrow
Z\circ\overline{W})$.

(2) We only give the proof for the case that $\mathcal{R}$ is
$(\land\Rightarrow)$, $(\Rightarrow\land)$ or $(\to\Rightarrow^{\prime})$. The
proof for other cases is similar.

Consider the case that $\mathcal{R}$ is $(\land\Rightarrow)$. Then
$\mathcal{S}^{\prime}$ is of the form $\varphi\land\psi\Rightarrow Y$ and
$\mathcal{D}^{\prime}$ ends with

$\frac{\varphi\circ\psi\Rightarrow Y}{\varphi\land\psi\Rightarrow Y}$

By induction hypothesis, there is a 3-reduced proof for
$r(\varphi\circ\psi\Rightarrow Y)$. By Definition 11,
$\mathfrak{r}(\varphi\circ\psi)\Rightarrow\mathfrak{r}(Y)$ is 2-reduced. By
Lemma 8, $r(\varphi\circ\psi\Rightarrow
Y)\vdash^{3}\mathfrak{r}(\varphi\circ\psi)\Rightarrow\mathfrak{r}(Y)$.

There are two subcases:

  1. (a)

$\mathfrak{r}(\varphi\circ\psi)=\varphi$. Then $\varphi=\psi$. First we apply
$(Wl)$ to derive $\varphi\circ\varphi\Rightarrow\mathfrak{r}(Y)$ from
$\varphi\Rightarrow\mathfrak{r}(Y)$. Then by $(\land\Rightarrow)$, we have
$\varphi\land\varphi\Rightarrow\mathfrak{r}(Y)$. It may not be
$r(\varphi\land\varphi\Rightarrow Y)$ since $\mathfrak{r}(Y)$ may contain an
occurrence of $\varphi\land\varphi$ that need to be deleted. This can be
handled by Lemma 8.

  2. (b)

$\mathfrak{r}(\varphi\circ\psi)=\varphi\circ\psi$. Then by
$(\land\Rightarrow)$, we have $\varphi\land\varphi\Rightarrow\mathfrak{r}(Y)$.
Then we proceed as in item (a).

Consider the case that $\mathcal{R}$ is $(\Rightarrow\land)$. Then
$\mathcal{S}^{\prime}$ is of the form $X_{1}\circ X_{2}\Rightarrow A\land B$
and $\mathcal{D}^{\prime}$ ends with

$\frac{X_{1}\Rightarrow\varphi\quad X_{2}\Rightarrow\psi}{X_{1}\circ
X_{2}\Rightarrow\varphi\land\psi}$

By the induction hypothesis, there are 3-reduced proofs for
$r(X_{1}\Rightarrow A)$ and $r(X_{2}\Rightarrow B)$.

By Definition 11, $\mathfrak{r}(X_{1})\Rightarrow\varphi$ and
$\mathfrak{r}(X_{2})\Rightarrow\psi$ are 2-reduced. We proceed as follows:

$r(X_{1}\Rightarrow\varphi)$ Lemma 8 $\mathfrak{r}(X_{1})\Rightarrow\varphi$
$r(X_{2}\Rightarrow\psi)$ Lemma 8 $\mathfrak{r}(X_{2})\Rightarrow\psi$
$(\Rightarrow\land)$
$\mathfrak{r}(X_{1})\circ\mathfrak{r}(X_{2})\Rightarrow\varphi\land\psi$

$\mathfrak{r}(X_{1})\circ\mathfrak{r}(X_{2})\Rightarrow\varphi\land\psi$ is
3-reduced, since the worst case is that each of $\mathfrak{r}(X_{1})$,
$\mathfrak{r}(X_{2})$ and $\varphi\land\psi$ contains a matching occurrence of
$\varphi\land\psi$. Moreover,
$\mathfrak{r}(X_{1})\circ\mathfrak{r}(X_{2})\Rightarrow\varphi\land\psi$ may
not be $r(X_{1}\circ X_{2}\Rightarrow\varphi\land\psi)$ because
$\mathfrak{r}(X_{1})\circ\mathfrak{r}(X_{2})$ may contain an occurrence of
$\varphi\land\varphi$ that need to be deleted. This can be handled by Lemma 8.

Consider the case that $\mathcal{R}$ is $(\to\Rightarrow^{\prime})$. Then
$\mathcal{S}^{\prime}$ is of the form
$\varphi\to\psi\Rightarrow\overline{X}\circ Y$ and $\mathcal{D}^{\prime}$ ends
with

$\frac{X\Rightarrow\varphi\quad\psi\Rightarrow
Y}{\varphi\to\psi\vdash\overline{X}\circ Y}$

By induction hypothesis, there are 3-reduced proofs for
$r(X\Rightarrow\varphi)$ and $r(\psi\Rightarrow Y)$. By Definition 11,
$\mathfrak{r}(X)\Rightarrow\varphi$ and $\psi\Rightarrow\mathfrak{r}(Y)$ are
2-reduced. We proceed as follows:

$r(X\Rightarrow\varphi)$ Lemma 8 $\mathfrak{r}(X)\Rightarrow\varphi$
$r(\psi\Rightarrow Y)$ Lemma 8 $\psi\Rightarrow\mathfrak{r}(Y)$
$(\to\Rightarrow^{\prime})$
$\varphi\to\psi\Rightarrow\overline{\mathfrak{r}(X)}\circ\mathfrak{r}(Y)$

$\varphi\to\psi\Rightarrow\overline{\mathfrak{r}(X)}\circ\mathfrak{r}(Y)$ is
$3$-reduced, since the worst case is that each of $\varphi\to\psi$,
$\overline{\mathfrak{r}(X)}$ and $\mathfrak{r}(Y)$ contains a matching
occurrence of $\varphi\to\psi$. Moreover,
$\varphi\to\psi\Rightarrow\overline{\mathfrak{r}(X)}\circ\mathfrak{r}(Y)$ may
not be $r(\varphi\to\psi\Rightarrow\overline{X}\circ Y)$ because
$\varphi\to\psi\Rightarrow\overline{\mathfrak{r}(X)}\circ\mathfrak{r}(Y)$ may
contain an occurrence of $\varphi\to\varphi$ that need to be deleted. This can
be handled by Lemma 8.

(3) The proof for (Ql), (Qr), ($\mathrm{I}$l), ($\mathrm{I}$r), (Wl), (Wr),
(Cl), (Cr), (Ml) and (Mr) is straightforward.

If $\mathcal{R}$ is (Ql), (Qr), (Wl), (Wr), (Ml) or (Mr), we apply the
induction hypothesis to the premise and then apply $\mathcal{R}$. Take (Ql) as
an example. Then $\mathcal{D}^{\prime}$ ends with

$\mathrm{I}\Rightarrow Y$ (Ql) $\ast\mathrm{I}\Rightarrow Y$

By induction hypothesis, there exists a 3-reduced proof for
$r(\mathrm{I}\Rightarrow Y)$. Since $r(\mathrm{I}\Rightarrow
Y)=\mathrm{I}\Rightarrow\mathfrak{r}(Y)$, this is also a 3-reduced proof for
$\mathrm{I}\Rightarrow\mathfrak{r}(Y)$. Then by (Ql), we have
$\ast\mathrm{I}\Rightarrow\mathfrak{r}(Y)$, which is
$r(\ast\mathrm{I}\Rightarrow Y)$.

If $\mathcal{R}$ is ($\mathrm{I}$l), ($\mathrm{I}$r), (Cl) or (Cr), then the
reduced sequent from the premise of $\mathcal{R}$ and that of the conclusion
of $\mathcal{R}$ are the same. So the claim follows directly from the
induction hypothesis.

##  6 Irredundancy, $r$-complexity increasing property and subformula property

This section introduces the remaining requirements for sequents in finite
proof searching.

####  Irredundant proofs

A proof is said to be _irredundant_ if no sequent appear twice in any of its
branches. Any redundant proof can be transformed into an irredundant one
simply by excising the branch sections between repetitions of a sequent.
Therefore,

###### Lemma 10

For any sequent $\mathcal{S}$ and display calculus $\mathrm{D}$, if
$\mathcal{S}$ is provable in $\mathrm{D}$, then there is an irredundant proof
for $\mathcal{S}$ in $\mathrm{D}$.

####  $r$-complexity increasing property

Recall that $l(\varphi)$ denotes the length of $\varphi$ for any formula
$\varphi$.

###### Definition 12

The complexity $c(X\vdash Y)$ of the sequent $X\vdash Y$ is defined inductive
as follows:

$\displaystyle c(\varphi)=l(\varphi)$ $\displaystyle c(\mathrm{I})=0$
$\displaystyle c(\ast X)=c(X)$ $\displaystyle c(\bullet X)=c(X)$
$\displaystyle c(X\circ Y)=\max\\{c(X),c(Y)\\}$

Then we set $c(X\Rightarrow Y)=\max\\{c(X),c(Y)\\}+n_{\bullet}(X\Rightarrow
Y)$, where $n_{\bullet}(X\Rightarrow Y)$ is the number of $\bullet$ in
$X\Rightarrow Y$.

Note that $\bullet$’s are considered at the final stage of complexity
calculation, which ensures that $(\Rightarrow\bullet)$ is complexity-
preserving.

It follows immediate that equivalent sequents are of the same complexity.

###### Lemma 11

For any sequent $\mathcal{S}$, if $\mathcal{S}_{1}$ and $\mathcal{S}_{2}$ are
reduced sequents obtained from sequent $\mathcal{S}$, then $\mathcal{S}_{1}$
and $\mathcal{S}_{2}$ are complexity-preservingly inter-provable.

###### Proof

By Proposition 6, $\mathcal{S}_{1}$ and $\mathcal{S}_{2}$ are inter-provable
with display rules, $(Al)$, $(Ar)$, $(Pl)$, $(Pr)$ and $(\mathrm{I}r)$ in
$\mathrm{D.K}^{-}_{\ast}$. Since these rule are complexity-preserving,
$\mathcal{S}_{1}$ and $\mathcal{S}_{2}$ are complexity-preservingly inter-
provable.

By this lemma, let the _r-complexity_ $rc(\mathcal{S})$ of $\mathcal{S}$ be
$c(r(\mathcal{S}))$, where $r(\mathcal{S})$ is the reduced sequent from
$\mathcal{S}$ and is discussed after Proposition 6.

We will show that each proof in $\mathrm{D.K}^{-}_{\ast}$ is $r$-complexity
increasing. Before that, we prove a lemma.

###### Lemma 12

For any proof in $\mathrm{D.K}^{-}_{\ast}$, $r$-complexity increases from
leaves to the root.

###### Proof

We prove by induction on the height $h$ of the proof. If $h=1$, the claim
holds trivially.

If $h>1$, consider the last rule $\mathcal{R}$ applied in the proof. If
$\mathcal{R}$ is a display rule, $(Al)$, $(Ar)$, $(Pl)$ or $(Pr)$, let the
derivation end with

$\frac{\mathcal{S}}{\mathcal{S}^{\prime}}$

By definition, $rc(\mathcal{S})=c(r(\mathcal{S}))$ and
$rc(\mathcal{S}^{\prime})=c(r(\mathcal{S^{\prime}}))$. By assumption,
$\mathcal{S}$ and $\mathcal{S}^{\prime}$ are equivalent. By Proposition 5,
$r(\mathcal{S})$ and $r(\mathcal{S^{\prime}})$ are equivalent. Since
equivalent sequents are of the same complexity,
$c(r(\mathcal{S}))=c(r(\mathcal{S}^{\prime}))$. Therefore,
$rc(\mathcal{S})=rc(\mathcal{S}^{\prime})$.

For example, consider the case that $\mathcal{R}$ is the top-to-bottom rule of
$(\Rightarrow\bullet)$. Then the proof ends with

Now suppose that $\mathcal{R}$ is not a display rule, $(Al)$, $(Ar)$, $(Pl)$
or $(Pr)$. Take $(\Rightarrow\land)$ as an example. Let the derivation end
with

$\frac{X\Rightarrow\varphi\quad Y\Rightarrow\psi}{X\circ
Y\Rightarrow\varphi\land\psi}$

By definition, $rc(X\Rightarrow\varphi)=c(r(X\Rightarrow\varphi))$,
$rc(Y\Rightarrow\varphi)=c(r(Y\Rightarrow\psi))$ and $rc(X\circ
Y\Rightarrow\varphi\land\psi)=c(r(X\circ Y\Rightarrow\varphi\land\psi))$. By
the definition of $\mathfrak{r}$, $r(X\Rightarrow\varphi)$ is
$r(\mathfrak{r}(X)\Rightarrow\varphi)$, where $\mathfrak{r}(X)$ is the
substructure of $X$ after reducing $X$ in $X\Rightarrow\varphi$. Similarly,
$r(X\circ Y\Rightarrow\varphi\land\psi)$ is
$r(\mathfrak{r}(X)\circ\mathfrak{r}(Y)\Rightarrow\varphi\land\psi)$. It
follows that $c(r(\mathfrak{r}(X)\Rightarrow\varphi))\leq
c(r(\mathfrak{r}(X)\circ\mathfrak{r}(Y)\Rightarrow\varphi\land\psi))$.
Similarly, $c(r(\mathfrak{r}(Y)\Rightarrow\psi))\leq
c(r(\mathfrak{r}(X)\circ\mathfrak{r}(Y)\Rightarrow\varphi\land\psi))$.

The proofs for other rules are similar.

#### Subformula property

A proof with conclusion $\mathcal{S}$ satisfies the _subformula property_ if
each formula appearing in the proof is a subformula of a formula in
$\mathcal{S}$.

By observation on rules in $\mathrm{D.K}^{-}_{\ast}$, it follows that:

###### Lemma 13

Any proof in $\mathrm{D.K}^{-}_{\ast}$ satisfies the subformula property.

##  7 Decidability

Previous sections show that a sequent $\mathcal{S}$ is provable in
$\mathrm{D.K}^{-}_{\ast}$ iff there is a $\ast$-reduced, 3-reduced,
irredundant, r-complexity-increasing proof satisfying subformula property for
$r(\mathcal{S})$ in $\mathrm{D.K}^{-}_{\ast}$. Therefore, to decide whether
$\mathcal{S}$ is provable in $\mathrm{D.K}^{-}_{\ast}$, one algorithm is to
check all such possible proofs for $r(\mathcal{S})$.

Denote by $\Gamma^{n}_{\mathcal{S}}$ the set of $\ast$-reduced and $n$-reduced
sequents made of subformuals in $\mathcal{S}$, and with $r$-complexity less
than or equal to $\mathcal{S}$555Note that the set of subformulas in
$\mathcal{S}$ equals the set of subfomulas in $r(\mathcal{S})$ and
$rc(r(\mathcal{S}))=rc(\mathcal{S})$. For convenience,
$\Gamma^{n}_{\mathcal{S}}$ is defined in terms of $\mathcal{S}$ instead of
$r(\mathcal{S})$.. To show that $\mathrm{D.K}^{-}_{\ast}$ is decidable, it
suffices to show that $\Gamma^{3}_{\mathcal{S}}$ is finite.

Section 6 will discuss the decidability of extensions of
$\mathrm{D.K}^{-}_{\ast}$, where the more general notion of
$\Gamma^{n}_{\mathcal{S}}$ ($n\in\mathbb{N}$) is in need. Therefore, we will
show that $\Gamma^{n}_{\mathcal{S}}$ is finite, instead of just
$\Gamma^{3}_{\mathcal{S}}$.

To show that $\Gamma^{n}_{\mathcal{S}}$ is finite, we will show that it is a
subset of a finite set defined as follows.

###### Definition 13

Given a finite set $\Phi$ of formulas, the set $\Omega^{\Phi}$ of structures
is defined as follows:

  1. (1)

$\Phi\subseteq\Omega^{\Phi}$;

  2. (2)

If $X,Y\in\Omega^{\Phi}$, then $X\circ Y\in\Omega^{\Phi}$;

  3. (3)

If $X\in\Omega^{\Phi}$ and $X$ is not of the form $\ast X^{\prime}$, then
$\ast X\in\Omega^{\Phi}$;

  4. (4)

If $X\in\Omega^{\Phi}$, then $\bullet X\in\Omega^{\Phi}$.

  5. (5)

If $X\in\Omega^{\Phi}$, then $X\circ\mathrm{I}$ and $\mathrm{I}\circ X$ belong
to $\Omega^{\Phi}$.

Let $\Omega_{m,n}^{\Phi}$ the smallest subset of $\Omega^{\Phi}$ such that for
any $X\in\Omega_{m,n}^{\Phi}$, (1) $X$ contains at most $m$ $\bullet$’s, (2)
each formula in $X$ occurs at most $n$ times in $X$, and (3) $X$ contains at
most $m$ dependent occurrences of $\mathrm{I}$.

Now we show that $\Omega_{m,n}$ is finite.

###### Lemma 14

Let $\Phi$ be a finite set of formulas with $k$ elements. Then
$\Omega_{m,n}^{\Phi}$ is finite.

###### Proof

It suffices to show that there is an upper bound of the length of structures
in $\Omega_{m,n}^{\Phi}$. Let the length of the longest formulas in $\Phi$ be
$t$. An upper bound is $(k+1)nt+2((k+1)n-1)+m$. The proof is as follows.

Let $x_{1},\ldots,x_{(k+1)n}$ be an enumeration of elements from
$\Phi\cup\\{\mathrm{I}\\}$ such that each element occurs exactly $n$ times.

The idea to construct one of the longest structures in $\Omega_{m.n}^{\Phi}$
is as follows. Every element in $x_{1},\ldots,x_{(k+1)n}$ is used to form a
structure and $\ast$ is added to this structure whenever possible. Finally,
$m$ $\bullet$’s are prefixed to the structure.

We formalize this idea and define a sequence of structures as follows:

$\displaystyle X_{1}=\ast x_{1}$ $\displaystyle X_{j}=\ast(X_{j-1}\circ\ast
x_{j})$

Then one of the longest structures in $\Omega_{m,n}^{\Phi}$ is as follows:

$\underbrace{\bullet\ldots\bullet}_{m}X_{(k+1)n}$

This structure contains $(k+1)n$ atomic structure, $2((k+1)n-1)$ $\ast$’s and
$m$ $\bullet$’s. Since the length of each formula in $\Phi$ is less than or
equal to $t$, its length is less than or equal to $(k+1)nt+2((k+1)n-1)+m$.

###### Lemma 15

Let $\mathcal{S}$ be a sequent. Then $\Gamma^{n}_{\mathcal{S}}$ is finite for
$n\in\mathbb{N}$.

###### Proof

Assume that $\mathcal{S}$ is of complexity $m$. Let $\Phi$ be the set of
subformulas in $\mathcal{S}$. Then $\Phi$ is finite.

Let $\Delta=\\{W\Rightarrow Z\mid W,Z\in\Omega^{\Phi}_{mn,(2n+1)mn}\\}$. By
Lemma 14, $\Delta$ is finite. It follows from the definition that for any
sequent $W\Rightarrow Z$, $W\Rightarrow Z\in\Delta$ iff (1) $W\Rightarrow Z$
is made of subformulas in $\mathcal{S}$, (2) $W\Rightarrow Z$ is
$\ast$-reduced, (3) $W$ contains at most $(2n+1)mn$ dependent occurrences of
$\mathrm{I}$, (4) $Z$ contains contains at most $(2n+1)mn$ dependent
occurrences of $\mathrm{I}$, (5) the number of $\bullet$’s in $W$ is at most
$mn$, (6) the number of $\bullet$’s in $Z$ is at most $mn$, (7) each formula
occurs at most $(2n+1)mn$ times in $W$ and (8) each formulas occurs at most
$(2n+1)mn$ times in $Z$.

To show that $\Gamma^{n}_{\mathcal{S}}$ is finite, it suffices to show that
$\Gamma^{n}_{\mathcal{S}}\subseteq\Delta$. We prove by contradiction and
assume that $W\Rightarrow Z\in\Gamma^{n}_{\mathcal{S}}$ and $W\Rightarrow
Z\not\in\Delta$ for some sequent $W\Rightarrow Z$. Since $W\Rightarrow
Z\in\Gamma^{n}_{\mathcal{S}}$, it follows directly from the definition that
$W\Rightarrow Z$ satisfies items (1)-(4) mentioned in the last paragraph.

Now we show that the number of $\bullet$’s in $W$ is at most $mn$. Since
$W\Rightarrow Z\in\Gamma^{n}_{\mathcal{S}}$, by definition, $rc(W\Rightarrow
Z)\leq rc(\mathcal{S})=m$ and $W\Rightarrow Z$ is $n$-reduced. Then the number
of $\bullet$’s in $r(W\Rightarrow Z)$ is less than or equal to $m$. Since
$W\Rightarrow Z$ is $n$-reduced and is obtained from $r(W\Rightarrow Z)$ by
duplicating substructures of the form $\ast^{n}X$ in $r(W\Rightarrow Z)$ (see
Definition 9) or adding dependent $\mathrm{I}$’s, the number of $\bullet$’s in
$W\Rightarrow Z$ is at most $mn$.

It can be proved in a similar way that the number of $\bullet$’s in $Z$ is at
most $mn$. Therefore, $W\Rightarrow Z$ satisfies items (1)-(6) mentioned
above.

Since $W\Rightarrow Z\not\in\Delta$, either there exists a formula $\varphi$
that occurs more than $(2n+1)mn$ times in $W$ or there exists a formula
$\varphi$ that occurs more than $(2n+1)mn$ times in $Z$. Without loss of
generality, we assume the former.

Since the number of $\bullet$’s is at most $mn$ in $W$ and formula $\varphi$
occurs more than $(2n+1)mn$ times in $W$, distribute these occurrences of
$\varphi$ to these $\bullet$’s and one will find that there exists a
substructure $W^{\prime}$ of $W$, which is of the form

$\bullet(\underbrace{\varphi\circ\ldots\circ\varphi}_{j_{1}}\circ\underbrace{\ast\varphi\circ\ldots\ast\circ\varphi}_{j_{2}}\circ
W^{\prime\prime})$

after applications of the commutative law and associative law of $\circ$,
where $W^{\prime\prime}$ is a structure and
$j_{1}+j_{2}\geq\frac{(2n+1)mn}{mn}=2n+1$ .

Since $j_{1}+j_{2}\geq 2n+1$, either the number of occurrences of $\varphi$ or
the number of occurrences of $\ast\varphi$ is larger than $n$, contradicting
the fact that $W\Rightarrow Z$ is $n$-reduced.

######  Theorem 7.1 (Decidability of $\mathrm{D.K}$, $\mathrm{D.K}^{-}$ and
$\mathrm{D.K}^{-}_{\ast}$)

For any sequent $\mathcal{S}$, whether $\mathcal{S}$ is provable or not in
$\mathrm{D.K}$, $\mathrm{D.K}^{-}$ or $\mathrm{D.K}^{-}_{\ast}$ is decidable.

###### Proof

By Lemmas 1, 9, 10, 12 and 13, $\mathcal{S}$ is provable in
$\mathrm{D.K}^{-}_{\ast}$ iff $\mathcal{S}$ is $\ast$-reduced and there exists
a 3-reduced, irredundant, r-complexity-increasing proof with subformula
property for $r(\mathcal{S})$, each sequent in which is of $r$-complexity less
than or equal to $\mathcal{S}$. Recall that $\Gamma_{\mathcal{S}}^{3}$ denotes
the set of $\ast$-reduced and 3-reduced sequents made of subformulas in
$\mathcal{S}$ and of $r$-complexity less than or equal to $\mathcal{S}$.
Therefore, one algorithm to decide whether $\mathcal{S}$ is provable in
$\mathrm{D.K}^{-}_{\ast}$ is to generate all possible proofs only consisting
of sequents in $\Gamma_{\mathcal{S}}^{3}$.

By Lemma 15, $\Gamma^{3}_{\mathcal{S}}$ is finite. Therefore,
$\mathrm{D.K}^{-}_{\ast}$ is decidable.

By Proposition 2, $\mathcal{S}$ is provable in $\mathrm{D.K}^{-}$ iff
$\tau_{\ast}(\mathcal{S})$ is provable in $\mathrm{D.K}^{-}$. Therefore,
$\mathrm{D.K}^{-}$ is decidable.

By Theorem 2.2, the cut rule is admissible in $\mathrm{D.K}^{-}$. Therefore,
$\mathrm{D.K}$ is decidable.

##  8 Decidability of extensions of $\mathrm{D.K}^{-}_{\ast}$

This section discusses how to generalize the method for finite proof-searching
in $\mathrm{D.K}^{-}_{\ast}$ to extensions of $\mathrm{D.K}^{-}_{\ast}$.

For an extension $\mathrm{D.}\Xi$ of $\mathrm{D.K}^{-}_{\ast}$, to show that
$\mathrm{D.}\Xi$ is decidable, by Lemma 15, it suffices to show that a sequent
$\mathcal{S}$ is provable in $\mathrm{D.}\Xi$ iff there is a $\ast$-reduced,
$n$-reduced, irredundant, r-complexity-increasing proof satisfying subformula
property for $r(\mathcal{S})$ in $\mathrm{D.}\Xi$, where $n\in\mathbb{N}$.

Section 8.1 introduces _normal extensions of $\mathrm{D.K}^{-}_{\ast}$_ and
show that they are decidable in this way. Section 8.2 discusses some examples
of extensions of $\mathrm{D.K}^{-}_{\ast}$.

###  8.1 Normal extensions of $\mathrm{D.K}^{-}_{\ast}$

Recall that we use $\star$ with or without superscripts or subscripts to
denote a sequence of $\ast$ and $\bullet$. Let $l(\star)$ be the number of
symbols in $\star$.

###### Definition 14

Let $\Phi=\\{X_{1},\ldots,X_{n}\\}$ be a set of structural variables. The set
$\mathfrak{S}$ of structural schemes is defined recursively as follows:

$\mathfrak{S}::=X\mid\ast X\mid\bullet X\mid X\circ X$

where $X\in\\{X_{1},\ldots,X_{n}\\}$. A structural scheme is called _$\Phi$
-normal_ if it contains each variable in $\Phi$ and each variable occurs
exactly once.

Two structural schemes are said to be _equivalent_ if they are inter-provable
with display rules, $(Al)$, $(Ar)$, $(Pl)$ and $(Pr)$.

_Being $\ast$-reduced, equivalence, superfluous substructures and $\mathrm{I}$
and their deletion and reduction_ for structural schemes are the same as those
for sequents. One can obtain the definitions by substituting ‘structural
schemes’ for ‘sequents’ in the related definitions in Sections 4 and 5.

The _complexity_ of a structural schemes is defined by deleting the clause
about formulas in Definition 12 and adding $c(X)=1$ for $X\in\Phi$. Then let
the _r-complexity_ $rc(\mathfrak{S})=c(r(\mathfrak{S}))$.

###### Definition 15

Let $\Phi=\\{X_{1},\ldots,X_{n}\\}$ be a set of structural variables. A rule
$\mathcal{R}$ is called a _left $\Phi$-normal rule_ if it is of the form

$\frac{\mathfrak{S}_{1}\Rightarrow
Y\quad\ldots\quad\mathfrak{S}_{k}\Rightarrow Y}{\mathfrak{S}\Rightarrow Y}$

where

  1. (1)

$k\in\mathbb{N}$;

  2. (2)

Each $\mathfrak{S}_{i}(1\leq i\leq k)$ and $\mathfrak{S}$ are $\Phi$-normal.

  3. (3)

Each premise and the conclusion are $\ast$-reduced;

  4. (4)

For each $1\leq i\leq k$, $rc(\mathfrak{S}_{i})\leq rc(\mathfrak{S})$

A rule $\mathcal{R}$ is called a _right $\Phi$-normal rule_ if it is of the
form

$\frac{Y\Rightarrow\mathfrak{S}_{1}\quad\ldots\quad
Y\Rightarrow\mathfrak{S}_{k}}{Y\Rightarrow\mathfrak{S}}$

and satisfies the above conditions. Given a finite set $\Phi$ of structural
variables, a rule is called _$\Phi$ -normal_ if it is either a left
$\Phi$-normal rule or a right $\Phi$-normal rule. An extension of
$\mathrm{D.K}^{-}_{\ast}$ is called _$\Phi$ -normal_ if it is obtained by
adding to $\mathrm{D.K}^{-}_{\ast}$ a set of $\Phi$-normal rules.

Then we have the following result.

###### Lemma 16

For any normal extension $\mathrm{D.}\Xi$ of $\mathrm{D.K}^{-}_{\ast}$, it is
immediate that

  1. (1)

each provable sequent has an irredundant proof;

  2. (2)

each proof is $\ast$-reduced, r-complexity-increasing and satisfies the
subformula property;

###### Proof

Item (1) is holds because any redundant proof can be transformed into an
irredundant one simply by excising the branch sections between repetitions of
a sequent.

Since the premise(s) and the conclusion are $\ast$-reduced for each rule in
$\Xi$ and each proof in $\mathrm{D.K}^{-}_{\ast}$ is $\ast$-reduced (Lemma 1),
each proof in $\mathrm{D}.\Xi$ is $\ast$-reduced.

Since each rule in $\Xi$ is $r$-complexity increasing and each proof in
$\mathrm{D.K}^{-}_{\ast}$ is $r$-complexity increasing (Lemma 12), each proof
in $\mathrm{D}.\Xi$ is $r$-complexity increasing.

Since each rule in $\Xi$ is $\Phi$-normal and each proof in
$\mathrm{D.K}^{-}_{\ast}$ satisfies the subformula property (Lemma 13), each
proof in $\mathrm{D}.\Xi$ satisfies the subformula property.

Next is a generalization of Lemma 9 to any normal extension of
$\mathrm{D.K}^{-}_{\ast}$. Its proof makes use of Lemma 8, which also holds
for any normal extension of $\mathrm{D.K}^{-}_{\ast}$, because only display
rules, $(Al)$, $(Ar)$, $(Pl)$, $(Pr)$, $(\mathrm{I}l)$, $(\mathrm{I}r)$,
$(Cl)$ and $(Cr)$ are needed in the proof.

###### Lemma 17

Let $\Phi=\\{X_{1},\ldots,X_{n}\\}$ be a set of structural variables. Let
$\Xi$ be a set of $\Phi$-normal rules. If $\mathcal{S}$ is reduced and is
provable in $\mathrm{D.}\Xi$, then there is a $\max\\{n+1,3\\}$-reduced proof
for $\mathcal{S}$ in $\mathrm{D.}\Xi$.

###### Proof

Since $\mathcal{S}$ is derivable in $\mathrm{D.}\Xi$, there exists a proof
$\mathcal{D}$ of height $h$ for $\mathcal{S}$. We prove by induction on $1\leq
i\leq h$ that for each sub-proof $\mathcal{D}^{\prime}$ of $\mathcal{D}$ of
height $i$ with the last sequent being $\mathcal{S}^{\prime}$, there is an
$\max\\{n+1,3\\}$-reduced proof for $r(\mathcal{S}^{\prime})$.

The base step and the induction step where the last rule applied is a rule in
$\mathrm{D.K}^{-}_{\ast}$ are the same as Lemma 9.

Consider the case that $\mathcal{R}$ is a left $\Phi$-normal rule. Let
$\mathcal{R}$ be

$\frac{\mathfrak{S}_{1}\Rightarrow
Y\quad\ldots\quad\mathfrak{S}_{k}\Rightarrow Y}{\mathfrak{S}\Rightarrow Y}$

By Definition 15, the $\mathfrak{S}_{i}$ is $\Phi$-normal. It follows that it
contains each variable in $\Phi$ and each variable occurs exactly once. Then
$\mathfrak{S}_{i}\Rightarrow Y$ can be written as
$\mathfrak{S}_{i}[X_{1},\ldots,X_{n}]\Rightarrow Y$. By Definition 11,
$\mathfrak{S}_{i}[\mathfrak{r}(X_{1})\backslash
X_{1},\ldots,\mathfrak{r}(X_{n})\backslash X_{n}]\Rightarrow\mathfrak{r}(Y)$
is $(n+1)$-reduced, since the worst case is that each of
$\mathfrak{r}(X_{i})(1\leq i\leq n)$ and $\mathfrak{r}(Y)$ contains a matching
occurrence of a substructure or is $\mathrm{I}$.

For each $1\leq i\leq k$, by Lemma 8,

$r(\mathfrak{S}_{i}\Rightarrow
Y)\vdash^{n+1}\mathfrak{S}_{i}[\mathfrak{r}(X_{1})\backslash
X_{1},\ldots,\mathfrak{r}(X_{n})\backslash X_{n}]\Rightarrow\mathfrak{r}(Y).$

By the induction hypothesis, there is a $\max\\{n+1,3\\}$-reduced proofs for
$r(\mathfrak{S}_{i}\Rightarrow Y)(1\leq i\leq k)$. It follows that there is a
$\max\\{n+1,3\\}$-reduced proof for
$\mathfrak{S}_{i}[\mathfrak{r}(X_{1})\backslash X_{1},$
$\ldots,\mathfrak{r}(X_{n})\backslash X_{n}]\Rightarrow\mathfrak{r}(Y)$.

Then apply $\mathcal{R}$ and we have

$\frac{\mathfrak{S}_{1}[\mathfrak{r}(X_{1})\backslash
X_{1},\ldots,\mathfrak{r}(X_{n})\backslash
X_{n}]\Rightarrow\mathfrak{r}(Y)\ldots\mathfrak{S}_{k}[\mathfrak{r}(X_{1})\backslash
X_{1},\ldots,\mathfrak{r}(X_{n})\backslash
X_{n}]\Rightarrow\mathfrak{r}(Y)}{\mathfrak{S}[\mathfrak{r}(X_{1})\backslash
X_{1},\ldots,\mathfrak{r}(X_{n})\backslash X_{n}]\Rightarrow\mathfrak{r}(Y)}$

$\mathfrak{S}[\mathfrak{r}(X_{1})\backslash
X_{1},\ldots,\mathfrak{r}(X_{n})\backslash X_{n}]\Rightarrow\mathfrak{r}(Y)$
is $(n+1)$-reduced and it may not be $r(\mathfrak{S}\Rightarrow Y)$ because it
may contains superfluous substructures or superfluous occurrences of
$\mathrm{I}$. This can be handled by Lemma 8.

To illustrate the above proof, consider a $\\{X,Y\\}$-normal rule
$\mathcal{R}_{.3}$ as follows :

$\frac{\triangleright(X\circ\triangleright Y)\Rightarrow
Z\quad\triangleright(X\circ Y)\Rightarrow Z\quad\triangleright(\triangleright
X\circ Y)\Rightarrow Z}{\triangleright X\circ\triangleright Y\Rightarrow Z}$

where $\triangleright$ is a shorthand for $\ast\bullet\ast$.

By the induction hypothesis, there are $3$-reduced proofs for
$r(\triangleright(X\circ\triangleright Y)\Rightarrow Z)$,
$r(\triangleright(X\circ Y)\Rightarrow Z)$ and
$r(\triangleright(\triangleright X\circ Y)\Rightarrow Z)$.

By Definition 11,
$\triangleright(\mathfrak{r}(X)\circ\triangleright\mathfrak{r}(Y))\Rightarrow\mathfrak{r}(Z)$,
$\triangleright(\mathfrak{r}(X)\circ\mathfrak{r}(Y))\Rightarrow\mathfrak{r}(Z)$
and
$\triangleright(\triangleright\mathfrak{r}(X)\circ\mathfrak{r}(Y))\Rightarrow\mathfrak{r}(Z))$
are $3$-reduced. Then we proceed as follows, in which the upper part is by
Lemma 8 and the final step is by $\mathcal{R}_{.3}$.

$r(\triangleright(X\circ\triangleright Y)\Rightarrow Z)$
$\triangleright(\mathfrak{r}(X)\circ\triangleright\mathfrak{r}(Y))\Rightarrow\mathfrak{r}(Z)$
$r(\triangleright(X\circ Y)\Rightarrow Z)$
$\triangleright(\mathfrak{r}(X)\circ\mathfrak{r}(Y))\Rightarrow\mathfrak{r}(Z)$
$r(\triangleright(\triangleright X\circ Y)\Rightarrow Z)$
$\triangleright(\triangleright\mathfrak{r}(X)\circ\mathfrak{r}(Y))\Rightarrow\mathfrak{r}(Z))$
$\triangleright\mathfrak{r}(X)\circ\triangleright\mathfrak{r}(Y)\Rightarrow\mathfrak{r}(Z)$

$\triangleright\mathfrak{r}(X)\circ\triangleright\mathfrak{r}(Y)\Rightarrow\mathfrak{r}(Z)$
is $3$-reduced. It may not be $r(\triangleright X\circ\triangleright
Y\Rightarrow Z)$ because it may contains superfluous substructures or
superfluous occurrences of $\mathrm{I}$. This can be handled by Lemma 8.

The case that $\mathcal{R}$ is a right $\Phi$-normal rule is similar to the
case that $\mathcal{R}$ is a left $\Phi$-normal rule.

###### Theorem 8.1

Let $\Xi$ be a set of $\Phi$-normal rules. Then $\mathrm{D}.\Xi$ is decidable.

###### Proof

Let $n$ be the cardinality of $\Xi$. By Lemmas 16 and 17, $\mathcal{S}$ is
provable in $\mathrm{D}.\Xi$ iff $\mathcal{S}$ is $\ast$-reduced and there
exists a $\max\\{n+1,3\\}$-reduced, irredundant, r-complexity-increasing proof
with subformula property for $r(\mathcal{S})$, each sequent in which is of
$r$-complexity less than or equal to $\mathcal{S}$.

By Lemma 15, the set of possible proofs only consisting of sequents in
$\Gamma_{\mathcal{S}}^{\max\\{n+1,3\\}}$ is finite. Therefore,
$\mathrm{D}.\Xi$ is decidable.

###  8.2 Scott-Lemmon axioms and primitive axioms

A class of axioms called _Scott-Lemmon axiomss_ subsumes a range of standard
normal modal axioms, e.g., reflexivity, transitivity, euclideanness, etc. They
are of the form:

$\Diamond^{h}\Box^{i}\varphi\to\Box^{j}\Diamond^{k}\varphi$

where $h,i,j,k\geq 0$ and $\Diamond^{n}\varphi$ (likewise, $\Box^{n}\varphi$)
denotes the formula $\varphi$ prefixed with $n$-occurrecnes of $\Diamond$
(resp. $\Box$).

[8] showed that an axiomatic extension of Hilbert-style tense logic can be
properly displayed (by adding structural rules to $\mathrm{D.Kt}$) iff it is
axiomatizable by a set of primitive axioms. It also provided a method to
obtain display calculi from such axiomatizations, which transform primitive
axioms into structural rules such that the rules preserve cut elimination when
added to $\mathrm{D.K}$ or $\mathrm{D.Kt}$.

Specifically, a formula is called a _primitive axiom_ if it is of the form
$\varphi\to\psi$ where both $\varphi$ and $\psi$ contain only variables,
$\top$, $\land$, $\lor$, $\blacklozenge$ and $\Diamond$ and $\varphi$ contains
each propositional variable at most once.

It is known that any Scott-Lemmon axiom
$\Diamond^{h}\Box^{i}\varphi\to\Box^{j}\Diamond^{k}\varphi$ is equivalent to
the following primitive axiom

$\blacklozenge^{h}\Diamond^{j}\varphi\to\Diamond^{i}\blacklozenge^{k}\varphi$

and its corresponding structural rule that preserves cut elimination is as
follows:

$\frac{(\ast\bullet\ast)^{i}\bullet^{k}X\Rightarrow
Y}{\bullet^{h}(\ast\bullet\ast)^{j}X\Rightarrow Y}$

where $(\ast\bullet\ast)^{i}$ is the sequence of symbols consisting of $i$
$\ast\bullet\ast$’s and $(\ast\bullet\ast)^{j}$ is the sequence of symbols
consisting of $j$ $\ast\bullet\ast$’s. Note that it is a left $\\{X\\}$-normal
rule, if $i+k\leq h+j$. Then we have the following corollary of Theorem 8.1.

###### Corollary 1

Let $\Gamma$ be a set of Scott-Lemmon axioms such that each formula in $\Xi$
is of the form $\Diamond^{h}\Box^{i}\varphi\to\Box^{j}\Diamond^{k}\varphi$
where $i+k\leq h+j$. Let $\Xi$ be the set of normal rules obtained from
$\Gamma$. Then $\mathrm{D.K}+\Xi$ is decidable.

The following is a table for some Scott-Lemmon axioms and their corresponding
structural rules:

Axioms | Corresponding structural rules
---|---
(D) $\Box\varphi\to\Diamond\varphi$ | $\dfrac{\ast\bullet\ast\bullet X\Rightarrow Y}{X\Rightarrow Y}$
(T) $\Box\varphi\to\varphi$ | $\dfrac{\ast\bullet\ast X\Rightarrow Y}{X\Rightarrow Y}$
(4) $\Box\varphi\to\Box\Box\varphi$ | $\dfrac{\ast\bullet\ast X\Rightarrow Y}{\ast\bullet\ast\ast\bullet\ast X\Rightarrow Y}$
(5) $\Diamond\varphi\to\Box\Diamond\varphi$ | $\dfrac{\ast\bullet\ast\bullet X\Rightarrow Y}{\bullet\ast\bullet\ast X\Rightarrow Y}$
(B) $\varphi\to\Box\Diamond\varphi$ | $\dfrac{\bullet X\Rightarrow Y}{\ast\bullet\ast X\Rightarrow Y}$
$(Alt_{1})$ $\Diamond\varphi\to\Box\varphi$ | $\dfrac{X\Rightarrow Y}{\bullet\ast\bullet\ast X\Rightarrow Y}$
$(T^{c})$ $\varphi\to\Box\varphi$ | $\dfrac{X\Rightarrow Y}{\ast\bullet\ast X\Rightarrow Y}$
$(4^{c})$ $\Box\Box\varphi\to\Box\varphi$ | $\dfrac{\ast\bullet\ast\ast\bullet\ast X\Rightarrow Y}{\ast\bullet\ast X\Rightarrow Y}$

$(.3):\Diamond\varphi\land\Diamond\psi\to\Diamond(\varphi\land\Diamond\psi)\lor\Diamond(\varphi\land\psi)\lor\Diamond(\Diamond\varphi\land\psi)$
is a primitive axiom that is not a Scott-Lemmon axioms. Its corresponding
structural rule is as follows:

$\frac{\triangleright(X\circ\triangleright Y)\Rightarrow
Z\quad\triangleright(X\circ Y)\Rightarrow Z\quad\triangleright(\triangleright
X\circ Y)\Rightarrow Z}{\triangleright X\circ\triangleright Y\Rightarrow Z}$

where $\triangleright$ is a abbreviation for $\ast\bullet\ast$. This rule
appeared in the poof of Theorem 8.1 as an example.

The corresponding rules for (4), (5), (B), ($Alt_{1}$), ($T^{c}$) and (.3) are
left $\\{X\\}$-normal rules. By Theorem 8.1, $\mathrm{D.K}+\Xi$ is decidable
for any $\Xi\subseteq\\{(4),(5),(B),(Alt_{1}),$ $(T^{c}),$ $(.3)\\}$.

Note that the structural rule for $(T)$ is not a left $\\{X\\}$-normal rule.
Therefore, Theorem 8.1 does not imply that the display calculus $\mathrm{S5}$
is decidable.

##  9 Conclusion

Extracting decidability from display calculus is an important question in
proof theory. A negative reuslt concerning the decidability of display logics
from [8] is that for a logic with at least two modal operators, it is
undecidable whether or not its display calculus is decidable. And according to
[8], “it is not known so far whether for monomodal logics the theorem holds as
well”.

This paper provides a partial answer by proving the decidability of display
calculus $\mathrm{D.K}$ and some of its extensions. Our result is not
contradictory to the negative result mentioned above because $\Diamond$,
$\blacklozenge$, $\Box$ and $\blacksquare$ are one modal operator in essence.
This is because $\Diamond$ and $\Box$, $\blacklozenge$ and $\blacksquare$ are
inter-definable in normal modal logics repectively and $\blacklozenge$ is the
tense dual of $\Box$.

## References

  * [1] A. Avron.  The method of hypersequents in the proof theory of propositional non-classical logics.  Technical Report 294–94, Institute of Computer Science, Tel Aviv University, Israel, 1996.
  * [2] N. Belnap.  Display logic.  Journal of Philosophical Logic, 11:375–417, 1982.
  * [3] K. Brünnler.  Deep sequent systems for modal logic.  Archive for Mathematical Logic, 48(6):551–577, 2009.
  * [4] J. Chen, G. Greco, A. Palmigiano, and A. Tzimoulis.  Syntactic completeness of proper display calculi.  ACM Transactions on Computational Logic, 23(4):1–46, 2022.
  * [5] A. Ciabattoni and R. Ramanayake.  Power and limits of structural display rules.  ACM Transactions on Computational Logic (TOCL), 17(3):1–39, 2016\.
  * [6] R. Goré.  On the completeness of classical modal display logic.  Proof theory of modal logic, pages 137–140, 1996.
  * [7] G. Greco, M. Ma, A. Palmigiano, A. Tzimoulis, and Z. Zhao.  Unified correspondence as a proof-theoretic tool.  Journal of Logic and Computation, 28(7):1367–1442, 2018.
  * [8] M. Kracht.  Power and weakness of the modal display calculus.  In Proof theory of modal logic, pages 93–121. Springer, 1996.
  * [9] S. Negri.  Proof analysis in modal logic.  Journal of Philosophical Logic, 34(5-6):507, 2005.
  * [10] H. Ono et al.  Proof-theoretic methods in nonclassical logic–an introduction.  Theories of types and proofs, 2:207–254, 1998.
  * [11] F. Poggiolesi.  A cut-free simple sequent calculus for modal logic S5.  The Review of Symbolic Logic, 1(1):3–15, 2008.
  * [12] G. Restall.  Display logic and gaggle theory.  Reports Math. Log., 29:133–146, 1995.
  * [13] G. Restall.  Displaying and deciding substructural logics 1: Logics with contraposition.  Journal of Philosophical Logic, 27:179–216, 1998.
  * [14] M. Takano.  Subformula property as a substitute for cut-elimination in modal propositional logics.  Mathematica japonica, 37:1129–1145, 1992.
  * [15] H. Wansing.  Displaying modal logic, volume 3.  Springer Science & Business Media, 2013.