$\vdash\Diamond(\Gamma_{1}),\vec{r_{1}}.\Diamond(B),\vec{s_{1}}.\Diamond(\overline{B}),\vec{r}.1,\vec{s}.\overline{1}\vdash\Gamma_{1},\vec{r_{1}}.B,\vec{s_{1}}.\overline{B},\vec{r}.1,\vec{s}.\overline{1}$

The next lemma states that if $G$ is provable then the hypersequent obtained
by substituting an atom for a formula in $G$ is also provable.

######  Lemma 59.

If $\triangleright_{\textbf{HMR}}G$ then for all formulae $A$,
$\triangleright_{\textbf{HMR}}G[A/x]$.

######  Proof 4.3.

Similar to the proof of Lemma 25.

The following lemma, which will be useful in the proof of the completeness
theorem, states that the rules $\\{0,+,\times,\sqcup,\sqcap\\}$, are
invertible in HMR, in the sense that if the conclusion of one of these rules
is derivable (possibly using CAN rules) then its premises are also derivable
(possibly using CAN rules).

######  Lemma 60.

All the logical rules $\\{0,+,\times,\sqcup,\sqcap\\}$ are invertible.

######  Proof 4.4.

Similar to Lemma 26.

######  Remark 61.

The proof of Lemma 60 does not introduce any new T rule, so if the conclusion
of one of the logical rules $\\{0,+,\times,\sqcup,\sqcap\\}$ has a T–free
derivation, then the premises also have T–free derivations.

The next lemmas state that CAN–free derivability in the HMR system is
preserved by scalar multiplication.

######  Lemma 62.

Let $\vec{r}\in\mathbb{R}_{>0}$ be a non-empty vector and $G$ a hypersequent.
If $\triangleright_{\textbf{HMR}\backslash\\{\text{CAN}\\}}G\mid\
\vdash\vec{r}.\Gamma$ then
$\triangleright_{\textbf{HMR}\backslash\\{\text{CAN}\\}}G\mid\ \vdash\Gamma$.

######  Proof 4.5.

Similar to Lemma 28.

######  Lemma 63.

Let $\vec{r}\in\mathbb{R}_{>0}$ be a vector and $G$ a hypersequent. If
$\triangleright_{\textbf{HMR}\backslash\\{\text{CAN}\\}}G\mid\ \vdash\Gamma$
then $\triangleright_{\textbf{HMR}\backslash\\{\text{CAN}\\}}G\mid\
\vdash\vec{r}.\Gamma$.

######  Proof 4.6.

Similar to Lemma 29.

The above lemmas have two useful corollaries.

######  Corollary 64.

If $\triangleright_{\textbf{HMR}\backslash\\{\text{CAN}\\}}G\mid\
\vdash\Gamma,\vec{r}.A,\vec{s}.A$ and
$\triangleright_{\textbf{HMR}\backslash\\{\text{CAN}\\}}G\mid\
\vdash\Gamma,\vec{r}.B,\vec{s}.B$ then
$\triangleright_{\textbf{HMR}\backslash\\{\text{CAN}\\}}G\mid\
\vdash\Gamma,\vec{r}.A,\vec{s}.B$.

######  Proof 4.7.

Similar to Corollary 30

######  Corollary 65.

If $\triangleright_{\textbf{HMR}\backslash\\{\text{CAN}\\}}G\mid\
\vdash\vec{r}.A,\vec{s}.A,\Gamma\mid\ \vdash\vec{r}.B,\vec{s}.B,\Gamma\mid\
\vdash\vec{r}.A,\vec{s}.B,\Gamma$, then
$\triangleright_{\textbf{HMR}\backslash\\{\text{CAN}\\}}G\mid\
\vdash\vec{r}.A,\vec{s}.A,\Gamma\mid\ \vdash\vec{r}.B,\vec{s}.B,\Gamma$.

######  Proof 4.8.

Similar to Corollary 31.

###  4.3. Soundness – Proof of Theorem 50

The proof is similar to the one for Theorem 13: we prove that every rules is
sound and then conclude by induction on the complexity of derivations. Since
the proofs of soundness for the rules already in HR are exactly the same as
for the system HR done in Section 3.4, we only prove the soundness of the new
rules.

  * •

For the rule

$\vdash\Diamond\Gamma,\vec{r}.1,\vec{s}.\overline{1}\vdash\Gamma,\vec{r}.1,\vec{s}.\overline{1}$

the hypothesis is
$\llparenthesis\vdash\Gamma,\vec{r}.1,\vec{s}.\overline{1}\rrparenthesis\geq
0$ so

$\displaystyle\llparenthesis\vdash\Diamond\Gamma,\vec{r}.1,\vec{s}.\overline{1}\rrparenthesis$
$\displaystyle=$
$\displaystyle\llparenthesis\vdash\Diamond\Gamma,(\sum\vec{r}-\sum\vec{s}).1\rrparenthesis\text{
by distributivity}$ $\displaystyle\geq$
$\displaystyle\llparenthesis\vdash\Diamond\Gamma,(\sum\vec{r}-\sum\vec{s}).\Diamond
1\rrparenthesis\text{ since }\Diamond 1\leq 1$ $\displaystyle=$
$\displaystyle\Diamond(\llparenthesis\vdash\Gamma,(\sum\vec{r}-\sum\vec{s}).1\rrparenthesis)\text{
by linearity of }\Diamond$ $\displaystyle=$
$\displaystyle\Diamond(\llparenthesis\vdash\Gamma,\vec{r}.1,\vec{s}.\overline{1})\rrparenthesis\text{
by distributivity}$ $\displaystyle\geq$ $\displaystyle 0\text{ by the
hypothesis and the monotonocity of }\Diamond.$

  * •

For the rule

$G\mid\ \vdash\Gamma,\vec{r}.1,\vec{s}.\overline{1}G\mid\ \vdash\Gamma$

the hypothesis is $\llparenthesis G\mid\ \vdash\Gamma\rrparenthesis\geq 0$ so

$\displaystyle\llparenthesis G\mid\
\vdash\Gamma,\vec{r}.1,\vec{s}.\overline{1}\rrparenthesis$ $\displaystyle\geq$
$\displaystyle\llparenthesis G\mid\ \vdash\Gamma\rrparenthesis\text{ since
}\sum\vec{r}\geq\sum\vec{s}\text{ and }0\leq 1$ $\displaystyle\geq$
$\displaystyle 0$

###  4.4. Completeness – Proof of Theorem 51

The proof follows the same pattern as in Section 3.5: we first prove a similar
result that admits a simple proof by induction on the derivation of
$\mathcal{A}_{\text{Riesz}}^{\Diamond}\vdash A=B$ and then we use it and the
invertibility of the logical rules (Lemma 60) to prove Theorem 51, as shown in
Section 3.5.

######  Lemma 66.

If $\mathcal{A}_{\text{Riesz}}^{\Diamond}\vdash A=B$ then $\vdash
1.A,1.\overline{B}$ and $\vdash 1.B,1.\overline{A}$ are provable in HMR.

######  Proof 4.9.

Since the other cases are proven in the exact same way as in Theorem 14, we
will only derive the new axioms.

  * •

For the axiom $0\leq 1$.

$\vdash 1.(0\sqcap 1),1.0\vdash 1.(0\sqcap 1)\lx@proof@logical@and\vdash
1.0\vdash\vdash 1.1\vdash$

and

$\vdash 1.0,1.(0\sqcup\overline{1})\vdash 1.(0\sqcup\overline{1})\vdash
1.0\mid\ \vdash 1.\overline{1}\vdash 1.0\vdash$

  * •

For the axiom $\Diamond(1)\leq 1$.

$\vdash 1.(\Diamond(1)\sqcap
1),1.\Diamond(\overline{1})\lx@proof@logical@and\vdash
1.\Diamond(1),1.\Diamond(\overline{1})\vdash 1.1,1.\overline{1}\vdash\vdash
1.1,1.\Diamond(\overline{1})\vdash 1.1,1.\overline{1}\vdash$

and

$\vdash 1.\Diamond(1),1.(\Diamond(\overline{1})\sqcup\overline{1})\vdash
1.\Diamond(1),1.\Diamond(\overline{1})\mid\ \vdash
1.\Diamond(1),1.\overline{1}\vdash
1.\Diamond(1),1.\Diamond(\overline{1})\vdash 1.1,1.\overline{1}\vdash$

  * •

For the axiom $\Diamond(r_{1}x+r_{2}y)=r_{1}\Diamond(x)+r_{2}\Diamond(y)$.

$\vdash
1.\Diamond(r_{1}x+r_{2}y),1.(r_{1}\Diamond(\overline{x})+r_{2}\Diamond(\overline{y}))\vdash
1.\Diamond(r_{1}x+r_{2}y),1.r_{1}\Diamond(\overline{x}),1.r_{2}\Diamond(\overline{y})\vdash
1.\Diamond(r_{1}x+r_{2}y),r_{1}.\Diamond(\overline{x}),r_{2}.\Diamond(\overline{y})\vdash
1.(r_{1}x+r_{2}y),r_{1}.\overline{x},r_{2}.\overline{y}\vdash
1.r_{1}x,1.r_{2}y,r_{1}.\overline{x},r_{2}.\overline{y}\vdash
r_{1}.x,r_{2}.y,r_{1}.\overline{x},r_{2}.\overline{y}\vdash$

and

$\vdash
1.(r_{1}\Diamond(x)+r_{2}\Diamond(y)),1.\Diamond(r_{1}\overline{x}+r_{2}\overline{y})\vdash
1.r_{1}\Diamond(x),1.r_{2}\Diamond(y),1.\Diamond(r_{1}\overline{x}+r_{2}\overline{y})\vdash
r_{1}.\Diamond(x),r_{2}.\Diamond(y),1.\Diamond(r_{1}\overline{x}+r_{2}\overline{y})\vdash
r_{1}.x,r_{2}.y,1.(r_{1}\overline{x}+r_{2}\overline{y})\vdash
r_{1}.x,r_{2}.y,1.r_{1}\overline{x},1.r_{2}\overline{y}\vdash
r_{1}.x,r_{2}.y,r_{1}.\overline{x},r_{2}.\overline{y}\vdash$

  * •

For the axiom $0\leq\Diamond(0\sqcup x)$.

$\vdash 1.(0\sqcap\Diamond(0\sqcup x)),1.0\vdash 1.(0\sqcap\Diamond(0\sqcup
x))\lx@proof@logical@and\vdash 1.0\vdash\vdash 1.\Diamond(0\sqcup x)\vdash
1.(0\sqcup x)\vdash 1.0\mid\ \vdash 1.x\vdash 1.0\vdash$

and

$\vdash 1.0,1.(0\sqcup\Diamond(0\sqcap\overline{x}))\vdash
1.(0\sqcup\Diamond(0\sqcap\overline{x}))\vdash 1.0\mid\ \vdash
1.\Diamond(0\sqcap\overline{x})\vdash 1.0\vdash$

######  Remark 67.

By inspecting the proof of Lemma 66 it is possible to verify that the T rule
is never used in the construction of $\triangleright_{\textbf{HMR}}G$. This,
together with the similar Remark 61 regarding the Lemma 60, implies that the T
rule is never used in the proof of the completeness Theorem 51. From this we
get the following corollary.

######  Corollary 68.

The T rule is admissible in the system HMR.

As in the case of the system HR (see Lemma 35) there is no hope of eliminating
both the T rule and the CAN rule from the HMR system.

######  Lemma 69.

Let $r_{1}$ and $r_{2}$ be two irrational numbers that are incommensurable
over $\mathbb{Q}$ (so there is no $q\in\mathbb{Q}$ such that $qr_{1}=r_{2}$).
Then the atomic hypersequent $G$

$\vdash r_{1}.x\mid\ \vdash r_{2}.\overline{x}$

does not have a CAN–free and T–free derivation.

######  Proof 4.10.

The proof is similar to that of Lemma 35 but Lemma 70 below takes the place of
Lemma 36.

######  Lemma 70.

For all basic hypersequents $G$, built using the variables and negated
variables $x_{1},\overline{x_{1}},\dots,x_{k},\overline{x_{k}}$, of the form

$\vdash\Gamma_{1},\Diamond\Delta_{1},\vec{r^{\prime}}_{1}.1,\vec{s^{\prime}}_{1}.\overline{1}\mid\
...\mid\
\vdash\Gamma_{m},\Diamond\Delta_{m},\vec{r^{\prime}}_{m}.1,\vec{s^{\prime}}_{m}.\overline{1}$

where
$\Gamma_{i}=\vec{r}_{i,1}.x_{1},...,\vec{r}_{i,k}.x_{k},\vec{s}_{i,1}.\overline{x_{1}},...,\vec{s}_{i,k}.\overline{x_{i,k}}$,
the following are equivalent:

  1. (1)

$G$ has a CAN–free and T–free derivation.

  2. (2)

there exist natural numbers $n_{1},...,n_{m}\in\mathbb{N}$, one for each
sequent in $G$, such that:

     * •

there exists $i\in[1..m]$ such that $n_{i}\neq 0$, i.e., the numbers are not
all $0$’s, and

     * •

for every variable and covariable $(x_{j},\overline{x_{j}})$ pair, it holds
that

$\sum^{m}_{i=1}n_{i}(\sum\vec{r}_{i,j})=\sum^{m}_{i=1}n_{i}(\sum\vec{s}_{i,j})$

i.e., the scaled (by the numbers $n_{1}$ …$n_{m}$) sum of the coefficients in
front of the variable $x_{j}$ is equal to the scaled sum of the coefficients
in from of the covariable $\overline{x_{j}}$, and

     * •

$\sum_{i=1}^{m}n_{i}\sum\vec{s^{\prime}}_{i}\leq\sum_{i=1}^{m}n_{i}\sum\vec{r^{\prime}}_{i}$,
i.e., there are more $1$ than $\overline{1}$, and

     * •

the hypersequent consisting of only one sequent

$\vdash\Delta_{1}^{n_{1}},...,\Delta_{m}^{n_{m}},(\vec{r^{\prime}}_{1}.1)^{n_{1}},...,(\vec{r^{\prime}}_{m}.1)^{n_{m}},(\vec{s^{\prime}}_{1}.\overline{1})^{n_{1}},...,(\vec{s^{\prime}}_{m}.\overline{1})^{n_{m}}$

has a CAN–free and T–free derivation, where the notation $\Gamma^{n}$ means
$\underbrace{\Gamma,...,\Gamma}_{n\text{ times}}$.

######  Proof 4.11.

We prove $(1)\Rightarrow(2)$ by induction on the derivation of $G$. We show
only the M case, the other cases being simple. We write $\Gamma^{\prime}_{i}$
for
$\Gamma_{i},\Diamond\Delta_{i},\vec{r^{\prime}}_{i}.1,\vec{s^{\prime}}_{i}.\overline{1}$.

  * •

If the derivation finishes with

$\vdash\Gamma^{\prime}_{1}\mid\ ...\mid\
\vdash\Gamma^{\prime}_{m},\Gamma^{\prime}_{m+1}\lx@proof@logical@and\vdash\Gamma^{\prime}_{1}\mid\
...\mid\ \vdash\Gamma^{\prime}_{m}\vdash\Gamma^{\prime}_{1}\mid\ ...\mid\
\vdash\Gamma^{\prime}_{m+1}$

by induction hypothesis, there are $n_{1},...,n_{m}\in\mathbb{N}$ such that :

    * –

there exists $i\in[1..m]$ such that $n_{i}\neq 0$.

    * –

for every variable and covariable $(x_{j},\overline{x_{j}})$ pair, it holds
that $\sum_{i}n_{i}.\sum\vec{r}_{i,j}=\sum_{i}n_{i}.\sum\vec{s}_{i,j}$.

    * –

$\sum_{i=1}^{m}n_{i}\sum\vec{s^{\prime}}_{i}\leq\sum_{i=1}^{m}n_{i}\sum\vec{r^{\prime}}_{i}$.

    * –

$\vdash\Delta_{1}^{n_{1}},...,\Delta_{m}^{n_{m}},(\vec{r^{\prime}}_{1}.1)^{n_{1}},...,(\vec{r^{\prime}}_{m}.1)^{n_{m}},(\vec{s^{\prime}}_{1}.\overline{1})^{n_{1}},...,(\vec{s^{\prime}}_{m}.\overline{1})^{n_{m}}$
has a CAN–free and T–free derivation.

and $n^{\prime}_{1},...,n^{\prime}_{m}\in\mathbb{N}$ such that :

    * –

there exists $i\in[1..m]$ such that $n^{\prime}_{i}\neq 0$.

    * –

for every variable and covariable $(x_{j},\overline{x_{j}})$ pair, it holds
that
$\sum_{i=0}^{m-1}n^{\prime}_{i}.\sum\vec{r}_{i,j}+n^{\prime}_{m}.\sum\vec{r}_{m+1,j}=\sum_{i=0}^{m-1}n^{\prime}_{i}.\sum\vec{s}_{i,j}+n^{\prime}_{m}.\sum\vec{s}_{m+1,j}$.

    * –

$\sum_{i=1}^{m-1}n^{\prime}_{i}\sum\vec{s^{\prime}}_{i}+n^{\prime}_{m}\sum\vec{s^{\prime}}_{m+1}\leq\sum_{i=1}^{m-1}n^{\prime}_{i}\sum\vec{r^{\prime}}_{i}+n^{\prime}_{m}\sum\vec{r^{\prime}}_{m+1}$.

    * –

$\vdash\Delta_{1}^{n^{\prime}_{1}},...,\Delta_{m+1}^{n^{\prime}_{m}},(\vec{r^{\prime}}_{1}.1)^{n^{\prime}_{1}},...,(\vec{r^{\prime}}_{m+1}.1)^{n^{\prime}_{m}},(\vec{s^{\prime}}_{1}.\overline{1})^{n^{\prime}_{1}},...,(\vec{s^{\prime}}_{m+1}.\overline{1})^{n_{m}}$
has a CAN–free and T–free derivation.

If $n_{m}=0$ then $n_{1},...,n_{m-1},0$ satisfies the property.
Otherwise if $n^{\prime}_{m}=0$ then $n^{\prime}_{1},...,n^{\prime}_{m-1},0$
satisfies the property.
Otherwise,
$n_{m}.n^{\prime}_{1}+n^{\prime}_{m}.n_{1},n_{m}.n^{\prime}_{2}+n^{\prime}_{m}.n_{2},...,n_{m}.n^{\prime}_{m-1}+n^{\prime}_{m}.n_{m-1},n_{m}.n^{\prime}_{m}$
satisfies the property.

The other way ($(2)\Rightarrow(1)$) is more straightforward. If there exist
natural numbers $n_{1},...,n_{m}\in\mathbb{N}$, one for each sequent in $G$,
such that:

  * •

there exists $i\in[1..m]$ such that $n_{i}\neq 0$ and

  * •

for every variable and covariable $(x_{j},\overline{x_{j}})$ pair, it holds
that

$\sum^{m}_{i=1}n_{i}(\sum\vec{r}_{i,j})=\sum^{m}_{i=1}n_{i}(\sum\vec{s}_{i,j})$

and

  * •

$\sum_{i=1}^{m}n_{i}\sum\vec{s^{\prime}}_{i}\leq\sum_{i=1}^{m}n_{i}\sum\vec{r^{\prime}}_{i}$.and

  * •

$\vdash\Delta_{1}^{n_{1}},...,\Delta_{m}^{n_{m}},(\vec{r^{\prime}}_{1}.1)^{n_{1}},...,(\vec{r^{\prime}}_{m}.1)^{n_{m}},(\vec{s^{\prime}}_{1}.\overline{1})^{n_{1}},...,(\vec{s^{\prime}}_{m}.\overline{1})^{n_{m}}$
has a CAN–free and T–free derivation.

then we can use the W rule to remove the sequents corresponding to the numbers
$n_{i}=0$, and use the C rule $n_{i}-1$ times then the S rule $n_{i}-1$ times
on the $i$th sequent to multiply it by $n_{i}$. If we assume that there is a
natural number $l$ such that $n_{i}=0$ for all $i>l$ and $n_{i}\neq 0$ for all
$i\leq l$, then the CAN–free T–free derivation is:

$\vdash\Gamma_{1},\Diamond\Delta_{1},\vec{r^{\prime}}_{1}.1,\vec{s^{\prime}}_{1}.\overline{1}\mid\
...\mid\
\vdash\Gamma_{m},\Diamond\Delta_{m},\vec{r^{\prime}}_{m}.1,\vec{s^{\prime}}_{m}.\overline{1}\vdash\Gamma_{1},\Diamond\Delta_{1},\vec{r^{\prime}}_{1}.1,\vec{s^{\prime}}_{1}.\overline{1}\mid\
...\mid\
\vdash\Gamma_{l},\Diamond\Delta_{l},\vec{r^{\prime}}_{l}.1,\vec{s^{\prime}}_{l}.\overline{1}\vdash(\Gamma_{1},\Diamond\Delta_{1},\vec{r^{\prime}}_{1}.1,\vec{s^{\prime}}_{1}.\overline{1})^{n_{1}}\mid\
\dots\mid\
\vdash(\Gamma_{l},\Diamond\Delta_{l},\vec{r^{\prime}}_{l}.1,\vec{s^{\prime}}_{l}.\overline{1})^{n_{l}}\vdash(\Gamma_{1},\Diamond\Delta_{1},\vec{r^{\prime}}_{1}.1,\vec{s^{\prime}}_{1}.\overline{1})^{n_{1}},\dots,(\Gamma_{l},\Diamond\Delta_{l},\vec{r^{\prime}}_{l}.1,\vec{s^{\prime}}_{l}.\overline{1})^{n_{l}}\vdash(\Diamond\Delta_{1},\vec{r^{\prime}}_{1}.1,\vec{s^{\prime}}_{1}.\overline{1})^{n_{1}},\dots,(\Diamond\Delta_{l},\vec{r^{\prime}}_{l}.1,\vec{s^{\prime}}_{l}.\overline{1})^{n_{l}}\vdash(\Delta_{1},\vec{r^{\prime}}_{1}.1,\vec{s^{\prime}}_{1}.\overline{1})^{n_{1}},\dots,(\Delta_{l},\vec{r^{\prime}}_{l}.1,\vec{s^{\prime}}_{l}.\overline{1})^{n_{l}}$

and we can conclude using the last condition that states that

$\vdash(\Delta_{1},\vec{r^{\prime}}_{1}.1,\vec{s^{\prime}}_{1}.\overline{1})^{n_{1}},\dots,(\Delta_{l},\vec{r^{\prime}}_{l}.1,\vec{s^{\prime}}_{l}.\overline{1})^{n_{l}}$

has a CAN–free and T–free derivation.

###  4.5. CAN–free Invertibility – Proof of Theorem 53

The proofs presented in this section follow the same pattern of those in
Section 3.6: we will prove the CAN–free invertibility of more general rules.
The generalised non–modal rules are the same as those in Figure 7 from Section
3.6 and the generalised $\Diamond$ rule has the following shape:

$[\vdash\Diamond\Gamma_{i},\vec{r}_{i}.1,\vec{s}_{i}.\overline{1}]_{i=1}^{n}[\vdash\Gamma_{i},\vec{r}_{i}.1,\vec{s}_{i}.\overline{1}]_{i=1}^{n}$

######  Remark 71.

The generalized $\Diamond$ rule is unsound, the hypersequent $\vdash
1.\Diamond(\overline{x}\sqcap\overline{y}),1.\Diamond(x)\sqcup\Diamond(y)$ is
derivable using this rule (see Remark 52, a similar derivation can be used to
derive the hypersequent). Yet, even if the generalized $\Diamond$ rule is not
sound, it still enjoys CAN–free invertibility.

We will prove that those rules are CAN–free invertible by induction on the
derivation of the conclusion. The proof steps dealing with the rules already
present in HR are the same as in Section 3.6. In what follows we just show the
details of the proof steps associated with the new cases associated with the
$\Diamond$–rule and $1$–rule of HMR.

######  Lemma 72.

If $[\vdash\Gamma_{i},\vec{r}_{i}.(A\sqcup B)]_{i=1}^{n}$ has a CAN–free
derivation then $[\vdash\Gamma_{i},\vec{r}_{i}.A\mid\
\vdash\Gamma_{i},\vec{r}_{i}.B]_{i=1}^{n}$ has a CAN–free derivation.

######  Proof 4.12.

By induction on the derivation.

  * •

If the derivation finishes with

$[\vdash\Gamma_{i},\vec{r}_{i}.(A\sqcup B)]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.(A\sqcup
B),\vec{r}.1,\vec{s}.\overline{1}[\vdash\Gamma_{i},\vec{r}_{i}.(A\sqcup
B)]_{i=2}^{n}\mid\ \vdash\Gamma_{1},\vec{r}_{1}.(A\sqcup B)$

then by induction hypothesis on the CAN–free derivation of the premise we have
that

$\triangleright_{\textbf{HMR}\backslash\\{\text{CAN}\\}}[\vdash\Gamma_{i},\vec{r}_{i}.A\mid\
\vdash\Gamma_{i},\vec{r}_{i}.B]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.A\mid\ \vdash\Gamma_{1},\vec{r}_{1}.B$

so

$G^{\prime}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.A,\vec{r}.1,\vec{s}.\overline{1}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.B,\vec{r}.1,\vec{s}.\overline{1}G^{\prime}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.A\mid\ \vdash\Gamma_{1},\vec{r}_{1}.B$

with $G^{\prime}=[\vdash\Gamma_{i},\vec{r}_{i}.A\mid\
\vdash\Gamma_{i},\vec{r}_{i}.B]_{i=2}^{n}$

  * •

If the derivation finishes with an application of the $\Diamond$ rule, the
shape of the conclusion is

$\vdash\Diamond\Gamma_{1},\vec{r}.1,\vec{s}.\overline{1}$

with $\vec{r_{1}}=\emptyset$ so the hypersequent

$\vdash\Diamond\Gamma_{1},\vec{r_{1}}.A,\vec{r}.1,\vec{s}.\overline{1}\mid\
\vdash\Diamond\Gamma_{1},\vec{r_{1}}.B,\vec{r}.1,\vec{s}.\overline{1}=\
\vdash\Diamond\Gamma_{1},\vec{r}.1,\vec{s}.\overline{1}\mid\
\vdash\Diamond\Gamma_{1},\vec{r}.1,\vec{s}.\overline{1}$

is CAN–free derivable using the C rule.

######  Lemma 73.

If $[\vdash\Gamma_{i},\vec{r}_{i}(A+B)]_{i=1}^{n}$ has a CAN–free derivation
then $[\vdash\Gamma_{i},\vec{r}_{i}A,\vec{r}_{i}B]_{i=1}^{n}$ has a CAN–free
derivation.

######  Proof 4.13.

By induction on the derivation.

  * •

If the derivation finishes with

$[\vdash\Gamma_{i},\vec{r}_{i}.(A+B)]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.(A+B),\vec{r}.1,\vec{s}.\overline{1}[\vdash\Gamma_{i},\vec{r}_{i}.(A+B)]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.(A+B)$

then by induction hypothesis on the CAN–free derivation of the premise we have
that

$\triangleright_{\textbf{HMR}\backslash\\{\text{CAN}\\}}[\vdash\Gamma_{i},\vec{r}_{i}.A,\vec{r}_{i}.B]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.A,\vec{r}_{1}.B$

so

$[\vdash\Gamma_{i},\vec{r}_{i}.A,\vec{r}_{i}.B]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.A,\vec{r}_{1}.B,\vec{r}.1,\vec{s}.\overline{1}[\vdash\Gamma_{i},\vec{r}_{i}.A,\vec{r}_{i}.B]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.A,\vec{r}_{1}.B$

  * •

If the derivation finishes with an application of the $\Diamond$ rule, the
shape of the conclusion is

$\vdash\Diamond\Gamma_{1},\vec{r}.1,\vec{s}.\overline{1}$

with $\vec{r_{1}}=\emptyset$ so the hypersequent
$\vdash\Diamond\Gamma_{1},\vec{r_{1}}.A,\vec{r_{1}}.B,\vec{r}.1,\vec{s}.\overline{1}=\
\vdash\Diamond\Gamma_{1},\vec{r}.1,\vec{s}.\overline{1}$ is derivable.

######  Lemma 74.

If $\vdash\Gamma_{i},\vec{r}_{i}.(A\sqcap B)]_{i=1}^{n}$ has a CAN–free
derivation then $[\vdash\Gamma_{i},\vec{r}_{i}.A]_{i=1}^{n}$ and
$[\vdash\Gamma_{i},\vec{r}_{i}.B]_{i=1}^{n}$ have CAN–free derivations.

######  Proof 4.14.

By induction on the derivation. We will only show that
$\triangleright_{\textbf{HMR}\backslash\\{\text{CAN}\\}}[\vdash\Gamma_{i},\vec{r}_{i}.A]_{i=1}^{n}$,
the other case is similar.

  * •

If the derivation finishes with

$[\vdash\Gamma_{i},\vec{r}_{i}.(A\sqcap B)]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.(A\sqcap
B),\vec{r}.1,\vec{s}.\overline{1}[\vdash\Gamma_{i},\vec{r}_{i}.(A\sqcap
B)]_{i=2}^{n}\mid\ \vdash\Gamma_{1},\vec{r}_{1}.(A\sqcap B)$

then by induction hypothesis on the CAN–free derivation of the premise we have
that

$\triangleright_{\textbf{HMR}\backslash\\{\text{CAN}\\}}[\vdash\Gamma_{i},\vec{r}_{i}.A]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.A$

so

$[\vdash\Gamma_{i},\vec{r}_{i}.A]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.A,\vec{r}.1,\vec{s}.\overline{1}[\vdash\Gamma_{i},\vec{r}_{i}.A]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.A$

  * •

If the derivation finishes with an application of the $\Diamond$ rule, the
shape of the conclusion is

$\vdash\Diamond\Gamma_{1},\vec{r}.1,\vec{s}.\overline{1}$

with $\vec{r_{1}}=\emptyset$ so the hypersequent
$\vdash\Diamond\Gamma_{1},\vec{r_{1}}.A,\vec{r}.1,\vec{s}.\overline{1}=\
\vdash\Diamond\Gamma_{1},\vec{r}.1,\vec{s}.\overline{1}$ is derivable.

######  Lemma 75.

If
$[\vdash\Diamond\Gamma_{i},\vec{r}_{i}.1,\vec{s}_{i}.\overline{1}]_{i=1}^{n}$
has a CAN–free derivation then
$[\vdash\Gamma_{i},\vec{r}_{i}.1,\vec{s}_{i}.\overline{1}]_{i=1}^{n}$ has a
CAN–free derivation.

######  Proof 4.15.

By induction on the derivation. Since the hypersequent under consideration is
basic, we do not need to deal with any logical rule beside the
$\Diamond$–rule, which leads immediately to the desired result, and the cases
regarding the structural rules are very simple. For instance, if the
derivation finishes with the W rule:

$[\vdash\Diamond\Gamma_{i},\vec{r}_{i}.1,\vec{s}_{i}.\overline{1}]_{i=2}^{n}\mid\
\vdash\Diamond\Gamma_{1},\vec{r}_{1}.1,\vec{s}_{1}.\overline{1}[\vdash\Diamond\Gamma_{i},\vec{r}_{i}.1,\vec{s}_{i}.\overline{1}]_{i=2}^{n}$

then by induction hypothesis

$\triangleright_{\textbf{HMR}\backslash\\{\text{CAN}\\}}[\vdash\Gamma_{i},\vec{r}_{i}.1,\vec{s}_{i}.\overline{1}]_{i=2}^{n}$

so

$[\vdash\Gamma_{i},\vec{r}_{i}.1,\vec{s}_{i}.\overline{1}]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.1,\vec{s}_{1}.\overline{1}[\vdash\Gamma_{i},\vec{r}_{i}.1,\vec{s}_{i}.\overline{1}]_{i=2}^{n}$

###  4.6. M-elimination – Proof of Theorem 55

Following the same pattern of Section 3.7, we need to show that for each
hypersequent $G$ and sequents $\Gamma$ and $\Delta$, if there exist CAN–free
and M–free derivations $d_{1}$ of $G\mid\ \vdash\Gamma$ and $d_{2}$ of $G\mid\
\vdash\Delta$, then there also exists a CAN–free and M–free derivation of
$G\mid\ \vdash\Gamma,\Delta$.

The general idea presented in Section 3.7 is to combine the derivations
$d_{1}$ and $d_{2}$ in a sequential way, first constructing a prederivation
$d_{1}^{\prime}$ of $G\mid\ G\mid\ \vdash\Gamma,\Delta$ (using $d_{1}$) whose
leaves are either axioms or hypersequents of the form $G\mid\
\vdash\vec{r}.\Delta$, and then by completing this prederivation into a
derivation (using $d_{2}$). Finally, $G\mid\ G\mid\ \vdash\Gamma,\Delta$ can
be easily turned into a derivation of $G\mid\ \vdash\Gamma,\Delta$ as desired.

However, this technique cannot be directly applied in the context of the
system HMR due to the constraints imposed on the shape of the hypersequent by
the $\Diamond$ rule. Indeed an application of the $\Diamond$ rule in $d_{1}$
acting on some hypersequent of the form

$\vdash\Diamond\Gamma_{1},\vec{r}_{1}.1,\vec{s}_{1}.\overline{1}$

cannot turned into an application of the $\Diamond$ rule on

$G\mid\
\vdash\Delta,\Diamond\Gamma_{1},\vec{r}_{1}.1,\vec{s}_{1}.\overline{1}$

because this hypersequent cannot be the conclusion of a $\Diamond$ rule as it
does not satisfy the constraints.

For this reason, when constructing the prederivation $d^{\prime}_{1}$
inductively from $d_{1}$, we stop at the applications of the $\Diamond$–rule.
Hence, the inductive procedure takes the derivation $d_{1}$ and produces a
CAN–free and M–free prederivation $d_{1}^{\prime}$ of

$G\mid\ G\mid\ \vdash\Gamma,\Delta$

where all the leaves in the prederivation are either:

  1. (1)

terminated, or

  2. (2)

non–terminated and having the shape

$G\mid\ \vdash\vec{r}.\Delta$

which can then be completed using the derivation $d_{2}$ in the exact same way
explained in Section 3.7, or

  3. (3)

non–terminated and having the shape:

$G\mid\
\vdash\Diamond\Gamma^{\prime},\vec{r}.\Delta,\vec{s}.1,\vec{t}.\overline{1}$

for some sequent $\Gamma^{\prime}$ and vectors $\vec{r},\vec{s},\vec{t}$. For
each of these leaves there is a corresponding derivation of

$\vdash\Gamma^{\prime},\vec{s}.1,\vec{t}.\overline{1}$ (1)

To obtain derivations of the leaves of $d_{1}^{\prime}$ of the third type, and
thus complete the derivation, we proceed as follows. First, we use the
derivation $d_{2}$ to construct a CAN–free and M–free derivation
$d_{2,\vec{r}}$

$G\mid\ \vec{r}.\Delta$

for each vector of scalars $\vec{r}$ in the leaves. We then modify each
derivation $d_{2,\vec{r}}$ into a prederivation $d_{2}^{\prime}$ of

$G\mid\ G\mid\
\vdash\Diamond\Gamma^{\prime},\vec{r}.\Delta,\vec{s}.1,\vec{t}.\overline{1}$

using the exact same inductive procedure (which stops when reaching
applications of $\Diamond$ formulas) introduced above for producing
$d_{1}^{\prime}$ from $d_{1}$. Note that in this case, the leaves of the third
kind in $d_{2}^{\prime}$ are of the form:

$\vdash\vec{r^{\prime}}.(\Diamond\Gamma^{\prime},\vec{s}.1,\vec{t}.\overline{1}),\Diamond\Delta^{\prime},\vec{s^{\prime}}.1,\vec{t^{\prime}}.\overline{1}$

and have associated derivations of

$\vdash\Delta^{\prime},\vec{s^{\prime}}.1,\vec{t^{\prime}}.\overline{1}$ (2)

Therefore, we can legitimately apply the $\Diamond$ rule (Lemma 76 below
ensures that the proviso of the rule is respected) and reduce these leaves to
leaves of the form

$\vdash\vec{r^{\prime}}.(\Gamma^{\prime},\vec{s}.1,\vec{t}.\overline{1}),\Delta^{\prime},\vec{s^{\prime}}.1,\vec{t^{\prime}}.\overline{1}$

which, importantly, have a lower modal depth compared to the conclusion
$G\mid\ \vdash\Gamma$ of the derivation $d_{1}$ we started with above.

In order the produce a derivation for the leaves
$\vdash\vec{r^{\prime}}.(\Gamma^{\prime},\vec{s}.1,\vec{t}.\overline{1}),\Delta^{\prime},\vec{s^{\prime}}.1,\vec{t^{\prime}}.\overline{1}$,
and thus conclude the completion of $d_{1}^{\prime}$ into a full derivation,
it is sufficient to re–apply the whole process using the derivations of
Equation 1 and Equation 2 above. This process is well founded and eventually
terminates because the modal depth is decreasing.

We now proceeds with the technical statements.

######  Lemma 76.

Let $d_{1}$ be a CAN–free and M–free derivation of $G\mid\ \vdash\Gamma$ using
the $\Diamond$ rule and let $\Delta$ be a sequent. Then there exists a
prederivation of

$G\mid\ G\mid\ \vdash\Gamma,\Delta.$

where all non–terminated leaves are either of the form $G\mid\
\vdash\vec{r}.\Delta$ or of the form $G\mid\
\vdash\Diamond\Gamma^{\prime},\vec{r}.\Delta,\vec{s}.1,\vec{t}.\overline{1}$
for some sequent $\Gamma^{\prime}$ and vectors $\vec{r},\vec{s},\vec{t}$ such
that

  * •

$\sum\vec{s}\geq\sum\vec{t}$ and

  * •

$\vdash\Gamma^{\prime},\vec{s}.1,\vec{t}.\overline{1}$ has a derivation
$d_{1}^{\prime}$ with a strictly lower modal depth than $d_{1}$.

######  Proof 4.16.

This is an instance of the slightly more general statement of Lemma 79 below
where:

  * •

$[\vdash\Gamma_{i}]_{i=1}^{n-1}=G$ and $\Gamma_{n}=\Gamma$.

  * •

$\vec{r}_{i}=\emptyset$ for $1\leq i<n$ and $\vec{r}_{n}=\vec{r}$.

######  Lemma 77.

Let $d_{2}$ be CAN–free and M–free derivation of $G\mid\ \vdash\Delta$. Then,
for every vector $\vec{r}$, there exists a CAN–free and M–free derivation of

$G\mid\ \vdash\vec{r}.\Delta$

with a modal depth lower or equal than $d_{2}$.

######  Proof 4.17.

This is an instance of the slightly more general statement of Lemma 80 below
where:

  * •

$[\vdash\Delta_{i}]_{i=1}^{n-1}=G$ and $\Delta_{n}=\Delta$.

  * •

$\vec{r}_{i}=1$ for $1\leq i<n$ and $\vec{r}_{n}=\vec{r}$.

######  Lemma 78.

Let $d_{1}$ be a CAN–free and M–free derivation of $G\mid\ \vdash\Gamma$
without any $\Diamond$ rule and let $\Delta$ be a sequent. Then there exists a
prederivation of

$G\mid\ G\mid\ \vdash\Gamma,\Delta.$

where all non–terminated leaves are of the form $G\mid\ \vdash\vec{r}.\Delta$
for some vector $\vec{r}$.

######  Proof 4.18.

This is an other intance of Lemma 79 where:

  * •

$[\vdash\Gamma_{i}]_{i=1}^{n-1}=G$ and $\Gamma_{n}=\Gamma$.

  * •

$\vec{r}_{i}=\emptyset$ for $1\leq i<n$ and $\vec{r}_{n}=\vec{r}$.

Since the leaves of the form $G\mid\
\vdash\Diamond\Gamma^{\prime},\vec{r}.\Delta,\vec{s}.1,\vec{t}.\overline{1}$
are generated only by the $\Diamond$ rule, and there is no $\Diamond$ rule in
$d_{1}$, then all non–terminated leaves are of the form $G\mid\
\vdash\vec{r}.\Delta$ for some vector $\vec{r}$.

######  Lemma 79.

Let $d_{1}$ be a CAN–free and M–free derivation of
$[\vdash\Gamma_{i}]_{i=1}^{n}$ and let $G$ be a hypersequent and $\Delta$ be a
sequent. Then for every sequence of vectors $\vec{r_{i}}$, there exists a
prederivation of

$G\mid\ [\vdash\Gamma_{i},\vec{r_{i}}.\Delta]_{i=1}^{n}$

where all non–terminated leaves are of the form $G\mid\
\vdash\Diamond\Gamma^{\prime},\vec{r}.\Delta,\vec{s}.1,\vec{t}.\overline{1}$
for some sequent $\Gamma^{\prime}$ and vectors $\vec{r},\vec{s},\vec{t}$ such
that

  * •

$\sum\vec{s}\geq\sum\vec{t}$ and

  * •

$\vdash\Gamma^{\prime},\vec{s}.1,\vec{t}.\overline{1}$ has a derivation
$d_{1}^{\prime}$ with a strictly lower modal depth than $d_{1}$.

######  Proof 4.19.

We prove the result by induction on $d_{1}$. We will only show the $\Diamond$
and the $1$ rules, since all other cases are done in the same way as in Lemma
42.

  * •

if $d_{1}$ finishes with:

$[\vdash\Gamma_{i}]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{s}.1,\vec{t}.\overline{1}[\vdash\Gamma_{i}]_{i=2}^{n}\mid\
\vdash\Gamma_{1}$

then by induction hypothesis, there is a prederivation of
$[\vdash\Gamma_{i},\vec{r}_{i}.\Delta]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.\Delta$ where all non–terminated leaves are of
the form $G\mid\
\vdash\Diamond\Gamma^{\prime},\vec{r}.\Delta,\vec{s}.1,\vec{t}.\overline{1}$
for some sequent $\Gamma^{\prime}$ and vectors $\vec{r},\vec{s},\vec{t}$ such
that

    * –

$\sum\vec{s}\geq\sum\vec{t}$ and

    * –

$\vdash\Gamma^{\prime},\vec{s}.1,\vec{t}.\overline{1}$ has a derivation
$d_{1}^{\prime}$ with a strictly lower modal depth than $d_{1}$.

We continue the prederivation with

$[\vdash\Gamma_{i},\vec{r}_{i}.\Delta]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.\Delta,\vec{s}.1,\vec{t}.\overline{1}[\vdash\Gamma_{i},\vec{r}_{i}.\Delta]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.\Delta$

  * •

If $d_{1}$ finishes with:

$\vdash\Diamond\Gamma_{1},\vec{s}.1,\vec{t}.\overline{1}\vdash\Gamma_{1},\vec{s}.1,\vec{t}.\overline{1}$

then the prederivation is simply the leaf
$\vdash\Diamond\Gamma_{1},\vec{r}_{1}.\Delta,\vec{s}.1,\vec{t}.\overline{1}$
which satisfies both

    * –

$\sum\vec{s}\geq\sum\vec{t}$ and

    * –

$\vdash\Gamma_{1},\vec{s}.1,\vec{t}.\overline{1}$ is derivable using stricly
less $\Diamond$ rule than in $d_{1}$.

######  Lemma 80.

If $d_{2}$ is a CAN–free M–free derivation of
$\left[\vdash\Delta_{i}\right]_{i=1}^{n}$ then for all $\vec{r_{i}}$, there is
a CAN–free M–free derivation of
$\left[\vdash\vec{r_{i}}.\Delta_{i}\right]_{i=1}^{n}$ with a modal depth lower
or equal than $d_{2}$.

######  Proof 4.20.

We will only show the $\Diamond$ and $1$ rules, the other cases being similar
to Lemma 43 – and so do not introduce any new $\Diamond$ rule.

  * •

if $d_{2}$ finishes with:

$[\vdash\Delta_{i}]_{i=2}^{n}\mid\
\vdash\Delta_{1},\vec{s}.1,\vec{t}.\overline{1}[\vdash\Delta_{i}]_{i=2}^{n}\mid\
\vdash\Delta_{1}$

then by induction hypothesis, there is a CAN–free M–free derivation of
$[\vdash\vec{r}_{i}.\Delta_{i}]_{i=2}^{n}\mid\ \vdash\vec{r}_{1}.\Delta_{1}$
with a modal depth lower or equal than $d_{2}$. We continue the derivation
with

$[\vdash\vec{r}_{i}.\Delta_{i}]_{i=2}^{n}\mid\
\vdash\vec{r}_{1}.\Delta_{1},(\vec{r}_{1}\vec{s}).1,(\vec{r}_{1}\vec{t}).\overline{1}[\vdash\vec{r}_{i}.\Delta_{i}]_{i=2}^{n}\mid\
\vdash\vec{r}_{1}.\Delta_{1}$

which does not increase the modal depth of the derivation.

  * •

If $d_{2}$ finishes with:

$\vdash\Diamond\Delta_{1},\vec{s}.1,\vec{t}.\overline{1}\vdash\Delta_{1},\vec{s}.1,\vec{t}.\overline{1}$

by induction hypothesis, there is a derivation of
$\vdash\vec{r}_{1}.\Delta_{1},(\vec{r}_{1}\vec{s}).1,(\vec{r}_{1}\vec{t}).\overline{1}$
with a modal depth strictly fewer than $d_{2}$. We continue the derivation
with

$\vdash\vec{r}_{1}.\Diamond\Delta_{1},(\vec{r}_{1}\vec{s}).1,(\vec{r_{1}}\vec{t}).\overline{1}\vdash\vec{r}_{1}.\Delta_{1},(\vec{r}_{1}\vec{s}).1,(\vec{r_{1}}\vec{t}).\overline{1}$

which gives a derivation with a modal depth lower or equal than $d_{2}$.

###  4.7. CAN elimination – Proof of Theorem 56

Recall that the CAN rule has the following form:

$G\mid\ \vdash\Gamma G\mid\ \vdash\Gamma,\vec{s}.A,\vec{r}.\overline{A}$

As in Section 3.8, we prove Theorem 56 by showing that if the hypersequent
$G\mid\ \vdash\Gamma,\vec{s}.A,\vec{r}.\overline{A}$ has a CAN–free
derivation, then so does the hypersequent $G\mid\ \vdash\Gamma$.

As explained in the discussion before Theorem 56 and in its proof sketch, the
proof cannot just invoke the CAN-free invertibility Theorem 53 to simplify the
logical complexity of the CAN formula, due to the constraints imposed by the
$\Diamond$–rule.

To circumvent this issue, we prove the slightly more general Lemma 83 by
double induction on both the formula $A$ and the derivation of $G\mid\
\vdash\Gamma,\vec{r}.A,\vec{s}.\overline{A}$.

We first prove the two basic cases where $A=x$ (or equivalently
$A=\overline{x})$ and $A=1$ (or again $A=\overline{1}$).

######  Lemma 81.

If there is a CAN–free derivation of $G\mid\
\vdash\Gamma,\vec{r}.x,\vec{s}.\overline{x}$, where $\sum\vec{r}=\sum\vec{s}$,
then there exists a CAN–free derivation of $G\mid\ \vdash\Gamma$.

######  Proof 4.21.

By the M–elimination Theorem 55, we can assume that the derivation is CAN–free
and also M–free. The statement then follows as a special case of Lemma 84
below where

  * •

$[\vdash\Gamma_{i}]_{i=1}^{n-1}=G$ and $\Gamma_{n}=\Gamma$.

  * •

$\vec{r_{i}}=\vec{r^{\prime}_{i}}=\vec{s_{i}}=\vec{s^{\prime}_{i}}=\emptyset$
for $1\leq i<n$.

  * •

$\vec{r_{n}}=\vec{r}$, $\vec{s_{n}}=\vec{s}$ and
$\vec{r^{\prime}_{n}}=\vec{s^{\prime}_{n}}=\emptyset$.

The formulation of Lemma 84 is more technical but allows for a simpler proof
by induction on the structure of the derivation.

######  Lemma 82.

If there is a CAN–free derivation of $G\mid\
\vdash\Gamma,\vec{r}.1,\vec{s}.\overline{1}$, where $\sum\vec{r}=\sum\vec{s}$
then there exists a CAN–free derivation of $G\mid\ \vdash\Gamma$.

######  Proof 4.22.

As in the previous Lemma 81, we can assume that the derivation is also M–free
and we prove the more technical Lemma 85 that allows a simpler proof by
induction on the derivation.

In order to better handle the cases associated with the $\Diamond$ rule in the
proof of Theorem 56, we prove the more general Lemma 83 of which the CAN
elimination theorem rule is just an instance.

######  Lemma 83.

For all formulae $A$ and number $n>0$ and for all sequents $\Gamma_{i}$ and
vectors $\vec{r}_{i},\vec{s}_{i}$ such that $\sum\vec{r}_{i}=\sum\vec{s}_{i}$,
for $1\leq i\leq n$,

if $[\vdash\Gamma_{i},\vec{r}_{i}.A,\vec{s}_{i}.\overline{A}]_{i=1}^{n}$ has a
CAN–free M–free derivation, then so does $[\vdash\Gamma_{i}]_{i=1}^{n}$.

######  Proof 4.23.

For the basic cases $A=x$, $A=\overline{x}$, $A=1$ and $A=\overline{1}$, we
use Lemmas 81 and 82. For complex formulae $A$ which are not $\Diamond$
formulae, we proceed by invoking the CAN–free invertibility Theorem 53 as
follows:

  * •

If $A=0$, we can conclude with the CAN–free invertibility of the rule $0$.

  * •

If $A=B+C$, since the $+$ rule is CAN–free invertible,
$\left[\vdash\Gamma_{i},\vec{r_{i}}.B,\vec{r_{i}}.C,\vec{s_{i}}.\overline{B},\vec{s_{i}}.\overline{C}\right]$
has a CAN–free, M–free derivation. Therefore we can have a CAN–free derivation
of the hypersequent $[\vdash\Gamma_{i}]_{i=1}^{n}$ by invoking the induction
hypothesis twice, since the complexity of $B$ and $C$ is lower than that of
$B+C$.

  * •

If $A=r^{\prime}B$, since the $\times$ rule is CAN–free invertible,
$\left[\vdash\Gamma_{i},(r^{\prime}\vec{r_{i}}.).B,(r^{\prime}\vec{s_{i}}.).\overline{B}\right]$
has a CAN–free, M–free derivation. Therefore we can have a CAN–free derivation
of the hypersequent $[\vdash\Gamma_{i}]_{i=1}^{n}$ by invoking the induction
hypothesis on the simpler formula $B$.

  * •

If $A=B\sqcup C$, since the $\sqcup$ rule is CAN–free invertible,

$\left[\vdash\Gamma_{i},\vec{r_{i}}.B,\vec{s_{i}}.(\overline{B}\sqcap\overline{C})\right]\mid\
\left[\vdash\Gamma_{i},\vec{r_{i}}.C,\vec{s_{i}}.(\overline{B}\sqcap\overline{C})\right]$

has a CAN–free, M–free derivation. Then since the $\sqcap$ is CAN–free
invertible,
$\left[\vdash\Gamma_{i},\vec{r_{i}}.B,\vec{s_{i}}.\overline{B}\right]\mid\
\left[\vdash\Gamma_{i},\vec{r_{i}}.C,\vec{s_{i}}.\overline{C}\right]$ has a
CAN–free, M–free derivation. Therefore we can obtain a CAN–free derivation of
the hypersequent $[\vdash\Gamma_{i}]_{i=1}^{n}$ by invoking the induction
hypothesis twice on the simpler formulas $B$ and $C$.

  * •

If $A=B\sqcap C$, we proceed in a similar way as for the case $A=B\sqcup C$.

Now for the case $A=\Diamond B$, we distinguish two cases:

  1. (1)

the derivation ends with an application of the $\Diamond$ rule which
simplifies $A=\Diamond B$ to $B$. In this case we can simply conclude by
invoking the induction hypothesis on $B$.

  2. (2)

The derivation ends with some other rule (recall that no CAN rules and no M
rules appear in the derivation). In this case we decrease the complexity of
the derivation, keeping $\Diamond B$ as the CAN formula, and then invoke the
induction hypothesis on the derivation having reduced complexity. This proof
step is rather long to prove, as it requires analysing of all possible rules
concluding the derivation. We just illustrate the two case when the derivation
ends with a logical rule $(+)$ and a structural rule (C) to illustrate the
general method.

     * •

if the derivation finishes with

$[\vdash\Gamma_{i},\vec{r}_{i}.\Diamond
B,\vec{s}_{i}.\Diamond\overline{B}]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.\Diamond
B,\vec{s}_{1}.\Diamond\overline{B},\vec{r^{\prime}}.(C+D)[\vdash\Gamma_{i},\vec{r}_{i}.\Diamond
B,\vec{s}_{i}.\Diamond\overline{B}]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.\Diamond
B,\vec{s}_{1}.\Diamond\overline{B},\vec{r^{\prime}}.C,\vec{r^{\prime}}.D$

by induction hypothesis, there is a CAN–free M–free derivation of

$[\vdash\Gamma_{i}]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r^{\prime}}.C,\vec{r^{\prime}}.D$

We continue the derivation with

$[\vdash\Gamma_{i}]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r^{\prime}}.(C+D)[\vdash\Gamma_{i}]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r^{\prime}}.C,\vec{r^{\prime}}.D$

     * •

if the derivation finishes with

$[\vdash\Gamma_{i},\vec{r}_{i}.\Diamond
B,\vec{s}_{i}.\Diamond\overline{B}]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.\Diamond
B,\vec{s}_{1}.\Diamond\overline{B}[\vdash\Gamma_{i},\vec{r}_{i}.\Diamond
B,\vec{s}_{i}.\Diamond\overline{B}]_{i=2}^{n}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.\Diamond B,\vec{s}_{1}.\Diamond\overline{B}\mid\
\vdash\Gamma_{1},\vec{r}_{1}.\Diamond B,\vec{s}_{1}.\Diamond\overline{B}$

by induction hypothesis, there is a CAN–free M–free derivation of

$[\vdash\Gamma_{i}]_{i=2}^{n}\mid\ \vdash\Gamma_{1}\mid\ \vdash\Gamma_{1}$

We continue the derivation with

$[\vdash\Gamma_{i}]_{i=2}^{n}\mid\
\vdash\Gamma_{1}[\vdash\Gamma_{i}]_{i=2}^{n}\mid\ \vdash\Gamma_{1}\mid\
\vdash\Gamma_{1}$

######  Lemma 84.

If there is a CAN–free, M–free derivation of
$\left[\vdash\Gamma_{i},\vec{r_{i}}.x,\vec{s_{i}}.\overline{x}\right]_{i=1}^{n}$
then for all $\vec{r^{\prime}_{i}}.$ and $\vec{s^{\prime}_{i}}.$ such that for
all
$i$,$\sum\vec{r}_{i}-\sum\vec{s}_{i}=\sum\vec{r^{\prime}}_{i}-\sum\vec{s^{\prime}}_{i}$,
there is a CAN–free, M–free derivation of
$\left[\vdash\Gamma_{i},\vec{r^{\prime}_{i}}.x,\vec{s^{\prime}_{i}}.\overline{x}\right]_{i=1}^{n}$.

######  Proof 4.24.

By induction on the derivation.

######  Lemma 85.

If there is a CAN–free, M–free derivation of
$\left[\vdash\Gamma_{i},\vec{r_{i}}.1,\vec{s_{i}}.\overline{1}\right]_{i=1}^{n}$
then for all $\vec{r^{\prime}_{i}}.$ and $\vec{s^{\prime}_{i}}.$ such that for
all
$i$,$\sum\vec{r}_{i}-\sum\vec{s}_{i}\leq\sum\vec{r^{\prime}}_{i}-\sum\vec{s^{\prime}}_{i}$,
there is a CAN–free, M–free derivation of
$\left[\vdash\Gamma_{i},\vec{r^{\prime}_{i}}.1,\vec{s^{\prime}_{i}}.\overline{1}\right]_{i=1}^{n}$.

######  Proof 4.25.

By induction on derivation. We show only the non–trivial case.

  * •

If the derivation finishes with:

$\left[\vdash\Gamma_{i},\vec{r_{i}}.1,\vec{s_{i}}.\overline{1}\right]_{i\geq
2}\mid\
\vdash\Gamma_{1},(\vec{a};\vec{b};\vec{c}).1,(\vec{a^{\prime}};\vec{b^{\prime}};\vec{c^{\prime}}).\overline{1}\left[\vdash\Gamma_{i},\vec{r_{i}}.1,\vec{s_{i}}.\overline{1}\right]_{i\geq
2}\mid\ \vdash\Gamma_{1},\vec{c}1,\vec{c^{\prime}}\overline{1}$

with $\vec{r_{1}}=\vec{b};\vec{c}$ and
$\vec{s_{1}}=\vec{b^{\prime}};\vec{c^{\prime}}$, then

$\displaystyle\sum\vec{c}-\sum\vec{c^{\prime}}$ $\displaystyle=$
$\displaystyle(\sum\vec{r}_{1}-\sum\vec{b})-(\sum\vec{s}_{1}-\sum\vec{b}^{\prime})$
$\displaystyle=$
$\displaystyle(\sum\vec{r}_{1}-\sum\vec{s}_{1})+(\sum\vec{b}^{\prime}-\sum\vec{b})$
$\displaystyle\leq$
$\displaystyle(\sum\vec{r^{\prime}}_{1}-\sum\vec{s^{\prime}}_{1})+(\sum\vec{a}-\sum\vec{a}^{\prime})$
$\displaystyle=$
$\displaystyle\sum\vec{r^{\prime}}_{1}+\sum\vec{a}-(\sum\vec{s^{\prime}}_{1}+\sum\vec{a^{\prime}})$

so by induction hypothesis

$\triangleright_{\textbf{HMR}}\left[\vdash\Gamma_{i},\vec{r^{\prime}_{i}}.1,\vec{s^{\prime}_{i}}.\overline{1}\right]_{i\geq
2}\mid\
\vdash\Gamma_{1},(\vec{r^{\prime}_{1}};\vec{a}).1,(\vec{s^{\prime}_{1}};\vec{a^{\prime}}).\overline{1}$

which is the result we want.

###  4.8. Decidability – Proof of Theorem 57

In this section we adapt the algorithm presented in Section 3.10 and prove the
decidability of the HMR system.

The procedure takes a hypersequent $G$, where scalars are polynomials over
scalar-variables $\vec{\alpha}$ as coefficients in weighted formulas, and
construct a formula $\phi_{G}(\vec{\alpha})\in FO(\mathbb{R},+,\times,\leq)$
in the language of the first order theory of the real closed field. The
procedure is recursive and terminates because each recursive call decreases
the logical complexity and the modal complexity (i.e., the maximal modal depth
of any formulas) of its input $G$. The key property is that a sequence of
scalars $\vec{s}\in\mathbb{R}$ satisfies $\phi_{G}$ if and only if the
hypersequent $G[s_{j}/\alpha_{j}]$ is derivable in the system HMR. The
decidability then follows from the well–known fact that the theory
$FO(\mathbb{R},+,\times,\leq)$ admits quantifier elimination and is decidable
[Tar51, Gri88].

The algorithm to construct $\phi_{G}$ takes as input $G$ and proceeds as
follows:

  1. (1)

if $G$ is not a basic hypersequent (i.e., if it contains any complex formula
whose outermost connective is not $\Diamond$ or $1$ or $\overline{1}$), then
the algorithm returns

$\phi_{G}=\bigwedge^{n}_{i=1}\phi_{G_{i}}$

where $G_{1},\dots,G_{n}$ are the basic hypersequents obtained by iteratively
applying the logical rules, and $\phi_{G_{i}}$ is the formula recursively
computed by the algorithm on input $G_{i}$.

  2. (2)

if $G$ has the shape $\vdash$ then $\phi_{G}=\top$.

  3. (3)

if $G$ is a basic hypersequent which is not $\vdash$ then $G$ has the shape

$\vdash\Gamma_{1},\Diamond\Delta_{1},\vec{R^{\prime}}_{1}.1,\vec{S^{\prime}}_{1}.\overline{1}\mid\
...\mid\
\vdash\Gamma_{m},\Diamond\Delta_{m},\vec{R^{\prime}}_{m}.1,\vec{S^{\prime}}_{m}.\overline{1}$

where
$\Gamma_{i}=\vec{R}_{i,1}.x_{1},...,\vec{R}_{i,k}.x_{k},\vec{S}_{i,1}.\overline{x_{1}},...,\vec{S}_{i,k}.\overline{x_{k}}$.
For all $I\subsetneq[1...m]$, we define:

     * •

A formula $Z_{I}(\beta_{1},...,\beta_{m})$ that states that for all $i\in I$,
$\beta_{i}=0$.

$Z_{I}(\beta_{1},...,\beta_{m})=\bigwedge_{i\in I}(\beta_{i}=0)$

     * •

A formula $NZ_{I}(\beta_{1},...,\beta_{m})$ that states that for all $i\notin
I$, $0<\beta_{i}$.

$NZ_{I}(\beta_{1},...,\beta_{m})=\bigwedge_{i\notin
I}(0\leq\beta_{i})\wedge\neg(\beta_{i}=0)$

     * •

A formula $A_{I}(\beta_{1},...,\beta_{m})$ that states that all the atoms
cancel each other.

$A_{I}(\beta_{1},...,\beta_{m})=\bigwedge_{j=0}^{k}(\sum_{i=1}^{m}\beta_{i}\sum\vec{R}_{i,j}=\sum_{i=1}^{m}\beta_{i}\sum\vec{S}_{i,j})$

     * •

A formula $O_{I}(\beta_{1},...,\beta_{m})$ that states that there are more $1$
than $\overline{1}$,

$O_{I}(\beta_{1},...,\beta_{m})=\sum_{i=1}^{m}\beta_{i}\sum\vec{S^{\prime}}_{i}\leq\sum_{i=1}^{m}\beta_{i}\sum\vec{R^{\prime}}_{i}$

     * •

A hypersequent $H_{I}(\beta_{1},...,\beta_{m})$ which is the result of
cancelling the atoms using $\beta_{1},...,\beta_{m}$ and then using the
$\Diamond$ rule, i.e. is the leaf of the following prederivation:

$\vdash\Gamma_{k_{1}},\Diamond\Delta_{k_{1}},\vec{R^{\prime}}_{k_{1}}.1,\vec{S^{\prime}}_{k_{1}}.\overline{1}\mid\
...\mid\
\vdash\Gamma_{k_{l}},\Diamond\Delta_{k_{l}},\vec{R^{\prime}}_{k_{l}}.1,\vec{S^{\prime}}_{k_{l}}.\overline{1}\vdash\beta_{k_{1}}.\Gamma_{k_{1}},\beta_{k_{1}}.\Diamond\Delta_{k_{1}},(\beta_{k_{1}}\vec{R^{\prime}}_{k_{1}}).1,(\beta_{k_{1}}\vec{S^{\prime}}_{k_{1}}).\overline{1}\mid\
...\mid\
\vdash\beta_{k_{l}}.\Gamma_{k_{l}},\beta_{k_{l}}.\Diamond\Delta_{k_{l}},(\beta_{k_{l}}\vec{R^{\prime}}_{k_{l}}).1,(\beta_{k_{l}}\vec{S^{\prime}}_{k_{l}}).\overline{1}\vdash\beta_{k_{1}}.\Gamma_{k_{1}},\beta_{k_{1}}.\Diamond\Delta_{k_{1}},(\beta_{k_{1}}\vec{R^{\prime}}_{k_{1}}).1,(\beta_{k_{1}}\vec{S^{\prime}}_{k_{1}}).\overline{1},...,\beta_{k_{l}}.\Gamma_{k_{l}},\beta_{k_{l}}.\Diamond\Delta_{k_{l}},(\beta_{k_{l}}\vec{R^{\prime}}_{k_{l}}).1,(\beta_{k_{l}}\vec{S^{\prime}}_{k_{l}}).\overline{1}\vdash\beta_{k_{1}}.\Diamond\Delta_{k_{1}},(\beta_{k_{1}}\vec{R^{\prime}}_{k_{1}}).1,(\beta_{k_{1}}\vec{S^{\prime}}_{k_{1}}).\overline{1},...,\beta_{k_{l}}.\Diamond\Delta_{k_{l}},(\beta_{k_{l}}\vec{R^{\prime}}_{k_{l}}).1,(\beta_{k_{l}}\vec{S^{\prime}}_{k_{l}}).\overline{1}\vdash\beta_{k_{1}}.\Delta_{k_{1}},(\beta_{k_{1}}\vec{R^{\prime}}_{k_{1}}).1,(\beta_{k_{1}}\vec{S^{\prime}}_{k_{1}}).\overline{1},...,\beta_{k_{l}}.\Delta_{k_{l}},(\beta_{k_{l}}\vec{R^{\prime}}_{k_{l}}).1,(\beta_{k_{l}}\vec{S^{\prime}}_{k_{l}}).\overline{1}$

where $\\{k_{1},...,k_{l}\\}=[1..m]\backslash I$.

     * •

The formula $\phi_{H_{I}(\beta_{1},...,\beta_{m})}$ computed recursively from
$H_{I}(\beta_{1},...,\beta_{m})$ above.

     * •

A formula $\phi_{G,I}$ that corresponds to $\phi_{G^{\prime}}$ where
$G^{\prime}$ is the hypersequent obtained on using the W rule on all $i$-th
sequents for $i\in I$, i.e. the leaf of the following prederivation:

$\vdash\Gamma_{1},\Diamond\Delta_{1},\vec{R^{\prime}}_{1}.1,\vec{S^{\prime}}_{1}.\overline{1}\mid\
...\mid\
\vdash\Gamma_{m},\Diamond\Delta_{m},\vec{R^{\prime}}_{m}.1,\vec{S^{\prime}}_{m}.\overline{1}\vdash\Gamma_{k_{1}},\Diamond\Delta_{k_{1}},\vec{R^{\prime}}_{k_{1}}.1,\vec{S^{\prime}}_{k_{1}}.\overline{1}\mid\
...\mid\
\vdash\Gamma_{k_{l}},\Diamond\Delta_{k_{l}},\vec{R^{\prime}}_{k_{l}}.1,\vec{S^{\prime}}_{k_{l}}.\overline{1}$

with $\\{k_{1},...,k_{l}\\}=[1..m]\backslash I$. Then $\phi_{G,I}=$

$\exists\beta_{1},...,\beta_{m},Z_{I}(\beta_{1},...,\beta_{m})\wedge
NZ_{I}(\beta_{1},...,\beta_{m})\wedge A_{I}(\beta_{1},...,\beta_{m})\wedge
O_{I}(\beta_{1},...,\beta_{m})\wedge\phi_{H_{I}(\beta_{1},...,\beta_{m})}$

Finally, we return $\phi_{G}$ defined as follow:

$\phi_{G}=\bigvee_{I\subsetneq[1...m]}\phi_{G,I}$

The following theorem states the soundness of the above described algorithm.

######  Theorem 86.

Let $G$ be a hypersequent having polynomials
$R_{1},\dots,R_{k}\in\mathbb{R}[\vec{\alpha}]$ over scalar–variables
$\vec{\alpha}$. Let $\phi_{G}(\vec{\alpha})$ be the formula returned by the
algorithm described above on input $G$. Then, for all $\vec{s}\in\mathbb{R}$
such that for all $i\in[1..k],R_{i}(\vec{s})>0$, the following are equivalent:

  1. (1)

$\phi_{G}(\vec{s})$ holds in $\mathbb{R}$,

  2. (2)

$G[s_{j}/\alpha_{j}]$ is derivable in HMR.

######  Proof 4.26.

As in Theorem 47, by using the CAN–free invertibility Theorem 53, we can
assume that $G$ is a basic hypersequent. If $G$ has the shape $\vdash$, the
result is trivial. Otherwise, the result is a direct corollary of Lemma 88
below since the formula $NZ_{I}$ corresponds to the first property, the
formula $A_{I}$ corresponds to the second property, the formula $O_{I}$
corresponds to the third one and the formula $\phi_{H_{I}}$ corresponds to the
last one.

Even though the problem is decidable, the algorithm described previously is
non elementary since the size of the formula $\phi_{G}$ can not be bound by a
finite tower of exponentials.

######  Lemma 87.

We define by induction on $n$ the formula $A_{n}$ as follows:

  * •

$A_{0}=x$ for some variable $x$

  * •

$A_{n+1}=\Diamond A_{n}\sqcup\Diamond A_{n}$

For $i\in\mathbb{N}$, we define $G_{i}=\ \vdash 1.A_{i}$. Then for all $i$,
$\phi_{G_{i}}$ has at least $\underbrace{2^{2^{\iddots^{2}}}}_{i\text{
times}}$ existentials (with the convention
$\underbrace{2^{2^{\iddots^{2}}}}_{0\text{ times}}=1$).

######  Proof 4.27.

For $i,j,k\in\mathbb{N}$ and
$R_{1},...,R_{j}\in\mathbb{R}[\alpha_{1},...,\alpha_{k}]$, we define
$H_{i,j}(R_{1},...,R_{j})=\ \vdash R_{1}.A_{i},...,R_{j}.A_{i}$. We will show
by induction that for all $0<i$ and $0<j$, $\phi_{H_{i,j}}$ has at least
$\underbrace{2^{2^{\iddots^{2^{j}}}}}_{i\text{ times}}$ existentials..

For all $j\in\mathbb{N}_{>0}$, $k\in\mathbb{N}$ and
$R_{1},...,R_{j}\in\mathbb{R}[\alpha_{1},...,\alpha_{k}]$,
$H_{0,j}[R_{1},...,R_{j}]$ is an atomic hypersequent with only one sequent, so
$\phi_{H_{0,j}}$ has only one existential.

Let $j\in\mathbb{N}_{>0}$, $k\in\mathbb{N}$ and
$R_{1},...,R_{j}\in\mathbb{R}[\alpha_{1},...,\alpha_{k}]$. By applying
iteratively the logical rules on $H_{1,j}$, we obtain the basic hypersequent
$H^{b}=[\vdash R_{1}.\Diamond x,...,R_{j}.\Diamond x]^{2^{j}}$ and
$\phi_{H^{b}}$ has $(2^{2^{j}}-1)(2^{j}+1)$ existentials. So
$\phi_{H_{1,j}}(R_{1},...,R_{j})$ has $(2^{2^{j}}-1)(2^{j}+1)\geq 2^{j}$
existentials.

Let’s now analyse $\phi_{H_{i+1,j}}(R_{1},...,R_{j})$ for $i>0$. By applying
iteratively the logical rules, we obtain only one basic hypersequent :
$H^{b}_{i+1,j}(R_{1},...,R_{j})=\ [\vdash R_{1}.\Diamond
A_{i},...,R_{j}.\Diamond A_{i}]^{2^{j}}$. We notice that one of the subformula
of $\phi_{H^{b}_{i+1,j}}(R_{1},...,R_{j})$ is $\phi_{H_{i,j\times
2^{j}}}(\vec{R^{\prime}})$ for some
$\vec{R^{\prime}}\in(\mathbb{R}[\alpha_{1},....,\alpha_{k},\beta_{1},...,\beta_{2^{j}}])^{j\times
2^{j}}$, which has at least $\underbrace{2^{2^{\iddots^{2^{j\times
2^{j}}}}}}_{i\text{ times}}\geq\underbrace{2^{2^{\iddots^{2^{j}}}}}_{i+1\text{
times}}$ existentials. So $\phi_{H_{i+1,j}}(R_{1},...,R_{j})$ has at least
$\underbrace{2^{2^{\iddots^{2^{j}}}}}_{i+1\text{ times}}$ existentials.

Since $G_{i}=H_{i,1}(1)$, $G_{i}$ has at least
$\underbrace{2^{2^{\iddots^{2}}}}_{i\text{ times}}$ existentials.

The following result is similar to Lemma 70, the only difference is that since
the T rule can multiply a sequent by any strictly positive real number, the
coefficients in the property are real numbers instead of natural numbers.

######  Lemma 88.

For all basic hypersequents $G$, built using the variables and negated
variables $x_{1},\overline{x_{1}},\dots,x_{k},\overline{x_{k}}$, of the form

$\vdash\Gamma_{1},\Diamond\Delta_{1},\vec{r^{\prime}}_{1}.1,\vec{s^{\prime}}_{1}.\overline{1}\mid\
...\mid\
\vdash\Gamma_{m},\Diamond\Delta_{m},\vec{r^{\prime}}_{m}.1,\vec{s^{\prime}}_{m}.\overline{1}$

where
$\Gamma_{i}=\vec{r}_{i,1}.x_{1},...,\vec{r}_{i,k}.x_{k},\vec{s}_{i,1}.\overline{x_{1}},...,\vec{s}_{i,k}.\overline{x_{i,k}}$,
the following are equivalent:

  1. (1)

$G$ has a derivation.

  2. (2)

there exist numbers $t_{1},...,t_{m}\in\mathbb{R}_{\geq 0}$, one for each
sequent in $G$, such that:

     * •

there exists $i\in[1..m]$ such that $t_{i}\neq 0$, i.e., the numbers are not
all $0$’s, and

     * •

for every variable and covariable $(x_{j},\overline{x_{j}})$ pair, it holds
that

$\sum^{m}_{i=1}t_{i}(\sum\vec{r}_{i,j})=\sum^{m}_{i=1}t_{i}(\sum\vec{s}_{i,j})$

i.e., the scaled (by the numbers $t_{1}$ …$t_{m}$) sum of the coefficients in
front of the variable $x_{j}$ is equal to the scaled sum of the coefficients
in from of the covariable $\overline{x_{j}}$.

     * •

$\sum_{i=1}^{n}t_{i}\sum\vec{s^{\prime}}_{i}\leq\sum_{i=1}^{n}t_{i}\sum\vec{r^{\prime}}_{i}$,
i.e, there are more $1$ than $\overline{1}$ and,

     * •

the hypersequent consisting of only one sequent

$\vdash
t_{1}.\Delta_{1},...,t_{m}.\Delta_{m},(t_{1}\vec{r^{\prime}}_{1}).1,...,(t_{m}\vec{r^{\prime}}_{m}).1,(t_{1}\vec{s^{\prime}}_{1}).\overline{1},...,(t_{m}\vec{s^{\prime}}_{m}).\overline{1}$

has a derivation, where the notation $0.\Gamma$ means $\emptyset$.

######  Proof 4.28.

Similar to Lemma 46.

###  4.9. One open problem regarding HMR

We have not been able to prove or disprove the equivalent of Proposition 20 in
the context of the system HMR. We leave this as an open problem.

Question. Let $G$ be a hypersequent whose scalars are all rational numbers. Is
it true that, if $G$ has a CAN–free derivation in HMR then $G$ also has a
CAN–free and T–free derivation in HMR?

This is a question of practical importance. Indeed the T rule is the only
non–analytical rule (beside the CAN rule which, however, can be eliminated) of
the system HMR and, as a consequence, it makes the proof search endeavour more
difficult.

##  Appendix A GA system

For reference, the following table lists the rules of the hypersequent
calculus GA of [MOG05, MOG09] for the theory of lattice–ordered abelian
groups, which provides the basis of the systems HR and HMR introduced in this
paper.

Axioms: $\vdash$ $A\vdash A$ Structural rules: Logical rules:
$G|\Gamma,0\vdash\Delta G|\Gamma\vdash\Delta$
$G|\Gamma\vdash\Delta,0G|\Gamma\vdash\Delta$ $G|\Gamma,A+B\vdash\Delta
G|\Gamma,A,B\vdash\Delta$ $G|\Gamma\vdash\Delta,A+BG|\Gamma\vdash\Delta,A,B$
$G|\Gamma,-A\vdash\Delta G|\Gamma\vdash\Delta,A$
$G|\Gamma\vdash\Delta,-AG|\Gamma,A\vdash\Delta$ $G|\Gamma,A\sqcup
B\vdash\Delta\lx@proof@logical@and G|\Gamma,A\vdash\Delta
G|\Gamma,B\vdash\Delta$ $G|\Gamma\vdash\Delta,A\sqcup
BG|\Gamma\vdash\Delta,A|\Gamma\vdash\Delta,B$ $G|\Gamma,A\sqcap B\vdash\Delta
G|\Gamma,A\vdash\Delta|\Gamma,B\vdash\Delta$ $G|\Gamma\vdash\Delta,A\sqcap
B\lx@proof@logical@and G|\Gamma\vdash\Delta,AG|\Gamma\vdash\Delta,B$ CUT rule:
$G\mid\Gamma_{1},\Gamma_{2}\vdash\Delta_{1},\Delta_{2}\lx@proof@logical@and
G\mid\Gamma_{1}\vdash\Delta_{1},AG\mid\Gamma_{2},A\vdash\Delta_{2}$

Figure 9. Inference rules of the hypersequent system GA of [MOG05].

## References

  * [Avr87] A. Avron.  A constructive analysis of RM.  Journal of Symbolic Logic, 52(4):939–951, 1987.
  * [BCF03] Matthias Baaz, Agata Ciabattoni, and Christian G. Fermüller.  Hypersequent calculi for gödel logics - a survey.  J. Log. Comput., 13(6):835–861, 2003.
  * [BK08] Christel Baier and Joost Pieter Katoen.  Principles of Model Checking.  The MIT Press, 2008.
  * [Bus98] Samuel R. Buss.  Handbook of Proof Theory, chapter An Introduction to Proof Theory, pages 1–78.  Elsevier, 1998.
  * [CGT08] Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui.  From axioms to analytic rules in nonclassical logics.  In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 229–240. IEEE Computer Society, 2008.
  * [Cia01] Agata Ciabattoni.  Hypersequent calculi for some intermediate logics with bounded kripke models.  J. Log. Comput., 11(2):283–294, 2001.
  * [Cia18] Agata Ciabattoni.  Intermediate logics: From hypersequents to concurrent computation.  In Guram Bezhanishvili, Giovanna D’Agostino, George Metcalfe, and Thomas Studer, editors, Advances in Modal Logic 12, proceedings of the 12th conference on "Advances in Modal Logic," held in Bern, Switzerland, August 27-31, 2018, page 3. College Publications, 2018.
  * [CLR19] Agata Ciabattoni, Timo Lang, and Revantha Ramanayake.  Bounded sequent calculi for non-classical logics via hypersequents.  In Serenella Cerrito and Andrei Popescu, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings, volume 11714 of Lecture Notes in Computer Science, pages 94–110. Springer, 2019.
  * [FMM20] Robert Furber, Radu Mardare, and Matteo Mio.  Probabilistic logics based on Riesz spaces.  Logical Methods in Computer Science, Volume 16, Issue 1, 2020.
  * [FR75] Jeanne Ferrante and Charles Rackoff.  A decision procedure for the first order theory of real addition with order.  SIAM Journal on Computing, 4(1):69–76, 1975.
  * [Gen34] Gerhard Gentzen.  Untersuchungen über das logische schließen.  Mathematische Zeitschrift, 39:405–431, 1934.
  * [Gri88] D. Yu Grigor’ev.  Complexity of deciding tarski algebra.  Journal of Symbolic Computation, 5(1):65 – 108, 1988.
  * [JR77] E. De Jonge and A.C.M. Van Rooij.  Introduction to Riesz Spaces, volume 78.  Mathematical Centre Tracts, Amsterdam, 1977.
  * [Koz81] Dexter Kozen.  Semantics of probabilistic programs.  Journal of Computer and System Sciences, 1981.
  * [Koz83] Dexter Kozen.  Results on the propositional mu-calculus.  In Theoretical Computer Science, pages 333–354, 1983.
  * [Koz85] Dexter Kozen.  A probabilistic PDL.  Journal of Computer and System Sciences, 30(2):162–178, 1985.
  * [KPS13] Agnieszka Kulacka, Dirk Pattinson, and Lutz Schröder.  Syntactic labelled tableaux for lukasiewicz fuzzy ALC.  In Francesca Rossi, editor, IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, pages 962–968. IJCAI/AAAI, 2013.
  * [Lah13] Ori Lahav.  From frame properties to hypersequent rules in modal logics.  In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 408–417. IEEE Computer Society, 2013.
  * [LM19] Christophe Lucas and Matteo Mio.  Towards a structural proof theory of probabilistic mu-calculi.  In Mikolaj Bojanczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures, Prague, Czech Republic, volume 11425 of Lecture Notes in Computer Science, pages 418–435. Springer, 2019\.
  * [Luc20] Christophe Lucas.  A complete Coq formalisation of this article is available at: https://doi.org/10.5281/zenodo.4430858.  Technical report, ENS–Lyon, 2020.
  * [LvA07] C. C. A. Labuschagne and C. J. van Alten.  On the variety of Riesz spaces.  Indagationes Mathematicae, 18(1), 2007.
  * [LZ71] W. A. J. Luxemburg and A. C. Zaanen.  Riesz Spaces, volume 1.  North-Holland Mathematical Library, 1971.
  * [MFM17] Matteo Mio, Robert Furber, and Radu Mardare.  Riesz modal logic for Markov processes.  In 32nd ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–12. IEEE, 2017.
  * [Mio11] Matteo Mio.  Probabilistic modal _$\mu$_ -calculus with independent product.  In Prof. of 14th FOSSACS, volume 6604 of Lecture Notes in Computer Science, pages 290–304. Springer, 2011.
  * [Mio12a] Matteo Mio.  On the equivalence of denotational and game semantics for the probabilistic $\mu$-calculus.  Logical Methods in Computer Science, 8(2), 2012.
  * [Mio12b] Matteo Mio.  Probabilistic Modal $\mu$-Calculus with Independent product.  Logical Methods in Computer Science, 8(4), 2012.
  * [Mio14] Matteo Mio.  Upper-Expectation bisimilarity and Lukasiewicz $\mu$-Calculus.  In Proc. of FoSSaCS, volume 8412 of Lecture Notes in Computer Science, pages 335–350. Elsevier, 2014.
  * [Mio18] Matteo Mio.  Riesz modal logic with threshold operators.  In 33rd ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 710–719. ACM, 2018.
  * [MOG05] George Metcalfe, Nicola Olivetti, and Dov M. Gabbay.  Sequent and hypersequent calculi for abelian and Łukasiewicz logics.  ACM Transactions on Computational Logic, 6(3):578–613, 2005.
  * [MOG09] George Metcalfe, Nicola Olivetti, and Dov M. Gabbay.  Proof Theory for Fuzzy Logics, volume 36 of Applied Logic Series.  Springer Netherlands, 2009.
  * [MS13a] Matteo Mio and Alex Simpson.  Łukasiewicz mu-calculus.  In Proceedings Workshop on Fixed Points in Computer Science, FICS, volume 126 of EPTCS, pages 87–104, 2013.
  * [MS13b] Matteo Mio and Alex Simpson.  A proof system for compositional verification of probabilistic concurrent processes.  In Proc. of 16th FOSSACS, volume 7794 of LNCS, pages 161–176. Springer, 2013.
  * [MS17] Matteo Mio and Alex Simpson.  Łukasiewicz $\mu$-calculus.  Fundamenta Informaticae, 150(3-4):317–346, 2017.
  * [Pot83] G. Pottinger.  Uniform, cut–free formulations of T, S4 and S5 (abstract).  Journal of Symbolic Logic, 48(3):898–910, 1983.
  * [Tar51] Alfred Tarski.  A decision method for elementary algebra and geometry.  Quantifier Elimination and Cylindrical Algebraic Decomposition, 1951\.