text:
\section{Hypersequent calculi}
\label{sec:def hyp calc}

In order to define our calculi, we extend the structure of sequents in
two ways.  Firstly, sequents can contain so-called \emph{blocks of
  formulas} in addition to formulas of $\lan$.  Secondly, we use {\em
  hypersequents} rather than simple sequents.

\begin{definition}
  A \emph{block} \index{block} is a structure $\str\Sigma$, where
  $\Sigma$ is a finite multiset of formulas of $\lan$.  A
  \emph{sequent} is a pair $\G\seq \D$, where $\G$ is a finite
  multiset of formulas and blocks, and $\D$ is a finite multiset of
  formulas.  A \emph{hypersequent} is a finite multiset of sequents,
  and is written
  \begin{center}
    $\G_1 \seq \D_1 \hyp \ldots \hyp \G_n \seq \D_n$.
  \end{center}
  Given a hypersequent
  $\hH = \G_1 \seq \D_1 \hyp \ldots \hyp \G_n \seq \D_n$, we call
  \emph{components} of $\hH$ the sequents
  $\G_i \seq \D_i,\;1\leq i\leq n$.
\end{definition}

Observe that blocks can occur only in the antecedent of sequents and
not in their succedent.  Both blocks and sequents, but not
hypersequents, can be interpreted as formulas of $\lan$.  The
\emph{formula interpretation} of sequents is as follows:
\begin{center}
  $\fint(A_1, \ldots, A_n, \str\Sigma_1, \ldots, \str\Sigma_m \seq B_1, \ldots, B_k) =
  A_1 \land \ldots \land A_n \land \Box\AND \Sigma_1 \land \ldots \land \Box\AND\Sigma_m  \to
  B_1 \lor \ldots \lor B_k$.
\end{center}
By contrast, there is no formula interpretation for hypersequents in
$\lan$.  The reason is that non-normal modalities are not \emph{strong
  enough} to express the structural connective ``$\hyp$'' of
hypersequents: Intuitively, every component of a hypersequent
corresponds to a world in a model, and all worlds of a model are
potentially relevant for calculating the truth set of a formula, so we
would need a global modality to express the hypersequent structure.

The semantic interpretation of sequents and hypersequents is as
follows.

\begin{definition}
  We say that a sequent $S$ is \emph{valid} in a possible-worlds model
  $\M$ (written $\M\models S$) if for every world $w$ of $\M$,
  $\M, w\Vd \fint(S)$.  We say that a hypersequent $H$ is \emph{valid}
  in $\M$ if for some component $S$ of $\hH$, $\M \models S$.
  Finally, we say that an inference rule $\varR$ is \emph{sound} with
  respect to a model $\M$ (resp.~a class of models $\C$) if in case
  all premisses of $\varR$ are valid in $\M$ (resp.~$\C$), then the
  conclusion of $\varR$ is also valid in $\M$ (resp.~$\C$).
\end{definition}

\begin{figure}
\noindent
\fbox{\begin{minipage}{\textwidth}
\begin{small}
\vspace{0.1cm}

\noindent
\textbf{Propositional rules}

\vspace{0.3cm}
\noindent
\ax{}
\llab{\init}
\uinf{$\hG \hyp \G, p \seq p, \D$}
\disp
\hfill
\ax{}
\llab{\lbot}
\uinf{$\hG \hyp \G, \bot \seq \D$}
\disp
\hfill
\ax{}
\llab{\rtop}
\uinf{$\hG \hyp \G \seq \top, \D$}
\disp

\vspace{0.4cm}
\noindent
\resizebox{\textwidth}{!}{
\ax{$\hG \hyp \G, A \to B \seq A, \D$}
\ax{$\hG \hyp \G, A \to B, B \seq \D$}
\llab{\lto}
\binf{$\hG \hyp \G,  A \to B \seq \D$}
\disp
\hfill
\ax{$\hG \hyp \G, A \seq B, A\to B, \D$}
\llab{\rto}
\uinf{$\hG \hyp \G \seq  A \to B, \D$}
\disp}

\vspace{0.4cm}
\noindent
\ax{$\hG \hyp \G, A \land B, A, B \seq \D$}
\llab{\lland}
\uinf{$\hG \hyp \G, A \land B \seq \D$}
\disp
\hfill
\ax{$\hG \hyp \G \seq A, A \land B, \D$}
\ax{$\hG \hyp \G \seq B, A \land B, \D$}
\llab{\rland}
\binf{$\hG \hyp \G \seq A \land B, \D$}
\disp

\vspace{0.4cm}
\noindent
\ax{$\hG \hyp \G, A \lor B, A \seq \D$}
\ax{$\hG \hyp \G, A \lor B, B \seq \D$}
\llab{\llor}
\binf{$\hG \hyp \G, A \lor B \seq \D$}
\disp
\hfill
\ax{$\hG \hyp \G \seq A, B, A \lor B, \D$}
\llab{\rlor}
\uinf{$\hG \hyp \G \seq A \lor B, \D$}
\disp

\vspace{0.5cm}
\noindent
\textbf{Modal rules for the classical cube}

\vspace{0.4cm}
\noindent
\ax{$\hG \hyp \G, \Box A, \str A \seq \D$}
\llab{\lbox}
\uinf{$\hG \hyp \G, \Box A \seq \D$}
\disp
\hfill
\ax{$\hG \hyp \G, \langle\Sigma\rangle \seq  \Box B, \D \hyp \Sigma \seq B$}
\llab{\rboxm}
\uinf{$\hG \hyp \G, \langle\Sigma\rangle \seq \Box B, \D$}
\disp

\vspace{0.4cm}
\noindent
\ax{$\hG \hyp \G, \langle\Sigma\rangle \seq \Box B, \D \hyp \Sigma \seq B$}
\ax{$\{  \hG \hyp \G,  \langle\Sigma\rangle \seq \Box B, \D \hyp B \seq A  \}_{A\in\Sigma}$}
\llab{\rbox}
\binf{$\hG \hyp \G,  \langle\Sigma\rangle \seq \Box B, \D$}
\disp

\vspace{0.4cm}
\noindent
\ax{$\hG \hyp \G, \langle \top\rangle \seq \D$}
\llab{\rulen}
\uinf{$\hG \hyp \G \seq \D$}
\disp
\hfill
\ax{$\hG \hyp \G, \langle\Sigma\rangle, \langle\Pi\rangle,  \langle\Sigma,\Pi\rangle \seq \D$}
\llab{\rulec}
\uinf{$\hG \hyp \G, \langle\Sigma\rangle, \langle\Pi\rangle \seq \D$}
\disp

\vspace{0.5cm}
\noindent
\textbf{Modal rules for extensions}

\vspace{0.4cm}
\noindent
\ax{$\hG \hyp \G, \str\Sigma, \Sigma \seq \D$}
\llab{\rulet}
\uinf{$\hG \hyp \G, \str\Sigma \seq \D$}
\disp
\hfill
\ax{$\hG \hyp \G, \str\Sigma \seq \D \hyp \Sigma \seq$}
\llab{\rulep}
\uinf{$\hG \hyp \G, \str\Sigma \seq \D$}
\disp

\vspace{0.4cm}
\noindent
\ax{$\hG \hyp \G, \str{\Sigma_1}, \ldots, \str{\Sigma_n} \seq \D \hyp \Sigma_1, \ldots, \Sigma_n \seq$}
\llab{\rulednplus}
\uinf{$\hG \hyp \G, \str{\Sigma_1}, \ldots, \str{\Sigma_n} \seq \D$}
\disp

\vspace{0.4cm}
\noindent
\ax{$\hG \hyp \G, \str\Sigma, \str\Pi \seq \D \hyp \Sigma, \Pi \seq$}
\ax{$\{ \hG \hyp \G,  \str\Sigma, \str\Pi \seq \D \hyp \ \seq A, B\}_{A\in\Sigma, B\in\Pi}$}
\llab{\ruled}
\binf{$\hG \hyp \G, \str\Sigma, \str\Pi \seq \D$}
\disp

\vspace{0.4cm}
\noindent
\ax{$\hG \hyp \G, \str\Sigma \seq \D \hyp \Sigma \seq$}
\ax{$\{ \hG \hyp \G,  \str\Sigma \seq \D \hyp \ \seq A\}_{A\in\Sigma}$}
\llab{\ruledaux}
\binf{$\hG \hyp \G, \str\Sigma \seq \D$}
\disp

\end{small}
\end{minipage}}
\caption{\label{fig:hypersequent rules} Rules of the hypersequent calculi $\HEstar$.}
\end{figure}

For every logic $\Estar$, the corresponding hypersequent calculus
$\HEstar$ is defined by a subset of the rules in
Figure~\ref{fig:hypersequent rules}, as summarised in
Table~\ref{tab:hyp calculi}.

\begin{table}[t]
\centering
\begin{tabular}{l l l}
$\hypcalc\E$ := \{propositional rules, \lbox, \rbox\}.
&
$\hypcalc\EM$ := \{propositional rules, \lbox, \rboxm\}.
\\

$\hypcalc\ENstar$ := $\hypcalc\Estar$ $\cup$ \{\rulen\}.
&
$\hypcalc\EMNstar$ := $\hypcalc\EMstar$ $\cup$ \{\rulen\}.
\\

$\hypcalc\ECstar$ := $\hypcalc\Estar$ $\cup$ \{\rulec\}.
&
$\hypcalc\EMCstar$ := $\hypcalc\EMstar$ $\cup$ \{\rulec\}.
\\

$\hypcalc\ETstar$ := $\hypcalc\Estar$ $\cup$ \{\rulet\}.
&
$\hypcalc\EMTstar$  := $\hypcalc\EMstar$ $\cup$ \{\rulet\}.
\\

$\hypcalc\EPstar$ := $\hypcalc\Estar$ $\cup$ \{\rulep\}.
&
$\hypcalc\EMPstar$ := $\hypcalc\EMstar$ $\cup$ \{\rulep\}.
\\

$\hypcalc\EDstar$ := $\hypcalc\Estar$ $\cup$ \{\ruledaux, \ruled\}.
&
$\hypcalc\EMDstar$  := $\hypcalc\EMstar$ $\cup$
\{\ruledoneplus, \ruledtwoplus\}.
\\

$\hypcalc\EDnplusstar$ := $\hypcalc\Estar$ $\cup$
\{\rulediplus $\mid$ $1 \leq i \leq n$\}.
&
$\hypcalc\EMDnplusstar$  := $\hypcalc\EMstar$ $\cup$
\{\rulediplus $\mid$ $1 \leq i \leq n$\}.
\\
\end{tabular}
\caption{\label{tab:hyp calculi} Hypersequent calculi $\HEstar$.}
\end{table}

The rules are given in their cumulative, or \emph{kleene'd}, versions,
\ie\ the principal formulas or blocks are copied to the premiss(es).
The propositional rules are just the hypersequent versions of kleene'd
rules of sequent calculi.

As mentioned in the introduction, the hypersequent structure \emph{is
  not needed } to obtain a sound and complete calculus for the logics
under investigation. Moreover, it can be checked that whenever a
hypersequent $\hH = \G_1 \seq \D_1 \hyp \ldots \hyp \G_n \seq \D_n$ is
derivable, then there is some component $\G_i \seq \D_i$ which is
derivable.

The choice of both the hypersequent structure and also of cumulative
rules is motivated by the possibility of \emph{directly} obtaining
countermodels of non-valid formulas.  In particular, the hypersequent
structure allows us to make all rules invertible.  In this respect,
observe that backward applications of rules \rbox, \rboxm, \rulep,
\ruledaux, \ruled, and \rulednplus\ create new components, but the
principal component in the conclusion is kept in the premiss in order
keep the possibility of potential alternative rule applications.

Similarly to propositional connectives, boxed formulas are handled by
separate left and right rules.  Observe that rule \rbox\ has multiple
premisses, but the number of the premisses is fixed by the cardinality
of the principal block $\str\Sigma$.  The rule \rboxm\ is a right rule
for $\Box$ which replaces \rbox\ in the definition of monotonic
calculi.  Apart from the distinction between monotonic and
non-monotonic calculi, the calculi are modular; in particular,
extensions of $\HE$ and $\hypcalc\EM$ do not require to modify the
basic rules for $\Box$, being defined by simply adding the rules
corresponding to the additional axioms.

Every axiom has a corresponding rule, with the only exceptions of
axiom \axD\ and rules \RDnplus: axiom \axD\ needs both \ruledaux\ and
\ruled\ in the non-monotonic case, whereas it needs \ruledoneplus\ and
\ruledtwoplus\ in the monotonic case.  Moreover, the rules \RDnplus\
need \ruledmplus\ for every $1 \leq m \leq n$.  These requirements
makes contraction admissible (see
Proposition~\ref{prop:adm-struct-rules} and
Section~\ref{sec:struct-prop}), and we could forego them by instead
adopting explicit contraction rules.  Finally, as we shall see in the
countermodel extraction (see Section~\ref{sec:countermodels hyp}), the
rule \ruledaux\ is the syntactic counterpart of the property
$(\0,\0)\notin\N(w)$, which is satified by every \bin\ \cD-model.

Blocks have a central role in all modal rules.  Modal rules
essentially state how to handle blocks.  Notice that the only rule
which expands blocks is \rulec, thus in absence of this rule the
blocks occurring in a proof for a single formula contain only one
formula.  The possibility of collecting formulas by means of blocks
allows us to avoid rules with $n$ principal boxed formulas, as are
common in standard sequent calculi (compare~\cite{Lellmann:2019}).  As
we shall see, blocks also allow for an easy computation of the \bin\
function for the definition of countermodels.

\begin{figure}
\begin{small}

\noindent
\begin{tabular}{l c}
\vspace{1.0cm}
(\RE) &
\ax{$A \seq B$}
\llab{\exwk}
\uinf{$\Box A, \str A \seq \Box B \hyp A \seq B$}
\ax{$B \seq A$}
\rlab{\exwk}
\uinf{$\Box A, \str A \seq \Box B \hyp B \seq A$}
\rlab{\rbox}
\binf{$\Box A, \str A \seq \Box B$}
\rlab{\lbox}
\uinf{$\Box A \seq \Box B$}
\disp \\

\vspace{1.0cm}
(\axM) &
\ax{$\Box (A\land B), \str{A \land B} \seq \Box A \hyp A\land B, A, B \seq A$}
\rlab{\lland}
\uinf{$\Box (A\land B), \str{A \land B} \seq \Box A \hyp A\land B \seq A$}
\rlab{\rboxm}
\uinf{$\Box (A\land B), \str{A \land B} \seq \Box A$}
\rlab{\lbox}
\uinf{$\Box (A\land B) \seq \Box A$}
\disp \\

\vspace{1.0cm}
(\axN) &
\ax{$\str\top \seq \Box \top \hyp \top\seq\top$}
\ax{$\str\top \seq \Box \top \hyp \top\seq\top$}
\rlab{\rbox}
\binf{$\str\top \seq \Box \top$}
\rlab{\rulen}
\uinf{$\seq \Box \top$}
\disp \\

(\axC) &
\ax{$\ldots,  \str{A,B} \seq \Box (A \land B) \hyp A, B \seq A\land  B$}
\ax{$\ldots \hyp A\land B \seq A$}
\ax{$\ldots \hyp A \land B \seq B$}
\rlab{\rbox}
\TrinaryInfC{$\Box A \land \Box B, \Box A, \Box B, \str A, \str B, \str{A,B} \seq \Box (A \land B)$}
\rlab{\rulec}
\uinf{$\Box A \land \Box B, \Box A, \Box B, \str A, \str B \seq \Box (A\land B)$}
\rlab{\lbox}
\uinf{$\Box A \land \Box B, \Box A, \Box B, \str A \seq \Box (A\land B)$}
\rlab{\lbox}
\uinf{$\Box A \land \Box B, \Box A, \Box B \seq \Box (A\land B)$}
\rlab{\lland}
\uinf{$\Box A \land \Box B \seq \Box (A\land B)$}
\disp
\end{tabular}

\vspace{1.0cm}

\begin{tabular}{l}
(\axT)\qquad
\ax{$\Box A, \str A, A \seq A$}
\rlab{\rulet}
\uinf{$\Box A, \str A \seq A$}
\rlab{\lbox}
\uinf{$\Box A \seq A$}
\disp
\qquad\qquad\qquad\qquad
(\axP)\qquad
\ax{$\Box \bot, \str\bot \seq \ \hyp \bot \seq $}
\rlab{\rulep}
\uinf{$\Box \bot, \str\bot \seq$}
\rlab{\lbox}
\uinf{$\Box \bot \seq$}
\disp
\end{tabular}

\vspace{1.0cm}

\resizebox{\textwidth}{!}{
\begin{tabular}{l}
\begin{large}(\axD)\end{large}
\ax{$\Box A \land \Box \neg A, \Box A, \Box \neg A, \str A, \str{\neg A} \seq \ \hyp A \seq A$}
\llab{\lneg}
\uinf{$\Box A \land \Box \neg A, \Box A, \Box \neg A, \str A, \str{\neg A} \seq \ \hyp A, \neg A \seq$}
\ax{$\Box A \land \Box \neg A, \Box A, \Box \neg A, \str A, \str{\neg A} \seq \ \hyp A \seq A$}
\rlab{\rneg}
\uinf{$\Box A \land \Box \neg A, \Box A, \Box \neg A, \str A, \str{\neg A} \seq \ \hyp \  \seq A, \neg A$}
\rlab{\ruled}
\binf{$\Box A \land \Box \neg A, \Box A, \Box \neg A, \str A, \str{\neg A} \seq$}
\rlab{\lbox}
\uinf{$\Box A \land \Box \neg A, \Box A, \Box \neg A, \str A \seq$}
\rlab{\lbox}
\uinf{$\Box A \land \Box \neg A, \Box A, \Box \neg A \seq$}
\rlab{\lland}
\uinf{$\Box A \land \Box \neg A \seq$}
\disp
\end{tabular}}

\vspace{1.0cm}

\begin{tabular}{l}
(\RDnplus)\qquad\qquad
\ax{$A_1, \ldots, A_n \seq$}
\rlab{\exwk}
\uinf{$\Box A_1 \land \ldots \land \Box A_n, \Box A_1, \ldots, \Box A_n, \str{A_1}, \ldots, \str{A_n} \seq \ \hyp A_1, \ldots, A_n \seq$}
\rlab{\rulednplus}
\uinf{$\Box A_1 \land \ldots \land \Box A_n, \Box A_1, \ldots, \Box A_n, \str{A_1}, \ldots, \str{A_n} \seq$}
\rlab{\lland\ $\times$ $n$}
\uinf{$\Box A_1 \land \ldots \land \Box A_n, \Box A_1, \ldots, \Box A_n \seq$}
\rlab{\lland\ $\times$ $n$}
\uinf{$\Box A_1 \land \ldots \land \Box A_n \seq$}
\disp
\end{tabular}
\end{small}
\caption{\label{fig:hypersequent derivations} Derivations of modal axioms and rules.}
\end{figure}

Derivations of modal axioms and rules are displayed in
Figure~\ref{fig:hypersequent derivations}. Note that the simulations
of the rules make use of the external weakening rule \exwk, which is
shown to be admissible in Prop.~\ref{prop:adm-struct-rules}.  In the
derivations we further implicitly make use of the following lemma,
which states that initial hypersequents can be generalised to
arbitrary formulas.

\begin{proposition}\label{prop:extended initial sequents hyp}
  $\hG \hyp \G, A \seq A, \D$ is derivable in $\HEstar$ for every
  $A, \G, \D, \hG$.
\end{proposition}

\begin{proof}
  By structural induction on $A$.  If $A = p, \bot, \top$, then
  $\hG \hyp \G, A \seq A, \D$ is an initial hypersequent, whence it is
  derivable.  If $A = B \land C$ we consider the following derivation

  \begin{center}
    \ax{$\hG \hyp \G, B \land C, B, C \seq B, B \land C, \D$}
    \ax{$\hG \hyp \G, B \land C, B, C \seq C, B \land C, \D$}
    \rlab{\rland}
    \binf{$\hG \hyp \G, B \land C, B, C \seq B \land C, \D$}
    \rlab{\lland}
    \uinf{$\hG \hyp \G, B \land C \seq B \land C, \D$}
    \disp
  \end{center}

  \noindent
  where the premisses are derivable by \ih.  The cases $A = B \lor C$
  or $A = B \land C$ are analogous.  If $A = \Box B$ we consider the
  following derivation

  \begin{center}
    \ax{$\hG \hyp \G,\Box B, \str B \seq \Box B, \D \hyp B \seq B$}
    \ax{$\hG \hyp \G,\Box B, \str B \seq \Box B, \D \hyp B \seq B$}
    \rlab{\rbox}
    \binf{$\hG \hyp \G,\Box B, \str B \seq \Box B, \D$}
    \rlab{\lbox}
    \uinf{$\hG \hyp \G,\Box B \seq \Box B, \D$}
    \disp
  \end{center}

  \noindent
  where the premisses are derivable by \ih.
\end{proof}

The hypersequent calculi are sound with respect to the corresponding
\bin\ models.

\begin{theorem}[Soundness]\label{th:soundness hyp}
  If $\hH$ is derivable in $\HEXstar$, then it is valid in all \cX-models.
\end{theorem}

\begin{proof}
  The initial hypersequents are clearly valid.  We show that all rules
  are sound with respect to the corresponding \bin\ models.  Since the
  proof is standard for propositional rules, we just consider the
  modal rules.

  (\lbox) Assume $\M \models \hG \hyp \G, \Box A, \str A \seq \D$.
  Then $\M\models\hG$, or $\M\models \G, \Box A, \str A \seq \D$.  In
  the first case we are done.  In the second case,
  $\M \models \fint(\G, \Box A, \str A \seq \D) = \fint(\G, \Box A,
  \Box A \seq \D)$, which is equivalent to
  $\fint(\G, \Box A \seq \D)$.

  (\rbox) Assume
  $\M \models \hG \hyp \G, \str \Sigma \seq \Box B, \D \hyp \Sigma
  \seq B$ and
  $\M \models \hG \hyp \G, \str\Sigma \seq \Box B, \D \hyp B \seq A$
  for all $A\in\Sigma$.  Then (i) $\M \models \hG$, or (ii)
  $\M \models \G, \str\Sigma \seq \Box B, \D$, or (iii)
  $\M \models \Sigma \seq B$ and $\M \models B \seq A$ for all
  $A\in\Sigma$.  If (i) or (ii) we are done.  If (iii), then
  $\M \models \AND\Sigma \to B$ and $\M \models B \to A$ for all
  $A\in\Sigma$, that is $\M \models \AND\Sigma \leftrightarrow B$.
  Since \RE\ is valid,
  $\M \models \Box\AND\Sigma \to \Box B = \fint(\str\Sigma \seq \Box
  B)$.  Thus $\M \models \fint(\G, \str \Sigma \seq \Box B, \D)$.

  (\rboxm) Analogous to \rbox, by considering that in \cM-models
  $\M\models \AND \Sigma \to B$ implies
  $\M\models \Box \AND \Sigma \to \Box B$.

  (\rulen) Suppose $\M$ is a \cN-model and assume
  $\M \models\hG \hyp \G, \str\top \seq \D$.  Then $\M\models\hG$, or
  $\M\models \G, \str\top \seq \D$.  In the first case we are done.
  In the second case, $\M\models \fint(\G, \str\top \seq \D)$, which
  is equivalent to $\Box \top \to \fint(\G \seq \D)$.  Since
  $\Box \top$ is valid in $\M$, $\M\models \G \seq \D$.

  (\rulec) Suppose $\M$ is a \cC-model and assume
  $\M \models \hG \hyp \G, \str\Sigma, \str\Pi, \str{\Sigma,\Pi} \seq
  \D$.  Then $\M \models \hG$ or
  $\M \models \G, \str\Sigma, \str\Pi, \str{\Sigma,\Pi} \seq \D$.  In
  the first case we are done.  In the second case,
  $\M \models \fint(\G, \str\Sigma, \str\Pi, \str{\Sigma,\Pi} \seq \D)
  = \fint(\G, \Box\AND\Sigma, \Box\AND\Pi,
  \Box(\AND\Sigma\land\AND\Pi) \seq \D)$.  This is equivalent to
  $\Box\AND\Sigma \land \Box\AND\Pi \land \Box(\AND\Sigma\land\AND\Pi)
  \to \fint(\G \seq \D)$, and since axiom \axC\ is valid in $\M$, this
  is equivalent to
  $\Box\AND\Sigma \land \Box\AND\Pi \to \fint(\G \seq \D)$.  Thus
  $\M \models \fint(\G, \str\Sigma, \str\Pi \seq \D)$.

  (\rulet) Suppose $\M$ is a \cT-model and assume
  $\M \models \hG \hyp \G, \str\Sigma, \Sigma \seq \D$.  Then
  $\M \models \hG$ or $\M \models \G, \str\Sigma, \Sigma \seq \D$.  In
  the first case we are done.  In the second case,
  $\M \models \fint(\G, \str\Sigma, \Sigma \seq \D) = \Box\AND\Sigma
  \land \AND\Sigma \to \fint(\G \seq \D)$.  Since axiom \axT\ is valid
  in $\M$, this is equivalent to
  $\Box\AND\Sigma \to \fint(\G \seq \D)$.  Then
  $\M \models \G, \str\Sigma \seq \D$.

  (\rulep) Suppose $\M$ is a \cP-model and assume
  $\M \models \hG \hyp \G, \str\Sigma \seq \D \hyp \Sigma \seq$.  Then
  (i) $\M\models \hG$, or (ii) $\M\models \G, \str\Sigma \seq \D$, or
  (iii) $\M \models \Sigma \seq$.  If (i) or (ii) we are done.  If
  (iii), then $\M \models \AND\Sigma \to \bot$.  and by the validity
  of axiom \axP,
  $\M \models \Box\AND\Sigma \to \bot = \fint(\str\Sigma \seq)$.  Then
  $\M\models \G, \str\Sigma \seq \D$.

  (\rulednplus) Suppose $\M$ is a \cRDnplus-model and assume
  $\M \models \hG \hyp \G, \str{\Sigma_1}, \ldots, \str{\Sigma_n} \seq
  \D \hyp \Sigma_1, \ldots, \Sigma_n \seq$.  Then (i) $\M\models \hG$,
  or (ii)
  $\M\models \G, \str{\Sigma_1}, \ldots, \str{\Sigma_n} \seq \D$, or
  (iii) $\M \models \Sigma_1, \ldots, \Sigma_n \seq$.  If (i) or (ii)
  we are done.  If (iii), then
  $\M \models \neg(\AND\Sigma_1 \land \ldots \land \AND\Sigma_n)$.
  And by the soundness of rule \RDnplus,
  $\M \models \neg(\Box\AND\Sigma_1 \land \ldots \land
  \Box\AND\Sigma_n) = \fint(\str{\Sigma_1}, \ldots, \str{\Sigma_n}
  \seq)$.  Then
  $\M\models \G, \str{\Sigma_1}, \ldots, \str{\Sigma_n} \seq \D$.

  (\ruled) Suppose $\M$ is a \cD-model and assume
  $\M \models \hG \hyp \G, \str\Sigma, \str\Pi \seq \D \hyp \Sigma,
  \Pi \seq$, and
  $\M \models \hG \hyp \G, \str\Sigma, \str\Pi \seq \D \hyp \ \seq A,
  B$ for all $A \in\Sigma, B \in\Pi$.  Then (i) $\M\models \hG$, or
  (ii) $\M\models \G, \str\Sigma, \str\Pi \seq \D$, or (iii)
  $\M \models \Sigma, \Pi \seq$ and $\M \models \ \seq A, B$ for all
  $A \in\Sigma, B \in\Pi$.  If (i) or (ii) we are done.  If (iii),
  then $\M \models \AND\Sigma \land \AND\Pi \to \bot$ and
  $\M \models A \lor B$ for all $A \in\Sigma, B \in\Pi$.  Thus
  $\M \models \AND\Sigma \leftrightarrow \neg \AND\Pi$.  By the
  soundness of axiom \axD,
  $\M \models \Box\AND\Sigma \land \Box\AND\Pi \to \bot =
  \fint(\str\Sigma, \str\Pi \seq)$.  Then
  $\M\models \G, \str\Sigma, \str\Pi \seq \D$.

  (\ruledaux) Assume
  $\M \models \hG \hyp \G, \str\Sigma \seq \D \hyp \Sigma \seq$, and
  $\M \models \hG \hyp \G, \str\Sigma \seq \D \hyp \ \seq A$ for all
  $A \in\Sigma$.  Then (i) $\M\models \hG$, or (ii)
  $\M\models \G, \str\Sigma \seq \D$, or (iii)
  $\M \models \Sigma \seq$ and $\M \models \ \seq A$ for all
  $A \in\Sigma$.  If (i) or (ii) we are done.  If (iii), then
  $\M \models \AND\Sigma \to \bot$ and $\M \models \AND\Sigma$, which
  is impossible.  Then (i) or (ii) holds.
\end{proof}

\subsection{Structural properties and syntactic completeness}
\label{sec:struct-prop}

We now investigate the structural properties of our calculi.  We first
show that weakening and contraction are height-preserving admissible,
both in their internal and in their external variants, and that all
rules are invertible.  We then prove that the cut rule is admissible,
which allows us to directly prove the completeness of the calculi with
respect to the corresponding axiomatisations.

\begin{definition}
  \label{def:weight hyp}
  The {\em weight} $\w$ of a formula is recursively defined as
  $\w(\bot) =\w(\top) = \w(p) = 0$; for
  $\circ\in\{\land, \lor, \to\}$, $\w(A \circ B) = \w(A) + \w(B) + 1$;
  $\w(\langle A_1, \ldots, A_n \rangle) = max\{\w(A_1), \ldots,
  \w(A_n)\} + 1$; $\w(\Box A) = \w(A) + 2$.

  The {\em height} of a derivation is the greatest number of
  successive applications of rules in it, where axioms have height
  $0$. A property is {\em height-preserving} if the height of
  derivations is an invariant.
\end{definition}

\begin{proposition}\label{prop:adm-struct-rules}
  The following structural rules are height-preserving admissible in
  $\HEstar$, where $\phi$ is any formula $A$ or block $\str\Sigma$.
  Moreover, all rules in $\HEstar$ are height-preserving invertible.

\begin{center}
\begin{small}
\begin{tabular}{lllll}
\vspace{0.3cm}
\ax{$\hG \hyp \G \seq \D $}
\llab{\hyplwk}
\uinf{$\hG \hyp \G, \phi \seq \D$}
\disp
&
\ax{$\hG \hyp \G \seq \D $}
\llab{\hyprwk}
\uinf{$\hG \hyp \G \seq A, \D$}
\disp
&
\ax{$\hG$}
\llab{\exwk}
\uinf{$\hG \hyp \G \seq \D$}
\disp
\\

\vspace{0.3cm}
\ax{$\hG \hyp  \G, \phi, \phi \seq \D $}
\llab{\hyplctr}
\uinf{$\hG \hyp \G, \phi \seq \D$}
\disp
&
\ax{$\hG \hyp \G \seq A, A, \D$}
\llab{\hyprctr}
\uinf{$\hG \hyp \G \seq A, \D$}
\disp
&
\ax{$\hG \hyp \G \seq \D \hyp \G \seq \D$}
\llab{\exctr}
\uinf{$\hG \hyp \G \seq \D$}
\disp
\\

\ax{$\hG \hyp  \G, \str{\Theta,A,A} \seq \D $}
\llab{\textsf{Sctr}}
\uinf{$\hG \hyp \G, \str{\Theta,A} \seq \D$}
\disp
&
\ax{$\hG \hyp  \G, \str{\Theta,A} \seq \D $}
\llab{\textsf{Smgl}}
\uinf{$\hG \hyp \G, \str{\Theta,A,A} \seq \D$}
\disp
\end{tabular}
\end{small}
\end{center}
\end{proposition}

\begin{proof}
  For each rule $\varR$, we prove that if the premise is derivable
  with height at most $n$, then the conclusion is also derivable with
  height at most $n$. The proof is by induction on the height of the
  derivation of the premise, highlighting that rules \hyplctr\ and
  \hyprctr\ are simultaneously proved admissible by mutual
  induction. Moreover, admissibility of \textsf{Sctr} and
  \textsf{Smgl} rely on height-preserving admissibility of contraction
  and weakening on formulae outside blocks, respectively.

  We will illustrate with the following cases
  \begin{itemize}
  \item Case \exctr\ + \rboxm. Suppose that
    \[
      \infer[\mbox{\rboxm}]{\hG \hyp \G, \str\Sigma \seq \Box B, \D \hyp \G, \str\Sigma \seq \Box B, \D}{
        \deduce{\hG \hyp \G, \str\Sigma \seq \Box B, \D \hyp \G, \str\Sigma \seq \Box B, \D \hyp \Sigma \seq B}{\pi}}
    \]
    where the height of $\pi$ is at most $n$.  By induction
    hypothesis, there is a proof $\pi'$, with height at most $n$, of
    $\hG \hyp \G, \str\Sigma \seq \Box B, \D \hyp \Sigma \seq
    B$. Hence
    \[
      \infer[\mbox{\rboxm}]{\hG \hyp \G, \str\Sigma \seq \Box B, \D}{\deduce{\hG \hyp  \G, \str\Sigma \seq \Box B, \D \hyp \Sigma \seq B}{\pi'}}
    \]
  \item Case \hyplctr\ + \ruled. Consider the derivation
    \[
      \infer[\mbox{\ruled}]{\hG \hyp \G, \str\Sigma, \str\Sigma \seq \D}
      {\deduce{\hG \hyp \G, \str\Sigma, \str\Sigma \seq \D \hyp \Sigma, \Sigma \seq}{\pi_1} & \deduce{\{ \hG \hyp \G,  \str\Sigma, \str\Sigma \seq \D \hyp \ \seq A, B\}_{A, B \in\Sigma}}{\pi_2^{A,B}}}
    \]
    where the heights of $\pi_1$ and $\pi_2^{A,B}$ are at most
    $n$. Observe that, in particular, there are proofs $\pi_2^{A,A}$
    of
    $\{\hG \hyp \G, \str\Sigma, \str\Sigma \seq \D \hyp \ \seq A,
    A\}_{A \in\Sigma}$.  By induction hypothesis, there are proofs
    $\pi_1',\pi_2^{A}$, with height at most $n$, of
    $\hG \hyp \G, \str\Sigma \seq \D \hyp \Sigma \seq$ and
    $\{ \hG \hyp \G, \str\Sigma \seq \D \hyp \ \seq A\}_{A
      \in\Sigma}$, respectively. Hence
    \[
      \infer[\mbox{\ruledaux}]{\hG \hyp \G,  \str\Sigma \seq \D}
      {\deduce{\hG \hyp \G, \str\Sigma \seq \D \hyp \Sigma \seq}{\pi_1} & \deduce{\{ \hG \hyp \G,  \str\Sigma \seq \D \hyp \ \seq A\}_{A \in\Sigma}}{\pi_2^{A}}}
    \]
  \end{itemize}

  Finally, note that since all rules are cumulative, height-preserving
  invertibility of all rules is an immediate consequence of
  height-preserving admissibility of weakening.  For instance,
  invertibility of rule \rboxm\ is proved as follows

  \begin{center}
    \ax{$\hG \hyp \G,  \langle\Sigma\rangle \seq \Box B, \D$}
    \rlab{\exwk}
    \uinf{$\hG \hyp \G, \langle\Sigma\rangle \seq \Box B, \D \hyp \Sigma \seq B$}
    \disp
  \end{center}
  \vspace{-0.3cm}
\end{proof}

We note that due to the fact that the \rbox\ rule isolates single
formulae from block in its right premiss, in the non-monotonic case
the full-blown weakening inside blocks is \emph{not}
admissible. However, the weaker rule of \emph{mingle} inside blocks
\textsf{Smgl} is.

The proof of admissibility of \hypcut\ is more intricate and deserves
more attention.  In the hypersequent framework, the \hypcut\ rule is
formulated as follows
\begin{center}
  \ax{$\hG \hyp \G \seq A, \D$}
  \ax{$\hG \hyp \G, A \seq \D$}
  \llab{\hypcut}
  \binf{$\hG \hyp \G \seq \D$}
  \disp
\end{center}
The admissibility of \hypcut\ is proved simultaneously with the
admissibility of the following rule \subrule{}, which states that a
formula $A$ inside one or more blocks can be replaced by any
equivalent multiset of formulas $\Sigma$
\begin{center}
  \ax{$\hG \hyp \Sigma \seq A$}
  \ax{$\{  \hG \hyp  A \seq B  \}_{B\in\Sigma}$}
  \ax{$\hG \hyp \G, \langle A^{n_1}, \Pi_1 \rangle, \ldots, \langle A^{n_k}, \Pi_k \rangle \seq \D$}
  \llab{\subrule}
  \TrinaryInfC{$\hG \hyp \G, \langle \Sigma^{n_1}, \Pi_1 \rangle, \ldots, \langle \Sigma^{n_k}, \Pi_k \rangle \seq \D$}
  \disp
\end{center}
where $A^{n_i}$ (resp.~$\Sigma^{n_i}$) is a compact way to denote
$n_i$ occurrences of $A$ (resp.~$\Sigma$).  In the monotonic case we
need to consider, instead of \subrule{}, the rule

\begin{center}
  \ax{$\hG \hyp \Sigma \seq A$}
  \ax{$\hG \hyp \G, \langle A^{n_1}, \Pi_1 \rangle, \ldots, \langle A^{n_k}, \Pi_k \rangle \seq \D$}
  \llab{\subrulem}
  \binf{$\hG \hyp \G, \langle \Sigma^{n_1}, \Pi_1 \rangle, \ldots, \langle \Sigma^{n_k}, \Pi_k \rangle \seq \D$}
  \disp
\end{center}

\begin{theorem}\label{thm:cut}
  If $\HEstar$ is non-monotonic, then the rules \hypcut{} and
  \subrule{} are admissible in $\HEstar$; otherwise \hypcut{} and
  \subrulem{} are admissible in $\HEstar$.
\end{theorem}

\begin{proof}
  We prove that \hypcut{} and \subrule{} are admissible in
  non-monotonic $\HEstar$; the proof in the monotonic case is
  analogous.  Recall that, for an application of \hypcut, the
  \emph{cut formula} is the formula which is deleted by that
  application, while the \emph{cut height} is the sum of the heights
  of the derivations of the premisses of \hypcut.  The theorem is a
  consequence of the following claims, where $Cut(c, h)$ means that
  all applications of \hypcut{} of height $h$ on a cut formula of
  weight $c$ are admissible, and $Sub(c)$ means that all applications
  of \subrule{} where the principal formula $A$ has weight $c$ are
  admissible (for any $\Sigma, \Pi_1, \ldots, \Pi_k$)
  \begin{itemize}
  \item \textbf{(A)}  $\forall c. Cut(c, 0)$.
  \item \textbf{(B)}  $\forall h. Cut(0, h)$.
  \item \textbf{(C)}  $\forall c. (\forall h. Cut(c, h) \to Sub(c))$.
  \item \textbf{(D)}  $\forall c. \forall h. ((\forall c'<c. (Sub(c') \land \forall h'. Cut(c', h')) \land \forall h''<h. Cut (c, h'') ) \to Cut(c, h))$.
  \end{itemize}
  \textbf{(A)} If the cut height is 0, then \hypcut\ is applied to
  initial hypersequents $\hG \hyp \G \seq A, \D$ and
  $\hG \hyp \G, A \seq \D$.  We show that the conclusion of \hypcut\
  $\hG \hyp \G \seq \D$ is an inital hypersequent, whence it is
  derivable without \hypcut.  If $\hG$ is an inital hypersequent we
  are done.  Otherwise $\G \seq A, \D$ and $\G, A \seq \D$ are initial
  sequents.  For the first sequent there are three possibilities: (i)
  $\G \seq \D$ is an initial sequent, or (ii) $A = \top$, or (iii)
  $A = p$ and $\G = \G', p$.  If (ii), then the second sequent is
  $\G, \top \seq \D$, which implies that $\G \seq \D$ is an initial
  sequent.  If (iii), then the second sequent is $\G', p, p \seq \D$.
  Then $\G' \seq \D$ is an initial sequent, or $\D = p, \D'$, which
  implies that $\G', p \seq p, \D' = \G \seq \D$ is an initial
  sequent.

  \bigskip \textbf{(B)} If the cut formula has weight $0$, then it is
  $\bot$, $\top$, or a propositional variable $p$.  For all three
  possibilities the proof is by complete induction on $h$. The basic
  case $h=0$ is a particular case of \textbf{(A)}.  For the inductive
  step, we distinguish three cases.

  (i) The cut formula $\bot$, $\top$, or $p$ is not principal in the
  last rule applied in the derivation of the left premiss.  By
  examining all possible rule applications, we show that the
  application of \hypcut{} can be replaced by one or more applications
  of \hypcut{} at a smaller height.  For instance, assume that the
  last rule applied is \lbox.

  \begin{center}
    \ax{$\hG \hyp \angA, \Box A, \G \seq \D, \bot$}
    \llab{\lbox}
    \uinf{$\hG \hyp \Box A,  \G \seq \D, \bot$}
    \ax{$\hG \hyp \bot, \Box A, \G \seq \D$}
    \rlab{\hypcut}
    \binf{$\hG \hyp \Box A, \G \seq \D$}
    \disp
  \end{center}
  The derivation is transformed as follows, with a \hp\ application of
  \hyplwk{} and an application of \hypcut{} of smaller height.
  \begin{center}
    \ax{$\hG \hyp \angA, \Box A, \G \seq \D, \bot$}
    \ax{$\hG \hyp \bot, \Box A, \G \seq \D$}
    \rlab{\hyplwk}
    \uinf{$\hG \hyp \bot, \angA, \Box A, \G \seq \D$}
    \rlab{\hypcut}
    \binf{$\hG  \hyp \angA, \Box A, \G \seq \D$}
    \rlab{\lbox}
    \uinf{$\hG  \hyp \Box A, \G \seq \D$}
    \disp
  \end{center}
  The situation is similar if the last rule in the derivation of the
  left premiss is applied to some sequent in $\hG$.

  (ii) The cut formula $\bot$, $\top$, or $p$ is not principal in the
  last rule applied in the derivation of the right premiss.  The case
  is analogous to (i).  As an example, suppose that the last rule
  applied is \rboxm{}.

  \begin{center}
    \ax{$\hG \hyp \angSigma, \G \seq \D, \Box B, \bot$}
    \ax{$\hG \hyp \bot, \angSigma, \G \seq \D, \Box B \hyp \Sigma \seq B$}
    \rlab{\rboxm}
    \uinf{$\hG \hyp \bot, \angSigma, \G \seq \D, \Box B$}
    \rlab{\hypcut}
    \binf{$\hG \hyp \angSigma, \G \seq \D, \Box B$}
    \disp
  \end{center}

  The derivation is converted into

  \begin{center}
    \ax{$\hG \hyp \angSigma, \G \seq \D, \Box B, \bot$}
    \llab{\exwk}
    \uinf{$\hG \hyp \angSigma, \G \seq \D, \Box B, \bot \hyp \Sigma \seq B$}
    \ax{$\hG \hyp \bot, \angSigma, \G \seq \D, \Box B \hyp \Sigma \seq B$}
    \rlab{\hypcut}
    \binf{$\hG \hyp \angSigma, \G \seq \D, \Box B \hyp \Sigma \seq B$}
    \rlab{\rboxm}
    \uinf{$\hG \hyp \angSigma, \G \seq \D, \Box B$}
    \disp
  \end{center}
  where \hypcut{} is applied at a smaller height.

  (iii) The cut formula $\bot$, $\top$, or $p$ is principal in the
  last rule applied in the derivation of both premisses.  Then the cut
  formula is $p$, as $\bot$ (resp.~$\top$) is never principal on the
  right-hand side (resp.~the left-hand side) of the conclusion of any
  rule application.  This means that both premisses are derived by
  \init, which implies that $h=0$.  Then we are back to case
  \textbf{(A)}.

  \bigskip \textbf{(C)} Assume $\forall h Cut(c,h)$.  We prove that
  all applications of \subrule\ where $A$ has weight $c$ are
  admissible.  The proof is by induction on the height $m$ of the
  derivation of
  $\hG \hyp \langle A^{n_1}, \Pi_1 \rangle, \ldots, \langle A^{n_k},
  \Pi_k \rangle, \G \seq \D$.  If $m = 0$ or no block among
  $\langle A, \Pi_1 \rangle, \ldots, \langle A, \Pi_k \rangle$ is
  principal in the last rule application, then the proof proceeds
  similarly to previous cases.  If $m>0$ and at least one block among
  $\langle A, \Pi_1 \rangle, \ldots, \langle A, \Pi_k \rangle$ is
  principal in the last rule application we have the following
  possibilities.

  $\bullet$ The last rule applied is \rbox:

\begin{center}
  \resizebox{\textwidth}{!}{ \ax{\textcircled{\footnotesize{1}}}
    \noLine
    \uinf{$\hG \hyp \langle A^{n_i}, \Pi_i \rangle, \G \seq \D, \Box D
      \hyp A^{n_i}, \Pi_i \seq D$}
    \ax{$\qquad \quad \ \{ \hG \hyp \langle A^{n_i}, \Pi_i \rangle, \G
      \seq \D, \Box D \hyp D \seq C \}_{C\in\Pi_i}$} \noLine
    \uinf{$\{ \hG \hyp \langle A^{n_i}, \Pi_i \rangle, \G \seq \D,
      \Box D \hyp D \seq A \}_1^{n_i}$ \quad $\vdots$} \rlab{\rbox}
    \BinaryInfC{$\hG \hyp \langle A^{n_i}, \Pi_i \rangle, \G \seq \D,
      \Box D$} \disp }
\end{center}

The derivation is converted as follows.  First we derive:

\begin{center}
  \vspace{0.2cm}
  \noindent
\resizebox{\textwidth}{!}{
\ax{$\hG \hyp \Sigma \seq A$}
\rlab{\exwk}
\uinf{$\hG \hyp \Sigma \seq A \hyp A^{n_i}, \Pi_i \seq D$}
\ax{$\hG \hyp A \seq B$}
\llab{$\Big\{$}
\rlab{\exwk $\Big\}_{B\in\Sigma}$}
\uinf{$\hG \hyp A \seq B \hyp A^{n_i}, \Pi_i \seq D$}
\ax{\textcircled{\footnotesize{1}}}
\rlab{\subrule}
\TrinaryInfC{$\hG \hyp \langle \Sigma^{n_i}, \Pi_i \rangle, \G \seq \D, \Box D \hyp A^{n_i}, \Pi_i \seq D$}
\disp}
\end{center}

\noindent
(where rule \subrule\ possibly applies to further blocks inside $\G$).
Then by applying \exwk{} to $\hG \hyp \Sigma \seq A$ we obtain
$\hG \hyp \langle \Sigma^{n_i}, \Pi_i \rangle, \G \seq \D, \Box D \hyp
\Sigma \seq A$.  By auxiliary applications of \wk{} we can cut $A$ and
get
$\hG \hyp \langle \Sigma^{n_i}, \Pi_i \rangle, \G \seq \D, \Box D \hyp
\Sigma, A^{n_i - 1}, \Pi_i \seq D$.  Then with further applications of
cut (each time with auxiliary applications of \wk{}) we obtain
$\hG \hyp \langle \Sigma^{n_i}, \Pi_i \rangle, \G \seq \D, \Box D \hyp
\Sigma^{n_i}, \Pi_i \seq D.$ By doing the same with the other
premisses of \rbox{} in the initial derivation we obtain also
$\{ \{ \hG \hyp \langle \Sigma^{n_i}, \Pi_i \rangle, \G \seq \D, \Box
D \hyp D \seq B \}_{B\in\Sigma} \}_1^{n_1}$ and
$\{ \hG \hyp \langle \Sigma^{n_i}, \Pi_i \rangle, \G \seq \D, \Box D
\hyp D \seq C \}_{C\in\Pi_i}.$ Finally by \rbox{} we derive the
conclusion of \subrule{}
$\hG \hyp \langle \Sigma^{n_i}, \Pi_i \rangle, \G \seq \D, \Box D.$

$\bullet$ The last rule applied is \rulec:

\begin{center}
\ax{$\hG \hyp \langle A^{n_i}, \Pi_i \rangle, \langle A^{n_j}, \Pi_j  \rangle, \langle A^{n_i}, A^{n_j}, \Pi_i, \Pi_j  \rangle, \G \seq \D$}
\rlab{\rulec}
\uinf{$\hG \hyp \langle A^{n_i}, \Pi_i \rangle, \langle A^{n_j}, \Pi_j \rangle,  \G \seq \D$}
\disp
\end{center}

\noindent
By applying \subrule\
to the premiss we obtain\\
$\hG \hyp \langle \Sigma^{n_i}, \Pi_i \rangle, \langle \Sigma^{n_j},
\Pi_j \rangle, \langle \Sigma^{n_i}, \Sigma^{n_j}, \Pi_i, \Pi_j,
\rangle, \G \seq \D$,
then by \rulec\ we derive\\
$\hG \hyp \langle \Sigma^{n_i}, \Pi_i \rangle, \langle \Sigma^{n_j},
\Pi_j \rangle, \G \seq \D$.

$\bullet$ The last rule applied is \rulet:

\begin{center}
\ax{$\hG \hyp A^{n_i}, \Pi_i, \str{A^{n_i}, \Pi_i}, \G \seq \D$}
\rlab{\rulet}
\uinf{$\hG \hyp \str{A^{n_i}, \Pi_i}, \G \seq \D$}
\disp
\end{center}
By applying the inductive hypothesis to the premiss we obtain\\
$\hG \hyp A^{n_i}, \Pi_i, \str{\Sigma^{n_i}, \Pi_i}, \G \seq \D$.
Then, from this and $\hG \hyp \Sigma \seq A$,
by several applications of \hypcut{}
(each time with auxiliary applications of \wk{})
we obtain
$\hG \hyp \Sigma^{n_i}, \Pi_i, \str{\Sigma^{n_i}, \Pi_i}, \G \seq \D$.
Finally, by \rulet{} we derive
$\hG \hyp \str{\Sigma^{n_i}, \Pi_i}, \G \seq \D$.

$\bullet$ The last rule applied is \rulep:

\begin{center}
\ax{$\hG \hyp \str{A^{n_i}, \Pi_i}, \G \seq \D \hyp A^{n_i}, \Pi_i \seq$}
\rlab{\rulep}
\uinf{$\hG \hyp \str{A^{n_i}, \Pi_i}, \G \seq \D$}
\disp
\end{center}
By applying the inductive hypothesis to the premiss (after auxiliary
applications of \exwk{} to the other premisses of \subrule) we obtain
$\hG \hyp \str{\Sigma^{n_i}, \Pi_i}, \G \seq \D \hyp A^{n_i}, \Pi_i
\seq$.  Then, from this and $\hG \hyp \Sigma \seq A$, by several
applications of \hypcut{} (each time with auxiliary applications of
\wk{}) we obtain
$\hG \hyp \str{\Sigma^{n_i}, \Pi_i}, \G \seq \D \hyp \Sigma^{n_i},
\Pi_i \seq$.  Finally, by \rulep{} we derive
$\hG \hyp \str{\Sigma^{n_i}, \Pi_i}, \G \seq \D$.

$\bullet$ The last rule applied is \ruled:
Then $\hG \hyp \langle A^{n_i}, \Pi_i \rangle, \langle A^{n_j}, \Pi_j \rangle,  \G \seq \D$
has been derived by the following premisses.
$\hG \hyp \langle A^{n_i}, \Pi_i \rangle, \langle A^{n_j}, \Pi_j \rangle,  \G \seq \D \hyp A^{n_i}, A^{n_j}, \Pi_i, \Pi_j \seq $;
$\{\hG \hyp \langle A^{n_i}, \Pi_i \rangle, \langle A^{n_j}, \Pi_j \rangle,  \G \seq \D \hyp \seq A,A\}_1^{n_i+n_j}$;
$\{\{\hG \hyp \langle A^{n_i}, \Pi_i \rangle, \langle A^{n_j}, \Pi_j \rangle,  \G \seq \D \hyp \seq A,C\}_{C\in\Pi_i}\}_1^{n_j}$;
$\{\{\hG \hyp \langle A^{n_i}, \Pi_i \rangle, \langle A^{n_j}, \Pi_j \rangle,  \G \seq \D \hyp \seq A,D\}_{D\in\Pi_j}\}_1^{n_i}$;
and
$\{\hG \hyp \langle A^{n_i}, \Pi_i \rangle, \langle A^{n_j}, \Pi_j \rangle,  \G \seq \D \hyp \seq A,A\}_{C\in\Pi_i, D\in\Pi_j}$.
We consider the other premisses of \subrule\ and apply \hypcut\ many times
(each time with auxiliary applications of \wk)
so to replace all occurrences of $A$ with formulas in $\Sigma$.
As final step we can apply \ruled\ and obtain
$\hG \hyp \langle \Sigma^{n_i}, \Pi_i \rangle, \langle \Sigma^{n_j}, \Pi_j  \rangle, \G \seq \D$.

$\bullet$ The remaining cases \rulednplus\ and \ruledaux\ are similar
to the previous ones.

\bigskip \textbf{(D)} Assume
$\forall c'<c.\, (Sub(c') \land \forall h'.\, Cut(c', h'))$ and
$\forall h''<h.\, Cut (c, h'')$.  We show that all applications of
\hypcut{} of height $h$ on a cut formula of weight $c$ can be replaced
by different applications of \hypcut{}, either of smaller height or on
a cut formula of smaller weight.  We can assume $h, c > 0$ as the
cases $h=0$ and $c=0$ have been already considered in \textbf{(A)} and
\textbf{(B)}.  We distinguish two cases.

(i) The cut formula is not principal in the last rule application in
the derivation of at least one of the two premisses of \hypcut.  This
case is analogous to (i) or (ii) in \textbf{(B)}.

(ii) The cut formula is principal in the last rule application in the
derivation of both premisses.  Then the cut formula is either
$B\circ C$, with $\circ\in\{\land, \lor, \to\}$, or $\Box B$.

$\bullet$ The case of boolean connective is standard. We consider as
an example $B \to C$.  We have:

\begin{center}
\resizebox{\textwidth}{!}{
\ax{$\textcircled{\footnotesize{1}}$}
\noLine
\uinf{$\hG \hyp B, \G \seq \D, B \to C, C$}
\llab{\rto}
\uinf{$\hG \hyp \G \seq \D, B \to C$}
\ax{$\textcircled{\footnotesize{2}}$}
\noLine
\uinf{$\hG \hyp B\to C, \G \seq \D, B$}
\ax{$\textcircled{\footnotesize{3}}$}
\noLine
\uinf{$\hG \hyp C, B\to C, \G \seq \D$}
\rlab{\lto}
\binf{$\hG \hyp B\to C, \G \seq \D$}
\rlab{\hypcut}
\binf{$\hG \hyp \G \seq \D$}
\disp }
\end{center}

The derivation is converted into the following one:

\begin{center}
\resizebox{\textwidth}{!}{
\ax{$\hG \hyp \G \seq \D, B \to C$}
\llab{\rwk}
\uinf{$\hG \hyp \G \seq \D, B \to C, B$}
\ax{$\textcircled{\footnotesize{2}}$}
\llab{\hypcut}
\binf{$\hG \hyp \G \seq \D, B$}
\llab{\rwk}
\uinf{$\hG \hyp \G \seq \D, B, C$}
\ax{$\textcircled{\footnotesize{1}}$}
\ax{$\hG \hyp B\to C, \G \seq \D$}
\rlab{\lwk}
\uinf{$\hG \hyp B, B\to C, \G \seq \D$}
\rlab{\rwk}
\uinf{$\hG \hyp B, B\to C, \G \seq \D, C$}
\rlab{\hypcut}
\binf{$\hG \hyp B, \G \seq \D, C$}
\rlab{\hypcut}
\binf{$\hG \hyp  \G \seq \D, C$}

\ax{$\hG \hyp \G \seq \D, B \to C$}
\llab{\lwk}
\uinf{$\hG \hyp C, \G \seq \D, B \to C$}
\ax{$\textcircled{\footnotesize{3}}$}
\llab{\hypcut}
\binf{$\hG \hyp C, \G \seq \D$}
\llab{\hypcut}
\binf{$\hG \hyp \G \seq \D$}
\disp}
\end{center}

$\bullet$ If the cut formula is $\Box B$ we have

\begin{center}
\resizebox{\textwidth}{!}{
\ax{$\hG \hyp \angSigma, \G \seq \D, \Box B \hyp \Sigma \seq B$
\qquad\qquad\qquad\qquad\qquad}
\noLine
\uinf{$\vdots$ \quad $\{\hG \hyp \angSigma, \G \seq \D, \Box B \hyp B \seq C \}_{C\in\Sigma}$}
\llab{\rbox}
\uinf{$\hG \hyp \angSigma, \G \seq \D, \Box B$}
\ax{$\hG \hyp \angB, \Box B, \angSigma, \G \seq \D$}
\rlab{\lbox}
\uinf{$\hG \hyp \Box B, \angSigma, \G \seq \D$}
\rlab{\hypcut}
\binf{$\hG \hyp \angSigma, \G \seq \D$}
\disp }
\end{center}

The derivation is converted as follows,
with several applications of \hypcut{} of smaller height
and an admissible application of \subrule.

\begin{center}
\ax{$\hG \hyp \angSigma, \G \seq \D, \Box B \hyp \Sigma \seq B$}
\ax{$\hG \hyp \Box B, \angSigma, \G \seq \D$}
\rlab{\exwk}
\uinf{$\hG \hyp \Box B, \angSigma, \G \seq \D \hyp \Sigma \seq B$}
\rlab{\hypcut}
\binf{$\textcircled{\footnotesize{4}} \ \hG \hyp \angSigma, \G \seq \D \hyp \Sigma \seq B$}
\disp

\vspace{0.5cm}
\ax{$\hG \hyp \angSigma, \G \seq \D, \Box B$}
\rlab{\hyplwk}
\uinf{$\hG \hyp \str B, \angSigma, \G \seq \D, \Box B$}
\ax{$\hG \hyp \angB, \Box B, \angSigma, \G \seq \D$}
\rlab{\hypcut}
\binf{$\hG \hyp \str B, \str\Sigma, \G \seq \D$}
\rlab{\exwk}
\uinf{$\textcircled{\footnotesize{5}} \ \hG \hyp \str\Sigma, \G \seq \D \hyp \str B, \str\Sigma, \G \seq \D$}
\disp

\vspace{0.5cm}
\resizebox{\textwidth}{!}{
\ax{\textcircled{\footnotesize{4}}}
\ax{$\hG \hyp \angSigma, \G \seq \D, \Box B \hyp B \seq C$}
\ax{$\hG \hyp \Box B, \angSigma, \G \seq \D$}
\rlab{\exwk}
\uinf{$\hG \hyp \Box B, \angSigma, \G \seq \D \hyp B \seq C$}
\llab{$\Big\{$}
\rlab{\hypcut $\Big\}_{C \in \Sigma}$}
\binf{$\hG \hyp \angSigma, \G \seq \D \hyp B \seq C$}
\ax{\textcircled{\footnotesize{5}}}
\rlab{\subrule}
\TrinaryInfC{$\hG \hyp \str\Sigma, \G \seq \D \hyp \str\Sigma, \str\Sigma, \G \seq \D$}
\rlab{\angctr}
\uinf{$\hG \hyp \str\Sigma, \G \seq \D \hyp \str\Sigma, \G \seq \D$}
\rlab{\exctr}
\uinf{$\hG \hyp \str\Sigma, \G \seq \D$}
\disp
}
\end{center}
\end{proof}

Given the admissibility of the structural rules and \hypcut\
we can prove that the calculi are syntactically complete
with respect to the corresponding axiom systems.

\begin{theorem}[Syntactic completeness]
  If $\vd_{\Estar} A$ then $\seq A$ is derivable in $\HEstar$.
\end{theorem}

\begin{proof}
  As usual, we have to show that all axioms of $\Estar$ are derivable
  in $\HEstar$, and that all rules of $\Estar$ are admissible in
  $\HEstar$.  The derivations of the modal axioms and rules are
  displayed in Figure~\ref{fig:hypersequent derivations}.  For the
  derivations of the axioms we implicitly consider
  Proposition~\ref{prop:extended initial sequents hyp}.  For the
  derivation of rule \RE\ we assume that $A \to B$ and $B \to A$ are
  derivable in $\Estar$, and for the derivation of rule \RDnplus\ we
  assume that $\neg(A_1, \ldots, A_n)$ is derivable in
  $\hEstar{D_n^+}$.  Finally, \MP{} is simulated by \hypcut{} in the
  usual way.
\end{proof}


TITLE: Quadratic congruence relation
QUESTION [2 upvotes]: Is there a general formula for solving quadratic congruence relation like $ax^2-bx+c = 0$ in $\mathbb{Z}_{n}$ where $n \in \mathbb{N}$?
For example, I am trying to solve $x^2-3x+2 = 0$ in $\mathbb{Z}_{200}$. What kind of tools I need to solve it?

REPLY [0 votes]: Another way to get something better is
$ax^2-bx+c=0\Rightarrow4a^2x^2-4abx+4ac=0\Rightarrow(2ax-b)^2=b^2-4ac=D$
So, if the first congruence has a solution mod $n$ then there must be an integer $y$
with $y^2=D$ holding true.
In other words $D$ must be a quadratic residue mod $n$.
(which sometimes is impossible for some $n$)


TITLE: Probability of selecting a type of chocolate
QUESTION [0 upvotes]: The probability of selecting a white chocolate from a box is
1/5 and the probability of selecting a dark chocolate from the same box is
1/3. The other chocolates are milk chocolates.
a) Find the probability of selecting a milk chocolate.
b) How many chocolates in total could be in the box? Give reasons. Is there more than one answer?

REPLY [1 votes]: Hint -
(1) Probabilities of all event equal to 1. So you can probability of milk chocolates by subtracting the sum of other two probabilities from 1.
(2) Total chocolates are in multiples. So we can't find exact value.