$\lambda_{2}:=\mathcal{R}_{2},\Gamma_{2}\Rightarrow\Delta_{2}$, and (ii)
$\lambda=\lambda_{1}^{\prime}\oplus_{u}\lambda_{2}^{\prime}$. By Lemma 5,
$\lambda_{1}\oplus_{w}\lambda_{2}$ and
$\lambda_{1}^{\prime}\oplus_{u}\lambda_{2}^{\prime}$ may be any arbitrary
$w$-partition and $u$-partition of $\lambda$.

Base case. We assume that length of the minimal path between $w$ and $u$ is is
one as the case when the length of the minimal path is zero (i.e. $w=u$)
follows from Lemma 5 above. We prove that
$\mathfrak{D}_{w}(\lambda)\equiv\mathfrak{D}_{u}(\lambda)$ and have four cases
to consider: either $Rwu\in\mathcal{R}_{1}$, $Ruw\in\mathcal{R}_{1}$,
$Rwu\in\mathcal{R}_{2}$, or $Ruw\in\mathcal{R}_{2}$. We argue the first case
as the others are proven in a similar fashion.

The display sequent
$\mathfrak{D}_{w}(\lambda)=\mathfrak{D}_{1}^{w}(\lambda_{1})\vdash\mathfrak{D}_{2}^{w}(\lambda_{2})$
is of the form shown below top, and we let $u_{1}=u$ for convenience.

$\mathfrak{D}_{w}(\lambda)=(\Gamma_{1}\restriction
w)\circ{\ast}(\Delta_{1}\restriction
w)\circ{\ast}{\bullet}{\ast}\mathfrak{D}_{1}^{u}(\lambda|^{w}_{u})\circ
X\vdash{\ast}(\Gamma_{2}\restriction w)\circ(\Delta_{2}\restriction w)\circ Y$
$X:=\mathop{\scalebox{1.5}{$\bigcirc$}}\limits_{i=2}^{n}{\ast}{\bullet}{\ast}\mathfrak{D}_{1}^{u_{i}}(\lambda|_{u_{i}}^{w})\circ\mathop{\scalebox{1.5}{$\bigcirc$}}\limits_{j=1}^{m}{\bullet}\mathfrak{D}_{1}^{v_{j}}(\lambda|_{v_{j}}^{w})\quad
Y:=\mathop{\scalebox{1.5}{$\bigcirc$}}\limits_{i=1}^{k}{\bullet}\mathfrak{D}_{2}^{x_{i}}(\lambda|_{x_{i}}^{w})\circ\mathop{\scalebox{1.5}{$\bigcirc$}}\limits_{j=1}^{l}{\ast}{\bullet}{\ast}\mathfrak{D}_{2}^{y_{j}}(\lambda|_{y_{j}}^{w})$

We may now apply the following sequence of rules to the display sequent above
to derive the conclusion shown below.

$(\Gamma_{1}\restriction w)\circ{\ast}(\Delta_{1}\restriction
w)\circ{\ast}{\bullet}{\ast}\mathfrak{D}_{1}^{u}(\lambda|^{w}_{u})\circ
X\vdash{\ast}(\Gamma_{2}\restriction w)\circ(\Delta_{2}\restriction w)\circ Y$
$(\delta_{2})$ $(\Gamma_{2}\restriction w)\circ(\Gamma_{1}\restriction
w)\circ{\ast}(\Delta_{1}\restriction
w)\circ{\ast}{\bullet}{\ast}\mathfrak{D}_{1}^{u}(\lambda|^{w}_{u})\circ
X\vdash(\Delta_{2}\restriction w)\circ Y$ $(p_{l})$
${\ast}(\Delta_{1}\restriction w)\circ(\Gamma_{1}\restriction
w)\circ(\Gamma_{2}\restriction
w)\circ{\ast}{\bullet}{\ast}\mathfrak{D}_{1}^{u}(\lambda|^{w}_{u})\circ
X\vdash(\Delta_{2}\restriction w)\circ Y$ $(\delta_{4})$
$(\Gamma_{1}\restriction w)\circ(\Gamma_{2}\restriction
w)\circ{\ast}{\bullet}{\ast}\mathfrak{D}_{1}^{u}(\lambda|^{w}_{u})\circ
X\vdash(\Delta_{1}\restriction w)\circ(\Delta_{2}\restriction w)\circ Y$ . =
$(\Gamma\restriction
w)\circ{\ast}{\bullet}{\ast}\mathfrak{D}_{1}^{u}(\lambda|^{w}_{u})\circ
X\vdash(\Delta\restriction w)\circ Y$ $(\delta_{2})$
${\ast}{\bullet}{\ast}\mathfrak{D}_{1}^{u}(\lambda|^{w}_{u})\circ
X\vdash{\ast}(\Gamma\restriction w)\circ(\Delta\restriction w)\circ Y$

By the display theorem (Theorem 3.2), we can display each a-part
$\mathfrak{D}_{1}^{u_{i}}(\lambda|_{u_{i}}^{w})$ and
$\mathfrak{D}_{1}^{v_{j}}(\lambda|_{v_{j}}^{w})$ in $X$ and apply Lemma 6 to
derive the following display sequent.

${\ast}{\bullet}{\ast}\mathfrak{D}_{1}^{u}(\lambda|^{w}_{u})\circ\mathop{\scalebox{1.5}{$\bigcirc$}}\limits_{i=2}^{n}{\ast}{\bullet}{\ast}{\ast}\mathfrak{D}_{2}^{u_{i}}(\lambda|_{u_{i}}^{w})\circ\mathop{\scalebox{1.5}{$\bigcirc$}}\limits_{j=1}^{m}{\bullet}{\ast}\mathfrak{D}_{2}^{v_{j}}(\lambda|_{v_{j}}^{w})\vdash{\ast}(\Gamma\restriction
w)\circ(\Delta\restriction w)\circ Y$

Applying display and reversible structural rules, the following display
sequent is derivable from the one above.

${\ast}{\bullet}{\ast}\mathfrak{D}_{1}^{u}(\lambda|^{w}_{u})\circ\mathop{\scalebox{1.5}{$\bigcirc$}}\limits_{i=2}^{n}{\ast}{\bullet}\mathfrak{D}_{2}^{u_{i}}(\lambda|_{u_{i}}^{w})\circ\mathop{\scalebox{1.5}{$\bigcirc$}}\limits_{j=1}^{m}{\bullet}{\ast}\mathfrak{D}_{2}^{v_{j}}(\lambda|_{v_{j}}^{w})\vdash{\ast}(\Gamma\restriction
w)\circ(\Delta\restriction w)\circ Y$

Again, we may apply display and reversible structural rules to derive the
following display sequent from the one above.

${\ast}{\bullet}{\ast}\mathfrak{D}_{1}^{u}(\lambda|^{w}_{u})\vdash{\ast}(\Gamma\restriction
w)\circ(\Delta\restriction w)\circ Y^{\prime}$
$Y^{\prime}:=\mathop{\scalebox{1.5}{$\bigcirc$}}\limits_{i=2}^{n}{\bullet}\mathfrak{D}_{2}^{u_{i}}(\lambda|_{u_{i}}^{w})\circ\mathop{\scalebox{1.5}{$\bigcirc$}}\limits_{i=1}^{k}{\bullet}\mathfrak{D}_{2}^{x_{i}}(\lambda|_{x_{i}}^{w})\circ\mathop{\scalebox{1.5}{$\bigcirc$}}\limits_{j=1}^{m}{\ast}{\bullet}{\ast}\mathfrak{D}_{2}^{v_{j}}(\lambda|_{v_{j}}^{w})\circ\mathop{\scalebox{1.5}{$\bigcirc$}}\limits_{j=1}^{l}{\ast}{\bullet}{\ast}\mathfrak{D}_{2}^{y_{j}}(\lambda|_{y_{j}}^{w})$

By using $(\rho_{1})$ from Figure 4, we can derive

$\mathfrak{D}_{1}^{u}(\lambda|^{w}_{u})\vdash{\ast}{\bullet}{\ast}({\ast}(\Gamma\restriction
w)\circ(\Delta\restriction w)\circ
Y^{\prime})=\mathfrak{D}_{1}^{u}(\lambda|^{w}_{u})\vdash\mathfrak{D}_{2}^{u}(\lambda|^{u}_{w}\otimes(Rwu\Rightarrow\emptyset))$

from the former display sequent above. By Lemma 5, since
$\lambda|^{w}_{u}\oplus_{u}(\lambda|^{u}_{w}\otimes(Rwu\Rightarrow\emptyset))$
is a $u$-partition of $\lambda$, we know that
$\mathfrak{D}_{u}(\lambda|^{w}_{u}\oplus_{u}(\lambda|^{u}_{w}\otimes(Rwu\Rightarrow\emptyset)))\equiv\mathfrak{D}_{u}(\lambda_{1}^{\prime}\otimes\lambda_{2}^{\prime})$,
and so, we have shown that
$\mathfrak{D}_{w}(\lambda)\equiv\mathfrak{D}_{u}(\lambda)$ since only display
and reversible structural rules were used above.

Inductive step. Suppose that the length of the minimal path of relational
atoms between $w$ and $u$ is $n+1$. Then, there exists a label $v$ such that
the length of the minimal path from $w$ to $v$ is at most length $n$ and
length of the minimal path from $v$ to $u$ is $1$. Hence, by IH ,
$\mathfrak{D}_{w}(\lambda)\equiv\mathfrak{D}_{v}(\lambda)$ and
$\mathfrak{D}_{v}(\lambda)\equiv\mathfrak{D}_{u}(\lambda)$, which implies the
desired result and concludes the inductive step.

Last, observe that only reversible rules were used in the proofs of Lemma 5,
Lemma 6, and in the derivation of $\mathfrak{D}_{u}(\lambda)$ from
$\mathfrak{D}_{w}(\lambda)$ above. Furthermore, the number of rules applied
only depends on the length $n$ of the path from $w$ to $u$ in $\mathcal{R}$
along with the number of incoming and outgoing edges (i.e. relational atoms)
from nodes (i.e. labels) along this path. The above proof describes an
algorithm that takes this path with incoming and outgoing edges as input and
computes successive rule applications by processing ever smaller terminal
segments of this path until $\mathfrak{D}_{u}(\lambda)$ is reached. Since the
length of the path $n\leq\ell(\lambda)$, one can verify that for a polynomial
$p$, $p(\ell(\lambda))$-many reversible inferences occur in the derivation of
$\mathfrak{D}_{u}(\lambda)$ from $\mathfrak{D}_{w}(\lambda)$.

##  7 From Display to Labeled Proofs

We show how to translate each display proof in $\mathsf{DK_{t}P}$ into a
strict labeled polytree proof in $\mathsf{G3K_{t}P}$. Moreover, we argue that
this translation is computable in $\mathrm{PTIME}$ and does not increase the
size of the proof. This result is significant for the following reasons:
first, we establish that each labeled calculus $\mathsf{G3K_{t}P}$ can
polynomially simulate each display calculus $\mathsf{DK_{t}P}$, showing that
display calculi cannot outperform (in terms of complexity) labeled calculi.
Second, we identify what subspace of labeled proofs correspond to display
proofs, and in the following section, we show that each labeled proof within
this space can be translated in $\mathrm{PTIME}$ into a display proof as well,
giving a characterization result. In essence, we find that display calculi are
a restriction of labeled calculi and that the space of display proofs is a
fragment of the space of labeled proofs.

Let us first show how to translate proofs from the base system
$\mathsf{DK_{t}}$ into $\mathsf{G3K_{t}}$. In the sequel, we explain how this
translation can be augmented to translate primitive tense structural rules as
well, giving the main result of the section (Theorem 7.2).

###### Theorem 7.1

If $\mathsf{DK_{t}},\Uppi\Vdash\delta$, then there exists a $\mathrm{PTIME}$
function $f$ in $s(\Uppi)$ such that
$\mathsf{G3K_{t}},f(\Uppi)\Vdash\mathfrak{L}_{w}(\delta)$,
$s(f(\Uppi))=\mathcal{O}(s(\Uppi)^{2})$, and $f(\Uppi)$ is a labeled polytree
proof.

###### Proof

Suppose $\mathsf{DK_{t}},\Uppi\Vdash\delta$. We show by induction on the
quantity of $\Uppi$ that it can be translated in $\mathrm{PTIME}$ into a
labeled polytree proof $f(\Uppi)$ of $\mathfrak{L}_{w}(\delta)$ in
$\mathsf{G3K_{t}}$ such that $s(f(\Uppi))\leq s(\Uppi)$. By Lemma 4, we need
not translate instances of $(I_{l})$, $(I_{r})$, $(q_{l})$, $(q_{r})$,
$(a_{l})$, $(a_{r})$, $(p_{l})$, $(p_{r})$, or the display rules, as all such
rules produce isomorphic or identical labeled polytree sequents under the
$\mathfrak{L}_{w}$ translation. Below, when we invoke the qp-admissibility of
$(w)$ (Theorem 4.1), we note that $(w)$ will always be an instance of
$(\bar{w})$, which ensures that the polytree structure of labeled sequents in
the target proof will be preserved (Theorem 5.2).

Base case. We show how the initial rules $(id)$, $(\top_{r})$, and
$(\bot_{l})$ are translated from $\mathsf{DK_{t}}$ to initial rules in
$\mathsf{LK_{t}}$. Observe that each initial sequent is a labeled polytree
sequent.

$(id)$ $p\vdash p$ | $\leadsto$ |  $(\top_{r})$ $\emptyset\Rightarrow w:\top$ . = $\mathfrak{L}_{1}^{w}(I)\otimes\mathfrak{L}_{2}^{w}(\top)$ . = $\mathfrak{L}_{w}(I\vdash\top)$
---|---|---
$(\bot_{l})$ $\bot\vdash I$ | $\leadsto$ |  $(\bot_{l})$ $w:\bot\Rightarrow\emptyset$ . = $\mathfrak{L}_{1}^{w}(\bot)\otimes\mathfrak{L}_{2}^{w}(I)$ . = $\mathfrak{L}_{w}(\bot\vdash I)$
---|---|---

Inductive step. For the inductive step, we give a few interesting cases of
translating inferences from the given display proof into the target labeled
proof. The remaining cases can be found in the appendix as they are either
simple or similar. In each case, it can be checked that the result is a
labeled polytree proof.

$I\vdash Y$ $(\top_{l})$ $\top\vdash Y$ | $\leadsto$ |  IH $\mathfrak{L}_{w}(I\vdash Y)$ . = $\mathfrak{L}_{1}^{w}(I)\otimes\mathfrak{L}_{2}^{w}(Y)$ $(\bar{w})$ $(w:\top\Rightarrow\emptyset)\otimes\mathfrak{L}_{1}^{w}(I)\otimes\mathfrak{L}_{2}^{w}(Y)$ . = $\mathfrak{L}_{1}^{w}(\top)\otimes\mathfrak{L}_{2}^{w}(Y)$ . = $\mathfrak{L}_{w}(\top\vdash Y)$
---|---|---
$X\vdash{\ast}A$ $(\neg_{r})$ $X\vdash\neg A$ | $\leadsto$ |  IH $\mathfrak{L}_{w}(X\vdash{\ast}A)$ . = $\mathfrak{L}_{2}^{w}(X)\otimes\mathfrak{L}_{1}^{w}(A)$ $(\neg_{r})$ $\mathfrak{L}_{1}^{w}(X)\otimes\mathfrak{L}_{2}^{w}(\neg A)$ . = $\mathfrak{L}_{w}(X\vdash\neg A)$
---|---|---

When translating the $(\rightarrow_{l})$ rule below, observe that we invoke
the qp-admissibility of $(\bar{w})$ (Lemma 4.1) to ensure that the contexts of
the premises in the labeled proof match.

$X\vdash A$ $B\vdash Y$ $(\rightarrow_{l})$ $A\rightarrow B\vdash{\ast}X\circ Y$ | $\leadsto$
---|---
IH $\mathfrak{L}_{w}(X\vdash A)$ . =
$\mathfrak{L}_{1}^{w}(X)\otimes\mathfrak{L}_{2}^{w}(A)$ . =
$\mathfrak{L}_{1}^{w}(X)\otimes(\emptyset\Rightarrow w:A)$ $(\bar{w})$
$\mathfrak{L}_{1}^{w}(X)\otimes\mathfrak{L}_{2}^{w}(Y)\otimes(\emptyset\Rightarrow
w:A)$ IH $\mathfrak{L}_{w}(B\vdash Y)$ . =
$\mathfrak{L}_{1}^{w}(B)\otimes\mathfrak{L}_{2}^{w}(Y)$ . =
$(w:B\Rightarrow\emptyset)\otimes\mathfrak{L}_{2}^{w}(Y)$ $(\bar{w})$
$(w:B\Rightarrow\emptyset)\otimes\mathfrak{L}_{1}^{w}(X)\otimes\mathfrak{L}_{2}^{w}(Y)$
$(\rightarrow_{l})$
$\mathfrak{L}_{1}^{w}(X)\otimes\mathfrak{L}_{2}^{w}(Y)\otimes(w:A\rightarrow
B\Rightarrow\emptyset)$ . =
$\mathfrak{L}_{2}^{w}({\ast}X)\otimes\mathfrak{L}_{2}^{w}(Y)\otimes(w:A\rightarrow
B\Rightarrow\emptyset)$ . = $\mathfrak{L}_{2}^{w}({\ast}X\circ
Y)\otimes(w:A\rightarrow B\Rightarrow\emptyset)$ . =
$\mathfrak{L}_{1}^{w}(A\rightarrow B)\otimes\mathfrak{L}_{2}^{w}({\ast}X\circ
Y)$ . = $\mathfrak{L}_{w}(A\rightarrow B\Rightarrow{\ast}X\circ Y)$
---

Lemma 4 is invoked in translating the $([\mathsf{G}]_{r})$ and
$(\langle\mathsf{P}\rangle_{r})$ inferences below.

${\bullet}X\vdash A$ $([\mathsf{G}]_{r})$ $X\vdash[\mathsf{G}]A$ | $\leadsto$ |  IH $\mathfrak{L}_{w}({\bullet}X\vdash A)$ . $\cong$ (Lemma 4) $\mathfrak{L}_{w}(X\vdash{\bullet}A)$ . = $\mathfrak{L}_{1}^{w}(X)\otimes\mathfrak{L}_{2}^{w}({\bullet}A)$ . = $\mathfrak{L}_{1}^{w}(X)\otimes(Rwu\Rightarrow u:A)$ $([\mathsf{G}]_{r})$ $\mathfrak{L}_{1}^{w}(X)\otimes(\emptyset\Rightarrow w:[\mathsf{G}]A)$ . = $\mathfrak{L}_{1}^{w}(X)\otimes\mathfrak{L}_{2}^{w}([\mathsf{G}]A)$ . = $\mathfrak{L}_{w}(X\vdash[\mathsf{G}]A)$
---|---|---
$X\vdash A$ $(\langle\mathsf{P}\rangle_{r})$ ${\bullet}X\vdash\langle\mathsf{P}\rangle A$ | $\leadsto$ |  IH $\mathfrak{L}_{w}(X\vdash A)$ . = $\mathfrak{L}_{1}^{w}(X)\otimes\mathfrak{L}_{2}^{w}(A)$ . = $\mathfrak{L}_{1}^{w}(X)\otimes(\emptyset\Rightarrow w:A)$ $(\langle\mathsf{P}\rangle_{r2})$ $\mathfrak{L}_{1}^{w}(X)\otimes(Ruw\Rightarrow u:\langle\mathsf{P}\rangle A)$ . = $\mathfrak{L}_{1}^{w}(X)\otimes(Ruw\Rightarrow\emptyset)\otimes(\emptyset\Rightarrow u:\langle\mathsf{P}\rangle A)$ . = $\mathfrak{L}_{1}^{w}({\bullet}X)\otimes\mathfrak{L}_{2}^{w}(A)$ . = $\mathfrak{L}_{u}({\bullet}X\vdash A)$ . $\cong$ (Lemma 3) $\mathfrak{L}_{w}({\bullet}X\vdash A)$
---|---|---

Since $(\bar{w})$ is not an explicit rule in $\mathsf{LK_{t}}$, we apply the
qp-admissibility of $(\bar{w})$ below to resolve the case of translating
$(w_{l})$.

$X\vdash Y$ $(w_{l})$ $Z\circ X\vdash Y$ | $\leadsto$ |  IH $\mathfrak{L}_{w}(X\vdash Y)$ . = $\mathfrak{L}_{1}^{w}(X)\otimes\mathfrak{L}_{2}^{w}(Y)$ $(\bar{w})$ $\mathfrak{L}_{1}^{w}(Z)\otimes\mathfrak{L}_{1}^{w}(X)\otimes\mathfrak{L}_{2}^{w}(Y)$ . = $\mathfrak{L}_{1}^{w}(Z\circ X)\otimes\mathfrak{L}_{2}^{w}(Y)$ . = $\mathfrak{L}_{u}(Z\circ X\vdash Y)$ . $\cong$ (Lemma 3) $\mathfrak{L}_{w}(Z\circ X\vdash Y)$
---|---|---

As can be seen below, $(c_{r})$ relies on the qp-admissibility of
$(\bar{ls})$, $(c_{l})$, and $(c_{r})$ in $\mathsf{G3K_{t}}$. After
$\mathfrak{L}_{1}^{w}(X)\otimes\mathfrak{L}_{2}^{w}(Y)\otimes\mathfrak{L}_{2}^{w}(Y)$
is obtained, we apply $(\bar{ls})$ to identify the two isomorphic copies of
$\mathfrak{L}_{2}^{w}(Y)$, making both copies _identical_ , and then the
contraction rules $(c_{l})$ and $(c_{r})$ are applied to contract identical
labeled formulae, yielding the desired conclusion. We note that these
operations can be applied in a manner to produce a labeled polytree proof as
the output (see Example 6).

$X\vdash Y\circ Y$ $(c_{r})$ $X\vdash Y$ | $\leadsto$ |  IH $\mathfrak{L}_{w}(X\vdash Y\circ Y)$ . = $\mathfrak{L}_{1}^{w}(X)\otimes\mathfrak{L}_{2}^{w}(Y\circ Y)$ . = $\mathfrak{L}_{1}^{w}(X)\otimes\mathfrak{L}_{2}^{w}(Y)\otimes\mathfrak{L}_{2}^{w}(Y)$ $(\bar{ls})$, $(c_{l})$, $(c_{r})$ $\mathfrak{L}_{1}^{w}(X)\otimes\mathfrak{L}_{2}^{w}(Y)$ . = $\mathfrak{L}_{u}(X\vdash Y)$
---|---|---

It is straightforward to check that the above translation is in
$\mathrm{PTIME}$ relative to $s(\Uppi)$ since each display sequent in $\Uppi$
is translated in $\mathrm{PTIME}$ and each qp-admissible rule application
transforms the target proof in $\mathrm{PTIME}$ (Remark 1). Also, since each
inference translated derives a labeled polytree sequent, $f(\Uppi)$ will be a
labeled polytree proof by Proposition 3. One can confirm in each case that
$q(f(\Uppi))\leq q(\Uppi)$ since either a single inference is performed in the
target proof, an qp-admissible rule (that does not appear in the target proof)
is applied, or a redundant, ineffectual inference occurs (see Lemma 4). By
Lemma 3, we know that for each $\delta$ in the input proof
$\ell(\mathfrak{L}_{w}(\delta))\leq\ell(\delta)$. Nevertheless, it is possible
for the length of a labeled polytree sequent to increase in the target proof
if the qp-admissibility of $(\bar{w})$ is applied. However, the length can
only increase by at most $w(\Uppi)\times q(\Uppi)$ since applying the qp-
admissibility of $(\bar{w})$ in the target proof runs an algorithm (see Remark
1) that permutes $(\bar{w})$ upward and ‘deposits’ at most $w(\Uppi)$ amount
of syntactic material in each labeled sequent (increasing its length) at most
$q(\Uppi)$ many times. Putting all of the above together, we have that

$s(f(\Uppi))=q(f(\Uppi))\times w(f(\Uppi))\leq q(\Uppi)\times q(\Uppi)\times
w(\Uppi)$

showing that $s(f(\Uppi))=\mathcal{O}(s(\Uppi)^{2})$.

Let us now consider translating display proofs to labeled (polytree) proofs in
the presence of primitive tense structural rules. We carry out this
translation by considering an instance of a primitive tense structural rule
$(pt_{\delta})$ under a substitution $\sigma$, and show that the instance can
be translated via $\mathfrak{L}_{w}$ to an instance of $(pt_{\lambda})$ under
a related substitution, denoted $\sigma^{\mathfrak{L}}$. This is sufficient to
prove the main result of this section (Theorem 7.2), which states that each
proof in $\mathsf{DK_{t}P}$ can be translated in $\mathrm{PTIME}$ into a
strict labeled polytree proof in $\mathsf{G3K_{t}P}$ such that the quantity of
the proof does not grow.

Let us consider an instance of a primitive tense structural rule
$(pt_{\delta})$ under a substitution $\sigma$, as shown below.

$(\psi(B_{1})\vdash\dot{X})\sigma$ $\ldots$ $(\psi(B_{m})\vdash\dot{X})\sigma$
$(pt_{\delta})$ $(\psi(A)\vdash\dot{X})\sigma$

Let us assume that $X_{p_{1}},\ldots,X_{p_{n}},\dot{X}$ are all of the
structure variables occurring in the $(pt_{\delta})$ rule above with $\sigma$
a substitution of the following form:

$\sigma:=[X_{1}/\dot{X}_{p_{1}},\ldots,X_{n}/\dot{X}_{p_{n}},X/\dot{X}].$

To translate the above instance of $(pt_{\delta})$ to an instance of
$(pt_{\lambda})$ under $\mathfrak{L}_{w}$, we define the substitution
$\sigma^{\mathfrak{L}}$ accordingly:

$\sigma^{\mathfrak{L}}:=[\mathfrak{L}_{1}^{u_{1}}(X_{1})/\dot{\lambda}_{p_{1}}^{\dot{u}_{1}},\ldots,\mathfrak{L}_{1}^{u_{n}}(X_{n})/\dot{\lambda}_{p_{n}}^{\dot{u}_{n}},\mathfrak{L}_{2}^{w}(X)/\dot{\lambda},u_{1}/\dot{u}_{1},\ldots,u_{n}/\dot{u}_{n},w/\dot{w}].$

In the definition of $\sigma^{\mathfrak{L}}$ above, we let all labels in
$\mathfrak{L}_{1}^{u_{1}}(X_{1})$, $\ldots$,
$\mathfrak{L}_{1}^{u_{n}}(X_{n})$, and $\mathfrak{L}_{2}^{w}(X)$ be fresh with
the exception of $u_{1}$, $\ldots$, $u_{n}$, and $w$, respectively. We note
that if $\dot{X}_{p_{i}}\sigma=X_{i}$ for $1\leq i\leq n$, then for each
labeled sequent variable
$\dot{\lambda}_{p_{i}}^{\dot{v}_{1}},\ldots,\dot{\lambda}_{p_{i}}^{\dot{v}_{k}}$
in $(pt_{\lambda})$ annotated with $p_{i}$, we have
$\dot{\lambda}_{p_{i}}^{\dot{v}_{j}}\sigma^{\mathfrak{L}}=\mathfrak{L}_{1}^{v_{j}}(X_{i})$
and $\dot{v}_{j}\sigma^{\mathfrak{L}}=v_{j}$ for $1\leq j\leq k$. In other
words, the substitution of a structure for a single structure variable in
$\sigma$ may give rise to multiple substitutions of labeled polytree sequents
for multiple labeled sequent variables in $\sigma^{\mathfrak{L}}$.

###### Example 9

We give an example of translating an instance of $(pt_{\delta})$ into an
instance of $(pt_{\lambda})$. The $(pt_{\delta})$ rule (shown below left)
corresponds to the simple primitive tense axiom $\langle\mathsf{F}\rangle
p\rightarrow\langle\mathsf{P}\rangle(p\land\langle\mathsf{F}\rangle p)$, where
we let $A=\langle\mathsf{F}\rangle p$ and
$B=\langle\mathsf{P}\rangle(p\land\langle\mathsf{F}\rangle p)$. An instance of
the rule under the substitution
$\sigma=[q/\dot{X}_{p},\langle\mathsf{P}\rangle p\lor q/\dot{X}]$ is shown
below right.

${\bullet}(\dot{X}_{p}\circ{\ast}{\bullet}{\ast}\dot{X}_{p})\vdash\dot{X}$ $(pt_{\delta})$ ${\ast}{\bullet}{\ast}\dot{X}_{p}\vdash\dot{X}$ |  ${\bullet}(q\circ{\ast}{\bullet}{\ast}q)\vdash\langle\mathsf{P}\rangle p\lor q$ $(pt_{\delta})$ ${\ast}{\bullet}{\ast}q\vdash\langle\mathsf{P}\rangle p\lor q$
---|---

If we transform $\langle\mathsf{F}\rangle
p\rightarrow\langle\mathsf{P}\rangle(p\land\langle\mathsf{F}\rangle p)$ into
$(pt_{\lambda})$, we obtain the rule shown below.

$(R\dot{w}\dot{u}\Rightarrow)\otimes(R\dot{v}\dot{w}\Rightarrow)\otimes(R\dot{v}\dot{z}\Rightarrow)\otimes\dot{\lambda}_{p}^{\dot{u}}\otimes\dot{\lambda}_{p}^{\dot{v}}\otimes\dot{\lambda}_{p}^{\dot{z}}\vdash\dot{\lambda}$
$(pt_{\delta})$
$(R\dot{w}\dot{u}\Rightarrow)\otimes\dot{\lambda}_{p}^{\dot{u}}\vdash\dot{\lambda}$

To obtain the corresponding instance of $(pt_{\delta})$, we apply the
following substitution

$\sigma^{\mathfrak{L}}:=[\lambda_{u}/\dot{\lambda}_{p}^{\dot{u}},\lambda_{v}/\dot{\lambda}_{p}^{\dot{v}},\lambda_{z}/\dot{\lambda}_{p}^{\dot{z}},\lambda/\dot{\lambda},u/\dot{u},v/\dot{v},z/\dot{z}]$

where $\lambda_{u}=(u:q\Rightarrow)$, $\lambda_{v}=(v:q\Rightarrow)$,
$\lambda_{z}=(z:q\Rightarrow)$, and $\lambda=(\Rightarrow
w:\langle\mathsf{P}\rangle p\lor r)$. Applying $\sigma^{\mathfrak{L}}$ to
$(pt_{\lambda})$ gives the following strict instance of the rule.

$Rwu,Rvw,Rvz,u:q,v:q,z:q\Rightarrow w:\langle\mathsf{P}\rangle p\lor q$
$(pt_{\lambda})$ $Rwu,u:q\Rightarrow w:\langle\mathsf{P}\rangle p\lor q$

It is interesting to observe that $(pt_{\delta})$ under $\sigma$ translates
via $\mathfrak{L}_{w}$ into $(pt_{\lambda})$ under $\sigma^{\mathfrak{L}}$.
Since $(pt_{\lambda})$ retains a copy of $\varphi_{\dot{w}}(A)$ in its
premise, we must include a copy of $\psi(A)$ when translating the premise of
$(pt_{\delta})$ under $\sigma$ as shown below.

$\mathfrak{L}_{w}(\underbrace{{\bullet}({\ast}{\bullet}{\ast}q)}_{\psi(A)\sigma}\circ\underbrace{{\bullet}(q\circ{\ast}{\bullet}{\ast}q)}_{\psi(B)\sigma}\vdash\dot{X})=Rwu,Rvw,Rvz,u:q,v:q,z:q\Rightarrow
w:\langle\mathsf{P}\rangle p\lor q$

Alternatively, the conclusion of $(pt_{\delta})$ under $\sigma$ translates to
the conclusion of $(pt_{\lambda})$ under $\sigma^{\mathfrak{L}}$ without
modification:
$\mathfrak{L}_{w}({\ast}{\bullet}{\ast}q\vdash\langle\mathsf{P}\rangle p\lor
q)=Rwu,u:q\Rightarrow w:\langle\mathsf{P}\rangle p\lor q$.

As demonstrated in the example above, instances of $(pt_{\delta})$ translate
to strict instances of $(pt_{\lambda})$. We use this fact below to prove the
main result of the section (Theorem 7.2), however, it will be helpful to first
prove the following lemma.

###### Lemma 8

Let us consider an instance of a primitive tense structural rule as shown
below.

$(\psi(B_{1})\vdash\dot{X})\sigma$ $\ldots$ $(\psi(B_{m})\vdash\dot{X})\sigma$
$(pt_{\delta})$ $(\psi(A)\vdash\dot{X})\sigma$

and let $C\in\\{A,B_{1},\ldots,B_{m}\\}$. Then,

  1. 1.

$\mathfrak{L}^{w}_{1}(\psi(C)\sigma)=\varphi_{\dot{w}}(C)\sigma^{\mathfrak{L}}$

  2. 2.

$\mathfrak{L}_{w}((\psi(C)\vdash\dot{X})\sigma)=(\varphi_{\dot{w}}(C)\otimes\dot{\lambda})\sigma^{\mathfrak{L}}$

###### Proof

We first prove claim 1 by induction on the complexity of $C$.

Base case. If $C$ is an atom $p_{i}$, then $\psi(p_{i})=\dot{X}_{p_{i}}$ and
the proof shown below left demonstrates the claim. If $A$ is the logical
constant $\top$, so that $\psi(A)=\psi(\top)=I$, then the proof shown below
right demonstrates the claim.
$\displaystyle\mathfrak{L}^{w}_{1}(\psi(p_{i})\sigma)$
$\displaystyle\mathfrak{L}^{w}_{1}(\dot{X}_{p_{i}}\sigma)$
$\displaystyle\mathfrak{L}^{w}_{1}(X_{i})$
$\displaystyle\dot{\lambda}_{p_{i}}^{\dot{w}}\sigma^{\mathfrak{L}}$
$\displaystyle\varphi_{\dot{w}}(p)\sigma^{\mathfrak{L}}$
$\displaystyle\mathfrak{L}^{w}_{1}(\psi(\top)\sigma)$
$\displaystyle\mathfrak{L}^{w}_{1}(I\sigma)$
$\displaystyle\mathfrak{L}^{w}_{1}(I)$
$\displaystyle\emptyset\Rightarrow\emptyset$
$\displaystyle\varphi_{\dot{w}}(\top)\sigma^{\mathfrak{L}}$

Inductive step. We consider the cases where $C=D\land E$,
$C=\langle\mathsf{F}\rangle D$, and $C=\langle\mathsf{P}\rangle D$ in turn.
First, if $A=B\land C$, so that $\psi(C)=\psi(D\land E)=\psi(D)\circ\psi(E)$,
then the following proof establishes the case.
$\displaystyle\mathfrak{L}^{w}_{1}(\psi(D\land E)\sigma)$
$\displaystyle\mathfrak{L}^{w}_{1}((\psi(D)\circ\psi(E))\sigma)$
$\displaystyle\mathfrak{L}^{w}_{1}(\psi(D)\sigma)\otimes\mathfrak{L}^{w}_{1}(\psi(E)\sigma)$
$\displaystyle\varphi_{\dot{w}}(D)\sigma^{\mathfrak{L}}\otimes\varphi_{\dot{w}}(E)\sigma^{\mathfrak{L}}$
$\displaystyle(\varphi_{\dot{w}}(D)\otimes\varphi_{\dot{w}}(E))\sigma^{\mathfrak{L}}$
$\displaystyle\varphi_{\dot{w}}(D\land E)\sigma^{\mathfrak{L}}$

If $C=\langle\mathsf{F}\rangle D$, so that
$\psi(C)=\psi(\langle\mathsf{F}\rangle D)={\ast}\bullet{\ast}\psi(D)$, then
the proof shown below left establishes the case, and if
$C=\langle\mathsf{P}\rangle D$, so that $\psi(C)=\psi(\langle\mathsf{P}\rangle
D)={\bullet}\psi(D)$, then the proof shown below right establishes the case.
$\displaystyle\mathfrak{L}^{w}_{1}(\psi(\langle\mathsf{F}\rangle D)\sigma)$
$\displaystyle\mathfrak{L}^{w}_{1}(({\ast}\bullet{\ast}\psi(D))\sigma)$
$\displaystyle\mathfrak{L}^{w}_{1}({\ast}\bullet{\ast}(\psi(D)\sigma))$
$\displaystyle(Rwu\Rightarrow\emptyset)\otimes\mathfrak{L}^{u}_{1}(\psi(D)\sigma)$
$\displaystyle(Rwu\Rightarrow\emptyset)\otimes\varphi_{\dot{u}}(D)\sigma^{\mathfrak{L}}$
$\displaystyle((Rwu\Rightarrow\emptyset)\otimes\varphi_{\dot{u}}(D))\sigma^{\mathfrak{L}}$
$\displaystyle\varphi_{\dot{w}}(\langle\mathsf{F}\rangle
D)\sigma^{\mathfrak{L}}$
$\displaystyle\mathfrak{L}^{w}_{1}(\psi(\langle\mathsf{P}\rangle D)\sigma)$
$\displaystyle\mathfrak{L}^{w}_{1}((\bullet\psi(D))\sigma)$
$\displaystyle\mathfrak{L}^{w}_{1}(\bullet(\psi(D)\sigma))$
$\displaystyle(Ruw\Rightarrow\emptyset)\otimes\mathfrak{L}^{u}_{1}(\psi(D)\sigma)$
$\displaystyle(Ruw\Rightarrow\emptyset)\otimes\varphi_{\dot{u}}(D)\sigma^{\mathfrak{L}}$
$\displaystyle((Ruw\Rightarrow\emptyset)\otimes\varphi_{\dot{u}}(D))\sigma^{\mathfrak{L}}$
$\displaystyle\varphi_{\dot{w}}(\langle\mathsf{P}\rangle
D)\sigma^{\mathfrak{L}}$

The following establishes claim 2 and invokes claim 1 in the third to fourth
line.

$\displaystyle\mathfrak{L}_{w}((\psi(C)\vdash X)\sigma)$
$\displaystyle\mathfrak{L}_{w}(\psi(C)\sigma\vdash X\sigma)$
$\displaystyle\mathfrak{L}_{1}^{w}(\psi(C)\sigma)\otimes\mathfrak{L}_{2}^{w}(X\sigma)$
$\displaystyle\varphi_{\dot{w}}(C)\sigma^{\mathfrak{L}}\otimes\mathfrak{L}_{2}^{w}(X)$
$\displaystyle\varphi_{\dot{w}}(C)\sigma^{\mathfrak{L}}\otimes\dot{\lambda}\sigma^{\mathfrak{L}}$
$\displaystyle(\varphi_{\dot{w}}(C)\otimes\dot{\lambda})\sigma^{\mathfrak{L}}$

###### Theorem 7.2

If $\mathsf{DK_{t}P},\Uppi\Vdash\delta$, then there exists a $\mathrm{PTIME}$
function $f$ in $s(\Uppi)$ such that
$\mathsf{G3K_{t}P},f(\Uppi)\Vdash\mathfrak{L}_{w}(\delta)$,
$s(f(\Uppi))=\mathcal{O}(s(\Uppi)^{2})$, and $f(\Uppi)$ is a strict labeled
polytree proof.

###### Proof

The proof is obtained by extending the inductive step of Theorem 7.1 with the
$(pt_{\delta})$ case. Therefore, let us consider an instance of
$(pt_{\delta})$ as shown below top. We translate it into the $(pt_{\lambda})$
instance shown below bottom, where each equality step is obtained from Lemma
8.

$(\psi(B_{1})\vdash\dot{X})\sigma$ $\ldots$ $(\psi(B_{m})\vdash\dot{X})\sigma$ $(pt_{\delta})$ $(\psi(A)\vdash\dot{X})\sigma$ | $\leadsto$
---|---

$\mathfrak{L}_{w}((\psi(B_{1})\vdash\dot{X})\sigma)$ . =
$(\varphi_{\dot{w}}(B_{1})\otimes\dot{\lambda})\sigma^{\mathfrak{L}}$
$(\bar{w})$
$(\varphi_{\dot{w}}(A)\otimes\varphi_{\dot{w}}(B_{1})\otimes\dot{\lambda})\sigma^{\mathfrak{L}}$
$\cdots$ $\mathfrak{L}_{w}((\psi(B_{m})\vdash\dot{X})\sigma)$ . =
$(\varphi_{\dot{w}}(B_{m})\otimes\dot{\lambda})\sigma^{\mathfrak{L}}$
$(\bar{w})$
$(\varphi_{\dot{w}}(A)\otimes\varphi_{\dot{w}}(B_{m})\otimes\dot{\lambda})\sigma^{\mathfrak{L}}$
$(pt_{\lambda})$
$(\varphi_{\dot{w}}(A)\otimes\dot{\lambda})\sigma^{\mathfrak{L}}$ . =
$\mathfrak{L}_{w}((\psi(A)\vdash\dot{X})\sigma)$

By the definition of $\mathfrak{L}_{w}$ and $\sigma^{\mathfrak{L}}$, it is
straightforward to confirm that the conditions
$\mathsf{(P_{1})}$–$\mathsf{(P_{7})}$ hold, showing that the application of
$(pt_{\lambda})$ is strict. Since our proof extends the proof of Theorem 7.1,
only introduces strict $(pt_{\lambda})$ instances, and the target proof
$f(\Uppi)$ derives a labeled polytree sequent, we know $f(\Uppi)$ will be a
strict labeled polytree proof by Theorem 5.1. Moreover, as seen above, each
instance of $(pt_{\delta})$ translates to a single instance of
$(pt_{\lambda})$ and may invoke the qp-admissibility of $(\bar{w})$. By an
argument similar to the one at the end of Theorem 7.1, one can confirm that
the translation is computed in $\mathrm{PTIME}$ and
$s(f(\Uppi))=\mathcal{O}(s(\Uppi)^{2})$.

##  8 From Labeled to Display Proofs

We now study the reverse translation, showing how to transform strict labeled
polytree proofs into display proofs. We find that translating a strict labeled
polytree proof $\Uppi$ gives a display proof $f(\Uppi)$ with a higher quantity
due to the introduction and use of display rules and structural rules in
$f(\Uppi)$. Nevertheless, the translation occurs within $\mathrm{PTIME}$, and
so we definitively confirm that the largest class of analytic (i.e. cut-free)
display calculi for tense logics can be polynomially simulated by analytic
labeled sequent calculi. This result solves an open problem first discussed by
Restall in 2006 [32], which was also left as an open problem in [10],
concerning the existence of embeddings between labeled and display
proofs.555In [10], it was shown how to translate labeled proofs into ‘one-
sided’ display calculus (i.e. shallow nested calculus) proofs for a small
subclass of primitive tense logics, namely, extension of $\mathsf{K_{t}}$ with
_path axioms_ of the form
$\langle?\rangle_{1}\cdots\langle?\rangle_{n}p\rightarrow\langle?\rangle_{n+1}p$
with
$\langle?\rangle_{i}\in\\{\langle\mathsf{F}\rangle,\langle\mathsf{P}\rangle\\}$
for $1\leq i\leq n+1$.

###### Theorem 8.1

If $\mathsf{G3K_{t}},\Uppi\Vdash\lambda$ and $\Uppi$ is a labeled polytree
proof, then there exists a $\mathrm{PTIME}$ function $f$ in $s(\Uppi)$ and
polynomial $p$ such that
$\mathsf{DK_{t}},f(\Uppi)\Vdash\mathfrak{D}_{w}(\lambda)$ and
$s(f(\Uppi))=\mathcal{O}(p(s(\Uppi)))$.

###### Proof

We prove the result by induction on the quantity of $\Uppi$ and make a case
distinction on the last rule applied. We consider a representative number of
cases and remark that the remaining cases are similar. In each case, we
translate a suitable $w$-partition of the input labeled polytree sequent. By
Lemma 5 we are permitted to select any $w$-partition to translate.

Base case. We show the $(id)$ case below and let
$\mathcal{R}=\mathcal{R}_{1},\mathcal{R}_{2}$, $\Gamma=\Gamma_{1},\Gamma_{2}$,
and $\Delta=\Delta_{1},\Delta_{2}$.

$(id)$ $\mathcal{R},\Gamma,w:p\Rightarrow w:p,\Delta$ . = $(\mathcal{R}_{1},\Gamma_{1},w:p\Rightarrow\Delta_{1})\oplus_{w}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow w:p,\Delta_{2})$ | $\leadsto$
---|---

$(id)$ $p\vdash p$ $(w_{l})$ $p\circ\mathfrak{D}_{1}^{w}(\lambda_{1})\vdash p$
$(w_{r})$ $p\circ\mathfrak{D}_{1}^{w}(\lambda_{1})\vdash
p\circ\mathfrak{D}_{2}^{w}(\lambda_{2})$ . =
$\mathfrak{D}_{1}^{w}(\mathcal{R}_{1},\Gamma_{1},w:p\Rightarrow\Delta_{1})\vdash\mathfrak{D}_{2}^{w}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow
w:p,\Delta_{2})$ . = $\mathfrak{D}_{w}(\mathcal{R},\Gamma,w:p\Rightarrow
w:p,\Delta)$

Inductive step. We show the $(\neg_{r})$, $(\wedge_{l})$,
$([\mathsf{G}]_{r})$, $(\langle\mathsf{F}\rangle_{r})$, and
$(\langle\mathsf{P}\rangle_{l})$ cases.

$(\neg_{r})$. In the second to third step in the target proof, we apply the
definition of $\mathfrak{D}_{w}$ and let
$(\mathcal{R},\Gamma,w:A\Rightarrow\Delta)=\lambda_{1}\oplus_{w}(\mathcal{R}_{2},\Gamma_{2},w:A\Rightarrow\Delta_{2})$.

$\mathcal{R},\Gamma,w:A\Rightarrow\Delta$ $(\neg_{r})$ $\mathcal{R},\Gamma\Rightarrow w:\neg A,\Delta$ | $\leadsto$
---|---

IH $\mathfrak{D}_{u}(\mathcal{R},\Gamma,w:A\Rightarrow\Delta)$ $\equiv$ (Lemma
7) $\mathfrak{D}_{w}(\mathcal{R},\Gamma,w:A\Rightarrow\Delta)$ . =
$\mathfrak{D}_{1}^{w}(\lambda_{1})\vdash\mathfrak{D}_{2}^{w}(\mathcal{R}_{2},\Gamma_{2},w:A\Rightarrow\Delta_{2})$
. =
$\mathfrak{D}_{1}^{w}(\lambda_{1})\vdash{\ast}A\circ\mathfrak{D}_{2}^{w}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow\Delta_{2})$
$(\delta_{3})$
$\mathfrak{D}_{1}^{w}(\lambda_{1})\circ{\ast}\mathfrak{D}_{2}^{w}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow\Delta_{2})\vdash{\ast}A$
$(\neg_{r})$
$\mathfrak{D}_{1}^{w}(\lambda_{1})\circ{\ast}\mathfrak{D}_{2}^{w}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow\Delta_{2})\vdash\neg
A$ $(\delta_{3})$ $\mathfrak{D}_{1}^{w}(\lambda_{1})\vdash\neg
A\circ\mathfrak{D}_{2}^{w}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow\Delta_{2})$ .
=
$\mathfrak{D}_{1}^{w}(\lambda_{1})\vdash\mathfrak{D}_{2}^{w}(\mathcal{R}_{2},\Gamma_{2},w:\neg
A\Rightarrow\Delta_{2})$ . = $\mathfrak{D}_{w}(\mathcal{R},\Gamma\Rightarrow
w:\neg A,\Delta)$ $\equiv$ (Lemma 7)
$\mathfrak{D}_{u}(\mathcal{R},\Gamma\Rightarrow w:\neg A,\Delta)$

$(\wedge_{l})$. In the second to third step in the target proof, we apply the
definition of $\mathfrak{D}_{w}$ and let
$(\mathcal{R},\Gamma,w:A,w:B\Rightarrow\Delta)=(\mathcal{R}_{1},\Gamma_{1},w:A,w:B\Rightarrow\Delta_{1})\oplus_{w}\lambda_{2}$.

$\mathcal{R},\Gamma,w:A,w:B\Rightarrow\Delta$ $(\wedge_{l})$ $\mathcal{R},\Gamma,w:A\wedge B\Rightarrow\Delta$ | $\leadsto$
---|---

IH $\mathfrak{D}_{u}(\mathcal{R},\Gamma,w:A,w:B\Rightarrow\Delta)$ $\equiv$
(Lemma 7) $\mathfrak{D}_{w}(\mathcal{R},\Gamma,w:A,w:B\Rightarrow\Delta)$ . =
$\mathfrak{D}_{1}^{w}(\mathcal{R}_{1},\Gamma_{1},w:A,w:B\Rightarrow\Delta_{1})\vdash\mathfrak{D}_{2}^{w}(\lambda_{2})$
. =
$\mathfrak{D}_{1}^{w}(\mathcal{R}_{1},\Gamma_{1}\Rightarrow\Delta_{1})\circ
A\circ B\vdash\mathfrak{D}_{2}^{w}(\lambda_{2})$ $(\delta_{2})$ $A\circ
B\vdash{\ast}\mathfrak{D}_{1}^{w}(\mathcal{R}_{1},\Gamma_{1}\Rightarrow\Delta_{1})\circ\mathfrak{D}_{2}^{w}(\lambda_{2})$
$(\wedge_{l})$ $A\land
B\vdash{\ast}\mathfrak{D}_{1}^{w}(\mathcal{R}_{1},\Gamma_{1}\Rightarrow\Delta_{1})\circ\mathfrak{D}_{2}^{w}(\lambda_{2})$
$(\delta_{2})$
$\mathfrak{D}_{1}^{w}(\mathcal{R}_{1},\Gamma_{1}\Rightarrow\Delta_{1})\circ
A\land B\vdash\mathfrak{D}_{2}^{w}(\lambda_{2})$ . =
$\mathfrak{D}_{1}^{w}(\mathcal{R}_{1},\Gamma_{1},w:A\land
B\Rightarrow\Delta_{1})\vdash\mathfrak{D}_{2}^{w}(\lambda_{2})$ . =
$\mathfrak{D}_{w}(\mathcal{R},\Gamma,w:A\land B\Rightarrow\Delta)$ $\equiv$
(Lemma 7) $\mathfrak{D}_{u}(\mathcal{R},\Gamma,w:A\land B\Rightarrow\Delta)$

$([\mathsf{G}]_{r})$. In the second to third step in the target proof, we
apply the definition of $\mathfrak{D}_{w}$ and let
$(\mathcal{R},Rwu,\Gamma\Rightarrow
u:A,\Delta)=\lambda_{1}\oplus_{w}(\mathcal{R}_{2},Rwv,\Gamma_{2}\Rightarrow
v:A,\Delta_{2})$.

$\mathcal{R},Rwu,\Gamma\Rightarrow u:A,\Delta$ $([\mathsf{G}]_{r})$ $\mathcal{R},\Gamma\Rightarrow w:[\mathsf{G}]A,\Delta$ | $\leadsto$
---|---

IH $\mathfrak{D}_{u}(\mathcal{R},Rwv,\Gamma\Rightarrow v:A,\Delta)$ $\equiv$
(Lemma 7) $\mathfrak{D}_{w}(\mathcal{R},Rwv,\Gamma\Rightarrow v:A,\Delta)$ . =
$\mathfrak{D}_{1}^{w}(\lambda_{1})\vdash\mathfrak{D}_{2}^{w}(\mathcal{R}_{2},Rwv,\Gamma_{2}\Rightarrow
v:A,\Delta_{2})$ . =
$\mathfrak{D}_{1}^{w}(\lambda_{1})\vdash{\bullet}A\circ\mathfrak{D}_{2}^{w}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow\Delta_{2})$
$(\delta_{3})$
$\mathfrak{D}_{1}^{w}(\lambda_{1})\circ{\ast}\mathfrak{D}_{2}^{w}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow\Delta_{2})\vdash{\bullet}A$
$(\delta_{9})$
${\bullet}(\mathfrak{D}_{1}^{w}(\lambda_{1})\circ{\ast}\mathfrak{D}_{2}^{w}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow\Delta_{2}))\vdash
A$ $([\mathsf{G}]_{r})$
$\mathfrak{D}_{1}^{w}(\lambda_{1})\circ{\ast}\mathfrak{D}_{2}^{w}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow\Delta_{2})\vdash[\mathsf{G}]A$
$(\delta_{3})$
$\mathfrak{D}_{1}^{w}(\lambda_{1})\vdash[\mathsf{G}]A\circ\mathfrak{D}_{2}^{w}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow\Delta_{2})$
. =
$\mathfrak{D}_{1}^{w}(\lambda_{1})\vdash\mathfrak{D}_{2}^{w}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow
w:[\mathsf{G}]A,\Delta_{2})$ . =
$\mathfrak{D}_{w}(\mathcal{R},\Gamma\Rightarrow w:[\mathsf{G}]A,\Delta)$
$\equiv$ (Lemma 7) $\mathfrak{D}_{u}(\mathcal{R},\Gamma\Rightarrow
w:[\mathsf{G}]A,\Delta)$

$(\langle\mathsf{F}\rangle_{r})$. In the second to third step in the target
proof, we apply the definition of $\mathfrak{D}_{w}$ and let
$(\mathcal{R},Rwv,\Gamma\Rightarrow w:\langle\mathsf{F}\rangle
A,v:A,\Delta)=\lambda_{1}\oplus_{w}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow
v:A,\Delta_{2})$. By Proposition 2 we are allowed to apply the $(\rho_{1})$
and $(\rho_{3})$ rules in the target proof. Also, in the ninth and tenth
lines, we let $\Gamma_{2}=\Gamma_{2}\restriction w,\Gamma_{2}^{\prime}$ and
$\Delta_{2}=\Delta_{2}\restriction w,\Delta_{2}^{\prime}$.

$\mathcal{R},Rwv,\Gamma\Rightarrow w:\langle\mathsf{F}\rangle A,v:A,\Delta$ $(\langle\mathsf{F}\rangle_{r})$ $\mathcal{R},Rwv,\Gamma\Rightarrow w:\langle\mathsf{F}\rangle A,\Delta$ | $\leadsto$
---|---

IH $\mathfrak{D}_{u}(\mathcal{R},\Gamma\Rightarrow v:A,\Delta)$ $\equiv$
(Lemma 7) $\mathfrak{D}_{v}(\mathcal{R},\Gamma\Rightarrow v:A,\Delta)$ . =
$\mathfrak{D}_{1}^{v}(\lambda_{1})\vdash\mathfrak{D}_{2}^{v}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow
v:A,\Delta_{2})$ . = $\mathfrak{D}_{1}^{v}(\lambda_{1})\vdash
A\circ\mathfrak{D}_{2}^{v}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow\Delta_{2})$
$(\delta_{3})$
${\ast}\mathfrak{D}_{2}^{v}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow\Delta_{2})\circ\mathfrak{D}_{1}^{v}(\lambda_{1})\vdash
A$ $(\langle\mathsf{F}\rangle_{r})$
${\ast}{\bullet}{\ast}({\ast}\mathfrak{D}_{2}^{v}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow\Delta_{2})\circ\mathfrak{D}_{1}^{v}(\lambda_{1}))\vdash\langle\mathsf{F}\rangle
A$ $(\rho_{1})$
${\ast}\mathfrak{D}_{2}^{v}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow\Delta_{2})\circ\mathfrak{D}_{1}^{v}(\lambda_{1})\vdash{\ast}{\bullet}{\ast}\langle\mathsf{F}\rangle
A$ $(\delta_{3})$
$\mathfrak{D}_{1}^{v}(\lambda_{1})\vdash{\ast}{\bullet}{\ast}\langle\mathsf{F}\rangle
A\circ\mathfrak{D}_{2}^{v}(\mathcal{R}_{2},\Gamma_{2}\Rightarrow\Delta_{2})$ .
=
$\mathfrak{D}_{1}^{v}(\lambda_{1})\vdash{\ast}{\bullet}{\ast}\langle\mathsf{F}\rangle
A\circ{\ast}{\bullet}{\ast}({\ast}(\Gamma_{2}\restriction
w)\circ(\Delta_{2}\restriction
w))\circ\mathfrak{D}_{2}^{v}(\mathcal{R},\Gamma_{2}^{\prime}\Rightarrow\Delta_{2}^{\prime})$
$(\rho_{3})$
$\mathfrak{D}_{1}^{v}(\lambda_{1})\vdash{\ast}{\bullet}{\ast}(\langle\mathsf{F}\rangle
A\circ{\ast}(\Gamma_{2}\restriction w)\circ(\Delta_{2}\restriction
w))\circ\mathfrak{D}_{2}^{v}(\mathcal{R},\Gamma_{2}^{\prime}\Rightarrow\Delta_{2}^{\prime})$
. =
$\mathfrak{D}_{1}^{v}(\lambda_{1})\vdash\mathfrak{D}_{2}^{v}(\mathcal{R}_{2},Rwv,\Gamma_{2}\Rightarrow
w:\langle\mathsf{F}\rangle A,\Delta_{2})$ . =
$\mathfrak{D}_{v}(\mathcal{R},Rwv,\Gamma\Rightarrow w:\langle\mathsf{F}\rangle
A,\Delta)$ $\equiv$ (Lemma 7)
$\mathfrak{D}_{u}(\mathcal{R},Rwv,\Gamma\Rightarrow w:\langle\mathsf{F}\rangle
A,\Delta)$

$(\langle\mathsf{P}\rangle_{l})$. In the second to third step in the target
proof, we apply the definition of $\mathfrak{D}_{w}$ and let
$(\mathcal{R},Rvw,\Gamma,v:A\Rightarrow\Delta)=(\mathcal{R}_{1},Rvw,\Gamma_{1}\Rightarrow
v:A,\Delta_{1})\oplus_{w}\lambda_{2}$.

$\mathcal{R},Rvw,\Gamma,v:A\Rightarrow\Delta$ $(\langle\mathsf{P}\rangle_{l})$ $\mathcal{R},\Gamma,w:\langle\mathsf{P}\rangle A\Rightarrow\Delta$ | $\leadsto$
---|---

IH $\mathfrak{D}_{u}(\mathcal{R},Rvw,\Gamma\Rightarrow v:A,\Delta)$ $\equiv$
(Lemma 7) $\mathfrak{D}_{w}(\mathcal{R},Rvw,\Gamma\Rightarrow v:A,\Delta)$ . =
$\mathfrak{D}_{1}^{w}(\mathcal{R}_{1},Rvw,\Gamma_{1}\Rightarrow
v:A,\Delta_{1})\vdash\mathfrak{D}_{2}^{w}(\lambda_{2})$ . =
${\bullet}A\circ\mathfrak{D}_{1}^{w}(\mathcal{R}_{1},\Gamma_{1}\Rightarrow\Delta_{1})\vdash\mathfrak{D}_{2}^{w}(\lambda_{2})$
$(\delta_{1})$
${\bullet}A\vdash\mathfrak{D}_{2}^{w}(\lambda_{2})\circ{\ast}\mathfrak{D}_{1}^{w}(\mathcal{R}_{1},\Gamma_{1}\Rightarrow\Delta_{1})$
$(\delta_{9})$
$A\vdash{\bullet}(\mathfrak{D}_{2}^{w}(\lambda_{2})\circ{\ast}\mathfrak{D}_{1}^{w}(\mathcal{R}_{1},\Gamma_{1}\Rightarrow\Delta_{1}))$
$(\langle\mathsf{P}\rangle_{l})$ $\langle\mathsf{P}\rangle
A\vdash\mathfrak{D}_{2}^{w}(\lambda_{2})\circ{\ast}\mathfrak{D}_{1}^{w}(\mathcal{R}_{1},\Gamma_{1}\Rightarrow\Delta_{1})$
$(\delta_{1})$
$\mathfrak{D}_{1}^{w}(\mathcal{R}_{1},\Gamma_{1}\Rightarrow\Delta_{1})\circ\langle\mathsf{P}\rangle
A\vdash\mathfrak{D}_{2}^{w}(\lambda_{2})$ . =
$\mathfrak{D}_{1}^{w}(\mathcal{R}_{1},\Gamma_{1},w:\langle\mathsf{P}\rangle
A\Rightarrow\Delta_{1})\vdash\mathfrak{D}_{2}^{w}(\lambda_{2})$ . =
$\mathfrak{D}_{w}(\mathcal{R},\Gamma,w:\langle\mathsf{P}\rangle
A\Rightarrow\Delta)$ $\equiv$ (Lemma 7)
$\mathfrak{D}_{u}(\mathcal{R},\Gamma,w:\langle\mathsf{P}\rangle
A\Rightarrow\Delta)$

This concludes the proof of the inductive step. Let us now analyze the
complexity of the translation and the relative sizes of the input and target
proofs.

Observe that each (logical) rule application in $\Uppi$ is considered once and
adds a single logical rule application in the target proof. Furthermore, each
application of Lemma 7 adds only polynomially many inferences to the target
proof and only a constant number of display and structural rules are added to
the target proof beyond these inferences, meaning for some polynomial
$p^{\prime}$, $q(f(\Uppi))=\mathcal{O}(p^{\prime}(q(\Uppi)))$. Also, each
display sequent in the target proof is polynomial in $w(\Uppi)$ by Remark 2.
Therefore, the translation takes place in $\mathrm{PTIME}$ and
$s(f(\Uppi))=\mathcal{O}(p(s(\Uppi)))$, for some polynomial $p$.

We now show how to extend the above translation to cover _strict_ primitive
tense structural rules. To carry out this translation, we suppose that we have
a strict instance of $(pt_{\lambda})$ under a substitution $\sigma$, and show
that this rule instance can be translated via $\mathfrak{D}_{w}$ to an
instance of $(pt_{\delta})$ under a substitution $\sigma^{\mathfrak{D}}$.
Therefore, let the following be a strict instance of $(pt_{\lambda})$:

$(\varphi_{\dot{w}}(A)\otimes\varphi_{\dot{w}}(B_{1})\otimes\dot{\lambda})\sigma$
$\ldots$
$(\varphi_{\dot{w}}(A)\otimes\varphi_{\dot{w}}(B_{m})\otimes\dot{\lambda})\sigma$
$(pt_{\lambda})$ $(\varphi_{\dot{w}}(A)\otimes\dot{\lambda})\sigma$

where the substitution $\sigma$ is defined accordingly:

$\sigma:=[\lambda_{1}/\dot{\lambda}_{p_{1}}^{\dot{u}_{1}},\ldots,\lambda_{k}/\dot{\lambda}_{p_{1}}^{\dot{u}_{k}},\ldots,\lambda_{m}/\dot{\lambda}_{p_{n}}^{\dot{u}_{m}},\ldots,\lambda_{\ell}/\dot{\lambda}_{p_{n}}^{\dot{u}_{\ell}},\lambda/\dot{\lambda},u_{1}/\dot{u}_{1},\ldots,u_{n}/\dot{u}_{n}]$

To translate the above instance of $(pt_{\lambda})$ to an instance of
$(pt_{\delta})$ under $\mathfrak{D}_{w}$, we define the substitution
$\sigma^{\mathfrak{D}}$ accordingly:

$\sigma^{\mathfrak{D}}:=[\mathfrak{D}_{1}^{u_{1}}(\lambda_{1})/\dot{X}_{p_{1}},\ldots,\mathfrak{D}_{1}^{u_{m}}(\lambda_{m})/\dot{X}_{p_{n}},\mathfrak{D}_{2}^{w}(\lambda)/\dot{X}]$

We note that multiple labeled sequent variables
$\dot{\lambda}_{p_{i}}^{\dot{v}_{1}},\ldots,\dot{\lambda}_{p_{i}}^{\dot{v}_{k}}$
annotated with the same propositional atom $p_{i}$ may occur in $\sigma$,
while in $\sigma^{\mathfrak{D}}$ only a single structure variable
$\dot{X}_{p_{i}}$ annotated with $p_{i}$ will occur. By condition
$\mathsf{(P_{2})}$ (see Definition 19), we know that
$\dot{\lambda}_{p_{i}}^{\dot{v}_{1}}\sigma\cong\cdots\cong\dot{\lambda}_{p_{i}}^{\dot{v}_{k}}\sigma$.
Therefore,
$\mathfrak{D}_{1}^{v_{1}}(\dot{\lambda}_{p_{i}}^{\dot{v}_{1}}\sigma)=\cdots=\mathfrak{D}_{1}^{v_{k}}(\dot{\lambda}_{p_{i}}^{\dot{v}_{k}}\sigma)$,
meaning we can arbitrarily choose any labeled sequent
$\dot{\lambda}_{p_{i}}^{\dot{v}_{j}}\sigma$ with $1\leq j\leq k$ to use to
substitute
$\mathfrak{D}_{1}^{v_{j}}(\dot{\lambda}_{p_{i}}^{\dot{v}_{j}}\sigma)$ for
$\dot{X}_{p_{i}}$ in $\sigma^{\mathfrak{D}}$. As shown above, we simply choose
the first labeled sequent mentioned in $\sigma$ in defining the substitution
$\sigma^{\mathfrak{D}}$. The interested reader should consult Example 9 in the
previous section to see how an instance of $(pt_{\delta})$ is obtained from an
instance of $(pt_{\lambda})$ by reversing the example and viewing $\sigma$ in
the example as $(\sigma^{\mathfrak{L}})^{\mathfrak{D}}$.

###### Lemma 9

Let us consider a strict instance of a primitive tense structural rule as
shown below.

$(\varphi_{\dot{w}}(A)\otimes\varphi_{\dot{w}}(B_{1})\otimes\dot{\lambda})\sigma$
$\ldots$
$(\varphi_{\dot{w}}(A)\otimes\varphi_{\dot{w}}(B_{m})\otimes\dot{\lambda})\sigma$
$(pt_{\lambda})$ $(\varphi_{\dot{w}}(A)\otimes\dot{\lambda})\sigma$

and let $C\in\\{A,B_{1},\ldots,B_{m}\\}$. Then,

  1. 1.

$\mathfrak{D}^{w}_{1}(\varphi_{\dot{w}}(C)\sigma)=\psi(C)\sigma^{\mathfrak{D}}$

  2. 2.

$\mathfrak{D}_{w}((\varphi_{\dot{w}}(C)\otimes\dot{\lambda})\sigma)=(\psi(C)\vdash\dot{X})\sigma^{\mathfrak{D}}$

###### Proof

We prove claim 1 by induction on the complexity of $C$. Claim 2 follows from
claim 1.

Base case. If $A$ is an atom $p_{i}$, so that
$\varphi_{\dot{w}}(p_{i})=\dot{\lambda}_{p_{i}}^{\dot{w}}$ and
$\sigma(\dot{\lambda}_{p_{i}}^{\dot{w}})=\lambda_{i}$, then the proof shown
below right proves the case. If $A$ is the logical constant $\top$, so that
$\varphi_{\dot{w}}(A)=\varphi_{\dot{w}}(\top)=(\emptyset\Rightarrow\emptyset)$,
then the proof shown below right establishes the case.

$\displaystyle\mathfrak{D}^{w}_{1}(\varphi_{\dot{w}}(p_{i})\sigma)$
$\displaystyle\mathfrak{D}^{w}_{1}(\dot{\lambda}_{p_{i}}^{\dot{w}}\sigma)$
$\displaystyle\mathfrak{D}^{w}_{1}(\lambda_{i})$
$\displaystyle\dot{X}_{p_{i}}\sigma^{\mathfrak{D}}$
$\displaystyle\psi(p_{i})\sigma^{\mathfrak{D}}$

$\displaystyle\mathfrak{D}^{w}_{1}(\varphi_{\dot{w}}(\top)\sigma)$
$\displaystyle\mathfrak{D}^{w}_{1}(\emptyset\Rightarrow\emptyset)$
$\displaystyle I$ $\displaystyle I\sigma^{\mathfrak{D}}$
$\displaystyle\psi(\top)\sigma^{\mathfrak{D}}$

Inductive step. We consider the cases where $C=D\land E$,
$C=\langle\mathsf{F}\rangle D$, and $C=\langle\mathsf{P}\rangle D$ in turn. In
the first case, we have that $\varphi_{\dot{w}}(C)=\varphi_{\dot{w}}(D\land
E)=\varphi_{\dot{w}}(D)\otimes\varphi_{\dot{w}}(E)$, and the proof below
establishes the claim in this case. The third to fourth step below follows
from the fact that $(pt_{\lambda})$ is strict; in particular, $\sigma$
satisfies conditions $\mathsf{(P_{4})}$, $\mathsf{(P_{5})}$, and
$\mathsf{(P_{7})}$ (see Definition 24).
$\displaystyle\mathfrak{D}^{w}_{1}(\varphi_{\dot{w}}(D\land E)\sigma)$
$\displaystyle\mathfrak{D}^{w}_{1}((\varphi_{\dot{w}}(D)\otimes\varphi_{\dot{w}}(E))\sigma)$
$\displaystyle\mathfrak{D}^{w}_{1}(\varphi_{\dot{w}}(D)\sigma\otimes\varphi_{\dot{w}}(E)\sigma)$
$\displaystyle\mathfrak{D}^{w}_{1}(\varphi_{\dot{w}}(D)\sigma)\circ\mathfrak{D}^{w}_{1}(\varphi_{\dot{w}}(E)\sigma)$
$\displaystyle\psi(D)\sigma^{\mathfrak{D}}\circ\psi(E)\sigma^{\mathfrak{D}}$
$\displaystyle(\psi(D)\circ\psi(E))\sigma^{\mathfrak{D}}$
$\displaystyle\psi(D\land E)\sigma^{\mathfrak{D}}$

The proof of the second case is shown below left, where
$\varphi_{\dot{w}}(A)=\varphi_{\dot{w}}(\langle\mathsf{F}\rangle
D)=(R\dot{w}\dot{u}\Rightarrow\emptyset)\otimes\varphi_{\dot{u}}(D)$, and the
proof of the final case is shown below right, where
$\varphi_{\dot{w}}(A)=\varphi_{\dot{w}}(\langle\mathsf{P}\rangle
D)=(R\dot{u}\dot{w}\Rightarrow\emptyset)\otimes\varphi_{\dot{u}}(D)$.

$\displaystyle\mathfrak{D}_{w}(\varphi_{\dot{w}}(\langle\mathsf{F}\rangle
D)\sigma)$
$\displaystyle\mathfrak{D}_{w}(((R\dot{w}\dot{u}\Rightarrow\emptyset)\otimes\varphi_{\dot{u}}(D))\sigma)$
$\displaystyle\mathfrak{D}_{w}((R\dot{w}\dot{u}\Rightarrow\emptyset)\otimes\varphi_{\dot{u}}(D)\sigma)$
$\displaystyle{\ast}{\bullet}{\ast}\mathfrak{D}_{u}(\varphi_{\dot{u}}(D)\sigma)$
$\displaystyle{\ast}{\bullet}{\ast}\psi(D)\sigma^{\mathfrak{D}}$
$\displaystyle({\ast}{\bullet}{\ast}\psi(D))\sigma^{\mathfrak{D}}$
$\displaystyle\psi(\langle\mathsf{F}\rangle D)\sigma^{\mathfrak{D}}$

$\displaystyle\mathfrak{D}_{w}(\varphi_{w}(\langle\mathsf{P}\rangle D)\sigma)$
$\displaystyle\mathfrak{D}_{w}(((Ruw\Rightarrow\emptyset)\otimes\varphi_{u}(D))\sigma)$
$\displaystyle\mathfrak{D}_{w}((Ruw\Rightarrow\emptyset)\otimes\varphi_{u}(D)\sigma)$
$\displaystyle{\bullet}\mathfrak{D}_{u}(\varphi_{u}(D)\sigma)$
$\displaystyle{\bullet}\psi(D)\sigma^{\mathfrak{D}}$
$\displaystyle({\bullet}\psi(D))\sigma^{\mathfrak{D}}$
$\displaystyle\psi(\langle\mathsf{P}\rangle D)\sigma^{\mathfrak{D}}$

###### Theorem 8.2

If $\mathsf{G3K_{t}P},\Uppi\Vdash\lambda$ and $\Uppi$ is a strict labeled
polytree proof, then there exists a $\mathrm{PTIME}$ function $f$ in
$s(\Uppi)$ and polynomial $p$ such that
$\mathsf{DK_{t}P},f(\Uppi)\Vdash\mathfrak{D}_{w}(\lambda)$ and
$s(f(\Uppi))=\mathcal{O}(p(s(\Uppi)))$.

###### Proof

We prove the result by extending the inductive step of Theorem 8.1 with the
$(pt_{\lambda})$ case. Let us suppose we are translating a strict labeled
polytree proof $\Uppi$, and let us consider a strict instance of
$(pt_{\lambda})$ as shown below top. The desired translation is obtained as
shown below bottom, where the $\cong$ steps follow from Lemma 7 and the
equality steps are obtained by Lemma 9.

$(\varphi_{\dot{w}}(A)\otimes\varphi_{w}(B_{1})\otimes\dot{\lambda})\sigma$ $\ldots$ $(\varphi_{\dot{w}}(A)\otimes\varphi_{w}(B_{m})\otimes\dot{\lambda})\sigma$ $(pt_{\lambda})$ $(\varphi_{\dot{w}}(A)\otimes\dot{\lambda})\sigma$ | $\leadsto$
---|---

$\mathfrak{D}_{u}((\varphi_{\dot{w}}(A)\otimes\varphi_{\dot{w}}(B_{1})\otimes\dot{\lambda})\sigma)$
. $\cong$
$\mathfrak{D}_{w}((\varphi_{\dot{w}}(A)\otimes\varphi_{\dot{w}}(B_{1})\otimes\dot{\lambda})\sigma)$
. = $(\psi(A)\circ\psi(B_{1})\vdash\dot{X})\sigma^{\mathfrak{D}}$
$(\delta_{2})$
$(\psi(B_{1})\vdash{\ast}\psi(A)\circ\dot{X})\sigma^{\mathfrak{D}}$ $\ldots$
$\mathfrak{D}_{u}((\varphi_{\dot{w}}(A)\otimes\varphi_{w}(B_{m})\otimes\dot{\lambda})\sigma)$
. $\cong$
$\mathfrak{D}_{w}((\varphi_{\dot{w}}(A)\otimes\varphi_{w}(B_{m})\otimes\dot{\lambda})\sigma)$
. = $(\psi(A)\circ\psi(B_{m})\vdash\dot{X})\sigma^{\mathfrak{D}}$
$(\delta_{2})$
$(\psi(B_{m})\vdash{\ast}\psi(A)\circ\dot{X})\sigma^{\mathfrak{D}}$
$(pt_{\delta})$
$(\psi(A)\vdash{\ast}\psi(A)\circ\dot{X})\sigma^{\mathfrak{D}}$ $(\delta_{2})$
$(\psi(A)\circ\psi(A)\vdash\dot{X})\sigma^{\mathfrak{D}}$ $(c_{l})$
$(\psi(A)\vdash\dot{X})\sigma^{\mathfrak{D}}$ . =
$\mathfrak{D}_{w}((\psi(A)\vdash\dot{Y})\sigma)$

By an argument similar to the one at the end of Theorem 8.1, it follows that
$f(\Uppi)$ is computable in $\mathrm{PTIME}$ and
$s(f(\Uppi))=\mathcal{O}(p(s(\Uppi)))$, for some polynomial $p$.

##  9 Concluding Remarks

We have established a $\mathrm{PTIME}$ correspondence between the maximal
analytic class of display calculi for tense logics (namely, all display
calculi for primitive tense logics) and labeled sequent systems, thus solving
an open problem posed in [10, 32]. Our translations show that the space of
cut-free display proofs is polynomially equivalent to the space of strict
labeled proofs. We also find that translating from display to labeled
preserves (or decreases) the quantity of the proof, while potentially
increasing the width; the reverse translation brings about a polynomial
increase in the size of the proof. Moreover, we made the interesting
observation that display structures translate to labeled polytree sequents and
that all display equivalent sequents translate to the same labeled sequent (up
to isomorphism), showing that labeled sequents are a canonical representation
of display sequents that enjoy less bureaucracy.

A fascinating avenue of future research would be to study translations and the
computational relationship between strict labeled proofs and non-strict
labeled proofs (which might include labeled sequents _not_ in a polytree
form). Composing such translations with the translations in this paper would
confirm if it is possible or not to translate any analytic display proof into
_any_ analytic labeled proof, or vice versa, in $\mathrm{PTIME}$. Transforming
a strict labeled proof into a non-strict one, where labeled sequents may
include disconnectivity or (un)directed cycles, is simple to obtain by
applying (1) the hp-admissibility of $(w)$ to add disjoint regions to labeled
sequents in the proof, and (2) by applying the hp-admissibility of $(ls)$ to
identify labels, bringing about the formation of cycles. Showing the converse,
i.e. that any non-strict labeled proof can be obtained from a strict proof via
applications of $(w)$ and $(ls)$ (up to admissible permutations of rules in a
proof), appears far more challenging and may require new proof-theoretic
techniques (or, operations beyond weakenings, label substitutions, and
permutations).

Nevertheless, the above suggested correspondence between strict and non-strict
labeled proofs would imply that every non-strict labeled proof is essentially
a homomorphic image of a strict proof. This would tell us that display calculi
are a special fragment of labeled calculi that generate proofs homomorphically
mappable into any other proof of the same conclusion (up to admissible
permutations of rules). It is not clear if transforming non-strict proofs into
strict proofs is possible in $\mathrm{PTIME}$ however (assuming
$\mathrm{PTIME}\neq\mathrm{NP}$) as finding the correct ‘homomorphic mapping’
from a strict to a non-strict proof may require an $\mathrm{NP}$ algorithm
(cf. [20]).

## References

  * [1] A. Avron.  The method of hypersequents in the proof theory of propositional non-classical logics.  In W. Hodges, M. Hyland, C. Steinhorn, and J. Truss, editors, Logic: From Foundations to Applications: European Logic Colloquium, page 1–32. Clarendon Press, USA, 1996.
  * [2] F. Baader, I. Horrocks, C. Lutz, and U. Sattler.  Introduction to Description Logic.  Cambridge University Press, 2017.
  * [3] N. D. Belnap.  Display logic.  Journal of philosophical logic, 11(4):375–417, 1982.
  * [4] P. Blackburn, M. de Rijke, and Y. Venema.  Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science.  Cambridge University Press, 2001.
  * [5] B. Boretti.  Proof Analysis in Temporal Logic.  PhD thesis, University of Milan, 2008.
  * [6] J. Brotherston.  Bunched logics displayed.  Stud. Log., 100(6):1223–1254, Dec. 2012.
  * [7] L. Buisman and R. Goré.  A cut-free sequent calculus for bi-intuitionistic logic.  In N. Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, pages 90–106, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg.
  * [8] R. A. Bull.  Cut elimination for propositional dynamic logic without *.  Z. Math. Logik Grundlag. Math., 38(2):85–100, 1992.
  * [9] C. Castellini and A. Smaill.  A systematic presentation of quantified modal logics.  Logic Journal of the IGPL, 10(6):571–599, 2002.
  * [10] A. Ciabattoni, T. S. Lyon, R. Ramanayake, and A. Tiu.  Display to labeled proofs and back again for tense logics.  ACM Trans. Comput. Logic, 22(3), July 2021.
  * [11] A. Deutsch, A. Nash, and J. B. Remmel.  The chase revisited.  In M. Lenzerini and D. Lembo, editors, Proceedings of the 27th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS’08), pages 149–158. ACM, 2008.
  * [12] R. Dyckhoff.  Contraction-free sequent calculi for intuitionistic logic.  The Journal of Symbolic Logic, 57(3):795–807, 1992.
  * [13] M. Fitting.  Tableau methods of proof for modal logics.  Notre Dame Journal of Formal Logic, 13(2):237–247, 1972.
  * [14] D. M. Gabbay.  Labelled deductive systems, volume 33 of Oxford Logic guides.  Clarendon Press/Oxford Science Publications, 1996.
  * [15] G. Gentzen.  Untersuchungen über das logische schließen. i.  Mathematische zeitschrift, 39(1):176–210, 1935.
  * [16] G. Gentzen.  Untersuchungen über das logische schließen. ii.  Mathematische Zeitschrift, 39(1):405–431, 1935.
  * [17] J.-Y. Girard.  Linear logic.  Theoretical computer science, 50(1):1–101, 1987.
  * [18] R. Goré.  Substructural logics on display.  Logic Journal of the IGPL, 6(3):451–504, 05 1998.
  * [19] R. Hein.  Geometric theories and proof theory of modal logic.  Master’s thesis, Technische Universität Dresden, 2005.
  * [20] P. Hell and J. Nesetril.  Graphs and Homomorphisms.  Oxford University Press, 07 2004.
  * [21] S. Kanger.  Provability in logic.  Almqvist & Wiksell, 1957.
  * [22] R. Kashima.  Cut-free sequent calculi for some tense logics.  Studia Logica, 53(1):119–135, 1994.
  * [23] M. Kracht.  Power and weakness of the modal display calculus.  In H. Wansing, editor, Proof Theory of Modal Logic, pages 93–121. Springer Netherlands, Dordrecht, 1996.
  * [24] S. A. Kripke.  Semantical considerations on modal logic.  Acta Philosophica Fennica, 16:83–94, 1963.
  * [25] B. Lellmann.  Linear nested sequents, 2-sequents and hypersequents.  In H. De Nivelle, editor, Automated Reasoning with Analytic Tableaux and Related Methods, volume 9323 of Lecture Notes in Computer Science, pages 135–150, Cham, 2015. Springer International Publishing.
  * [26] T. Lyon, A. Tiu, R. Goré, and R. Clouston.  Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents.  In M. Fernández and A. Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic (CSL), volume 152 of LIPIcs, pages 28:1–28:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
  * [27] S. Maehara.  On the interpolation theorem of craig.  Sûgaku, 12(4):235–237, 1960.
  * [28] K. L. McMillan.  Interpolation and model checking.  In E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, editors, Handbook of Model Checking, pages 421–446. Springer International Publishing, Cham, 2018.
  * [29] G. Mints.  Indexed systems of sequents and cut-elimination.  Journal of Philosophical Logic, 26(6):671–696, 1997.
  * [30] G. Pottinger.  Uniform, cut-free formulations of t, s4 and s5.  Journal of Symbolic Logic, 48(3):900, 1983.
  * [31] A. N. Prior.  Time and Modality.  Oxford University Press, 1957.
  * [32] G. Restall.  Comparing modal sequent systems.  unpublished, pages 1–13, 2006.
  * [33] A. K. Simpson.  The proof theory and semantics of intuitionistic modal logic.  PhD thesis, University of Edinburgh. College of Science and Engineering. School of Informatics, 1994.
  * [34] J. K. Slaney.  Minlog: A minimal logic theorem prover.  In W. McCune, editor, Automated Deduction - CADE-14, Proceedings, volume 1249 of Lecture Notes in Computer Science, pages 268–271. Springer, 1997.
  * [35] R. M. Smullyan.  First-Order Logic.  Springer-Verlag, 1968.
  * [36] P. Stouppa.  The design of modal proof theories: The case of s5.  Master’s thesis, Technische Universität Dresden, 2004.
  * [37] K. van Berkel and C. Straßer.  Reasoning with and about norms in logical argumentation.  In F. Toni, S. Polberg, R. Booth, M. Caminada, and H. Kido, editors, Computational Models of Argument - Proceedings of COMMA 2022, volume 353 of Frontiers in Artificial Intelligence and Applications, pages 332–343. IOS Press, 2022.
  * [38] L. Viganò.  Labelled Non-Classical Logics.  Springer Science & Business Media, 2000.
  * [39] H. Wansing.  Sequent calculi for normal modal propositional logics.  Journal of Logic and Computation, 4(2):125–142, 1994.
  * [40] F. Wolter.  On logics with coimplication.  Journal of Philosophical Logic, 27(4):353–387, 1998.