By IH, $\vDash\mathscr{c}\leftarrowtail A$, which is $\llbracket
A\rrbracket\subseteq\llbracket\mathscr{c}\rrbracket$, and
$\mu(\llbracket\mathscr{c}\rrbracket)<q$ holds. For basic set theory, also
$\mu(\llbracket A\rrbracket)<q$. Therefore,
$\llbracket\mathbf{C}^{q}A\rrbracket$ = $\emptyset$, and so
$\llbracket\mathbf{C}^{q}A\rrbracket\subseteq\llbracket\mathscr{b}\rrbracket$,
which is $\vDash\mathscr{b}\leftarrowtail\mathbf{C}^{q}A$.

$\mathsf{R}_{\mathbf{D}}^{\rightarrowtail}.$ If the last rule applied is an
instance of $\mathsf{R}_{\mathbf{D}}^{\rightarrowtail}$, the derivation has
the following form:

$\vdots$ $\vdash\mathscr{c}\leftarrowtail A$
$\mu(\llbracket\mathscr{c}\rrbracket)<q$
$\mathsf{R}_{\mathbf{D}}^{\rightarrowtail}$
$\vdash\mathscr{b}\rightarrowtail\mathbf{D}^{q}A$

By IH, $\vDash\mathscr{c}\leftarrowtail A$, which is $\llbracket
A\rrbracket\subseteq\llbracket\mathscr{c}\rrbracket$, and
$\mu(\llbracket\mathscr{c}\rrbracket)<q$ holds. For basic set theory,
$\mu(\llbracket A\rrbracket)<q$. But then,
$\llbracket\mathbf{D}^{q}A\rrbracket$ = $2^{\omega}$ and so (for every
$\mathscr{b}$)
$\llbracket\mathscr{b}\rrbracket\subseteq\llbracket\mathbf{D}^{q}A\rrbracket$,
which is $\vDash\mathscr{b}\rightarrowtail\mathbf{D}^{q}A$.

$\mathsf{R}_{\mathbf{D}}^{\leftarrowtail}.$ If the last rule applied is an
instance of $\mathsf{R}_{\mathbf{D}}^{\leftarrowtail}$, the derivation has the
following form:

$\vdots$ $\vdash\mathscr{c}\rightarrowtail A$
$\mu(\llbracket\mathscr{c}\rrbracket)\geq q$
$\mathsf{R}_{\mathbf{D}}^{\leftarrowtail}$
$\vdash\mathscr{b}\leftarrowtail\mathbf{D}^{q}A$

By IH, $\vDash\mathscr{c}\rightarrowtail A$, which is
$\llbracket\mathscr{c}\rrbracket\subseteq\llbracket A\rrbracket$, and
$\mu(\llbracket\mathscr{c}\rrbracket)\geq q$ holds. For basic set theory,
$\mu(\llbracket A\rrbracket)\geq q$. Therefore,
$\llbracket\mathbf{D}^{q}A\rrbracket$ = $\emptyset$ and, so
$\llbracket\mathbf{D}^{q}A\rrbracket\subseteq\llbracket\mathscr{b}\rrbracket$,
which is $\vDash\mathscr{b}\leftarrowtail\mathbf{D}^{q}A$.

∎

In order to prove the completeness of $\mathbf{GsCPL_{0}}$ with respect to the
semantics of $\textsf{{CPL}}_{0}$, some preliminary notions and lemmas have to
be introduced.

######  Definition A.3 (Basic Formulas).

A _basic formula_ of $\mathbf{GsCPL_{0}}$ is a labelled formula,
$\mathscr{b}\rightarrowtail A$ or $\mathscr{b}\leftarrowtail A$, such that its
logical part $A$ is atomic.

######  Definition A.4 (Regular Sequent).

A _regular sequent_ of $\mathbf{GsCPL_{0}}$ is a sequent of the form $\vdash
L$, such that $L$ is a basic formula.

The notion of decomposition rewriting reduction is defined by the following
decomposition rules.

######  Definition A.5 (Decomposition Rewriting Reduction, $\leadsto_{0}$).

The _decomposition rewriting reduction_ , $\leadsto_{0}$, from a sequent to a
set of sequents (both in the language of $\mathbf{GsCPL_{0}}$), is defined by
the following decomposition rules:

$\displaystyle\text{if }\mathscr{b}\vDash\neg\mathscr{c},\
\vdash\mathscr{b}\rightarrowtail\neg A\ \ $ $\displaystyle\leadsto_{0}\ \
\\{\vdash\mathscr{c}\leftarrowtail A\\}$ $\displaystyle\text{if
}\neg\mathscr{c}\vDash\mathscr{b},\ \vdash\mathscr{b}\leftarrowtail\neg A\ \ $
$\displaystyle\leadsto_{0}\ \ \\{\vdash\mathscr{c}\rightarrowtail A\\}$
$\displaystyle\text{if }\mathscr{b}\vDash\mathscr{c}\vee\mathscr{d},\
\vdash\mathscr{b}\rightarrowtail A\vee B\ \ $ $\displaystyle\leadsto_{0}\ \
\\{\vdash\mathscr{c}\rightarrowtail A,\vdash\mathscr{d}\rightarrowtail B\\}$
$\displaystyle\vdash\mathscr{b}\leftarrowtail A\vee B\ \ $
$\displaystyle\leadsto_{0}\ \ \\{\vdash\mathscr{b}\leftarrowtail
A,\vdash\mathscr{b}\leftarrowtail B\\}$
$\displaystyle\vdash\mathscr{b}\rightarrowtail A\wedge B\ \ $
$\displaystyle\leadsto_{0}\ \ \\{\vdash\mathscr{b}\rightarrowtail
A,\vdash\mathscr{b}\rightarrowtail B\\}$ $\displaystyle\text{if
}\mathscr{c}\wedge\mathscr{d}\vDash\mathscr{b},\
\vdash\mathscr{b}\leftarrowtail A\wedge B\ \ $ $\displaystyle\leadsto_{0}\ \
\\{\vdash\mathscr{c}\leftarrowtail A,\vdash\mathscr{d}\leftarrowtail B\\}$
$\displaystyle\text{if }\mu(\llbracket\mathscr{c}\rrbracket)\geq q,\
\vdash\mathscr{b}\rightarrowtail\mathbf{C}^{q}A\ \ $
$\displaystyle\leadsto_{0}\ \ \\{\vdash\mathscr{c}\rightarrowtail A\\}$
$\displaystyle\text{if }\mu(\llbracket\mathscr{c}\rrbracket)<q,\
\vdash\mathscr{b}\leftarrowtail\mathbf{C}^{q}A\ \ $
$\displaystyle\leadsto_{0}\ \ \\{\vdash\mathscr{c}\leftarrowtail A\\}$
$\displaystyle\text{if }\mu(\llbracket\mathscr{c}\rrbracket)<q,\
\vdash\mathscr{b}\rightarrowtail\mathbf{D}^{q}A\ \ $
$\displaystyle\leadsto_{0}\ \ \\{\vdash\mathscr{c}\leftarrowtail A\\}$
$\displaystyle\text{if }\mu(\llbracket\mathscr{c}\rrbracket)\geq q,\
\vdash\mathscr{b}\leftarrowtail\mathbf{D}^{q}A\ \ $
$\displaystyle\leadsto_{0}\ \ \\{\vdash\mathscr{c}\rightarrowtail A\\}$
$\displaystyle\text{if }\mu(\llbracket\mathscr{b}\rrbracket)=0,\
\vdash\mathscr{b}\rightarrowtail A\ \ $ $\displaystyle\leadsto_{0}\ \ \\{\\}$
$\displaystyle\text{if }\mu(\llbracket\mathscr{b}\rrbracket)=1,\
\vdash\mathscr{b}\leftarrowtail A\ \ $ $\displaystyle\leadsto_{0}\ \ \\{\\}$
$\displaystyle\text{if }\mu(\llbracket\mathscr{b}\rrbracket)\neq 0,\
\vdash\mathscr{b}\rightarrowtail\mathbf{D}^{0}A\ \ $
$\displaystyle\leadsto_{0}\ \ \\{\vdash\bot\\}$ $\displaystyle\text{if
}\mu(\llbracket\mathscr{b}\rrbracket)\neq 1,\
\vdash\mathscr{b}\leftarrowtail\mathbf{C}^{0}A\ \ $
$\displaystyle\leadsto_{0}\ \ \\{\vdash\bot\\}$

Remarkably, rewriting rules are so defined that each application of a
decomposition reduction on an arbitrary sequent, $\vdash L$, leads to a set of
sequents, $\\{\vdash L_{1},\dots,\vdash L_{n}\\}$, such that for every
$i\in\\{1,\dots,n\\}$, the number of connectives of $\vdash L_{i}$ is
(strictly) smaller than that of $\vdash L$. Basing on $\leadsto_{0}$, it is
possible to define a set-decomposition reduction, $\leadsto$, from a set of
sequents to a set of sequents.

######  Definition A.6 (Set Decomposition, $\leadsto$).

The _set-decomposition reduction_ , $\leadsto$, from a set of sequents to
another set of sequents (in $\mathbf{GsCPL_{0}}$), is defined as follows:

$\vdash L_{i}\leadsto_{0}\\{\vdash L_{i_{1}},\dots,\vdash L_{i_{m}}\\}$
$\\{\vdash L_{1},\dots,\vdash L_{i},\dots,\vdash L_{n}\\}\leadsto\\{\vdash
L_{1},\dots,\vdash L_{i_{1}},\dots,\vdash L_{i_{m}},\dots,\vdash L_{n}\\}$

In other words, $\leadsto$ is the natural lifting of $\leadsto_{0}$ to a
relation on sets.

Before introducing the crucial notions of normal form for these two reductions
it is worth mentioning that each predicate concerning one sequent can be
naturally generalized to sets of sequents by stipulating that a predicate
holds for the set when it holds for every sequent in the set. In order to make
our presentation straightforward, let us introduce the following auxiliary
notion of corresponding set.

######  Definition A.7 (Corresponding Set).

Given a sequent, $\vdash L$, we call its _corresponding set_ the set including
only this sequent as its element, $\\{\vdash L\\}$.

The notion of $\leadsto$-normal form is defined as predictable: a set of
sequents is in $\leadsto$-normal form when no set-decomposition reduction,
$\leadsto$, can be applied on it. Otherwise said, the set is such that there
is no sequent in it on which $\leadsto_{0}$ can be applied.

######  Definition A.8 ($\leadsto$-Normal Form).

A sequent is a _$\leadsto$ -normal form_ if no decomposition rewriting
reduction rule, $\leadsto_{0}$, can be applied on it. A set of sequents is in
_$\leadsto$ -normal form_ if it cannot be reduced by any $\leadsto$ set-
rewriting rule.

The proof of completeness crucially relies on the given rewriting reductions,
$\leadsto_{0}$ and $\leadsto$, and it is based on some auxiliary steps: (i)
validity is _existentially_ preserved through $\leadsto$-decomposition, which
is given a valid sequent, there has (at least) one valid $\leadsto$-normal
form (ii) each $\leadsto$-normal form is valid if and only if it is derivable,
(iii) derivability is somehow “back-preserved”, through
$\leadsto$-decomposition, which is, given a (set of) sequent(s) which is
$\leadsto$-decomposed into another set of sequents, if the
$\leadsto$-decomposed set is derivable, then it is possible to construct a
derivation for the original (set of) sequent(s).

$\leadsto$ is strongly normalizing. First it is proved that $\leadsto$ is
strongly normalizing, and so that each decomposition process terminates.

######  Definition A.9 (Number of Connectives, $\mathsf{cn}$).

The _number of connectives of a labelled formula_ $L$, $\mathsf{cn}(L)$, is
the number of connectives of its logical part (equally labelled
$\mathsf{cn}(A)$) and is inductively defined as follows:

$\displaystyle\mathsf{cn}(\mathscr{b}\rightarrowtail\mathbf{n})=\mathsf{cn}(\mathscr{b}\leftarrowtail\mathbf{n})=\mathsf{cn}(\mathbf{n})$
$\displaystyle=1$ $\displaystyle\mathsf{cn}(\mathscr{b}\rightarrowtail\neg
A)=\mathsf{cn}(\mathscr{b}\leftarrowtail\neg A)=\mathsf{cn}(\neg A)$
$\displaystyle=1+\mathsf{cn}(A)$
$\displaystyle\mathsf{cn}(\mathscr{b}\rightarrowtail
A^{*}B)=\mathsf{cn}(\mathscr{b}\leftarrowtail A^{*}B)=\mathsf{cn}(A^{*}B)$
$\displaystyle=1+\mathsf{cn}(A)+\mathsf{cn}(B)$
$\displaystyle\mathsf{cn}(\mathscr{b}\rightarrowtail*A)=\mathsf{cn}(\mathscr{b}\leftarrowtail*A)=\mathsf{cn}(*A)$
$\displaystyle=1+\mathsf{cn}(A)$

with ${}^{*}\in\\{\wedge,\vee\\}$ and
$*\in\\{\mathbf{C}^{q},\mathbf{D}^{q}\\}$. Given a sequent $\vdash L$, the
_number of connectives of the sequent_ , $\mathsf{cn}(\vdash L)$, is the
number of connectives of its labelled formulas:

$\mathsf{cn}(\vdash L)=\mathsf{cn}(L).$

######  Definition A.10 (Set Measure, $\mathsf{ms}$).

Given a set of sequents $\\{\vdash L_{1},\dots,\vdash L_{n}\\},$ its _measure_
, $\mathsf{ms}(\\{\vdash L_{1},\dots,\vdash L_{n}\\}$), is defined as follows:

$\displaystyle\mathsf{ms}(\\{\\})$ $\displaystyle=0$
$\displaystyle\mathsf{ms}\big{(}\\{\vdash L_{1},\dots,\vdash L_{n}\\}\big{)}$
$\displaystyle=3^{\mathsf{cn}(\vdash L_{1})}+\dots+3^{\mathsf{cn}(\vdash
L_{n})}.$

See 3

###### Proof.

That every set of sequents is $\leadsto$-strongly normalizable is proven by
showing that, if $\\{\vdash L_{1},\dots,\vdash L_{m}\\}\leadsto\\{\vdash
L_{1}^{\prime},\dots,\vdash L_{m}^{\prime}\\}$, then
$\mathsf{ms}(\\{\vdash\Delta_{1},\dots,\vdash\Delta_{m}\\})>\mathsf{ms}(\\{\vdash\Delta_{1}^{\prime},\dots,\vdash\Delta_{m}^{\prime}\\})$.
The proof is based on the exhaustive analysis of all possible forms of
$\leadsto$-reduction applicable to the given set, which is by dealing with all
possible forms of $\leadsto_{0}$-reduction of one of the $\vdash L_{i}$, with
$i\in\\{1,\dots,m\\}$ on which $\leadsto$ is based. Thus, we will take an
arbitrary $\vdash L_{i}$ to be the “active” sequent of $\leadsto$. Let us
consider all the possible forms of $\leadsto_{0}$ on which $\leadsto$ can be
based

Let $L=\mathscr{b}\rightarrowtail\neg A$. Assume that $\vdash L_{i}$ is the
active sequent of the $\leadsto$-decomposition and that $\leadsto$ is based on
the following $\leadsto_{0}$:

$\vdash\mathscr{b}\rightarrowtail\neg A\ \ \ \leadsto_{0}\ \ \ \
\\{\vdash\mathscr{c}\leftarrowtail A\\}$

where $\mathscr{b}\vDash\neg\mathscr{c}$. Thus:

$\displaystyle\mathsf{ms}\big{(}\\{\vdash
L_{1},\dots,\vdash\mathscr{c}\leftarrowtail A,\dots,\vdash L_{m}\\}\big{)}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:cn}}}{{=}}3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(\mathscr{c}\leftarrowtail
A)}+\dots+3^{\mathsf{cn}(L_{n})}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:ms}}}{{=}}3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(A)}+\dots+3^{\mathsf{cn}(L_{n})}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:ms}}}{{=}}3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(\neg
A)–1}+\dots+3^{\mathsf{cn}(L_{n})}$
$\displaystyle<3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(\mathscr{b}\rightarrowtail\neg
A)}+\dots+3^{\mathsf{cn}(L_{n})}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:ms}}}{{=}}\mathsf{ms}\big{(}\\{\vdash
L_{1},\dots,\vdash\mathscr{b}\rightarrowtail\neg A,\dots,\vdash
L_{m}\\}\big{)}.$

$L_{i}=\mathscr{b}\leftarrowtail\neg A$. Assume that $\vdash L_{i}$ is the
active sequent of the $\leadsto$-decomposition and that $\leadsto$ is based on
the following $\leadsto_{0}$:

$\vdash\mathscr{b}\leftarrowtail\neg A\ \ \ \leadsto_{0}\ \ \
\\{\vdash\mathscr{c}\rightarrowtail A\\}$

where $\neg\mathscr{c}\vDash\mathscr{b}$. Thus,

$\displaystyle\mathsf{ms}\big{(}\\{\vdash
L_{1},\dots,\vdash\mathscr{c}\rightarrowtail A,\dots,\vdash L_{m}\\}\big{)}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:ms}}}{{=}}3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(\mathscr{c}\rightarrowtail
A)}+\dots+3^{\mathsf{cn}(L_{n})}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:cn}}}{{=}}3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(A)}+\dots+3^{\mathsf{cn}(L_{n})}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:cn}}}{{=}}3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(\neg
A)–1}+\dots+3^{\mathsf{cn}(L_{n})}$
$\displaystyle<3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(\mathscr{b}\leftarrowtail\neg
A)}+\dots+3^{\mathsf{cn}(L_{n})}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:ms}}}{{=}}\mathsf{ms}\big{(}\\{\vdash
L_{1},\dots,\vdash\mathscr{b}\leftarrowtail\neg A,\dots,\vdash
L_{m}\\}\big{)}.$

$L_{i}=\mathscr{b}\rightarrowtail A\vee B$. Assume that $\vdash L_{i}$ is the
active sequent of $\leadsto$ and that $\leadsto$ is based on the following
$\leadsto_{0}$:

$\vdash\mathscr{b}\rightarrowtail A\vee B\ \ \ \leadsto_{0}\ \ \
\\{\vdash\mathscr{c}\rightarrowtail A,\vdash\mathscr{d}\rightarrowtail B\\}$

where $\mathscr{b}\vDash\mathscr{c}\vee\mathscr{d}$. Then,

$\displaystyle\mathsf{ms}\big{(}\\{\vdash
L_{i},\dots,\vdash\mathscr{c}\rightarrowtail
A,\vdash\mathscr{d}\rightarrowtail B,\dots,\vdash L_{m}\\}\big{)}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:ms}}}{{=}}3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(\mathscr{c}\rightarrowtail
A)}+3^{\mathsf{cn}(\mathscr{d}\rightarrowtail
B)}+\dots+3^{\mathsf{cn}(L_{m})}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:cn}}}{{=}}3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(A)}+3^{\mathsf{cn}(C)}+\dots+3^{\mathsf{cn}(L_{m})}$
$\displaystyle<3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(A)+\mathsf{cn}(B)+1}+\dots+3^{\mathsf{cn}(L_{m})}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:cn}}}{{=}}3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(\mathscr{b}\rightarrowtail
A\vee B)}+\dots+3^{\mathsf{cn}(L_{m})}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:ms}}}{{=}}\mathsf{ms}\big{(}\\{\vdash
L_{1},\dots,\vdash\mathscr{b}\rightarrowtail A\vee B,\dots,\vdash
L_{m}\\}\big{)}.$

$L_{i}=\mathscr{b}\leftarrowtail A\vee B$. Assume that $\vdash L_{i}$ is the
active sequent of $\leadsto$ and that $\leadsto$ is based on the following
$\leadsto_{0}$:

$\vdash\mathscr{b}\leftarrowtail A\vee B\ \ \ \leadsto_{0}\ \ \ \
\\{\vdash\mathscr{b}\leftarrowtail A,\vdash\mathscr{b}\leftarrowtail B\\}$

Then,

$\displaystyle\mathsf{ms}(\\{\vdash
L_{1},\dots,\vdash\mathscr{b}\leftarrowtail A,\vdash\mathscr{b}\leftarrowtail
B,\dots,\vdash L_{m}\\})$
$\displaystyle\stackrel{{\scriptstyle\ref{def:ms}}}{{=}}3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(\mathscr{b}\leftarrowtail
A)}+3^{\mathsf{cn}(\mathscr{b}\leftarrowtail B)}+\dots+3^{\mathsf{cn}(L_{m})}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:cn}}}{{=}}3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(A)}+3^{\mathsf{cn}(B)}+\dots+3^{\mathsf{cn}(L_{m})}$
$\displaystyle<3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(A)+\mathsf{cn}(B)+1}+\dots+3^{\mathsf{cn}(L_{m})}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:cn}}}{{=}}3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(\mathscr{b}\leftarrowtail
A\vee B)}+\dots+3^{\mathsf{cn}(L_{m})}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:ms}}}{{=}}\mathsf{ms}\big{(}\\{\vdash
L_{1},\dots,\vdash\mathscr{b}\leftarrowtail A\vee B,\dots,\vdash
L_{m}\\}\big{)}$

$L_{i}=\mathscr{b}\rightarrowtail A\wedge B$. The proof is equivalent to the
one for $\mathscr{b}\leftarrowtail A\vee B$.

$L_{i}=\mathscr{b}\leftarrowtail A\wedge B$. The proof is equivalent to the
one for $\mathscr{b}\rightarrowtail A\vee B$.

$L=\mathscr{b}\rightarrowtail\mathbf{C}^{q}A$. Assume that $\vdash L_{i}$ is
the active sequent of $\leadsto$ decomposition and that $\leadsto$ is based on
the following $\leadsto_{0}$:

$\vdash\mathscr{b}\rightarrowtail\mathbf{C}^{q}A\ \ \ \leadsto_{0}\ \ \
\\{\vdash\mathscr{c}\rightarrowtail A\\}$

where $\mu(\llbracket\mathscr{c}\rrbracket)\geq q$. Then,

$\displaystyle\mathsf{ms}\big{(}\\{\vdash
L_{1},\dots,\vdash\mathscr{c}\rightarrowtail A,\dots,\vdash L_{m}\\}\big{)}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:ms}}}{{=}}3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(\mathscr{c}\rightarrowtail
A)}+\dots+3^{\mathsf{cn}(L_{m})}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:cn}}}{{=}}3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(A)}+\dots+3^{\mathsf{cn}(L_{m})}$
$\displaystyle<3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(A)+1}+\dots+3^{\mathsf{cn}(L_{m})}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:cn}}}{{=}}3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(\mathscr{b}\rightarrowtail\mathbf{C}^{q}A)+1}+\dots+3^{\mathsf{cn}(L_{m})}$
$\displaystyle\stackrel{{\scriptstyle\ref{def:ms}}}{{=}}\mathsf{ms}\big{(}\\{\vdash
L_{1},\dots,\vdash\mathscr{b}\rightarrowtail\mathbf{C}^{q}A,\dots,\vdash
L_{m}\\}\big{)}.$

$L_{i}=\mathscr{b}\leftarrowtail\mathbf{C}^{q}A$,
$L_{i}=\mathscr{b}\rightarrowtail\mathbf{D}^{q}A$,
$L_{i}=\mathscr{b}\leftarrowtail\mathbf{D}^{q}A$. The proof is equivalent to
the one for $\mathscr{b}\rightarrowtail\mathbf{C}^{q}A$.

$L_{i}=\mathscr{b}\rightarrowtail A$. Assume that $\vdash L_{i}$ is the active
sequent of $\leadsto$ decomposition and that $\leadsto$ is based on the
following $\leadsto_{0}$:

$\vdash\mathscr{b}\rightarrowtail A\ \ \ \leadsto_{0}\ \ \ \\{\\}$

where $\mu(\llbracket\mathscr{b}\rrbracket)=0$. Since for Definition A.10 and
A.9, $\mathsf{cn}(\\{\\})=0$ and $\mathsf{cn}(\vdash\mathscr{b}\leftarrowtail
A)>0$, clearly
$\mathsf{cn}(\\{\\})<\mathsf{cn}(\vdash\mathscr{b}\leftarrowtail A)$.

$L_{i}=\mathscr{b}\leftarrowtail A$,
$L_{i}=\mathscr{b}\rightarrowtail\mathbf{D}^{0}A$,
$L_{i}=\mathscr{b}\leftarrowtail\mathbf{C}^{0}A$. The proof is equivalent to
the other for $\mathscr{b}\rightarrowtail A$. ∎

$\leadsto$-Normal Sequents. It is possible to show that $\leadsto$-normal
sequents are valid if and only if they are derivable in $\mathbf{GsCPL_{0}}$.
First, it is shown that sequents which are $\leadsto$-normal are regular.
Then, it is proved that regular sequents are derivable if and only if they are
valid. Putting these two results together it is shown that $\leadsto$-normal
sequents are valid only when they are derivable.

######  Lemma 22.

If a (non-empty) sequent is $\leadsto$-normal, then it is regular.

###### Proof.

The proof is by contraposition. Given an arbitrary _non-regular_ sequent, call
it $\vdash L$, it is shown that it is not $\leadsto$-normal. Every possible
form of lebelled formula $L$ is considered.

$L=\mathscr{b}\rightarrowtail\neg A$. Clearly,
$\llbracket\mathscr{b}\rrbracket\subseteq
2^{\omega}=\llbracket\neg\bot\rrbracket$, which is
$\mathscr{b}\vDash\neg\bot$. Then, the following decomposition is well-
defined:

$\vdash\mathscr{b}\rightarrowtail\neg A\ \ \ \leadsto_{0}\ \ \
\\{\vdash\bot\leftarrowtail A\\}.$

$L=\mathscr{b}\leftarrowtail\neg A$. Clearly,
$\llbracket\neg\top\rrbracket=\emptyset\subseteq\llbracket\mathscr{b}\rrbracket$,
which is $\neg\top\vdash\mathscr{b}$. Then, the following decomposition is
well-defined:

$\vdash\mathscr{b}\leftarrowtail\neg A\ \ \ \leadsto_{0}\ \ \
\\{\vdash\top\rightarrowtail A\\}.$

$L=\mathscr{b}\rightarrowtail A\vee B$. For every
$\llbracket\mathscr{b}\rrbracket\subseteq
2^{\omega}=\llbracket\top\vee\top\rrbracket$, which is
$\mathscr{b}\vDash(\top\vee\top)$. Then, the following decomposition is well-
defined:

$\vdash\mathscr{b}\rightarrowtail A\vee B\ \ \ \leadsto_{0}\ \ \
\\{\vdash\top\rightarrowtail A,\vdash\top\rightarrowtail B\\}.$

$L=\mathscr{b}\leftarrowtail A\vee B$. Then, the following decomposition is
well-defined:

$\vdash\mathscr{b}\leftarrowtail A\vee B\ \ \ \leadsto_{0}\ \ \
\\{\vdash\mathscr{b}\leftarrowtail A,\vdash\mathscr{b}\leftarrowtail B\\}.$

$L=\mathscr{b}\rightarrowtail A\wedge B$. Then, the following decomposition is
well-defined:

$\vdash\mathscr{b}\rightarrowtail A\wedge B\ \ \ \leadsto_{0}\ \ \
\\{\vdash\mathscr{b}\rightarrowtail A,\vdash\mathscr{b}\rightarrowtail B\\}.$

$L=\mathscr{b}\leftarrowtail A\wedge B$. For every
$\mathscr{b},\llbracket\bot\wedge\bot\rrbracket=\emptyset\subseteq\llbracket\mathscr{b}\rrbracket$,
which is $(\bot\wedge\bot)\vDash\mathscr{b}$. Then, the following
decomposition is well-defined:

$\vdash\mathscr{b}\leftarrowtail A\wedge B\ \ \ \leadsto_{0}\ \ \
\\{\vdash\bot\leftarrowtail A,\vdash\bot\leftarrowtail B\\}.$

$L=\mathscr{b}\rightarrowtail\mathbf{C}^{q}A$. For every $q\in[0,1]$,
$\mu(\llbracket\top\rrbracket)=\mu(2^{\omega})\geq q$. Then, the following
decomposition is well-defined:

$\vdash\mathscr{b}\rightarrowtail\mathbf{C}^{q}A\ \ \ \leadsto_{0}\ \ \
\\{\vdash\top\rightarrowtail A\\}.$

$L=\mathscr{b}\leftarrowtail\mathbf{C}^{q}A$. There are two possible cases,
basing on the value of $q\in[0,1]$:

  * •

Let $q\neq 0$. Then, $\mu(\llbracket\bot\rrbracket)=\mu(\emptyset)<q$ and the
following decomposition is well-defined:

$\vdash\mathscr{b}\leftarrowtail\mathbf{C}^{q}A\ \ \ \leadsto_{0}\ \ \
\\{\vdash\bot\leftarrowtail A\\}.$

  * •

Let $q=0$. There are two possible sub-cases:

    1. 1.

Let $\mu(\llbracket\mathscr{b}\rrbracket)=1$. Then, the following
decomposition is well-defined:

$\vdash\mathscr{b}\leftarrowtail\mathbf{C}^{0}A\ \ \ \leadsto_{0}\ \ \
\\{\\}.$

    2. 2.

Let $\mu(\llbracket\mathscr{b}\rrbracket)\neq 1$. Then, the following
decomposition is well-defined:

$\vdash\mathscr{b}\leftarrowtail\mathbf{C}^{0}A\ \ \ \leadsto_{0}\ \ \
\\{\vdash\bot\\}.$

$L=\mathscr{b}\rightarrowtail\mathbf{D}^{q}A$. There are two possible cases,
basing on the value of $q\in[0,1]$.

  * •

Let $q\neq 0$. Then $\mu(\llbracket\bot\rrbracket)=\mu(\emptyset)<q$ and the
decomposition is well-defined:

$\vdash\mathscr{b}\rightarrowtail\mathbf{D}^{q}A\ \ \ \leadsto_{0}\ \ \
\\{\vdash\bot\leftarrowtail A\\}.$

  * •

Let $q=0$. There are two possible sub-cases:

    1. 1.

Let $\mu(\llbracket\mathscr{b}\rrbracket)=0$. Then, the following
decomposition is well-defined:

$\vdash\mathscr{b}\rightarrowtail\mathbf{D}^{0}A\ \ \ \leadsto_{0}\ \ \
\\{\\}.$

    2. 2.

Let $\mu(\llbracket\mathscr{b}\rrbracket)\neq 0$. Then, the following
decomposition is well-defined:

$\vdash\mathscr{b}\rightarrowtail\mathbf{D}^{0}A\ \ \ \leadsto_{0}\ \ \
\\{\vdash\bot\\}.$

$L=\mathscr{b}\leftarrowtail\mathbf{D}^{q}A.$ For every $q\in[0,1]$,
$\mu(\llbracket\top\vee\top\rrbracket)=\mu(2^{\omega})\geq q$. Then, the
following decomposition is well-defined:

$\vdash\mathscr{b}\leftarrowtail\mathbf{D}^{q}A\ \ \ \leadsto_{0}\ \ \
\\{\vdash\top\rightarrowtail A\\}.$

∎

######  Lemma 23.

A regular sequent is valid if and only if it is derivable in
$\mathbf{GsCPL_{0}}$.

###### Proof.

Let $\vdash L$ be a regular sequent, which is let $L$ be basic.

  * $\Rightarrow$

Assume that $\vdash L$ is valid. Since $L$ is a basic formula, there are two
main cases.

$L=\mathscr{b}\rightarrowtail\mathbf{n}$, for arbitrary $\mathscr{b}$ and
$n\in\mathbb{N}$. Since for hypothesis
$\vDash\mathscr{b}\rightarrowtail\mathbf{n}$, which is
$\llbracket\mathscr{b}\rrbracket\subseteq\llbracket\mathbf{n}\rrbracket$, and
$(\llbracket\mathbf{n}\rrbracket=)\mathrm{Cyl}(n)=\mathscr{x}_{n}$, also
$\llbracket\mathscr{b}\rrbracket\subseteq\llbracket\mathscr{x}_{x}\rrbracket$,
which is $\mathscr{b}\vDash\mathscr{x}_{n}$. Therefore,
$\vdash\mathscr{b}\rightarrowtail\mathbf{n}$ is derivable by means of
$\mathsf{Ax1}$:

$\mathscr{b}\vDash\mathscr{x}_{n}$ $\mathsf{Ax1}$
$\vdash\mathscr{b}\rightarrowtail\mathbf{n}$

$L=\mathscr{b}\leftarrowtail\mathbf{n}$, for arbitrary $\mathscr{b}$ and
$n\in\mathbb{N}$. Since for hypothesis
$\vDash\mathscr{b}\leftarrowtail\mathbf{n}$, which is
$\llbracket\mathbf{n}\rrbracket\subseteq\llbracket\mathscr{b}\rrbracket$, and
$\llbracket\mathscr{x}_{n}\rrbracket=\mathrm{Cyl}(n)(=\mathbf{n})$, also
$\llbracket\mathscr{x}_{n}\rrbracket\subseteq\llbracket\mathscr{b}\rrbracket$,
which is $\mathscr{x}_{n}\vDash\mathscr{b}$. Therefore,
$\vdash\mathscr{b}\leftarrowtail\mathbf{n}$ is derivable by means of
$\mathsf{Ax2}$:

$\mathscr{x}_{n}\vDash\mathscr{b}$ $\mathsf{Ax2}$
$\vdash\mathscr{b}\leftarrowtail\mathbf{n}$

Therefore, in both cases, $\vdash L$ is derivable in $\mathbf{GsCPL_{0}}$.

Assume that $\vdash L$ is derivable in $\mathbf{GsCPL_{0}}$. Then, by
Proposition 2, $\vDash L$. ∎

######  Corollary 2.

If a sequent is $\leadsto$-normal, then it is valid if and only if it is
derivable in $\mathbf{GsCPL_{0}}$.

###### Proof.

By putting Lemma 22 and 23 together. ∎

All the given results can be naturally extended from sequents to sets,
obtaining in particular that, if a set of sequents is $\leadsto$-normal, which
is each of its sequents is $\leadsto$-normal, then it is valid if and only if
it is derivable, namely its sequents are valid if and only if they are
derivable.

Existential Preservation of Validity. It is possible to prove that the
validity is existentially preserved through $\leadsto$-decomposition. It is
first needed to establish the following auxiliary lemma.

######  Lemma 24.

For every formula of $\textsf{{CPL}}_{0}$, call it $A$, there is an expression
$\mathscr{b}_{A}$, such that $\llbracket
A\rrbracket=\llbracket\mathscr{b}_{A}\rrbracket$.

###### Proof.

The proof is by induction on the structure of $A$:

  * •

_Base case._ Let $A$ be atomic, which is $A\equiv\mathbf{n}$, for some
$n\in\mathbb{N}$. By Definition 3.2, $\llbracket\mathbf{n}\rrbracket$ =
$\mathrm{Cyl}(n)$, but also $\mathrm{Cyl}(n)$ =
$\llbracket\mathscr{x}_{n}\rrbracket$. Therefore, let us define
$\mathscr{b}_{A}=\mathscr{x}_{n}$, so that clearly
$\llbracket\mathbf{n}\rrbracket$ = $\llbracket\mathscr{x}_{n}\rrbracket$.

  * •

_Inductive case._ There are some possible cases.

$A=\neg B$. By IH, there is a $\mathscr{b}_{B}$ such that $\llbracket
B\rrbracket=\llbracket\mathscr{b}_{B}\rrbracket$. So, let us define
$\mathscr{b}_{A}$ = $\neg\mathscr{b}_{B}$, which is well-defined by Definition
3.2. Indeed, $\llbracket\mathscr{b}_{A}\rrbracket$ =
$\llbracket\neg\mathscr{b}_{B}\rrbracket$ = $2^{\omega}\ –\
\llbracket\mathscr{b}_{B}\rrbracket$ $\stackrel{{\scriptstyle\text{IH}}}{{=}}$
$2^{\omega}\ –\ \llbracket B\rrbracket$ = $\llbracket\neg B\rrbracket$.

$A$ = $B\vee C$. By IH, there are two $\mathscr{b}_{B}$ and $\mathscr{b}_{C}$
such that $\llbracket\mathscr{b}_{B}\rrbracket$ = $\llbracket B\rrbracket$ and
$\llbracket\mathscr{b}_{C}\rrbracket$ = $\llbracket C\rrbracket$. Thus, let us
define $\mathscr{b}_{A}$ = $\mathscr{b}_{B}$ $\vee$ $\mathscr{b}_{C}$, which
is well-defined by Definition 3.2. Indeed, as desired,
$\llbracket\mathscr{b}_{A}\rrbracket$ =
$\llbracket\mathscr{b}_{B}\vee\mathscr{b}_{C}\rrbracket$ =
$\llbracket\mathscr{b}_{B}\rrbracket\cup\llbracket\mathscr{b}_{C}\rrbracket$
$\stackrel{{\scriptstyle\text{IH}}}{{=}}$ $\llbracket
B\rrbracket\cup\llbracket C\rrbracket$ = $\llbracket B\vee C\rrbracket$.

$A$ = $B\wedge C$. By IH, there are two $\mathscr{b}_{B}$ and
$\mathscr{b}_{C}$ such that $\llbracket\mathscr{b}_{B}\rrbracket$ =
$\llbracket B\rrbracket$ and $\llbracket\mathscr{b}_{C}\rrbracket$ =
$\llbracket C\rrbracket$. Let us define $\mathscr{b}_{A}$ = $\mathscr{b}_{B}$
$\wedge$ $\mathscr{b}_{C}$, which is well-defined by Definition 3.2. Indeed,
$\llbracket\mathscr{b}_{A}\rrbracket$ =
$\llbracket\mathscr{b}_{B}\wedge\mathscr{b}_{C}\rrbracket$ =
$\llbracket\mathscr{b}_{B}\rrbracket\cap\llbracket\mathscr{b}_{C}\rrbracket$
$\stackrel{{\scriptstyle\text{IH}}}{{=}}$ $\llbracket
B\rrbracket\cap\llbracket C\rrbracket$ = $\llbracket B\wedge C\rrbracket$.

$A$ = $\mathbf{C}^{q}B$ or $A$ = $\mathbf{D}^{q}B$. In both cases, either
$\llbracket A\rrbracket$ = $2^{\omega}$ or $\llbracket A\rrbracket$ =
$\emptyset$. In the former case, let us define $\mathscr{b}_{A}$ = $\top$, as
$\llbracket\top\rrbracket$ = $2^{\omega}$ = $\llbracket A\rrbracket$. In the
latter case, let us define $\mathscr{b}_{A}$ = $\bot$, since
$\llbracket\bot\rrbracket$ = $\emptyset$ = $\llbracket A\rrbracket$.

∎

######  Lemma 25 (Existential Preservation of Validity).

Each valid sequent has a valid $\leadsto$-normal form.

###### Proof.

Let $\vdash L$ be an arbitrary, _valid_ sequent. It is shown that $\vdash L$
has a valid $\leadsto$-normal form. The proof is by exhaustive inspection.
There are two main cases.

  * •

Let $\vdash L$ be such that no $\leadsto_{0}$-reduction can be applied on it.
Then, for Lemma 22, the sequent is either empty or regular, which is $L$ is a
basic formula. In both cases, the sequent is trivially $\leadsto$-normal and,
for hypothesis, valid.

  * •

Let $\vdash L$ be $\leadsto$-reducible. By Lemma 32, there is no infinite
reduction sequence. Thus, it is sufficient to prove that each _reduction step_
existentially preserves validity, which is that for every possible $\leadsto$,
based on every possible $\leadsto_{0}$ reduction, if $\vDash L$, then there is
a $\leadsto_{0}$ such that $\vdash L\leadsto_{0}\Phi$, and $\Phi$ is valid.
The proof is based on the exhaustive consideration of all possible
$\leadsto_{0}$ form.

$L=\mathscr{b}\rightarrowtail\neg A$. Let us consider a Boolean formula
defined as $\mathscr{c}=\neg\mathscr{b}$. Thus,
$\llbracket\neg\mathscr{c}\rrbracket=2^{\omega}$ $–$
$\llbracket\mathscr{c}\rrbracket=2^{\omega}$ $–$ ($2^{\omega}$ $–$
$\llbracket\mathscr{b}\rrbracket$) = $\llbracket\mathscr{b}\rrbracket$ and so,
in particular $\mathscr{b}\vDash\neg\mathscr{c}$. Let us consider the
following well-defined $\leadsto_{0}$-decomposition (given
$\mathscr{b}\vDash\neg\mathscr{c}$):

$\vdash\mathscr{b}\rightarrowtail\neg A\ \ \ \leadsto_{0}\ \ \
\\{\vdash\mathscr{c}\leftarrowtail A\\}.$

For hypothesis $\mathscr{b}\rightarrowtail\neg A$, which is
$\llbracket\mathscr{b}\rrbracket\subseteq\llbracket\neg A\rrbracket$. By basic
set theory, also $\llbracket
A\rrbracket\subseteq\llbracket\neg\mathscr{b}\rrbracket$. Since for
construction $\mathscr{c}=\neg\mathscr{b}$, $\llbracket
A\rrbracket\subseteq\llbracket\mathscr{c}\rrbracket$ holds, which is
$\vDash\mathscr{c}\leftarrowtail A$, as desired. Therefore, there is a
$\leadsto_{0}$-decomposition which preserves validity.

$L=\mathscr{b}\leftarrowtail\neg A$. Let us consider a Boolean formula defined
as $\mathscr{c}=\neg\mathscr{b}$. Thus,
$\llbracket\mathscr{c}\rrbracket=\llbracket\neg\mathscr{b}\rrbracket$ and, in
particular, $\neg\mathscr{c}\vDash\mathscr{b}$. Let us consider the following
$\leadsto_{0}$-decomposition, which is well-defined (given
$\neg\mathscr{c}\vDash\mathscr{b}$):

$\vdash\mathscr{b}\leftarrowtail\neg A\ \ \ \leadsto_{0}\ \ \
\\{\vdash\mathscr{c}\rightarrowtail A\\}.$

For hypothesis $\mathscr{b}\leftarrowtail\neg A$, which is $\llbracket\neg
A\rrbracket\subseteq\llbracket\mathscr{b}\rrbracket$, so for basic set theory
$\llbracket\neg\mathscr{b}\rrbracket\subseteq\llbracket A\rrbracket$. Since
for construction
$\llbracket\mathscr{c}\rrbracket=\llbracket\neg\mathscr{b}\rrbracket$, also
$\llbracket\mathscr{c}\rrbracket\subseteq\llbracket A\rrbracket$, which is
$\vDash\mathscr{c}\rightarrowtail A$ and the described
$\leadsto_{0}$-decomposition is as desired.

$L=\mathscr{b}\rightarrowtail A\vee B$. Let us consider two $\mathscr{b}_{A}$
and $\mathscr{b}_{B}$ such that
$\llbracket\mathscr{b}_{A}\rrbracket=\llbracket A\rrbracket$ and
$\llbracket\mathscr{b}_{B}\rrbracket=\llbracket B\rrbracket$ (which must
exists by Lemma 24). For hypothesis $\vDash\mathscr{b}\rightarrowtail A\vee
B$, which is $\llbracket\mathscr{b}\rrbracket\subseteq\llbracket
A\rrbracket\cup\llbracket B\rrbracket$. Thus, for construction, also
$\llbracket\mathscr{b}\rrbracket\subseteq\llbracket\mathscr{b}_{A}\rrbracket\cup\llbracket\mathscr{b}_{B}\rrbracket$,
which is $\mathscr{b}\vDash\mathscr{b}_{A}\vee\mathscr{b}_{B}$. Let us
consider the following derivation, which is well-defined (given
$\mathscr{b}\vDash\mathscr{b}_{A}\vee\mathscr{b}_{B}$):

$\vdash\mathscr{b}\rightarrowtail A\vee B\ \ \ \leadsto_{0}\ \ \
\\{\vdash\mathscr{b}_{A}\rightarrowtail A,\vdash\mathscr{b}_{B}\rightarrowtail
B\\}.$

For construction $\llbracket\mathscr{b}_{A}\rrbracket=\llbracket A\rrbracket$
and $\llbracket\mathscr{b}_{B}\rrbracket=\llbracket B\rrbracket$ so, in
particular, $\llbracket\mathscr{b}_{A}\rrbracket\subseteq\llbracket
A\rrbracket$ and $\llbracket\mathscr{b}_{B}\rrbracket\subseteq\llbracket
B\rrbracket$. Therefore, $\vDash\mathscr{b}_{A}\rightarrowtail A$ and
$\vDash\mathscr{b}_{B}\rightarrowtail B$ and the given
$\leadsto_{0}$-decomposition is as desired.

$L=\mathscr{b}\leftarrowtail A\vee B$. Let us consider the following, well-
defined $\leadsto_{0}$-decomposition:

$\vdash\mathscr{b}\leftarrowtail A\vee B\ \ \ \leadsto_{0}\ \ \
\\{\vdash\mathscr{b}\leftarrowtail A,\vdash\mathscr{b}\leftarrowtail B\\}.$

For hypothesis $\vDash\mathscr{b}\leftarrowtail A\vee B$, which is $\llbracket
A\rrbracket\cup\llbracket
B\rrbracket\subseteq\llbracket\mathscr{b}\rrbracket$. Then, by basic set
theory, both $\llbracket A\rrbracket\subseteq\llbracket\mathscr{b}\rrbracket$
and $\llbracket B\rrbracket\subseteq\llbracket\mathscr{b}\rrbracket$, which is
$\vDash\mathscr{b}\leftarrowtail A$ and $\vDash\mathscr{b}\leftarrowtail B$,
as desired.

$L=\mathscr{b}\rightarrowtail A\wedge B$. The proof is equivalent to the one
for $\mathscr{b}\leftarrowtail A\vee B$.

$L=\mathscr{b}\leftarrowtail A\wedge B$. The proof is equivalent to the one
for $\mathscr{b}\rightarrowtail A\vee B$.

$L=\mathscr{b}\rightarrowtail\mathbf{C}^{q}A$. There are two main cases:

    1. 1.

Let $\mu(\llbracket\mathscr{b}\rrbracket)=0$. Then, the sequent can be
decomposed by means of the following, well-defined
$\leadsto_{0}$-decomposition:

$\vdash\mathscr{b}\rightarrowtail\mathbf{C}^{q}A\ \ \ \leadsto_{0}\ \ \
\\{\\}.$

$\\{\\}$ is vacuously valid so the given decomposition is as desired.

    2. 2.

Let $\mu(\llbracket\mathscr{b}\rrbracket)\neq 0$ For hypothesis
$\vDash\mathscr{b}\rightarrowtail\mathbf{C}^{q}A$, which is
$\llbracket\mathscr{b}\rrbracket\subseteq\llbracket\mathbf{C}^{q}A\rrbracket$.
Since $\llbracket\mathscr{b}\rrbracket\neq\emptyset$, also
$\llbracket\mathbf{C}^{q}A\rrbracket\neq\emptyset$, which is
$\llbracket\mathbf{C}^{q}A\rrbracket=2^{\omega}$, and so $\mu(\llbracket
A\rrbracket)\geq q$. Let us consider a Boolean formula $\mathscr{b}_{A}$, such
that $\llbracket\mathscr{b}_{A}\rrbracket=\llbracket A\rrbracket$ (it can be
constructed due to Lemma 24). Thus,
$\mu(\llbracket\mathscr{b}_{A}\rrbracket)\geq q$ and the following
decomposition is well-defined:

$\vdash\mathscr{b}\rightarrowtail\mathbf{C}^{q}A\ \ \ \leadsto_{0}\ \ \
\\{\mathscr{b}_{A}\rightarrowtail A\\}.$

Since for construction $\llbracket\mathscr{b}_{A}\rrbracket=\llbracket
A\rrbracket$, in particular also
$\llbracket\mathscr{b}_{A}\rrbracket\subseteq\llbracket A\rrbracket$, which is
$\vDash\mathscr{b}_{A}\rightarrowtail A$ as desired.

$L=\mathscr{b}\leftarrowtail\mathbf{C}^{q}A.$ There are two main cases:

    1. 1.

Let $\mu(\llbracket\mathscr{b}\rrbracket)=1$. Then, the sequent can be
decomposed by means of the following well-defined
$\leadsto_{0}$-decomposition:

$\vdash\mathscr{b}\leftarrowtail\mathbf{C}^{q}A\ \ \ \leadsto_{0}\ \ \
\\{\\}.$

$\\{\\}$ is vacuously valid, so the given decomposition is as desired.

    2. 2.

Let $\mu(\llbracket\mathscr{b}\rrbracket)\neq 1$. For hypothesis
$\vDash\mathscr{b}\leftarrowtail\mathbf{C}^{q}A$, which is
$\llbracket\mathbf{C}^{q}A\rrbracket\subseteq\llbracket\mathscr{b}\rrbracket$.
Since $\llbracket\mathscr{b}\rrbracket\neq 2^{\omega}$,
$\llbracket\mathbf{C}^{q}A\rrbracket=\emptyset$ and so $\mu(\llbracket
A\rrbracket)<q$. Let us consider a Boolean formula $\mathscr{b}_{A}$ such that
$\llbracket\mathscr{b}_{A}\rrbracket=\llbracket A\rrbracket$ (it can be
constructed due to Lemma 24). Thus,
$\mu(\llbracket\mathscr{b}_{A}\rrbracket)<q$, and the following decomposition
is well-defined:

$\vdash\mathscr{b}\leftarrowtail\mathbf{C}^{q}A\ \ \ \leadsto_{0}\ \ \
\\{\mathscr{b}_{A}\leftarrowtail A\\}.$

Since for construction $\llbracket\mathscr{b}_{A}\rrbracket=\llbracket
A\rrbracket$, in particular also $\llbracket
A\rrbracket\subseteq\llbracket\mathscr{b}\rrbracket_{A}$, which is
$\vDash\mathscr{b}_{A}\leftarrowtail A$ as desired.

$L=\mathscr{b}\rightarrowtail\mathbf{D}^{q}A$ or
$L=\mathscr{b}\leftarrowtail\mathbf{D}^{q}A$. The proof is equivalent to the
ones for $\mathscr{b}\leftarrowtail\mathbf{C}^{q}A$ and
$\mathscr{b}\rightarrowtail\mathbf{C}^{q}A$.

$L=\mathscr{b}\rightarrowtail A$ and $\mu(\llbracket\mathscr{b}\rrbracket)=0$.
Then, the following decomposition is well-defined:

$\vdash\mathscr{b}\rightarrowtail A\ \ \ \leadsto_{0}\ \ \ \\{\\}.$

$\\{\\}$ is vacuously valid so the given decomposition is as desired.

$L=\mathscr{b}\rightarrowtail A$ and $\mu(\llbracket\mathscr{b}\rrbracket)=1$.
Then, the following decomposition is well-defined:

$\vdash\mathscr{b}\leftarrowtail A\ \ \ \leadsto_{0}\ \ \ \\{\\}.$

$\\{\\}$ is vacuously valid so the given decomposition is as desired.

There is no other possible case. (Notice that if
$L=\mathscr{b}\rightarrowtail\mathbf{D}^{0}A$, for hypothesis,
$\vDash\mathscr{b}\rightarrowtail\mathbf{D}^{0}A$, which is
$\llbracket\mathscr{b}\rrbracket\subseteq\llbracket\mathbf{D}^{0}A\rrbracket$.
But clearly $\llbracket\mathbf{D}^{0}A\rrbracket=\emptyset$, so
$\llbracket\mathscr{b}\rrbracket=\emptyset$ and
$\mu(\llbracket\mathscr{b}\rrbracket)=0$; equally when
$L=\mathscr{b}\leftarrowtail\mathbf{C}^{0}A$,
$\mu(\llbracket\mathscr{b}\rrbracket$)=1.) ∎

Derivability Preservation. As anticipated, properties and proofs concerning
sequents can be easily generalized to corresponding proofs about sets of
sequents. Specifically, by considering together Lemma 22 and Lemma 23, it is
established a result, corresponding to Corollary 3, namely that a
$\leadsto_{0}$-normal set of sequents is derivable if and only if it is valid
is easily proved.

######  Definition A.11 (Derivable Set).

A set of sequents is _derivable_ if and only if all of its sequents are
derivable in $\mathbf{GsCPL_{0}}$.

######  Lemma 26.

Given two sets of sequent $\Phi,\Phi^{\prime}$, if $\Phi\leadsto\Phi^{\prime}$
and $\Phi^{\prime}$ is derivable in $\mathbf{GsCPL_{0}}$, then $\Phi$ is
derivable in $\mathbf{GsCPL_{0}}$ as well.

###### Proof.

Assume $\Phi\leadsto\Phi^{\prime}$. Then, there is a $\vdash L\in\Phi$ such
that it is the “active” sequent on which $\leadsto$ is based, which is
$\leadsto$ is based on the following $\leadsto_{0}$-decomposition:

$\vdash L\ \ \ \leadsto_{0}\ \ \ \\{\vdash L_{1},\dots,\vdash L_{n}\\}.$

The proof is by inspection of all possible forms of $\leadsto_{0}$.

Let $L=\mathscr{b}\rightarrowtail\neg A$ and its $\leadsto_{0}$-decomposition
be as follows:

$\vdash\mathscr{b}\rightarrowtail\neg A\ \ \ \leadsto_{0}\ \ \
\\{\vdash\mathscr{c}\leftarrowtail A\\}$

where $\mathscr{b}\vDash\neg\mathscr{c}$. Since
$\vdash\mathscr{c}\leftarrowtail A\in\Phi^{\prime}$, for hypothesis
$\vdash\mathscr{c}\leftarrowtail A$ is derivable by a derivation, call it
$\mathcal{D}$. Therefore, $\vdash\mathscr{b}\rightarrowtail\neg A$ can be
shown derivable in $\mathbf{GsCPL_{0}}$ as follows:

$\mathcal{D}$ $\vdash\mathscr{c}\leftarrowtail A$
$\mathscr{b}\vDash\neg\mathscr{c}$ $\mathsf{R}_{\neg}^{\rightarrowtail}$
$\vdash\mathscr{b}\rightarrowtail\neg A$

Let $L=\mathscr{b}\leftarrowtail\neg A$ and its $\leadsto_{0}$-decomposition
be as follows:

$\vdash\mathscr{b}\leftarrowtail\neg A\ \ \ \leadsto_{0}\ \ \
\\{\vdash\mathscr{c}\rightarrowtail A\\}$

where $\neg\mathscr{c}\vDash\mathscr{b}$. Since
$\vdash\mathscr{c}\rightarrowtail A\in\Phi^{\prime}$, for hypothesis
$\vdash\mathscr{c}\rightarrowtail A$ is derivable by a derivation, call it
$\mathcal{D}$. Therefore, $\vdash\mathscr{b}\leftarrowtail\neg A$ can be shown
derivable in $\mathbf{GsCPL_{0}}$ as follows:

$\mathcal{D}$ $\vdash\mathscr{c}\rightarrowtail A$
$\neg\mathscr{c}\vDash\mathscr{b}$ $\mathsf{R}_{\neg}^{\leftarrowtail}$
$\vdash\mathscr{b}\leftarrowtail\neg A$

Let $L=\mathscr{b}\rightarrowtail A\vee B$ and $\leadsto_{0}$-decomposition be
as follows:

$\vdash\mathscr{b}\rightarrowtail A\vee B\ \ \ \leadsto_{0}\ \ \
\\{\vdash\mathscr{c}\rightarrowtail A,\vdash\mathscr{d}\rightarrowtail B\\}$

where $\mathscr{b}\vDash\mathscr{c}\vee\mathscr{d}$. Since
$\vdash\mathscr{c}\rightarrowtail A,\vdash\mathscr{d}\rightarrowtail
B\in\Phi^{\prime}$, both $\vdash\mathscr{c}\rightarrowtail A$ and
$\vdash\mathscr{d}\rightarrowtail B$ are derivable by two derivations, call
them $\mathcal{D}$ and $\mathcal{D}^{\prime}$. Then,
$\mathscr{b}\rightarrowtail A\vee B$ can be shown derivable in
$\mathbf{GsCPL_{0}}$ as follows:

$\mathcal{D}$ $\vdash\mathscr{c}\rightarrowtail A$
$\mathsf{R1}_{\vee}^{\rightarrowtail}$ $\vdash\mathscr{c}\rightarrowtail A\vee
B$ $\mathcal{D}^{\prime}$ $\vdash\mathscr{d}\rightarrowtail B$
$\mathsf{R2}_{\vee}^{\rightarrowtail}$ $\vdash\mathscr{d}\rightarrowtail A\vee
B$ $\mathscr{b}\vDash\mathscr{c}\vee\mathscr{d}$
$\mathsf{R}_{\cup}^{\rightarrowtail}$ $\vdash\mathscr{b}\rightarrowtail A\vee
B$

Let $L=\mathscr{b}\leftarrowtail A\vee B$ and $\leadsto_{0}$-decomposition be
as follows:

$\vdash\mathscr{b}\leftarrowtail A\vee B\ \ \ \leadsto_{0}\ \ \
\\{\vdash\mathscr{b}\leftarrowtail A,\vdash\mathscr{b}\leftarrowtail B\\}.$

Since $\vdash\mathscr{b}\leftarrowtail A,\vdash\mathscr{b}\leftarrowtail
B\in\Phi^{\prime}$, both $\vdash\mathscr{b}\leftarrowtail A$ and
$\vdash\mathscr{b}\leftarrowtail B$ are derivable by two derivations, call
them $\mathcal{D}$ and $\mathcal{D}^{\prime}$. Then $\mathscr{b}\leftarrowtail
A\vee B$ can be shown derivable in $\mathbf{GsCPL_{0}}$ as follows:

$\mathcal{D}$ $\vdash\mathscr{b}\leftarrowtail A$ $\mathcal{D}^{\prime}$
$\vdash\mathscr{b}\leftarrowtail B$ $\mathsf{R}_{\vee}^{\leftarrowtail}$
$\vdash\mathscr{b}\leftarrowtail A\vee B$

Let $L=\mathscr{b}\rightarrowtail A\wedge B$ and $\leadsto_{0}$-decomposition
be as follows:

$\vdash\mathscr{b}\rightarrowtail A\wedge B\ \ \ \leadsto_{0}\ \ \
\\{\vdash\mathscr{b}\rightarrowtail A,\vdash\mathscr{b}\rightarrowtail B\\}.$

Since $\vdash\mathscr{b}\rightarrowtail A,\vdash\mathscr{b}\rightarrowtail
B\in\Phi^{\prime}$, both $\vdash\mathscr{b}\rightarrowtail A$ and
$\vdash\mathscr{b}\rightarrowtail B$ are derivable by two derivations, call
them $\mathcal{D}$ and $\mathcal{D}^{\prime}$. Then,
$\mathscr{b}\rightarrowtail A\wedge B$ can be shown derivable in
$\mathbf{GsCPL_{0}}$ as follows:

$\mathcal{D}$ $\vdash\mathscr{b}\rightarrowtail A$ $\mathcal{D}^{\prime}$
$\vdash\mathscr{b}\rightarrowtail B$ $\mathsf{R}_{\vee}^{\leftarrowtail}$
$\vdash\mathscr{b}\rightarrowtail A\wedge B$

Let $L=\mathscr{b}\leftarrowtail A\wedge B$ and $\leadsto_{0}$-decomposition
be as follows:

$\vdash\mathscr{b}\leftarrowtail A\wedge B\ \ \ \leadsto_{0}\ \ \ \
\\{\vdash\mathscr{c}\leftarrowtail A,\vdash\mathscr{d}\leftarrowtail B\\}$

where $\mathscr{c}\wedge\mathscr{d}\vDash\mathscr{b}$. Since
$\vdash\mathscr{c}\leftarrowtail A,\vdash\mathscr{d}\leftarrowtail
B\in\Phi^{\prime}$, both $\vdash\mathscr{c}\leftarrowtail A$ and
$\vdash\mathscr{d}\leftarrowtail B$ are derivable by two derivations, call
them $\mathcal{D}$ and $\mathcal{D}^{\prime}$. Then,
$\mathscr{b}\leftarrowtail A\wedge B$ can be shown derivable in
$\mathbf{GsCPL_{0}}$ as follows:

$\mathcal{D}$ $\vdash\mathscr{c}\leftarrowtail A$
$\mathsf{R1}_{\wedge}^{\leftarrowtail}$ $\vdash\mathscr{c}\leftarrowtail
A\wedge C$ $\mathcal{D}^{\prime}$ $\vdash\mathscr{d}\leftarrowtail B$
$\mathsf{R2}_{\wedge}^{\leftarrowtail}$ $\vdash\mathscr{d}\leftarrowtail
A\wedge B$ $\mathscr{c}\wedge\mathscr{d}\vDash\mathscr{b}$
$\mathsf{R}_{\cap}^{\leftarrowtail}$ $\vdash\mathscr{b}\leftarrowtail A\wedge
B$

Let $L=\mathscr{b}\rightarrowtail\mathbf{C}^{q}A$ and
$\leadsto_{0}$-decomposition be as follows:

$\vdash\mathscr{b}\rightarrowtail\mathbf{C}^{q}A\ \ \ \leadsto_{0}\ \ \
\\{\vdash\mathscr{c}\rightarrowtail A\\}$

where $\mu(\llbracket\mathscr{c}\rrbracket)\geq q$. Since
$\vdash\mathscr{c}\rightarrowtail A\in\Phi^{\prime}$,
$\vdash\mathscr{c}\rightarrowtail A$ is derivable by a derivation, call it
$\mathcal{D}$. Then, $\vdash\mathscr{b}\rightarrowtail\mathbf{C}^{q}A$ can be
shown derivable in $\mathbf{GsCPL_{0}}$ as follows:

$\mathcal{D}$ $\vdash\mathscr{c}\rightarrowtail A$
$\mu(\llbracket\mathscr{c}\rrbracket)\geq q$
$\mathsf{R}_{\mathbf{C}}^{\rightarrowtail}$
$\vdash\mathscr{b}\rightarrowtail\mathbf{C}^{q}A$

Let $L=\mathscr{b}\leftarrowtail\mathbf{C}^{q}A$ and
$\leadsto_{0}$-decomposition be as follows:

$\vdash\mathscr{b}\leftarrowtail\mathbf{C}^{q}A\ \ \ \leadsto_{0}\ \ \
\\{\vdash\mathscr{c}\leftarrowtail A\\}$

where $\mu(\llbracket\mathscr{c}\rrbracket)<q$. Since
$\vdash\mathscr{c}\leftarrowtail A\in\Phi^{\prime}$,
$\vdash\mathscr{c}\leftarrowtail A$ is derivable by a derivation, call it
$\mathcal{D}$. Then, $\vdash\mathscr{b}\leftarrowtail\mathbf{C}^{q}A$ can be
shown derivable in $\mathbf{GsCPL_{0}}$ as follows:

$\mathcal{D}$ $\vdash\mathscr{c}\leftarrowtail A$
$\mu(\llbracket\mathscr{c}\rrbracket)<q$
$\mathsf{R}_{\mathbf{C}}^{\leftarrowtail}$
$\vdash\mathscr{b}\leftarrowtail\mathbf{C}^{q}A$

Let $L=\mathscr{b}\rightarrowtail\mathbf{D}^{q}A$ and
$\leadsto_{0}$-decomposition be as follows:

$\vdash\mathscr{b}\rightarrowtail\mathbf{D}^{q}A\ \ \ \leadsto_{0}\ \ \
\\{\vdash\mathscr{c}\leftarrowtail A\\}$

where $\mu(\llbracket\mathscr{c}\rrbracket)<q$. Since
$\vdash\mathscr{c}\leftarrowtail A\in\Phi^{\prime}$,
$\vdash\mathscr{c}\leftarrowtail A$ is derivable by a derivation, call it
$\mathcal{D}$. Then, $\vdash\mathscr{b}\rightarrowtail\mathbf{D}^{q}A$ can be
shown derivable in $\mathbf{GsCPL_{0}}$ as follows:

$\mathcal{D}$ $\vdash\mathscr{c}\leftarrowtail A$
$\mu(\llbracket\mathscr{c}\rrbracket)<q$
$\mathsf{R}_{\mathbf{D}}^{\rightarrowtail}$
$\vdash\mathscr{b}\rightarrowtail\mathbf{D}^{q}A$

Let $L=\mathscr{b}\leftarrowtail\mathbf{D}^{q}A$ and
$\leadsto_{0}$-decomposition be as follows:

$\vdash\mathscr{b}\leftarrowtail\mathbf{D}^{q}A\ \ \ \leadsto_{0}\ \ \
\\{\vdash\mathscr{c}\rightarrowtail A\\}$

where $\mu(\llbracket\mathscr{c}\rrbracket)\geq q$. Since
$\vdash\mathscr{c}\rightarrowtail A\in\Phi^{\prime}$,
$\vdash\mathscr{c}\rightarrowtail A$ is derivable by a derivation, call it
$\mathcal{D}$. Then, $\vdash\mathscr{b}\leftarrowtail\mathbf{D}^{q}A$ can be
shown derivable in $\mathbf{GsCPL_{0}}$ as follows:

$\mathcal{D}$ $\vdash\mathscr{c}\rightarrowtail A$
$\mu(\llbracket\mathscr{c}\rrbracket)\geq q$
$\mathsf{R}_{\mathbf{D}}^{\leftarrowtail}$
$\vdash\mathscr{b}\leftarrowtail\mathbf{D}^{q}A$

Let $L=\mathscr{b}\rightarrowtail A$ and $\leadsto_{0}$-decomposition be as
follows

$\vdash\mathscr{b}\rightarrowtail A\ \ \ \leadsto_{0}\ \ \ \\{\\}$

where $\mu(\llbracket\mathscr{c}\rrbracket)=0$. Then,
$\mathscr{b}\rightarrowtail A$ can be shown derivable in $\mathbf{GsCPL_{0}}$
as follows:

$\mu(\llbracket\mathscr{b}\rrbracket)=0$ $\mathsf{R_{\mu}^{\rightarrowtail}}$
$\vdash\mathscr{b}\rightarrowtail A$

Let $L=\mathscr{b}\leftarrowtail A$ and $\leadsto_{0}$-decomposition be as
follows:

$\vdash\mathscr{b}\leftarrowtail A\ \ \ \leadsto_{0}\ \ \ \\{\\}$

where $\mu(\llbracket\mathscr{c}\rrbracket)=1$. Then,
$\mathscr{b}\leftarrowtail A$ can be shown derivable in $\mathbf{GsCPL_{0}}$
as follows:

$\mu(\llbracket\mathscr{b}\rrbracket)=1$ $\mathsf{R_{\mu}^{\leftarrowtail}}$
$\vdash\mathscr{b}\leftarrowtail A$

Notice that if $\vdash\mathscr{b}\rightarrowtail\mathbf{D}^{0}A$ is derivable,
by Lemma 2 $\vDash\mathscr{b}\rightarrowtail\mathbf{D}^{0}A$, which is
$\llbracket\mathscr{b}\rrbracket\subseteq\llbracket\mathbf{D}^{0}A\rrbracket$.
But $\llbracket\mathbf{D}^{0}A\rrbracket=0$, so
$\llbracket\mathscr{b}\rrbracket\subseteq\emptyset$, which is
$\llbracket\mathscr{b}\rrbracket=0$. Thus, when
$\vdash\mathscr{b}\rightarrowtail\mathbf{D}^{0}A$ is derivable, it cannot be
decomposed as follows:
$\vdash\mathscr{b}\rightarrowtail\mathbf{D}^{0}A\leadsto_{0}\\{\vdash\bot\\}$.
The same holds for $\mathscr{b}\leftarrowtail\mathbf{C}^{0}A$. Therefore, all
the possible forms of $\leadsto_{0}$ have been considered. ∎

The Completeness of $\mathbf{GsCPL_{0}}$. Putting these results together, it
is possible to conclude that $\mathbf{GsCPL_{0}}$ is complete with respect to
the semantics of $\textsf{{CPL}}_{0}$. See 5

###### Proof.

If the sequent is valid, by Lemma 25, it has a _valid_ $\leadsto$-normal form.
For Lemma LABEL:NormValDer, a $\leadsto$-normal form is valid if and only if
it is derivable, so the given $\leadsto$-normal form must be derivable as
well. Therefore, by Lemma 26, the given (valid) sequent must be derivable in
$\mathbf{GsCPL_{0}}$. ∎

###  A.3 $\textsf{{CPL}}_{0}$-validity is in $\textsf{P}^{\sharp\mathtt{SAT}}$

######  Lemma 27.

For every _closed_ formula of $\textsf{{CPL}}_{0}$, call it $A$, either
$\llbracket A\rrbracket$ = $2^{\omega}$ or $\llbracket A\rrbracket$ =
$\emptyset$.

###### Proof.

The proof is by induction on the structure of $A$.

  * •

_Base case._ If $A$ = $\mathbf{C}^{q}B$ or $A$ = $\mathbf{D}^{q}B$, then for
Definition 3.1 either $\llbracket A\rrbracket$ = $2^{\omega}$ or $\llbracket
A\rrbracket$ = $\emptyset$.

  * •

_Inductive case_. There are four possible cases:

$A=\neg B$. Since $B$ is a closed formula, for IH, either $\llbracket
B\rrbracket$ = $2^{\omega}$ or $\llbracket B\rrbracket$ = $\emptyset$. In the
former case,

$\llbracket A\rrbracket=\big{(}2^{\omega}\ –\ \llbracket
B\rrbracket\big{)}=\big{(}2^{\omega}\ –\ 2^{\omega}\big{)}=\emptyset.$

In the latter case,

$\llbracket A\rrbracket=\big{(}2^{\omega}\ –\ \llbracket
B\rrbracket\big{)}=\big{(}2^{\omega}\ –\ \emptyset\big{)}=2^{\omega}.$

$A=B\vee C$. Since $B$ and $C$ are closed formulas, for IH, both $\llbracket
B\rrbracket$ and $\llbracket C\rrbracket$ are either $2^{\omega}$ or
$\emptyset$. If both $\llbracket B\rrbracket$ and $\llbracket C\rrbracket$ are
$\emptyset$, then

$\llbracket A\rrbracket=\llbracket B\vee C\rrbracket=\llbracket
B\rrbracket\cup\llbracket C\rrbracket=\emptyset.$

Otherwise,

$\llbracket A\rrbracket=\llbracket B\vee C\rrbracket=\llbracket
B\rrbracket\cup\llbracket C\rrbracket=2^{\omega}.$

$A=B\wedge C$. Since $B$ and $C$ are closed formulas, for IH, both $\llbracket
B\rrbracket$ and $\llbracket C\rrbracket$ are either $2^{\omega}$ or
$\emptyset$. Thus, if both $\llbracket B\rrbracket$ and $\llbracket
C\rrbracket$ are $2^{\omega}$, then:

$\llbracket A\rrbracket=\llbracket B\wedge C\rrbracket=\llbracket
B\rrbracket\cap\llbracket C\rrbracket=2^{\omega}.$

Otherwise,

$\llbracket A\rrbracket=\llbracket B\wedge C\rrbracket=\llbracket
B\rrbracket\cap\llbracket C\rrbracket=\emptyset.$

$A=\mathbf{C}^{q}B$ or $A=\mathbf{D}^{q}B$. Then the proof is trivial for
Definition 3.1 of $\mathbf{C}$\- and $\mathbf{D}$-formulas.

∎

##  Appendix B Proofs from Section 4

###  B.1 Characterizing the Semantics of CPL using Boolean Formulas

######  Definition B.1 (Named Boolean Formulas).

_Named Boolean formulas_ are defined by the following grammar:

$\mathscr{b},\mathscr{c}:=\mathscr{x}_{i}^{a}\;\;\mbox{\Large{$\mid$}}\;\;\top\;\;\mbox{\Large{$\mid$}}\;\;\bot\;\;\mbox{\Large{$\mid$}}\;\;\lnot\mathscr{b}\;\;\mbox{\Large{$\mid$}}\;\;\mathscr{b}\land\mathscr{c}\;\;\mbox{\Large{$\mid$}}\;\;\mathscr{b}\vee\mathscr{c}$

The interpretation $\llbracket\mathscr{b}\rrbracket_{X}$ of a Boolean formula
with $\mathrm{FN}(\mathscr{b})\subseteq X$ is defined in a straightforward way
following Definition 4.3.

$\displaystyle\llbracket\mathscr{x}_{i}^{a}\rrbracket_{X}$
$\displaystyle:=\\{f:X\rightarrow 2^{\omega}\ |\ f(a)(\mathbf{i})=1\\}$
$\displaystyle\llbracket\top\rrbracket_{X}$ $\displaystyle:=(2^{\omega})^{X}$
$\displaystyle\llbracket\bot\rrbracket_{X}$ $\displaystyle:=\emptyset^{X}$

$\displaystyle\llbracket\neg\mathscr{b}\rrbracket_{X}$
$\displaystyle:=(2^{\omega})^{X}–\ \llbracket\mathscr{b}\rrbracket_{X}$
$\displaystyle\llbracket\mathscr{b}\wedge\mathscr{c}\rrbracket_{X}$
$\displaystyle:=\llbracket\mathscr{b}\rrbracket_{X}\cap\llbracket\mathscr{c}\rrbracket_{X}$
$\displaystyle\llbracket\mathscr{b}\vee\mathscr{c}\rrbracket_{X}$
$\displaystyle:=\llbracket\mathscr{b}\rrbracket_{X}\cup\llbracket\mathscr{c}\rrbracket_{X}.$

######  Lemma 28.

Any named Boolean formula $\mathscr{b}$ with
$\mathrm{FN}(\mathscr{b})\subseteq X\cup\\{a\\}$ admits an $a$-decomposition
in $X$.

###### Proof.

We will actually prove a stronger statement: any named Boolean formula
$\mathscr{b}$ admits an $a$-decomposition
$\bigvee_{i=1}^{k}\mathscr{d}_{i}\land\mathscr{e}_{i}$ where
$\llbracket\bigvee_{i=1}^{j}\mathscr{e}_{i}\rrbracket_{X}=\llbracket\top\rrbracket_{X}$.
We argue by induction on $\mathscr{b}$:

  * •

if $\mathscr{b}=\mathscr{x}_{i}^{a}$ or
$\mathscr{b}=\lnot\mathscr{x}_{i}^{a}$, then $k=1$,
$\mathscr{d}_{i}=\mathscr{b}$ and $\mathscr{e}_{i}=\top$

  * •

if $\mathscr{b}=\mathscr{x}_{i}^{b}$, where $b\neq a$, then $k=2$,
$\mathscr{d}_{0}=\top,\mathscr{d}_{1}=\bot$ and
$\mathscr{e}_{0}=\mathscr{b},\mathscr{e}_{1}=\lnot\mathscr{b}$

  * •

if $\mathscr{b}=\mathscr{b}_{1}\vee\mathscr{b}_{2}$ thenm by IH,
$\mathscr{b}_{1}=\bigvee_{i=0}^{k_{1}-1}\mathscr{d}^{1}_{i}\land\mathscr{e}^{1}_{i}$
and
$\mathscr{b}_{2}=\bigvee_{j=0}^{k_{2}-1}\mathscr{d}^{2}_{j}\land\mathscr{e}^{2}_{j}$.
Then,

$\displaystyle\mathscr{b}$
$\displaystyle\equiv\left(\bigvee_{i=0}^{k_{1}-1}\mathscr{d}^{1}_{i}\land\mathscr{e}^{1}_{i}\right)\vee\left(\bigvee_{j=0}^{k_{2}-1}\mathscr{d}^{2}_{j}\land\mathscr{e}^{2}_{j}\right)$
$\displaystyle\equiv\left(\bigvee_{i=0}^{k_{1}-1}\mathscr{d}^{1}_{i}\land\mathscr{e}^{1}_{i}\land\top\right)\vee\left(\bigvee_{j=0}^{k_{2}-1}\mathscr{d}^{2}_{j}\land\mathscr{e}^{2}_{j}\land\top\right)$
$\displaystyle\equiv\left(\bigvee_{i=0}^{k_{1}-1}\mathscr{d}^{1}_{i}\land\mathscr{e}^{1}_{i}\land\bigvee_{j}\mathscr{e}^{2}_{j}\right)\vee\left(\bigvee_{j=0}^{k_{2}-1}\mathscr{d}^{2}_{j}\land\mathscr{e}^{2}_{j}\land\bigvee_{i}\mathscr{e}^{1}_{i}\right)$
$\displaystyle\equiv\left(\bigvee_{i=0,j=0}^{k_{1}-1,k_{2}-1}(\mathscr{d}^{1}_{i}\land\mathscr{e}^{1}_{i}\land\mathscr{e}^{2}_{j})\right)\vee\left(\bigvee_{j=0,i=0}^{k_{2}-1,k_{1}-1}\mathscr{d}^{2}_{j}\land\mathscr{e}^{2}_{j}\land\mathscr{e}^{1}_{i}\right)$
$\displaystyle\equiv\bigvee_{i=0,j=0}^{k_{1}-1,k_{2}-1}(\mathscr{d}^{1}_{i}\vee\mathscr{d}^{2}_{j})\land(\mathscr{e}^{1}_{i}\land\mathscr{e}^{2}_{j}).$

Let $k=k_{1}\cdot k_{2}$. We can identify any $l\leq k-1$ with a pair $(i,j)$,
$i<k_{1}$ and $j<k_{2}$. Let
$\mathscr{d}_{i,j}=\mathscr{d}^{1}_{i}\lor\mathscr{d}^{2}_{j}$ and
$\mathscr{e}_{i,j}=\mathscr{e}^{1}_{i}\lor\mathscr{e}^{2}_{j}$. We have then
that

$\mathscr{b}=\bigvee_{i=0,j=0}^{k_{1}-1,k_{2}-1}\mathscr{d}_{i,j}\land\mathscr{e}_{i,j}.$

Observe that for $(i,j)\neq(i^{\prime},j^{\prime})$,
$\mathscr{e}_{i,j}\land\mathscr{e}_{i^{\prime},j^{\prime}}\equiv\bot$.
Moreover,
$\bigvee_{i,j}\mathscr{e}_{i,j}\equiv\bigvee_{i,j}\mathscr{e}^{1}_{i}\lor\mathscr{e}^{2}_{j}\equiv(\bigvee_{i}\mathscr{e}^{1}_{i})\lor(\bigvee_{j}\mathscr{e}^{2}_{j})\equiv\top\lor\top\equiv\top$.

  * •

if $\mathscr{b}=\mathscr{b}_{1}\land\mathscr{b}_{2}$, then, by IH,
$\mathscr{b}_{1}\equiv\bigvee_{i=0}^{k_{1}-1}\mathscr{d}^{1}_{i}\land\mathscr{e}^{1}_{i}$
and
$\mathscr{b}_{2}\equiv\bigvee_{j=0}^{k_{2}-1}\mathscr{d}^{2}_{j}\land\mathscr{e}^{2}_{j}$.
Then,

$\displaystyle\mathscr{b}$
$\displaystyle\equiv\left(\bigvee_{i=0}^{k_{1}-1}\mathscr{d}^{1}_{i}\land\mathscr{e}^{1}_{i}\right)\land\left(\bigvee_{j=0}^{k_{2}-1}\mathscr{d}^{2}_{j}\land\mathscr{e}^{2}_{j}\right)$
$\displaystyle\equiv\bigvee_{i=0,j=0}^{k_{1}-1,k_{2}-1}\mathscr{d}^{1}_{i}\land\mathscr{e}^{1}_{i}\land\mathscr{d}^{2}_{j}\land\mathscr{e}^{2}_{j}$
$\displaystyle\equiv\bigvee_{i=0,j=0}^{k_{1}-1,k_{2}-1}(\mathscr{d}^{1}_{i}\land\mathscr{d}^{2}_{j})\land(\mathscr{e}^{1}_{i}\land\mathscr{e}^{2}_{j}).$

As in the case above let $k_{1}\cdot k_{2}$. We can identify any $l\leq k-1$
with a pair $(i,j)$, $i<k_{1}$ and $j<k_{2}$. Let
$\mathscr{d}_{i,j}=\mathscr{d}^{1}_{i}\land\mathscr{d}^{2}_{j}$ and
$\mathscr{e}_{i,j}=\mathscr{e}^{1}_{i}\land\mathscr{e}^{2}_{j}$. We have then
that

$\mathscr{b}\equiv\bigvee_{i=0,j=0}^{k_{1}-1,k_{2}-1}\mathscr{d}_{i,j}\land\mathscr{e}_{i,j}.$

As in the previous case we have that for $(i,j)\neq(i^{\prime},j^{\prime})$,
$\mathscr{e}_{i,j}\land\mathscr{e}_{i^{\prime},j^{\prime}}\equiv\bot$ and
$\bigvee_{i,j}\mathscr{e}_{i,j}\equiv\bigvee_{i,j}\mathscr{e}^{1}_{i}\land\mathscr{e}^{2}_{j}\equiv(\bigvee_{i}\mathscr{e}^{1}_{i})\land(\bigvee_{j}\mathscr{e}^{2}_{j})\equiv\top\land\top\equiv\top$.

∎

See 8

###  B.2 The Proof Theory of CPL

######  Definition B.2 (Named External Hypothesis).

A _named external hypothesis_ is an expression of one of the following forms:

  * •

$\vDash\\{a\\}\in X$

  * •

$\mu\big{(}\llbracket\mathscr{b}\rrbracket_{X}\big{)}=0$ or
$\mu\big{(}\llbracket\mathscr{b}\rrbracket_{X}\big{)}=1$

  * •

$\mathscr{b}\vDash^{X}\mathscr{c}$

  * •

$\mathscr{b}\vDash^{X}\bigvee\\{\mathscr{c}_{i}\ |\
\mu\big{(}\llbracket\mathscr{d}_{i}\rrbracket_{Y}\big{)}$ $\triangleright$
$q\\}$, $\bigvee\\{\mathscr{c}_{i}$ $|$
$\mu\big{(}\llbracket\mathscr{d}_{i}\rrbracket_{Y}\big{)}\triangleright
q\\}\vDash^{X}\mathscr{b}$, with $\triangleright\in\\{\geq,\leq,>,<,=\\}$

where $i\in\mathbb{N},$ $X$ and $Y$ are name sets,
$\mathscr{b},\mathscr{c}_{i},\mathscr{d}_{i}$ are named Boolean formulas, and
$q\in\mathbb{Q}_{[0,1]}$.

######  Definition B.3 (Named Labelled Formulas).

A _named labelled formula_ is a formula of the form
$\mathscr{b}\rightarrowtail A$ or $\mathscr{b}\leftarrowtail A$, such that $A$
is a formula of CPL and $\mathscr{b}$ is a named Boolean formula.

For the sake of simplicity, given a labelled formula $L$ =
$\mathscr{b}\rightarrowtail A$ or $L$ = $\mathscr{b}\leftarrowtail A$, let us
introduce the notion of $\mathrm{FN}(L)$ =
$\mathrm{FN}(\mathscr{b})\cup\mathrm{FN}(A)$.

######  Definition B.4 (Named Sequent).

A _named sequent_ of $\mathbf{GsCPL}$ is an expression of the form
$\vdash^{X}L$, where $L$ is a named labelled formula, and
$\mathrm{FN}(L)\subseteq X$.

Let us now define a one-sided, single-succedent, and labelled sequent
calculus, call it $\mathbf{GsCPL}$.

######  Definition B.5 (The Proof System $\mathbf{GsCPL}$).

$\mathbf{GsCPL}$ is defined by the set of rules displayed in Fig. 7.

Initial Sequents $\vDash\\{a\\}\in X$
$\mathscr{b}\vDash^{X}\mathscr{x}_{i}^{a}$ $\mathsf{Ax1}$
$\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{i}_{a}$ $\vDash\\{a\\}\in X$
$\mathscr{x}_{i}^{a}\vDash^{X}\mathscr{b}$ $\mathsf{Ax2}$
$\vdash^{X}\Delta,\mathscr{b}\leftarrowtail\mathbf{i}_{a}$ Union and
Intersection Rules $\vdash^{X}\mathscr{c}\rightarrowtail A$
$\vdash^{X}\mathscr{d}\rightarrowtail A$
$\mathscr{b}\vDash^{X}\mathscr{c}\lor\mathscr{d}$
$\mathsf{R}_{\cup}^{\rightarrowtail}$ $\vdash^{X}\mathscr{b}\rightarrowtail A$
$\vdash^{X}\mathscr{c}\leftarrowtail A$ $\vdash^{X}\mathscr{d}\leftarrowtail
A$ $\mathscr{c}\land\mathscr{d}\vDash^{X}\mathscr{b}$
$\mathsf{R}_{\cap}^{\leftarrowtail}$ $\vdash^{X}\mathscr{b}\leftarrowtail A$
Logical Rules $\vdash^{X}\mathscr{c}\leftarrowtail A$
$\mathscr{b}\vDash^{X}\lnot\mathscr{c}$ $\mathsf{R}_{\neg}^{\rightarrowtail}$
$\vdash^{X}\mathscr{b}\rightarrowtail\neg A$
$\vdash^{X}\mathscr{c}\rightarrowtail A$
$\lnot{\mathscr{c}}\vDash^{X}\mathscr{b}$ $\mathsf{R}_{\neg}^{\leftarrowtail}$
$\vdash^{X}\mathscr{b}\leftarrowtail\neg A$
$\vdash^{X}\mathscr{b}\rightarrowtail A$
$\mathsf{R1}_{\vee}^{\rightarrowtail}$ $\vdash^{X}\mathscr{b}\rightarrowtail
A\vee B$ $\vdash^{X}\mathscr{b}\rightarrowtail B$
$\mathsf{R2}_{\vee}^{\rightarrowtail}$ $\vdash^{X}\mathscr{b}\rightarrowtail
A\vee B$ $\vdash^{X}\mathscr{b}\leftarrowtail A$
$\vdash^{X}\mathscr{b}\leftarrowtail B$ $\mathsf{R}_{\vee}^{\leftarrowtail}$
$\vdash^{X}\mathscr{b}\leftarrowtail A\vee B$
$\vdash^{X}\mathscr{b}\rightarrowtail A$ $\vdash^{X}\mathscr{b}\rightarrowtail
B$ $\mathsf{R}_{\wedge}^{\rightarrowtail}$
$\vdash^{X}\mathscr{b}\rightarrowtail A\wedge B$
$\vdash^{X}\mathscr{b}\leftarrowtail A$
$\mathsf{R1^{\leftarrowtail}_{\wedge}}$ $\vdash^{X}\mathscr{b}\leftarrowtail
A\wedge B$ $\vdash^{X}\mathscr{b}\leftarrowtail B$
$\mathsf{R2^{\leftarrowtail}_{\wedge}}$ $\vdash_{X}\mathscr{b}\leftarrowtail
A\wedge B$ Counting Rules $\mu(\llbracket\mathscr{b}\rrbracket_{X})=0$
$\mathsf{R_{\mu}^{\rightarrowtail}}$ $\vdash^{X}\mathscr{b}\rightarrowtail A$
$\mu(\llbracket\mathscr{b}\rrbracket_{X})=1$
$\mathsf{R_{\mu}^{\leftarrowtail}}$ $\vdash^{X}\mathscr{b}\leftarrowtail A$
$\vdash^{X\cup\\{a\\}}\mathscr{c}\rightarrowtail A$
$\mathscr{b}\vDash^{X}\bigvee_{i}\\{\mathscr{e}_{i}\ |\
\mu(\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}})\geq q\\}$
$\mathsf{R}_{\mathbf{C}}^{\rightarrowtail}$
$\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{C}^{q}_{a}A$
$\vdash^{X\cup\\{a\\}}\mathscr{c}\leftarrowtail A$
$\bigvee_{i}\\{\mathscr{e}_{i}\ |\
\mu(\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}})\geq
q\\}\vDash^{X}\mathscr{b}$ $\mathsf{R}_{\mathbf{C}}^{\leftarrowtail}$
$\vdash^{X}\mathscr{b}\leftarrowtail\mathbf{C}^{q}_{a}A$
$\vdash^{X\cup\\{a\\}}\mathscr{c}\leftarrowtail A$
$\mathscr{b}\vDash^{X}\bigvee_{i}\\{\mathscr{e}_{i}\ |\
\mu(\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}})<q\\}$
$\mathsf{R}_{\mathbf{D}}^{\rightarrowtail}$
$\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{D}^{q}_{a}A$
$\vdash^{X\cup\\{a\\}}\mathscr{c}\rightarrowtail A$
$\bigvee_{i}\\{\mathscr{e}_{i}\ |\
\mu(\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}})<q\\}\vDash^{X}\mathscr{b}$
$\mathsf{R}_{\mathbf{D}}^{\leftarrowtail}$
$\vdash^{X}\mathscr{b}\leftarrowtail\mathbf{D}^{q}_{a}A$ where
$\bigvee_{i}\mathscr{e}_{i}\wedge\mathscr{d}_{i}$ is an $a$-decomposition of
$\mathscr{c}$.

Figure 7: Proof system for CPL.

For the sake of simplicity, let $\mathsf{R_{\mu}^{\rightarrowtail}}$ and
$\mathsf{R_{\mu}^{\leftarrowtail}}$ be called $\mu$-rules. The notions of
derivation and of derivation height for $\mathbf{GsCPL}$ are defined in a
standard way.

######  Definition B.6 (Derivations in $\mathbf{GsCPL}$).

A _derivation in $\mathbf{GsCPL}$_ is either an initial sequent or a
$\mu$-rule, or it is obtained by applying one of the remaining rules to
derivations concluding its premisses.

######  Definition B.7 (Derivation Height in $\mathbf{GsCPL}$).

The _height of a derivation in $\mathbf{GsCPL}$_ is the greatest number of
successive applications of rules in it, where initial sequents and $\mu$-rules
have height 0.

$\mathbf{GsCPL}$ si sound and complete with respect to the semantics of CPL.
Let us start by presenting the notions of validity for labelled formulas and
sequents of $\mathbf{GsCPL}$. Similarly to $\textsf{{CPL}}_{0}$, given a named
Boolean formula $\mathscr{b}$, a formula of CPL, call it $A$, and an $X$, with
$\mathrm{FN}(\mathscr{b})\cup\mathrm{FN}(A)\subseteq X$, the labelled formula
$\mathscr{b}\rightarrowtail A$ (resp. $\mathscr{b}\leftarrowtail A$) is _X-
valid_ , when $\llbracket\mathscr{b}\rrbracket_{X}\subseteq\llbracket
A\rrbracket_{X}$ (resp. $\llbracket
A\rrbracket_{X}\subseteq\llbracket\mathscr{b}\rrbracket_{X}$). Formally,

######  Definition B.8 (Validity of Labelled Formulas).

The validity of a labelled formula is defined as follows:

  * •

$\mathscr{b}\rightarrowtail A$ is $X$-_valid_ iff
$\llbracket\mathscr{b}\rrbracket_{X}\subseteq\llbracket A\rrbracket_{X}$

  * •

$\mathscr{b}\leftarrowtail A$ is $X$-_valid_ iff $\llbracket
A\rrbracket_{X}\subseteq\llbracket\mathscr{b}\rrbracket_{X}$.

An external hypothesis containing $\mathscr{b}_{1},\dots,\mathscr{b}_{n}$
named Boolean variables is valid if and only if, for every $X$ such that
$\bigcup_{i=1}^{m}\mathrm{FN}(\mathscr{b}_{i})\subseteq X$ the hypothesis is
valid. The notion of $X$-validity for external hypothesis is as predictable.
For example, $\mathscr{b}\vDash^{X}\mathscr{x}_{\mathbf{i}}^{a}$ is valid if
and only if
$\mathrm{FN}(\mathscr{b})\cup\mathrm{FN}(\mathscr{x}_{\mathbf{i}}^{a})\subseteq
X$ and
$\llbracket\mathscr{b}\rrbracket_{X}\subseteq\llbracket\mathscr{x}_{\mathbf{i}}^{a}\rrbracket_{X}$
and $\mathscr{x}_{\mathbf{i}}^{a}\vDash^{X}\mathscr{b}$ is valid if and only
if
$\mathrm{FN}(\mathscr{b})\cup\mathrm{FN}(\mathscr{x}_{\mathbf{i}}^{a})\subseteq
X$ and
$\llbracket\mathscr{x}_{\mathbf{i}}^{a}\rrbracket_{X}\subseteq\llbracket\mathscr{b}\rrbracket_{X}$.
A named sequent $\vdash^{X}L$ is valid, denoted $\vDash^{X}L$, if $L$ is
$X$-valid.

######  Definition B.9 (Validity of Sequents).

A sequent of $\mathbf{GsCPL}$, $\vdash^{X}L$, is _valid_ if and only if
$\vDash^{X}L$. A set of such sequents,
$\\{\vdash^{X_{1}}L_{1},\dots,\vdash^{X_{m}}L_{m}\\}$ is _valid_ if and only
if all its sequents are valid.

######  Notation 1.

We write $A\equiv_{X}B$ when $\llbracket A\rrbracket_{X}=\llbracket
B\rrbracket_{X}$.

######  Theorem 29 (Soundness of $\mathbf{GsCPL}$).

If a sequent is derivable in $\mathbf{GsCPL}$, then it is valid.

###### Proof.

The proof is by induction on the height of the derivation of $\vdash^{X}L$,
call it $n$.

  * •

_Base case._ The sequent is either an initial sequent or it is derived by a
$\mu$-rule. Let us consider the case of $\mathsf{Ax1}$ only. The other cases
are analogously proved.

$\vDash\\{a\\}\in X$ $\mathscr{b}\vDash^{X}\mathscr{x}_{\mathbf{i}}^{a}$
$\mathsf{Ax1}$ $\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{i}_{a}$

As seen, if $\mathscr{b}\vDash^{X}\mathscr{x}_{\mathbf{i}}^{a}$, then
$\mathrm{FN}(\mathscr{b})\cup\mathrm{FN}(\mathscr{x}_{\mathbf{i}}^{a})\subseteq
X$, and
$\llbracket\mathscr{b}\rrbracket_{X}\subseteq\llbracket\mathscr{x}_{\mathbf{i}}^{a}\rrbracket_{X}$,
which is $\llbracket\mathscr{b}\rrbracket_{X}\subseteq\\{f\in(2^{\omega})^{X}$
$|$ $f$($a$)($i$) = 1$\\}$. But then, for Definition 4.3,
$\llbracket\mathbf{i}_{a}\rrbracket_{X}$ = $\\{f\in(2^{\omega})^{X}$ $|$
$f$($a$)($i$) = 1$\\}$, so
$\llbracket\mathscr{b}\rrbracket_{X}\subseteq\llbracket\mathbf{i}_{a}\rrbracket_{X}$.
By Definition B.8, $\mathscr{b}\rightarrowtail\mathbf{i}_{a}$ is $X$-valid, so
$\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{i}_{a}$ must be valid as well.

The proof for $\mathsf{Ax2}$ proof is equivalent to the one for
$\mathsf{Ax1}$, whereas $\mu$-cases are treated similarly to the corresponding
proofs in $\mathbf{GsCPL_{0}}$.

  * •

_Inductive case._ Let us assume soundness to hold for derivations of height up
to $n$ and show it holds for derivations of height $n$+1. The proof is
equivalent to that for $\mathbf{GsCPL_{0}}$, so let us just consider a few
examples. All the other cases are similar.

$\mathsf{R}_{\vee}^{\leftarrowtail}$. The derivation has the following form:

$\vdots$ $\vdash^{X}\mathscr{b}\leftarrowtail A$ $\vdots$
$\vdash^{X}\mathscr{b}\leftarrowtail B$ $\mathsf{R}_{\vee}^{\leftarrowtail}$
$\vdash^{X}\mathscr{b}\leftarrowtail A\vee B$

For IH, the premisses are valid, so $\vDash^{X}\mathscr{b}\leftarrowtail A$
and $\vDash^{X}\mathscr{b}\leftarrowtail B$, which is $\llbracket
A\rrbracket_{X}\subseteq\llbracket\mathscr{b}\rrbracket_{X}$ and $\llbracket
B\rrbracket_{X}\subseteq\llbracket\mathscr{b}\rrbracket_{X}$. But then also
$\llbracket A\rrbracket_{X}\cup\llbracket
B\rrbracket_{X}\subseteq\llbracket\mathscr{b}\rrbracket_{X}$, which is
$\llbracket A\vee B\rrbracket_{X}\subseteq\llbracket\mathscr{b}\rrbracket_{X}$
and, thus, $\vdash^{X}\mathscr{b}\leftarrowtail A\vee B$ is valid.

$\mathsf{R}_{\mathbf{C}}^{\rightarrowtail}.$ Let
$\bigvee_{i}\mathscr{e}_{i}\wedge\mathscr{d}_{i}$ be an $a$-decomposition of
$\mathscr{c}$. Then, the derivation has the following form:

$\vdash^{X\cup\\{a\\}}\mathscr{c}\rightarrowtail A$
$\mathscr{b}\vDash^{X}\bigvee\\{\mathscr{e}_{i}\ |\
\mu(\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}})\geq q\\}$
$\mathsf{R}_{\mathbf{C}}^{\rightarrowtail}$
$\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{C}^{q}_{a}A$

For IH, $\mathscr{c}\rightarrowtail A$ is $X\cup\\{a\\}$-valid. Furthermore,
since $\mathscr{b}\vDash^{X}\bigvee\\{\mathscr{e}_{i}\ |\
\mu(\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}})\geq q\\}$,
$\llbracket\mathscr{b}\rrbracket_{X}\subseteq\bigcup_{i}\\{\llbracket\mathscr{e}_{i}\rrbracket_{X}$
$|$ $\mu$($\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}})\geq q\\}$, which is
by Lemma 8 and given that $\bigvee_{i}\mathscr{e}_{i}\wedge\mathscr{d}_{i}$ be
an $a$-decomposition of $\mathscr{c}$,
$\llbracket\mathscr{b}\rrbracket_{X}\subseteq\\{f\in(2^{\omega})^{X}\ |\
\mu(\Pi_{f}(\llbracket\mathscr{c}\rrbracket_{X\cup\\{a\\}}$)) $\geq q\\}$. But
then, since for IH,
$\llbracket\mathscr{c}\rrbracket_{X\cup\\{a\\}}\subseteq\llbracket
A\rrbracket_{X\cup\\{a\\}}$, also
$\llbracket\mathscr{b}\rrbracket_{X}\subseteq\\{f\in(2^{\omega})^{X}\ |\
\mu(\Pi_{f}(\llbracket A\rrbracket_{X\cup\\{a\\}}))\geq q\\}$ (monotonicity).
Thus, $\\{f\in(2^{\omega})^{X}\ |\ \mu(\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}}$))$\geq q\\}$ =
$\llbracket\mathbf{C}^{q}_{a}A\rrbracket_{X}$. Therefore,
$\llbracket\mathscr{b}\rrbracket_{X}\subseteq\llbracket\mathbf{C}^{q}_{a}A\rrbracket_{X}$,
which is $\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{C}^{q}_{a}A$ is valid.

$\mathsf{R}_{\mathbf{C}}^{\leftarrowtail}.$ Let
$\bigvee_{i}\mathscr{e}_{i}\wedge\mathscr{d}_{i}$ be an $a$-decomposition of
$\mathscr{c}$. Then, the derivation has the following form:

$\vdots$ $\vdash^{X\cup\\{a\\}}\mathscr{c}\leftarrowtail A$
$\bigvee\\{\mathscr{e}_{i}\ |\
\mu(\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}})\geq
q\\}\vDash^{X}\mathscr{b}$ $\mathsf{R}_{\mathbf{C}}^{\leftarrowtail}$
$\vdash^{X}\mathscr{b}\leftarrowtail\mathbf{C}^{q}_{a}A$

For IH, $\mathscr{c}\leftarrowtail A$ is $X\cup\\{a\\}$-valid. Furthermore,
$\bigcup_{i}\\{\llbracket\mathscr{e}_{i}\rrbracket_{X}\ |\
\mu(\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}})\geq
q\\}\subseteq\llbracket\mathscr{b}\rrbracket_{X}$, that, given
$a$-decomposition for $\mathscr{c}$ and Lemma 8, $\\{f\in(2^{\omega})^{X}\ |\
\mu(\Pi_{f}(\llbracket\mathscr{c}\rrbracket_{X\cup\\{a\\}}))\geq
q\\}\subseteq\llbracket\mathscr{b}\rrbracket_{X}$. For IH, $\llbracket
A\rrbracket_{X}$ $\subseteq$ $\llbracket\mathscr{c}\rrbracket_{X}$, so
$\\{f\in(2^{\omega})^{X}$ $|$ $\mu(\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}}))\geq
q\\}\subseteq\llbracket\mathscr{b}\rrbracket_{X}.$ Thus,
$\llbracket\mathbf{C}^{q}_{a}A\rrbracket_{X}\subseteq\llbracket\mathscr{b}\rrbracket_{X}$,
which is $\mathscr{b}\leftarrowtail\mathbf{C}^{q}_{a}A$ is $X$-valid and,
thus, $\vdash^{X}\mathscr{b}\leftarrowtail\mathbf{C}^{q}_{a}A$ is valid.

$\mathsf{R}_{\mathbf{D}}^{\rightarrowtail}.$ Let
$\bigvee_{i}\mathscr{e}_{i}\wedge\mathscr{d}_{i}$ be an $a$-decomposition of
$\mathscr{c}$. Then, the derivation has the following form:

$\vdots$ $\vdash^{X\cup\\{a\\}}\mathscr{c}\leftarrowtail A$ $\vdots$
$\mathscr{b}\vDash^{X}\bigvee\\{\mathscr{e}_{i}\ |\
\mu(\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}})<q\\}$
$\mathsf{R}_{\mathbf{D}}^{\rightarrowtail}$
$\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{D}^{q}_{a}A$

So, $\mathscr{b}\leftarrowtail A$ is $X\cup\\{a\\}$-valid. Furthermore,
$\llbracket\mathscr{b}\rrbracket_{X}\subseteq\bigcup_{i}\\{\llbracket\mathscr{e}_{i}\rrbracket_{X}\
|$ $\mu(\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}})$ $<q\\}$, which, given
$a$-decomposition of $\mathscr{c}$ and Lemma 8, is
$\llbracket\mathscr{b}\rrbracket_{X}\subseteq\\{f\in(2^{\omega})^{X}\ |$
$\mu(\Pi_{f}(\llbracket\mathscr{c}\rrbracket_{X\cup\\{a\\}}))<q\\}$. For IH,
$\llbracket
A\rrbracket_{X\cup\\{a\\}}\subseteq\llbracket\mathscr{c}\rrbracket_{X\cup\\{a\\}}$,
so also $\llbracket\mathscr{b}\rrbracket_{X}\subseteq\\{f\in(2^{\omega})^{X}\
|\ \mu(\Pi_{f}(\llbracket A\rrbracket_{X\cup\\{a\\}}))<q\\}$. Thus,
$\llbracket\mathscr{b}\rrbracket_{X}\subseteq\llbracket\mathbf{D}^{q}_{a}A\rrbracket_{X}$.
Therefore, $\mathscr{b}\rightarrowtail\mathbf{D}^{q}_{a}A$ is $X$-valid, which
is $\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{D}^{q}_{a}A$ is valid.

$\mathsf{R}_{\mathbf{D}}^{\leftarrowtail}.$ Let
$\bigvee_{i}\mathscr{e}_{i}\wedge\mathscr{d}_{i}$ be an $a$-decomposition of
$\mathscr{c}$. The derivation has the following form:

$\vdots$ $\vdash^{X\cup\\{a\\}}\mathscr{c}\rightarrowtail A$ $\vdots$
$\bigvee\\{\mathscr{e}_{i}\ |\
\mu(\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}})<q\\}\vDash^{X}\mathscr{b}$
$\mathsf{R}_{\mathbf{D}}^{\leftarrowtail}$
$\vdash^{X}\mathscr{b}\leftarrowtail\mathbf{D}^{q}_{a}A$

So, $\mathscr{c}\rightarrowtail A$ is $X\cup\\{a\\}$-valid. Furthermore,
$\bigcup_{i}\\{\llbracket\mathscr{e}_{i}\rrbracket_{X}\ |\
\mu(\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}}<q\\}\subseteq\llbracket\mathscr{b}\rrbracket_{X}$
Given the $a$-decomposition of $\mathscr{c}$ and Lemma 8,
$\\{f\in(2^{\omega})^{X}$ $|$
$\mu(\Pi_{f}(\llbracket\mathscr{c}\rrbracket_{X\cup\\{a\\}}))<q\\}\subseteq\llbracket\mathscr{b}\rrbracket_{X}$.
Since, for IH,
$\llbracket\mathscr{c}\rrbracket_{X\cup\\{a\\}}\subseteq\llbracket
A\rrbracket_{X\cup\\{a\\}}$, also $\\{f\in(2^{\omega})^{X}$ $|$
$\mu(\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})<q\\}\subseteq\llbracket\mathscr{b}\rrbracket_{X}$.
Therefore,
$\llbracket\mathbf{D}^{q}_{a}A\rrbracket_{X}\subseteq\llbracket\mathscr{b}\rrbracket_{X}$,
which is $\vdash^{X}\mathscr{b}\leftarrowtail\mathbf{D}^{q}_{a}A$ is valid.

∎

The proof of the completeness of $\mathbf{GsCPL}$ is obtained similarly to the
one of $\mathbf{GsCPL_{0}}$. Let us start by defining the decomposition
relation $\leadsto$ between sets of sequents, which is based on
$\leadsto_{0}$.

######  Definition B.10 (Decomposition Rewriting Reduction, $\leadsto_{0}$).

The decomposition rewriting reduction, $\leadsto_{0}$, from a sequent to a set
of sequents (both in the language of $\mathbf{GsCPL}$), is defined by the
following decomposition rewriting rules:

$\displaystyle\text{if }\mathscr{b}\vDash^{X}\neg\mathscr{c},\
\vdash^{X}\mathscr{b}\rightarrowtail\neg A\ \ $ $\displaystyle\leadsto_{0}\ \
\\{\vdash^{X}\mathscr{c}\leftarrowtail A\\}$ $\displaystyle\text{if
}\neg\mathscr{c}\vDash^{X}\mathscr{b},\
\vdash^{X}\mathscr{b}\leftarrowtail\neg A\ \ $ $\displaystyle\leadsto_{0}\ \
\\{\vdash^{X}\mathscr{c}\rightarrowtail A\\}$ $\displaystyle\text{if
}\mathscr{b}\vDash^{X}\mathscr{c}\vee\mathscr{d},\
\vdash^{X}\mathscr{b}\rightarrowtail A\vee B\ \ $ $\displaystyle\leadsto_{0}\
\ \\{\vdash^{X}\mathscr{c}\rightarrowtail A,\
\vdash^{X}\mathscr{d}\rightarrowtail B\\}$
$\displaystyle\vdash^{X}\mathscr{b}\leftarrowtail A\vee B\ \ $
$\displaystyle\leadsto_{0}\ \ \\{\vdash^{X}\mathscr{b}\leftarrowtail A,\
\vdash^{X}\mathscr{b}\leftarrowtail B\\}$
$\displaystyle\vdash^{X}\mathscr{b}\rightarrowtail A\wedge B\ \ $
$\displaystyle\leadsto_{0}\ \ \\{\vdash^{X}\mathscr{b}\rightarrowtail A,\
\vdash^{X}\mathscr{b}\rightarrowtail B\\}$ $\displaystyle\text{if
}\mathscr{c}\wedge\mathscr{d}\vDash^{X}\mathscr{b},\
\vdash^{X}\mathscr{b}\leftarrowtail A\wedge B\ \ $ $\displaystyle\leadsto_{0}\
\ \\{\vdash^{X}\mathscr{c}\leftarrowtail A,\
\vdash^{X}\mathscr{d}\leftarrowtail B\\}$ $\displaystyle\text{if
}\mathscr{c}=\bigvee\mathscr{e}_{i}\wedge\mathscr{d}_{i}\
a\text{-decomposition of }\mathscr{c}$ $\displaystyle\text{and
}\mathscr{b}\vDash^{X}\bigvee\\{\mathscr{e}_{i}\ |\
\mu(\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}})\geq q\\},\
\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{C}^{q}_{a}A\ \ $
$\displaystyle\leadsto_{0}\\{\vdash^{X\cup\\{a\\}}\mathscr{c}\rightarrowtail
A\\}$ $\displaystyle\text{if
}\mathscr{c}=\mathscr{e}_{i}\wedge\mathscr{d}_{i}\ a\text{-decomposition of
}\mathscr{c}$ $\displaystyle\text{and }\bigvee\\{\mathscr{e}_{i}\ |\
\mu(\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}})\geq
q\\}\vDash^{X}\mathscr{b},\
\vdash^{X}\mathscr{b}\leftarrowtail\mathbf{C}^{q}_{a}A\ \ $
$\displaystyle\leadsto_{0}\\{\vdash^{X\cup\\{a\\}}\mathscr{c}\leftarrowtail
A\\}$ $\displaystyle\text{if
}\mathscr{c}=\bigvee\mathscr{e}_{i}\wedge\mathscr{d}_{i}\
a\text{-decomposition of }\mathscr{c}$ $\displaystyle\text{and
}\mathscr{b}\vDash^{X}\bigvee\\{\mathscr{e}_{i}\ |\
\mu(\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}})<q\\},\
\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{D}^{q}_{a}A\ \ $
$\displaystyle\leadsto_{0}\\{\vdash^{X\cup\\{a\\}}\mathscr{c}\leftarrowtail
A\\}$ $\displaystyle\text{if
}\mathscr{c}=\bigvee\mathscr{e}_{i}\wedge\mathscr{d}_{i}\
a\text{-decomposition of }\mathscr{c}$ $\displaystyle\text{and
}\bigvee\\{\mathscr{e}{i}\ |\
\mu(\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}})<q\\}\vDash^{X}\mathscr{b},\
\vdash^{X}\mathscr{b}\leftarrowtail\mathbf{D}^{q}_{a}A\ \ $
$\displaystyle\leadsto_{0}\\{\vdash^{X\cup\\{a\\}}\mathscr{c}\rightarrowtail
A\\}$

As anticipated, we define set-decomposition reduction, $\leadsto$, from a set
of sequents to a set of sequents, basing on $\leadsto_{0}$.

######  Definition B.11 (Set Decomposition, $\leadsto$).

The _set-decomposition reduction_ , $\leadsto$, from a set of sequents to
another set of sequents, is defined as follows:

$\vdash^{X}L_{i}\leadsto_{0}\\{\vdash^{X^{\prime}_{1}}L_{i_{1}},\dots,\vdash^{X^{\prime}_{m}}L_{i_{m}}\\}$
$\\{\vdash^{X_{1}}L_{1},\dots,\vdash^{X_{i}}L_{i},\dots,\vdash^{X_{n}}L_{n}\\}\leadsto\\{\vdash^{X_{1}}L_{1},\dots,\vdash^{X^{\prime}_{1}}L_{i_{1}},\dots,\vdash^{X^{\prime}_{m}}L_{i_{m}},\dots,\vdash^{X_{n}}L_{n}\\}$

As for $\textsf{{CPL}}_{0}$, $\leadsto$ is the natural lifting of
$\leadsto_{0}$ to a relation between sets of sequents. Again, predicate about
sequents can be generalized to ones on sets. Also the definitions of
corresponding sets, $\leadsto$-normal form, and normalizations are the
equivalent to the ones given for $\textsf{{CPL}}_{0}$. Also the notions of
basic and regular sequents are very close to the ones defined for
$\mathbf{GsCPL_{0}}$:

######  Definition B.12 (Regular Sequent).

A _basic formula_ is a named labelled formula $\mathscr{b}\rightarrowtail
A,\mathscr{b}\leftarrowtail A,$ where $A$ is atomic. A _regular sequent_ of
$\mathbf{GsCPL}$ is a sequent of the form $\vdash^{X}L$, such that, $L$ is a
(named) basic formula.

All the following lemmas and their respective proofs are analogous to those
for proving the completeness of $\mathbf{GsCPL_{0}}$.

######  Lemma 30.

A regular sequent is valid if and only if it is derivable in $\mathbf{GsCPL}$.

###### Proof.

Let $\vdash^{X}L$ be an arbitrary, _regular_ sequent, which is let $L$ be
basic.

  * $\Rightarrow$

Assume that $L$ is an $X$-valid formula. There are two possible cases.

Let $L=\mathscr{b}\rightarrowtail\mathbf{i}_{a}$ for some $i\in\mathbb{N}$.
Then,
$\llbracket\mathscr{b}\rrbracket_{X}\subseteq\llbracket\mathbf{i}_{a}\rrbracket_{X}$,
which is $\llbracket\mathscr{b}\rrbracket_{X}\subseteq\\{f\in(2^{\omega})^{X}$
$|$ $f(a)(i)=1\\}=\llbracket\mathscr{x}_{i}^{a}\rrbracket_{X}$, with
$\mathrm{FN}(\mathbf{i}_{a})\subseteq X$. Thus,
$\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{i}_{a}$ can be derived by means
of $\mathsf{Ax1}$ as follows:

$a\in X$ $\mathscr{b}\vDash^{X}\mathscr{x}_{i}^{a}$ $\mathsf{Ax1}$
$\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{i}_{a}$

Let $L=\mathscr{b}\leftarrowtail\mathbf{i}_{a}$ for some $i\in\mathbb{N}$.
Then,
$\llbracket\mathbf{i}_{a}\rrbracket_{X}\subseteq\llbracket\mathscr{b}\rrbracket_{X}$,
which is $\llbracket\mathscr{x}_{i}^{a}\rrbracket_{X}=\\{f\in(2^{\omega})^{X}$
$|$ $f(a)(i)=1\\}$ $\subseteq$ $\llbracket\mathscr{b}\rrbracket_{X}$, with
$\mathrm{FN}(\mathbf{i}_{a}\subseteq X$. Thus,
$\vdash^{X}\mathscr{b}\leftarrowtail\mathbf{i}_{a}$ is derivable by means of
$\mathsf{Ax2}$ as follows:

$a\in X$ $\mathscr{x}_{i}^{a}\vDash^{X}\mathscr{b}$ $\mathsf{Ax1}$
$\vdash^{X}\mathscr{b}\leftarrowtail\mathbf{i}_{a}$

  * $\Leftarrow$

By Theorem 29.

∎

The following auxiliary result is established by exhaustive inspection. Since
the proof idea is substantially the same as the one used for
$\textsf{{CPL}}_{0}$, just a few examples will be explicitly taken into
account.

######  Lemma 31.

If a (non-empty) sequent is $\leadsto_{0}$-normal, then it is regular.

###### Proof Sketch.

The lemma is proved by contraposition. Assume that $\vdash^{X}L$ is an
arbitrary, non-regular sequent, which is that $L$ is non-basic. Let us prove
that the sequent is not $\leadsto$-normal. The proof is by inspection. Let us
consider just a few cases.

$L=\mathscr{b}\rightarrowtail\neg A$. Then since for every $\mathscr{b}$,
$\bot\vDash^{X}\mathscr{b}$, the following $\leadsto_{0}$-decomposition is
well-defined:

$\vdash^{X}\mathscr{b}\rightarrowtail\neg A\ \ \ \leadsto_{0}\ \ \
\\{\vdash^{X}\top\leftarrowtail A\\}.$

$L=\mathscr{b}\rightarrowtail A\vee B$. Then, since for every $\mathscr{b}$,
$\mathscr{b}\vDash^{X}\top\vee\top$, the following
$\leadsto_{0}$-decomposition is well-defined:

$\vdash^{X}\mathscr{b}\rightarrowtail A\vee B\ \ \leadsto_{0}\ \
\\{\vdash^{X}\top\rightarrowtail A,\ \vdash^{X}\top\rightarrowtail B\\}.$

$L=\mathscr{b}\leftarrowtail A\vee B$. Then, the following
$\leadsto_{0}$-decomposition is well-defined:

$\vdash^{X}\mathscr{b}\leftarrowtail A\vee B\ \ \leadsto_{0}\ \
\\{\vdash^{X}\mathscr{b}\leftarrowtail A,\vdash^{X}\mathscr{b}\leftarrowtail
B\\}.$

$L=\mathscr{b}\rightarrowtail\mathbf{C}^{q}_{a}A$. Let
$\top=\bigvee\top\wedge\top$ be the $a$-decomposition of $\top$. Then, for
every $\mathscr{b}$ and $q\in[0,1]$, $\mathscr{b}\vDash^{X}\bigvee\\{\top$ $|$
$\mu(\llbracket\top\rrbracket)\geq q\\}$. Thus, the following
$\leadsto_{0}$-decomposition is well-defined:

$\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{C}^{q}_{a}A\ \ \leadsto_{0}\ \
\\{\vdash^{X\cup\\{a\\}}\top\rightarrowtail A\\}.$

∎

######  Corollary 3.

If a sequent is $\leadsto_{0}$-normal, then it is valid if and only if it is
derivable in $\mathbf{GsCPL}$.

###### Proof.

It is a straightforward consequence of Lemma 30 and Lemma 31. ∎

######  Lemma 32.

Reduction $\leadsto$ is strongly normalizing.

###### Proof Sketch.

The proof is again based on the notion of sequent measure. It is shown that if
$\\{\vdash^{X_{1}}L_{1},\dots,\vdash^{X_{m}}L_{m}\\}$ $\leadsto$
$\\{\vdash^{X_{1}^{\prime}}\vdash
L_{1}^{\prime},\dots,\vdash^{X_{m}^{\prime}}L_{m}^{\prime}\\}$, then
$\mathsf{ms}\big{(}\\{\vdash^{X_{1}}L_{1},\dots,\vdash^{X_{m}}L_{m}\\}\big{)}>\mathsf{ms}\big{(}\\{\vdash^{X_{1}^{\prime}}L_{1}^{\prime},\dots,\vdash^{X_{m}^{\prime}}L_{m}^{\prime}\\}\big{)}$.
This property is established by the exhaustive analysis of all possible forms
of $\leadsto_{0}$-reduction applicable to the set, which is by dealing with
all possible forms of $\leadsto_{0}$-reduction of $\vdash^{X_{i}}L_{i}$, with
$i\in\\{1,\dots,m\\}$, where $\vdash^{X_{i}}L_{i}$ is the active sequent on
which the $\leadsto$-reduction is based. These cases, are very closed to the
corresponding ones in $\textsf{{CPL}}_{0}$ proof, so just a few examples are
considered.

$L_{i}=\mathscr{b}\leftarrowtail\neg A$. Assume that
$\vdash^{X}\mathscr{b}\leftarrowtail\neg A$ is the sequent on which the
considered $\leadsto$-reduction of
$\\{\vdash^{X_{1}}L_{1},\dots,\vdash^{X_{m}}L_{m}\\}$ is based, and
specifically that the sequent is $\leadsto_{0}$-reduced as follows:

$\vdash^{X}\mathscr{b}\leftarrowtail\neg A\ \ \leadsto_{0}\ \
\\{\vdash^{X}\mathscr{c}\rightarrowtail A\\}$

for some $\mathscr{c}$ such that $\neg\mathscr{c}\vDash_{X}\mathscr{b}$. By
Definition A.9, $\mathsf{cn}(\mathscr{b}\leftarrowtail\neg
A)=\mathsf{cn}(\mathscr{c}\rightarrowtail A)+1$. Thus, since the considered
$\leadsto_{0}$-step reduces the active sequent
$\vdash^{X}\mathscr{b}\leftarrowtail\neg A$ only, for Definition A.10

$\mathsf{ms}\big{(}\\{\vdash^{X_{1}}L_{1},\dots,\vdash^{X}\mathscr{b}\leftarrowtail\neg
A,\dots,\vdash^{X_{m}}L_{m}\\}\big{)}>\mathsf{ms}\big{(}\\{\vdash^{X_{1}}L_{1},\dots,\vdash^{X}\mathscr{c}\rightarrowtail
A,\dots,\vdash^{X_{m}}L_{m}\\}\big{)}.$

$L_{i}=\mathscr{b}\rightarrowtail A\vee B$. Assume that $\vdash^{X}A\vee B$ is
the sequent on which the considered $\leadsto_{0}$-reduction of
$\\{\vdash^{X_{1}}L_{1},\dots,\vdash^{X_{m}}L_{m}\\}$ is based, and
specifically that the sequent is $\leadsto_{0}$-reduced as follows:

$\vdash^{X}\mathscr{b}\rightarrowtail A\vee B\ \ \leadsto_{0}\ \
\\{\mathscr{c}\rightarrowtail A,\vdash^{X}\mathscr{d}\rightarrowtail B\\}$

for some $\mathscr{c}$ and $\mathscr{d}$ such that
$\mathscr{b}\vDash^{X}\mathscr{c}\vee\mathscr{d}$. Thus, by Definition A.9 and
A.10,

$\displaystyle\mathsf{ms}\big{(}\\{\vdash^{X_{1}}L_{1},\dots,\vdash^{X}\mathscr{c}\rightarrowtail
A,\vdash^{X}\mathscr{d}\rightarrowtail B,\dots,\vdash^{X_{m}}L_{m}\\}\big{)}$
$\displaystyle=3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(\mathscr{c}\rightarrowtail
A)}+3^{\mathsf{cn}(\mathscr{d}\rightarrowtail
B)}+\dots+3^{\mathsf{cn}(L_{m})}$
$\displaystyle=3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(A)}+3^{\mathsf{cn}(B)}+\dots+3^{\mathsf{cn}(L_{m})}$
$\displaystyle<3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(A)+\mathsf{cn}(B)+1}+\dots+3^{\mathsf{cn}(L_{m})}$
$\displaystyle=3^{\mathsf{cn}(L_{1})}+\dots+3^{\mathsf{cn}(\mathscr{b}\rightarrowtail
A\vee B)}+\dots+3^{\mathsf{cn}(L_{m})}$
$\displaystyle=\mathsf{ms}\big{(}\\{\vdash^{X_{1}}L_{1},\dots,\vdash^{X}\mathscr{b}\rightarrowtail
A\vee B,\dots,\vdash^{X_{m}}L_{m}\\}\big{)}.$

$L_{i}=\mathscr{b}\leftarrowtail\mathbf{C}^{q}_{a}A$. Assume that
$\vdash^{X}\mathscr{b}\leftarrowtail\mathbf{C}^{q}_{a}A$ is the sequent on
which the considered $\leadsto_{0}$-reduction of
$\\{\vdash^{X_{1}}L_{1},\dots,\vdash^{X_{m}}L_{m}\\}$ is based, and
specifically that the sequent is $\leadsto_{0}$-reduced as follows:

$\vdash^{X}\mathscr{b}\leftarrowtail\mathbf{C}^{q}_{a}A\ \ \leadsto_{0}\ \
\\{\vdash^{X\cup\\{a\\}}\mathscr{c}\leftarrowtail A\\}$

for some $\mathscr{c}$ such that
$\mathscr{c}=\bigvee\mathscr{e}_{i}\wedge\mathscr{d}_{d}$ is the
$a$-decomposition of $\mathscr{c}$ and $\bigvee\\{\mathscr{e}_{i}$ $|$
$\mu(\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}})\geq q\\}$ $\vDash^{X}$
$\mathscr{b}$. By Definition A.9,
$\mathsf{cn}(\mathscr{b}\leftarrowtail\mathbf{C}^{q}_{a}A)=\mathsf{cn}(\mathscr{c}\leftarrowtail
A)+1$. Thus, since the considered $\leadsto_{0}$-step reduces the active
sequent $\vdash\mathscr{b}\leftarrowtail\mathbf{C}^{q}_{a}A$ only, for
Definition A.10,

$\mathsf{ms}\big{(}\\{\vdash^{X_{1}}L_{1},\dots,\vdash^{X}\mathscr{b}\leftarrowtail\neg
A,\dots,\vdash^{X_{m}}L_{m}\\}\big{)}>\mathsf{ms}\big{(}\\{\vdash^{X_{1}}L_{1},\dots,\vdash^{X}\mathscr{c}\rightarrowtail
A,\dots,\vdash^{X_{m}}L_{m}\\}\big{)}.$

∎

In order to prove that validity is existentially preserved through
$\leadsto$-decomposition, it is required to introduce the following auxiliary
lemma.

######  Lemma 33.

For every formula of CPL, call it $A$, there is a named Boolean formula
$\mathscr{b}_{A}$, such that, for every $X$, with
$\mathrm{FN}(A)\cup\mathrm{FN}(B)\subseteq X$:

$\llbracket A\rrbracket_{X}=\llbracket\mathscr{b}_{A}\rrbracket_{X}.$

###### Proof.

The proof is by induction on the structure of $\mathscr{b}$.

  * •

_Base case._ $A=\mathbf{i}_{a}$. Let $\mathrm{FN}(A)\subseteq X$. For
Definition 4.3,
$\llbracket\mathbf{i}_{a}\rrbracket_{X}=\\{f\in(2^{\omega})^{X}\ |\
f(a)(i)=1\\}=\llbracket\mathscr{x}_{\mathbf{i}}^{a}\rrbracket_{X}$. Thus,
$\mathscr{b}_{A}$ = $x^{a}_{i}$.

  * •

_Inductive case._ There are four possible cases.

$A=\neg B.$ By IH, there is a $\mathscr{b}_{B}$ such that, for every $X$
($\mathrm{FN}(\mathscr{b})\cup\mathrm{FN}(\mathscr{b}_{B})\subseteq X$),
$\llbracket A\rrbracket_{X}=\llbracket\mathscr{b}_{A}\rrbracket$. Thus, let
$\mathscr{b}_{A}$ = $\neg\mathscr{b}_{B}$. Then,

$\llbracket\neg\mathscr{b}_{B}\rrbracket_{X}=(2^{\omega})^{X}\ –\
\llbracket\mathscr{b}_{B}\rrbracket_{X}\stackrel{{\scriptstyle
IH}}{{=}}(2^{\omega})^{X}\ –\ \llbracket B\rrbracket_{X}=\llbracket\neg
B\rrbracket_{X}=\llbracket A\rrbracket_{X}.$

$A=B\vee C$. By IH, there are $\mathscr{b}_{B}$ and $\mathscr{b}_{C}$ such
that, for every $X$ ($\mathrm{FN}(B)\cup\mathrm{FN}(C)\subseteq X$),
$\llbracket\mathscr{b}_{B}\rrbracket_{X}=\llbracket B\rrbracket_{X}$ and
$\llbracket\mathscr{b}_{C}\rrbracket_{X}=\llbracket C\rrbracket_{X}$. Thus,
let $\mathscr{b}_{A}$ = $\mathscr{b}_{B}\vee\mathscr{b}_{C}$. Then,

$\llbracket\mathscr{b}_{B}\vee\mathscr{b}_{C}\rrbracket_{X}=\llbracket\mathscr{b}_{B}\rrbracket_{X}\cup\llbracket\mathscr{b}_{C}\rrbracket_{X}\stackrel{{\scriptstyle
IH}}{{=}}\llbracket B\rrbracket_{X}\cup\llbracket C\rrbracket_{X}=\llbracket
B\vee C\rrbracket_{X}=\llbracket A\rrbracket_{X}.$

$A=B\wedge C$. Equivalent to the previous case.

$A=\mathbf{C}^{q}_{a}B$ and $A=\mathbf{D}^{q}_{a}B$. By Lemma 8.

∎

######  Lemma 34.

For each sequent of $\mathbf{GsCPL}$, if it is valid, then it has a valid
$\leadsto$-normal form.

###### Proof.

The proof is by analytic inspection of all possible cases. Given an arbitrary
single-succedent sequent $\phi=\ \vdash^{X}L$, there are two main cases to be
taken into account:

  * •

Let $\phi$ be such that no $\leadsto_{0}$-decomposition reduction can be
applied on it. Thus, since the sequent is $\leadsto_{0}$-normal, it is either
empty or regular, by Lemma 31. Thus, it is already a $\leadsto$-normal form,
and for hypothesis it is valid.

  * •

Let $\phi$ be $\leadsto_{0}$-reducible. By Theorem 32, $\leadsto$ is strongly
normalizing, so no infinite reduction sequence is possible. Consequently, it
is enough to prove that each reduction step existentially preserves validity,
which is that for each possible $\leadsto$ based on $\leadsto_{0}$-reduction,
if $\phi$ is valid, then there is a set of sequents
$\\{\phi_{1},\dots,\phi_{m}\\}$, such that
$\phi\leadsto_{0}\\{\phi_{1},\dots,\phi_{m}\\}$ and
$\\{\phi_{1},\dots,\phi_{m}\\}$ is valid. The proof consists in taking into
account all possible forms of $\leadsto_{0}$, on which the reduction step can
be based. Since these cases are very similar to the corresponding one
considered for $\textsf{{CPL}}_{0}$, just a few examples will be taken into
account.

$L=\mathscr{b}\leftarrowtail\neg A$. Assume
$\phi=\vdash^{X}\mathscr{b}\leftarrowtail\neg A$. Let us show that there is a
well-defined $\leadsto_{0}$-reduction of $\phi$ of the following form such
that the reduced set is valid. For hypothesis
$\vdash^{X}\mathscr{b}\leftarrowtail\neg A$ is valid, which is
$\mathscr{b}\leftarrowtail\neg A$ is $X$-valid. Let us consider a Boolean
expression $\mathscr{c}=\neg\mathscr{b}$. Then,

$\llbracket\neg\mathscr{c}\rrbracket=(2^{\omega})^{X}\ –\
\llbracket\mathscr{c}\rrbracket_{X}=(2^{\omega})^{X}\ –\
\big{(}(2^{\omega})^{X}–\llbracket\mathscr{b}\rrbracket_{X}\big{)}=\llbracket\mathscr{b}\rrbracket_{X}$

and in particular
$\llbracket\neg\mathscr{c}\rrbracket_{X}\subseteq\llbracket\mathscr{b}\rrbracket_{X}$,
which is $\neg\mathscr{c}\vDash^{X}\mathscr{b}$. Consequently, the following
$\leadsto_{0}$-reduction is well-defined,

$\vdash^{X}\mathscr{b}\leftarrowtail\neg A\ \ \leadsto_{0}\ \
\\{\vdash^{X}\mathscr{c}\rightarrowtail A\\}.$

Since $\mathscr{b}\leftarrowtail\neg A$ is $X$-valid, also $\llbracket\neg
A\rrbracket_{X}\subseteq\llbracket\mathscr{b}\rrbracket_{X}$. Thus, for basic
set theory, $\llbracket\neg\mathscr{b}\rrbracket_{X}\subseteq\llbracket
A\rrbracket_{X}$. But for construction $\mathscr{c}=\neg\mathscr{b}$, so also
$\llbracket\mathscr{c}\rrbracket_{X}\subseteq\llbracket A\rrbracket_{X}$,
which is $\mathscr{c}\rightarrowtail A$ is $X$-valid. Consequently,
$\vdash^{X}\mathscr{b}\rightarrowtail A$ is valid as well.

$L=\mathscr{b}\rightarrowtail\mathbf{C}^{q}_{a}A$. Assume $\phi=\
\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{C}^{q}_{a}A$. Let us show that
there is a well-defined $\leadsto_{0}$-reduction of $\phi$ of the following
form such that the reduced set is valid. For hypothesis,
$\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{C}^{q}_{a}A$ is valid, which is
$\mathscr{b}\rightarrowtail\mathbf{C}^{q}_{a}A$ is $X$-valid. For Lemma 33,
$\llbracket A\rrbracket_{X\cup\\{a\\}}=\mathscr{b}_{A}$ and, by Lemma 8, there
is an $a$-decomposition of
$\mathscr{b}_{A}:\mathscr{c}=\bigvee\mathscr{d}_{i}\wedge\mathscr{e}_{i}$.
Furthermore, $\llbracket\mathbf{C}^{q}_{a}A\rrbracket_{X}$ =
$\\{f\in(2^{\omega}){X}$ $|$ $\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\big{)}\geq q\\}$ and $\\{f\in(2^{\omega})^{X}$ $|$
$\mu\big{(}\Pi_{f}(\llbracket\mathscr{b}_{A}\rrbracket_{X\cup\\{a\\}})\big{)}\geq
q\\}=\bigcup_{i}\\{\llbracket\mathscr{e}_{i}\rrbracket_{X}$ $|$
$\mu(\llbracket\mathscr{d}\rrbracket_{\\{a\\}})\geq q\\}$. Therefore,
$\llbracket\mathbf{C}^{q}_{a}A\rrbracket_{X}$ =
$\bigcup_{i}\\{\llbracket\mathscr{e}_{i}\rrbracket_{X}$ $|$
$\mu(\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}})\geq q\\}$, the following
$\leadsto_{0}$-decomposition is well-defined:

$\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{C}^{q}_{a}A\ \ \leadsto_{0}\ \
\\{\vdash^{X\cup\\{a\\}}\mathscr{c}\rightarrowtail A\\}.$

For construction $\mathscr{c}$ is an $a$-decomposition of $\mathscr{b}_{A}$ so
$\llbracket\mathscr{b}_{A}\rrbracket_{X\cup\\{a\\}}$ =
$\llbracket\mathscr{c}\rrbracket_{X\cup\\{a\\}}$. In particular,
$\llbracket\mathscr{c}\rrbracket_{X\cup\\{a\\}}\subseteq\llbracket
A\rrbracket_{X\cup\\{a\\}}$, which is $\mathscr{c}\rightarrowtail A$ is
$X\cup\\{a\\}$-valid. Then,
$\\{\vdash^{X\cup\\{a\\}}\mathscr{c}\rightarrowtail A\\}$ is valid as well.

∎

Finally, it is proved that derivability in $\mathbf{GsCPL}$ is preserved in
the following sense.

######  Lemma 35.

Given the set of sequents $\Phi,\Phi^{\prime}$, if $\Phi\leadsto\Phi^{\prime}$
and $\Phi^{\prime}$ is derivable in $\mathbf{GsCPL}$, then $\Phi$ is derivable
in $\mathbf{GsCPL}$ as well.

###### Proof.

For hypothesis $\Phi\leadsto\Phi^{\prime}$, which is, for some $\phi\in\Phi$,
there is a $\leadsto_{0}$-decomposition

$\phi\ \ \leadsto_{0}\ \ \\{\phi_{1},\dots,\phi_{m}\\}$

on which the considered $\leadsto_{0}$ is based, so that
$\phi_{1},\dots,\phi_{m}\in\Phi^{\prime}$. Since the number of possible
$\leadsto_{0}$ is finite, the proof is obtained by considering all forms of
reduction applicable to the set.

$L=\mathscr{b}\rightarrowtail\neg A$. Assume
$\phi=\vdash^{X}\mathscr{b}\rightarrowtail\neg A$ and that the considered
$\leadsto_{0}$ is based on the following $\leadsto_{0}$-decomposition

$\vdash^{X}\mathscr{b}\rightarrowtail\neg A\ \ \leadsto_{0}\ \
\\{\vdash^{X}\mathscr{c}\leftarrowtail A\\}$

for some $\mathscr{c}$ such that $\mathscr{b}\vDash^{X}\neg\mathscr{c}$. For
hypothesis $\Phi^{\prime}$ is derivable, so each of its sequents is. Thus, in
this case, $\vdash^{X}\mathscr{c}\leftarrowtail A$ ($\in\Phi^{\prime}$) is
derivable. Given that $\mathscr{b}\vDash^{X}\neg\mathscr{c}$, it is easily
possible to derive $\vdash^{X}\mathscr{b}\rightarrowtail\neg A$ by applying
$\mathsf{R}_{\neg}^{\rightarrowtail}$ as follows:

$\vdots$ $\vdash^{X}\mathscr{c}\leftarrowtail A$
$\mathscr{b}\vDash^{X}\neg\mathscr{c}$ $\mathsf{R}_{\neg}^{\rightarrowtail}$
$\vdash^{X}\mathscr{b}\rightarrowtail\neg A$

$L=\mathscr{b}\leftarrowtail\neg A$. Assume
$\phi=\vdash^{X}\mathscr{b}\leftarrowtail\neg A$ and that the considered
$\leadsto$ is based on the following $\leadsto_{0}$-decomposition

$\vdash^{X}\mathscr{b}\leftarrowtail\neg A\ \ \leadsto_{0}\ \
\\{\vdash^{X}\mathscr{c}\rightarrowtail A\\}$

for some $\mathscr{c}$ such that $\neg\mathscr{c}\vDash^{X}\mathscr{b}$. For
hypothesis $\Phi^{\prime}$ is derivable, so each of its sequents is. Thus,
$\vdash^{X}\mathscr{c}\rightarrowtail A$ is derivable and, since
$\neg\mathscr{c}\vDash^{X}\mathscr{b}$, it is easily possible to derive
$\vdash^{X}\mathscr{b}\rightarrowtail\neg A$ by applying
$\mathsf{R}_{\neg}^{\leftarrowtail}$ as follows:

$\vdots$ $\vdash^{X}\mathscr{c}\rightarrowtail A$
$\neg\mathscr{c}\vDash^{X}\mathscr{b}$ $\mathsf{R}_{\neg}^{\leftarrowtail}$
$\vdash^{X}\mathscr{b}\leftarrowtail\neg A$

$L=\mathscr{b}\rightarrowtail A\vee B$. Assume
$\phi=\vdash^{X}\mathscr{b}\rightarrowtail A\vee B$ and that the considered
$\leadsto$ is based on the following $\leadsto_{0}$-decomposition

$\vdash^{X}\mathscr{b}\rightarrowtail A\vee B\ \ \leadsto_{0}\ \
\\{\vdash^{X}\mathscr{c}\rightarrowtail A,\vdash^{X}\mathscr{d}\rightarrowtail
B\\}$

where $\mathscr{c}$ and $\mathscr{d}$ are two Boolean formulas such that
$\mathscr{b}\vDash^{X}\mathscr{c}\vee\mathscr{d}$. For hypothesis
$\Phi^{\prime}$ is derivable, so each of its sequents is. Therefore, both
$\vdash^{X}\mathscr{c}\rightarrowtail A$ ($\in\Phi^{\prime}$) and
$\vdash^{X}\mathscr{d}\rightarrowtail A$ ($\in\Phi^{\prime}$) are derivable
and, since $\mathscr{b}\vDash^{X}\mathscr{c}\vee\mathscr{d}$, then also
$\vdash^{X}\mathscr{b}\rightarrowtail A\vee B$ is derivable in
$\mathbf{GsCPL}$ in the following way:

$\vdots$ $\vdash^{X}\mathscr{c}\rightarrowtail A$
$\mathsf{R1}_{\vee}^{\rightarrowtail}$ $\vdash^{X}\mathscr{c}\rightarrowtail
A\vee B$ $\vdots$ $\vdash^{X}\mathscr{d}\rightarrowtail B$
$\mathsf{R2}_{\vee}^{\rightarrowtail}$ $\vdash^{X}\mathscr{d}\rightarrowtail
A\vee B$ $\mathscr{b}\vDash^{X}\mathscr{c}\vee\mathscr{d}$
$\mathsf{R}_{\cup}^{\rightarrowtail}$ $\vdash^{X}\mathscr{c}\rightarrowtail
A\vee B$

$L=\mathscr{b}\leftarrowtail A\vee B$. Assume
$\phi=\vdash^{X}\mathscr{b}\leftarrowtail A\vee B$ and that the given
$\leadsto$ step is based on the following $\leadsto_{0}$-decomposition:

$\vdash^{X}\mathscr{b}\leftarrowtail A\vee B\ \ \leadsto_{0}\ \
\\{\vdash^{X}\mathscr{b}\leftarrowtail A,\vdash^{X}\mathscr{b}\leftarrowtail
B\\}.$

For hypothesis, $\Phi^{\prime}$ is derivable, so each of its sequent is.
Therefore, both $\vdash^{X}\mathscr{b}\leftarrowtail A$ ($\in\Phi^{\prime}$)
and $\vdash^{X}\mathscr{b}\leftarrowtail B$ ($\in\Phi^{\prime}$) are derivable
as well. Then, $\vdash^{X}\mathscr{b}\leftarrowtail A\vee B$ is easily shown
to be derivable by applying $\mathsf{R}_{\vee}^{\leftarrowtail}$ as follows:

$\vdots$ $\vdash^{X}\mathscr{b}\leftarrowtail A$ $\vdots$
$\vdash^{X}\mathscr{b}\leftarrowtail B$ $\mathsf{R}_{\vee}^{\leftarrowtail}$
$\vdash^{X}\mathscr{b}\leftarrowtail A\vee B$

$L=\mathscr{b}\rightarrowtail A\wedge B$. Assume
$\phi=\vdash^{X}\mathscr{b}\rightarrowtail A\wedge B$ and that the considered
$\leadsto$ is based on the following $\leadsto_{0}$-decomposition:

$\vdash^{X}\mathscr{b}\rightarrowtail A\wedge B\ \ \leadsto_{0}\ \
\\{\vdash^{X}\mathscr{b}\rightarrowtail A,\vdash^{X}\mathscr{b}\rightarrowtail
B\\}.$

For hypothesis, $\Phi^{\prime}$ is derivable, so each of its sequents is.
Therefore, both $\vdash^{X}\mathscr{b}\rightarrowtail A$ ($\in\Phi^{\prime}$)
and $\vdash^{X}\mathscr{b}\rightarrowtail B$ ($\in\Phi^{\prime}$) are
derivable as well. Then, $\vdash^{X}\mathscr{b}\rightarrowtail A\wedge B$ is
easily shown to be derivable by applying
$\mathsf{R}_{\wedge}^{\rightarrowtail}$ as follows:

$\vdots$ $\vdash^{X}\mathscr{b}\rightarrowtail A$ $\vdots$
$\vdash^{X}\mathscr{b}\rightarrowtail B$
$\mathsf{R}_{\wedge}^{\rightarrowtail}$ $\vdash^{X}\mathscr{b}\rightarrowtail
A\wedge B$

$L=\mathscr{b}\leftarrowtail A\wedge B$. Assume
$\phi=\vdash^{X}\mathscr{b}\leftarrowtail A\wedge B$ and that the given
$\leadsto$ is based on the following $\leadsto_{0}$-decomposition

$\vdash^{X}\mathscr{b}\leftarrowtail A\wedge B\ \ \leadsto_{0}\ \
\\{\vdash^{X}\mathscr{c}\leftarrowtail A,\vdash^{X}\mathscr{d}\leftarrowtail
B\\}$

where $\mathscr{c}$ and $\mathscr{d}$ and two Boolean expressions such that
$\mathscr{c}\wedge\mathscr{d}\vDash^{X}\mathscr{b}$. For hypothesis
$\Phi^{\prime}$ is derivable, so each of its sequents is. Therefore, both
$\vdash^{X}\mathscr{c}\leftarrowtail A$ ($\in\Phi^{\prime}$) and
$\vdash^{X}\mathscr{d}\leftarrowtail A$ ($\in\Phi^{\prime}$) are derivable
and, since $\mathscr{b}\vDash^{X}\mathscr{c}\wedge\mathscr{d}$, then also
$\vdash^{X}\mathscr{b}\leftarrowtail A\wedge B$ is derivable in
$\mathbf{GsCPL}$ in the following way:

$\vdots$ $\vdash^{X}\mathscr{c}\leftarrowtail A$
$\mathsf{R1}_{\wedge}^{\leftarrowtail}$ $\vdash^{X}\mathscr{c}\leftarrowtail
A\wedge B$ $\vdots$ $\vdash^{X}\mathscr{d}\leftarrowtail B$
$\mathsf{R2}_{\wedge}^{\leftarrowtail}$ $\vdash^{X}\mathscr{d}\leftarrowtail
A\wedge B$ $\mathscr{c}\wedge\mathscr{d}\vDash^{X}\mathscr{b}$
$\mathsf{R}_{\cap}^{\leftarrowtail}$ $\vdash^{X}\mathscr{b}\leftarrowtail
A\wedge B$

$L=\mathscr{b}\rightarrowtail\mathbf{C}^{q}_{a}A$. Assume
$\phi=\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{C}^{q}_{a}A$ and that the
considered $\leadsto$ is based on the following $\leadsto_{0}$-decomposition

$\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{C}^{q}_{a}A\ \ \leadsto_{0}\ \
\\{\vdash^{X\cup\\{a\\}}\mathscr{c}\rightarrowtail A\\}$

for some $\mathscr{c}$ such that $\bigvee\mathscr{e}_{i}\wedge\mathscr{d}_{i}$
is an $a$-decomposition of $\mathscr{c}$ and that
$\mathscr{c}\vDash^{X}\bigvee\\{\mathscr{e}_{i}$ $|$
$\mu(\llbracket\mathscr{d}_{i}\rrbracket)\geq q\\}$. For hypothesis
$\Phi^{\prime}$ is derivable, so also
$\vdash^{X\cup\\{a\\}}\mathscr{c}\rightarrowtail A$ ($\in\Phi^{\prime}$) is
and, for the given definition of $\mathscr{c}$,
$\vdash^{X}\mathscr{c}\rightarrowtail\mathbf{C}^{q}_{a}A$ is derived by
$\mathsf{R}_{\mathbf{C}}^{\rightarrowtail}$ as follows:

$\vdots$ $\vdash^{X\cup\\{a\\}}\mathscr{c}\rightarrowtail A$
$\mathscr{b}\vDash^{X}\bigvee\\{\mathscr{e}_{i}\ |\
\mu\big{(}\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}}\big{)}\geq q\\}$
$\mathsf{R}_{\mathbf{C}}^{\rightarrowtail}$
$\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{C}^{q}_{a}A$

$L=\mathscr{b}\leftarrowtail\mathbf{C}^{q}_{a}A$. Assume
$\phi=\vdash^{X}\mathscr{b}\leftarrowtail\mathbf{C}^{q}_{a}A$ and that the
considered $\leadsto$ is based on the following $\leadsto_{0}$-decomposition

$\vdash^{X}\mathscr{b}\leftarrowtail\mathbf{C}^{q}_{a}A\ \ \leadsto_{0}\ \
\\{\vdash^{X\cup\\{a\\}}\mathscr{c}\leftarrowtail A\\}$

for some $\mathscr{c}$ such that $\bigvee\mathscr{e}_{i}\wedge\mathscr{d}_{i}$
is an $a$-decomposition of $\mathscr{c}$ and that $\bigvee\\{\mathscr{e}_{i}$
$|$ $\mu(\llbracket\mathscr{d}_{i}\rrbracket)\\}\vDash^{X}\mathscr{b}$. For
hypothesis, $\Phi^{\prime}$ is derivable, so also
$\vdash^{X\cup\\{a\\}}\mathscr{c}\leftarrowtail A$ ($\in\Phi^{\prime}$) is
and, for the given definition of $\mathscr{c}$,
$\vdash^{X}\mathscr{c}\leftarrowtail\mathbf{C}^{q}_{a}A$ is derived by
$\mathsf{R}_{\mathbf{C}}^{\leftarrowtail}$ as follows:

$\vdots$ $\vdash^{X\cup\\{a\\}}\mathscr{c}\leftarrowtail A$
$\bigvee\\{\mathscr{e}_{i}\ |\
\mu\big{(}\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}}\big{)}\vDash^{X}\mathscr{b}$
$\mathsf{R}_{\mathbf{C}}^{\rightarrowtail}$
$\vdash^{X}\mathscr{b}\leftarrowtail\mathbf{C}^{q}_{a}A$

$L=\mathscr{b}\rightarrowtail\mathbf{D}^{q}_{a}A$. Assume
$\phi=\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{D}^{q}_{a}A$ and that the
considered $\leadsto$ is based on the following $\leadsto_{0}$-decomposition

$\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{D}^{q}_{a}A\ \ \leadsto_{0}\ \
\\{\vdash^{X\cup\\{a\\}}\mathscr{c}\leftarrowtail A\\}$

for some $\mathscr{c}$ such that $\bigvee\mathscr{e}_{i}\wedge\mathscr{d}_{i}$
is an $a$-decomposition of $\mathscr{c}$ and that
$\mathscr{c}\vDash^{X}\bigvee\\{\mathscr{e}_{i}\ |\
\mu(\llbracket\mathscr{d}_{i}\rrbracket)<q\\}$. For hypothesis,
$\Phi^{\prime}$ is derivable, so also
$\vdash^{X\cup\\{a\\}}\mathscr{c}\leftarrowtail A$ ($\in\Phi^{\prime}$) is
and, for the given definition of $\mathscr{c}$,
$\vdash^{X}\mathscr{c}\rightarrowtail\mathbf{D}^{q}_{a}A$ is derivable by
$\mathsf{R}_{\mathbf{D}}^{\rightarrowtail}$ as follows:

$\vdots$ $\vdash^{X\cup\\{a\\}}\mathscr{c}\leftarrowtail A$
$\mathscr{b}\vDash^{X}\bigvee\\{\mathscr{e}_{i}\ |\
\mu\big{(}\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}}\big{)}<q$
$\mathsf{R}_{\mathbf{D}}^{\rightarrowtail}$
$\vdash^{X}\mathscr{b}\rightarrowtail\mathbf{D}^{q}_{a}A$

$L=\mathscr{b}\leftarrowtail\mathbf{D}^{q}_{a}A$. Assume
$\phi=\vdash^{X}\mathscr{b}\leftarrowtail\mathbf{D}^{q}_{a}A$ and that the
considered $\leadsto$ is based on the following $\leadsto_{0}$-decomposition

$\vdash^{X}\mathscr{b}\leftarrowtail\mathbf{D}^{q}_{a}A\ \ \leadsto_{0}\ \
\\{\vdash^{X\cup\\{a\\}}\mathscr{c}\rightarrowtail A\\}$

for some $\mathscr{c}$ such that $\bigvee\mathscr{e}_{i}\wedge\mathscr{d}_{i}$
is an $a$-decomposition of $\mathscr{c}$ and that $\bigvee\\{\mathscr{e}_{i}\
|\ \mu(\llbracket\mathscr{d}_{i}\rrbracket)<q\\}\vDash^{X}\mathscr{b}$. For
hypothesis, $\Phi^{\prime}$ is derivable, so also
$\vdash^{X\cup\\{a\\}}\mathscr{c}\rightarrowtail A$ ($\in\Phi^{\prime}$) is
and, for the given definition of $\mathscr{c}$,
$\vdash^{X}\mathscr{c}\leftarrowtail\mathbf{D}^{q}_{a}A$ is derived by
$\mathsf{R}_{\mathbf{D}}^{\leftarrowtail}$ as follows:

$\vdots$ $\vdash^{X\cup\\{a\\}}\mathscr{c}\rightarrowtail A$
$\bigvee\\{\mathscr{e}_{i}\ |\
\mu\big{(}\llbracket\mathscr{d}_{i}\rrbracket_{\\{a\\}}\big{)}\vDash^{X}\mathscr{b}$
$\mathsf{R}_{\mathbf{D}}^{\leftarrowtail}$
$\vdash^{X}\mathscr{b}\leftarrowtail\mathbf{D}^{q}_{a}A$

∎

######  Theorem 36 (Completeness of $\mathbf{GsCPL}$).

If a sequent of $\mathbf{GsCPL}$ is valid, then it is derivable in
$\mathbf{GsCPL}$.

###### Proof.

By combining the given Lemma 34, Corollary 3, and Lemma 35. ∎

##  Appendix C Proofs from Section 5

###  C.1 Prenex Normal Forms

######  Lemma 37.

For every $X$ such that $\mathrm{FN}(A)\subseteq X$ and $a\in X$, it holds
that:

$\llbracket\mathbf{C}^{0}_{a}A\rrbracket_{X}=(2^{\omega})^{X}\qquad\qquad\qquad\qquad\llbracket\mathbf{D}^{0}_{a}A\rrbracket_{X}=\emptyset^{X}.$

###### Proof.

Let us consider
$\llbracket\mathbf{C}^{0}_{a}A\rrbracket_{X}=(2^{\omega})^{X}.$ Since for
every $\Pi_{f}(\llbracket A\rrbracket_{X\cup\\{a\\}})$, also
$\mu\big{(}\Pi_{f}(\llbracket A\rrbracket_{X\cup\\{a\\}})\big{)}\geq 0$ holds.
So, trivially,

$\displaystyle\llbracket\mathbf{C}^{0}_{a}A\rrbracket_{X}$
$\displaystyle=\\{f\in(2^{\omega})^{X}\ |\ \mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\big{)}\geq 0\\}$ $\displaystyle=(2^{\omega})^{X}.$

Let us now consider
$\llbracket\mathbf{D}^{0}_{a}A\rrbracket_{X}=\emptyset^{X}$. Since for not
$\Pi_{f}(\llbracket A\rrbracket_{X\cup\\{a\\}})$, also
$\mu\big{(}\Pi_{f}(\llbracket A\rrbracket_{X\cup\\{a\\}})\big{)}<0$ holds. So,
trivially,

$\displaystyle\llbracket\mathbf{D}^{0}_{a}A\rrbracket_{X}$
$\displaystyle=\\{f\in(2^{\omega})^{X}\ |\ \mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\big{)}<0\\}$ $\displaystyle=\emptyset^{X}.$

∎

Without loss of generality, let us assume $a\not\in\mathrm{FN}(A)$.

######  Corollary 4.

For every $X$ such that $\mathrm{FN}(A)\cup\mathrm{FN}(B)\subseteq X$ and
$a\in X$, it holds that:

$\displaystyle A\wedge\mathbf{C}^{0}_{a}B$ $\displaystyle\equiv_{X}A$
$\displaystyle A\vee\mathbf{C}^{0}_{a}B$
$\displaystyle\equiv_{X}(2^{\omega})^{X}$ $\displaystyle
A\wedge\mathbf{D}^{0}_{a}B$ $\displaystyle\equiv_{X}\emptyset^{X}$
$\displaystyle A\vee\mathbf{D}^{0}_{a}B$ $\displaystyle\equiv_{X}A.$

###### Proof.

Let us consider $A\wedge\mathbf{C}^{0}_{a}B\equiv_{X}A$. Thus,

$\llbracket A\wedge\mathbf{C}^{0}_{a}B\rrbracket_{X}=\llbracket
A\rrbracket_{X}.$

By Definition 4.3,

$\displaystyle\llbracket A\wedge\mathbf{C}^{0}_{a}B\rrbracket_{X}=\ \ \ $
$\displaystyle\llbracket
A\rrbracket_{X}\cap\llbracket\mathbf{C}^{0}_{a}B\rrbracket_{X}$
$\displaystyle\stackrel{{\scriptstyle\text{L}\leavevmode\nobreak\
\ref{Lq0}}}{{=}}$ $\displaystyle\llbracket
A\rrbracket_{X}\cap(2^{\omega})^{X}$ $\displaystyle=\ \ \ $
$\displaystyle\llbracket A\rrbracket_{X}.$

Let us now consider $A\vee\mathbf{C}^{0}_{a}B\equiv_{X}(2^{\omega})^{X}$.
Thus,

$\llbracket A\vee\mathbf{C}^{0}_{a}B\rrbracket_{X}=(2^{\omega})^{X}.$

Again for Definition 4.3,191919Well-definition is ensured by the fact that
$a\not\in X$.

$\displaystyle\llbracket A\vee\mathbf{C}^{0}_{a}B\rrbracket_{X}=\ \ \ $
$\displaystyle\llbracket
A\rrbracket_{X}\cup\llbracket\mathbf{C}^{0}_{a}B\rrbracket_{X}$
$\displaystyle\stackrel{{\scriptstyle\text{L}\leavevmode\nobreak\
\ref{Lq0}}}{{=}}$ $\displaystyle\llbracket
A\rrbracket_{X}\cup(2^{\omega})^{X}$ $\displaystyle=\ \ \ $
$\displaystyle(2^{\omega})^{X}.$

Let us consider $A\wedge\mathbf{D}^{0}_{a}B\equiv_{X}\emptyset^{X}$. Thus,

$\llbracket A\wedge\mathbf{D}^{0}_{a}B\rrbracket_{X}=\emptyset^{X}.$

For Definition 4.3,

$\displaystyle\llbracket A\wedge\mathbf{D}^{0}_{a}B\rrbracket_{X}=\ \ \ $
$\displaystyle\llbracket
A\rrbracket_{X}\cap\llbracket\mathbf{D}^{0}_{a}B\rrbracket_{X}$
$\displaystyle\stackrel{{\scriptstyle\text{L}\leavevmode\nobreak\
\ref{Lq0}}}{{=}}$ $\displaystyle\llbracket A\rrbracket_{X}\cap\emptyset^{X}$
$\displaystyle=\ \ \ $ $\displaystyle\emptyset^{X}.$

Let us finally consider $A\vee\mathbf{D}^{0}_{a}B\equiv_{X}A$. Thus,

$\llbracket A\vee\mathbf{D}^{0}_{a}B\rrbracket_{X}=\llbracket
A\rrbracket_{X}.$

For Definition 4.3,

$\displaystyle\llbracket A\vee\mathbf{D}^{0}_{a}B\rrbracket_{X}=\ \ \ $
$\displaystyle\llbracket
A\rrbracket_{X}\cup\llbracket\mathbf{D}^{0}_{a}B\rrbracket_{X}$
$\displaystyle\stackrel{{\scriptstyle\text{L}\leavevmode\nobreak\
\ref{Lq0}}}{{=}}$ $\displaystyle\llbracket A\rrbracket_{X}\cup\emptyset^{X}$
$\displaystyle=\ \ \ $ $\displaystyle\llbracket A\rrbracket_{X}.$

∎

In order to prove Lemma 10, some auxiliary lemmas has to be preliminarily
considered.

######  Lemma 38.

Given $\mathcal{Z}\subseteq(2^{\omega})^{X\cup Y}$ and
$f\in\mathcal{X}\subseteq(2^{\omega})^{X}$, then
$\Pi_{f}(\mathcal{Z})=\Pi_{f}(\mathcal{Z}\cap(X)^{\Uparrow Y})$.

###### Proof.

  * $\subseteq$

If $g\in\Pi_{f}$($\mathcal{Z}$), then $f+g\in\mathcal{Z}$. Since
$f\in\mathcal{X},$ by $(X)^{\Uparrow Y}$ definition, $f+g\in(X)^{\Uparrow Y}$.
As a consequence, $f+g\in\mathcal{Z}\cap(X)^{\Uparrow Y}$ and
$g\in\Pi_{f}$($\mathcal{Z}\cap(X)^{\Uparrow Y}$).

  * $\supseteq$

Trivial, since the projection operator is monotone.

∎

######  Lemma 39.

Let $f\in(2^{\omega})^{X}$, $\mathcal{Z}\subseteq(2^{\omega})^{X\cup Y}$, and
$\mathcal{X}\subseteq(2^{\omega})^{X}$, with $X\cap Y=\emptyset$. If
$\mu\big{(}\Pi_{f}(\mathcal{Z}\cap(\mathcal{X})^{\Uparrow Y})\big{)}>0$, then
$f\in\mathcal{X}$.

###### Proof.

By contraposition. Assume $f\not\in\mathcal{X}$. There are two possible cases.

  * •

If $\mathcal{Z}\cap(X)^{\Uparrow Y}$ = $\emptyset$, then

$\displaystyle\mu(\Pi_{f}\big{(}\mathcal{Z}\cap(X)^{\Uparrow Y})\big{)}$
$\displaystyle=\mu\big{(}\Pi_{f}(\emptyset)\big{)}$
$\displaystyle=\mu(\emptyset)$ $\displaystyle=0.$

  * •

Otherwise,

$\displaystyle\mu\big{(}\Pi_{f}(\mathcal{Z}\cap(X)^{\Uparrow Y})\big{)}$
$\displaystyle\ =\mu\big{(}\\{g\in(2^{\omega})^{Y}\ |\
f+g\in(\mathcal{Z}\cap(X)^{\Uparrow Y})\\}\big{)}$
$\displaystyle\stackrel{{\scriptstyle
f\not\in\mathcal{X}}}{{=}}\mu(\emptyset)$ $\displaystyle\ =0.$

Indeed by definition, $(X)^{\Uparrow Y}$ = $\\{h+y\in(2^{\omega})^{X\cup Y}$
$|$ $h\in\mathcal{X}\\}$. So (since $X\cap Y$ = $\emptyset$), if
$f\not\in\mathcal{X}$, $\\{g\in$ ($2^{\omega}$)Y $|$ $f+g\in(X)^{\Uparrow
Y}\\}$ = $\emptyset$. Trivially, also $\\{g\in$ ($2^{\omega}$)Y $|$
$f+g\in\mathcal{Z}\cap(X)^{\Uparrow Y}\\}$ = $\emptyset$.

∎

It is possible to prove that, for $a\not\in X,\mathrm{FN}(A)\subseteq X,$ and
$f\in$ ($2^{\omega}$)X, if $f\in\llbracket A\rrbracket_{X},$ then
$\Pi_{f}$($\llbracket A\rrbracket_{X\cup\\{a\\}}$) = ($2^{\omega}$){a}.
Intuitively, since $a\not\in\mathrm{FN}(A),\llbracket
A\rrbracket_{X\cup\\{a\\}}$ is a set of $f\in$ ($2^{\omega}$)X∪{a}, the
characterization of which _does not_ rely on $\\{a\\}$. So, for each
$\alpha\in Y$, either $f$($\alpha$) $\in\llbracket A\rrbracket_{X}$, and
$f+g\in\llbracket A\rrbracket_{X\cup\\{a\\}}$, or $f$($\alpha$)
$\not\in\llbracket A\rrbracket_{X}$, and $f+g\not\in\llbracket
A\rrbracket_{X\cup\\{a\\}}$. Therefore if $f\in\llbracket
A\rrbracket_{X},\Pi_{f}(\llbracket A\rrbracket_{X\cup\\{a\\}}$) =
($2^{\omega}$){a}

######  Lemma 40.

Let $a\not\in X,\mathrm{FN}(A)\subseteq X,$ and $f\in(2^{\omega})^{X}$:

  * •

if $f\in\llbracket A\rrbracket_{X},$ then $\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})=(2^{\omega})^{\\{a\\}}$

  * •

if $f\not\in\llbracket A\rrbracket_{X},$ then $\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})=\emptyset^{\\{a\\}}$

(or equivalently, $\llbracket A\rrbracket_{X\cup\\{a\\}}=\llbracket
A\rrbracket_{X}^{\Uparrow\\{a\\}}$).

###### Proof.

Since $a\not\in\mathrm{FN}(A)$ for every $a\in Y$, there are two possible
cases:

  * •

if $f$($\alpha$) $\in\llbracket A\rrbracket_{X}$, then $f+g\in\llbracket
A\rrbracket_{X\cup\\{a\\}}$

  * •

if $f$($\alpha$) $\not\in\llbracket A\rrbracket_{X}$, then
$f+g\not\in\llbracket A\rrbracket_{X\cup\\{a\\}}$.

Thus, Let $f\in\llbracket A\rrbracket_{X}$. Then,

$\displaystyle\Pi_{f}(\llbracket A\rrbracket_{X\cup\\{a\\}})$
$\displaystyle=\\{g\in(2^{\omega})^{\\{a\\}}\ |\ f+g\in\llbracket
A\rrbracket_{X\cup\\{a\\}}\\}$ $\displaystyle=\\{g\in(2^{\omega})^{\\{a\\}}\
|\ f\in\llbracket A\rrbracket_{X}\\}$ $\displaystyle=(2^{\omega})^{\\{a\\}}.$

Let $f\not\in\llbracket A\rrbracket_{X}$. Then,

$\displaystyle\Pi_{f}(\llbracket A\rrbracket_{X\cup\\{a\\}})$
$\displaystyle=\\{g\in(2^{\omega})^{\\{a\\}}\ |\ f+g\in\llbracket
A\rrbracket_{X\cup\\{a\\}}\\}$ $\displaystyle=\\{g\in(2^{\omega})^{\\{a\\}}\
|\ f\in\llbracket A\rrbracket_{X}\\}$ $\displaystyle=\emptyset^{\\{a\\}}.$

∎

######  Corollary 5.

Let $a\not\in X,\mathrm{FN}(A)\subseteq X,f\in(2^{\omega})^{X},$ and $q>0$.
Then:

$\displaystyle\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\big{)}\geq q$ $\displaystyle\text{ iff
}f\in\llbracket A\rrbracket_{X}$ $\displaystyle\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cap\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q\wedge\mu\big{(}\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q$ $\displaystyle\text{ iff
}f\in\llbracket A\rrbracket_{X}$ $\displaystyle\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cup\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q\vee\mu\big{(}\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q$ $\displaystyle\text{ iff
}f\in\llbracket A\rrbracket_{X}$ $\displaystyle\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cup\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}<q\wedge\mu\big{(}\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}<q$ $\displaystyle\text{ iff
}f\not\in\llbracket A\rrbracket_{X}$

###### Proof.

First, let us consider:

$\mu\big{(}\Pi_{f}(\llbracket A\rrbracket_{X\cup\\{a\\}})\big{)}\geq q\text{
iff }f\in\llbracket A\rrbracket_{X}$

For every $\alpha^{\prime}\in X$, there are two possible cases:

  * •

$f$($\alpha^{\prime}$) $\in\llbracket A\rrbracket_{X}$. Then
$\Pi_{f}$($\llbracket A\rrbracket_{X\cup\\{a\\}}$) = $\\{g\in$
($2^{\omega}$){a} $|$ $f$($\alpha^{\prime}$) $\in\llbracket
A\rrbracket_{X}\\}$ = ($2^{\omega}$){a}. So, for every $q$,
$\Pi_{f}$($\llbracket A\rrbracket_{X\cup\\{a\\}}$) $\geq q$

  * •

$f$($\alpha^{\prime}$) $\not\in\llbracket A\rrbracket_{X}$. Then
$\Pi_{f}$($\llbracket A\rrbracket_{X\cup\\{a\\}}$) = $\\{g\in$
($2^{\omega}$){a} $|$ $f$($\alpha^{\prime}$) $\in\llbracket
A\rrbracket_{X}\\}$ = $\emptyset^{\\{a\\}}$. So, for every $q$ ($q\neq$ 0),
$\Pi_{f}$($\llbracket A\rrbracket_{X\cup\\{a\\}}$) $<q$.

Let us now consider:

$\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cap\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q\wedge\mu\big{(}\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q\text{ iff }f\in\llbracket
A\rrbracket_{X}.$

There are two cases to be taken into account:

  * •

$f\in\llbracket A\rrbracket_{X}$. For Lemma 40 ($a\not\in X$),
$\Pi_{f}(\llbracket A\rrbracket_{X\cup\\{a\\}})$ = $(2^{\omega})^{\\{a\\}}$,
so

$\displaystyle\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cap\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$
$\displaystyle=\mu\big{(}(2^{\omega})^{\\{a\\}}\cap\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$
$\displaystyle=\mu\big{(}\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}.$

  * •

$f\not\in\llbracket A\rrbracket_{X}$. For Lemma 40, $\Pi_{f}$($\llbracket
A\rrbracket_{X\cup\\{a\\}}$) = $\emptyset^{X}$, so

$\displaystyle\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cap\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$
$\displaystyle=\mu\big{(}\emptyset^{\\{a\\}}\cap\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$
$\displaystyle=\mu\big{(}\emptyset^{\\{a\\}}\big{)}$ $\displaystyle=0.$

Therefore,

  * $\Leftarrow$

If $f\in\llbracket A\rrbracket_{X}$ and $\mu\big{(}\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q$, then for the first clause
$\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cap\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$ = $\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}}))$. Therefore, $\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cap\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q$.

  * $\Rightarrow$

If $f\not\in\llbracket A\rrbracket_{X},$ then for the second clause
$\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cap\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}=0$. Therefore,
$\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cap\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}<q$.
If $f\in\llbracket A\rrbracket_{X}$ and $\mu\big{(}\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}<q$, for the first clause
$\mu\big{(}\Pi_{f}(\llbracket A\rrbracket_{X\cup\\{a\\}}\cap\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$ = $\mu\big{(}\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$. So, $\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cap\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}<q$.

It is now possible to take into account:

$\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cup\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q\vee\mu\big{(}\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q\text{ iff }f\in\llbracket
A\rrbracket_{X}.$

There are two cases to be considered:

  * •

$f\in\llbracket A\rrbracket_{X}$. For Lemma 40, ($a\not\in X$),
$\Pi_{f}$($\llbracket A\rrbracket_{X\cup\\{a\\}}$) = ($2^{\omega}$){a}, so

$\displaystyle\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cup\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$
$\displaystyle=\mu\big{(}(2^{\omega})^{\\{a\\}}\cup\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$
$\displaystyle=\mu\big{(}(2^{\omega})^{\\{a\\}}\big{)}$
$\displaystyle=1.\normalsize$

  * •

$f\not\in\llbracket A\rrbracket_{X}$. For Lemma 40, $\Pi_{f}$($\llbracket
A\rrbracket_{X\cup\\{a\\}}$) = $\emptyset^{X}$, so

$\displaystyle\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cup\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$
$\displaystyle=\mu\big{(}\emptyset^{\\{a\\}}\cup\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$
$\displaystyle=\mu\big{(}\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}.$

Therefore,

  * $\Leftarrow$

If $f\in\llbracket A\rrbracket_{X},$ then, for the first clause,
$\mu$($\Pi$($\llbracket A\rrbracket_{X\cup\\{a\\}}$) $\cup$
$\Pi_{f}$($\llbracket B\rrbracket_{X\cup\\{a\\}}$)) = 1. So, for every $q$,
$\mu$($\Pi_{f}$($\llbracket A\rrbracket_{X\cup\\{a\\}}$) $\cup$
$\Pi$($\llbracket B\rrbracket_{X\cup\\{a\\}}$)) $\geq q$.
If $\mu$($\Pi_{f}$($\llbracket B\rrbracket_{X\cup\\{a\\}}$)) $\geq q$, then
also $\mu$($\Pi_{f}$($\llbracket A\rrbracket_{X\cup\\{a\\}}$) $\cup$
$\Pi_{f}$($\llbracket B\rrbracket_{X\cup\\{a\\}}$)) $\geq q$.

  * $\Rightarrow$

If $f\not\in\llbracket A\rrbracket_{X}$ and $\mu$($\Pi_{f}$($\llbracket
B\rrbracket_{X\cup\\{a\\}}$)) $<q$, then, for the second clause,
$\mu$($\Pi_{f}$($\llbracket A\rrbracket_{X\cup\\{a\\}}$) $\cup$
$\Pi_{f}$($\llbracket B\rrbracket_{X\cup\\{a\\}}$)) =
$\mu$($\Pi_{f}$($\llbracket B\rrbracket_{X\cup\\{a\\}}$)) $<q$.

It is now possible to deal with:

$\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cup\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}<q\wedge\mu\big{(}\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}<q\text{ iff }f\not\in\llbracket
A\rrbracket_{X}.$

Let us take into account two cases:

  * •

$f\in\llbracket A\rrbracket_{X}$. By Lemma 40 ($a\not\in X$),
$\Pi_{f}\big{(}\llbracket A\rrbracket_{X\cup\\{a\\}}\big{)}$ =
($2^{\omega}$){a}, so

$\displaystyle\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cup\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$
$\displaystyle=\mu\big{(}(2^{\omega})^{\\{a\\}}\cup\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$
$\displaystyle=\mu\big{(}(2^{\omega})^{\\{a\\}}\big{)}$ $\displaystyle=1$

  * •

$f\not\in\llbracket A\rrbracket_{X}$. By Lemma 40, $\Pi_{f}\big{(}\llbracket
A\rrbracket_{X\cup\\{a\\}}\big{)}$ = $\emptyset^{\\{a\\}}$, so

$\displaystyle\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cup\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$
$\displaystyle=\mu\big{(}\emptyset^{\\{a\\}}\cup\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$
$\displaystyle=\mu\big{(}\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}.$

Therefore,

  * $\Leftarrow$

Let $f\not\in\llbracket A\rrbracket_{X}$ and $\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\big{)}<q$. For the second clause,
$\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cup\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$ = $\mu\big{(}\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$. Since for hypothesis
$\mu\big{(}\Pi_{f}(\llbracket B\rrbracket_{X\cup\\{a\\}})\big{)}<q$, also
$\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cup\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}<q$.

  * $\Rightarrow$

Let $f\in\llbracket A\rrbracket_{X}$. For the first clause
$\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cup\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}=1$. Thus, for every $q$,
$\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cup\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}>q$.
Let $f\not\in\llbracket A\rrbracket_{X}$ and $\mu\big{(}\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q$. For the second clause,
$\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cup\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$ = $\mu\big{(}\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$. For hypothesis,
$\mu\big{(}\Pi_{f}(\llbracket A\rrbracket_{X\cup\\{a\\}})\big{)}\geq q$, thus
also $\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cup\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q$.

∎

See 10

###### Proof.

Let us show:

$\llbracket
A\wedge\mathbf{C}^{q}_{a}B\rrbracket_{X}=\llbracket\mathbf{C}^{q}_{a}(A\wedge
B)\rrbracket_{X}.$

For the Definition 4.3,202020That $\mathbf{C}^{q}_{a}$ is well-defined is
guaranteed by the fact that $X$ = $X_{A}\cup(X_{B}/\\{a\\})$ so, for
hypothesis, $a\not\in X$.

$\llbracket A\wedge\mathbf{C}^{q}_{a}B\rrbracket_{X}=\llbracket
A\rrbracket_{X}\cap\llbracket\mathbf{C}^{q}_{a}B\rrbracket_{X}.$

Let $f\in$ ($2^{\omega}$)X. There are two cases:

  * •

$\mu\big{(}\Pi_{f}(\llbracket B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q$. Since
$\\{f\in(2^{\omega})^{X}\ |$ $\mu\big{(}\Pi_{f}(\llbracket
B\rrbracket)_{X\cup\\{a\\}})\big{)}\geq q\\}$ = ($2^{\omega}$)X,

$\displaystyle\llbracket A\wedge\mathbf{C}^{q}_{a}B\rrbracket_{X}$
$\displaystyle=\llbracket
A\rrbracket_{X}\cap\llbracket\mathbf{C}^{q}_{a}B\rrbracket_{X}$
$\displaystyle=\llbracket A\rrbracket_{X}\cap(2^{\omega})^{X}$
$\displaystyle=\llbracket A\rrbracket_{X}$

  * •

$\mu\big{(}\Pi_{f}(\llbracket A\rrbracket_{X\cup\\{a\\}})\big{)}<q$. Since
$\\{f\in$ ($2^{\omega}$)X $|$ $\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X})\big{)}\geq q\\}$ = $\emptyset^{X}$,

$\displaystyle\llbracket A\wedge\mathbf{C}^{q}_{a}B\rrbracket_{X}$
$\displaystyle=\llbracket
A\rrbracket_{X}\cap\llbracket\mathbf{C}^{q}_{a}B\rrbracket_{X}$
$\displaystyle=\llbracket A\rrbracket_{X}\cap\emptyset^{X}$
$\displaystyle=\emptyset^{X}.$

So,

$\llbracket A\wedge\mathbf{C}^{q}_{a}B\rrbracket_{X}=\begin{cases}\llbracket
A\rrbracket_{X}\ \ \ &\text{ if }\mu(\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\geq q\\\ \emptyset^{X}\ \ \ &\text{
otherwise}\end{cases}$

On the other hand,

$\displaystyle\llbracket\mathbf{C}^{q}_{a}(A\wedge B)\rrbracket_{X}$
$\displaystyle=\\{f\in(2^{\omega})^{X}\ |\ \mu\big{(}\Pi_{f}(\llbracket
A\wedge B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q\\}$
$\displaystyle=\\{f\in(2^{\omega})^{X}\ |\ \mu\big{(}\Pi(\llbracket
A\rrbracket_{X\cup\\{a\\}}\cap\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q\\}$
$\displaystyle=\\{f\in(2^{\omega})^{X}\ |\ \mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cap\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q\\}$

There are two possible cases:

  * •

Let $\mu\big{(}\Pi_{f}(\llbracket B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q$.
Then,

$\displaystyle\llbracket\mathbf{C}^{q}_{a}(A\wedge B)\rrbracket_{X}=\ \ $
$\displaystyle\\{f\in(2^{\omega})^{X}\ |\ \mu(\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cap\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}}))\geq q\\}$
$\displaystyle\stackrel{{\scriptstyle\text{C}\leavevmode\nobreak\
\ref{C1}}}{{=}}$ $\displaystyle\\{f\in(2^{\omega})^{X}\ |\ f\in\llbracket
A\rrbracket_{X}\wedge\mu(\Pi_{f}(\llbracket B\rrbracket_{X\cup\\{a\\}}))\geq
q\\}$ $\displaystyle=\ \ $ $\displaystyle\\{f\in(2^{\omega})^{X}\ |\
f\in\llbracket A\rrbracket_{X}\\}$ $\displaystyle=\ \ $
$\displaystyle\llbracket A\rrbracket_{X}$

  * •

Let $\mu\big{(}\Pi_{f}(\llbracket B\rrbracket_{X\cup\\{a\\}})\big{)}<q$. Since
$\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cap(\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$ $\leq$ $\mu\big{(}\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}$, then $\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cap\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}<q$. So, $\\{f\in(2^{\omega}$)X $|$
$\mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cap\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q\\}=\emptyset$:

$\displaystyle\llbracket\mathbf{C}^{q}_{a}(A\wedge B)\rrbracket_{X}$
$\displaystyle=\\{f\in(2^{\omega})^{X}\ |\ \mu\big{(}\Pi_{f}(\llbracket
A\rrbracket_{X\cup\\{a\\}})\cap\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q\\}$ $\displaystyle=\emptyset^{X}.$

Therefore,

$\displaystyle\llbracket\mathbf{C}^{q}_{a}(A\wedge B)\rrbracket_{X}$
$\displaystyle=\begin{cases}\llbracket A\rrbracket_{X}\ \ \ &\text{ if
}\mu(\Pi_{f}(\llbracket B\rrbracket_{X\cup\\{a\\}}))\geq q\\\ \emptyset^{X}\ \
\ &\text{ otherwise}\end{cases}$ $\displaystyle=\llbracket
A\wedge\mathbf{C}^{q}_{a}B\rrbracket_{X}$

Let us now show that:

$\llbracket
A\vee\mathbf{C}^{q}_{a}B\rrbracket_{X}=\llbracket\mathbf{C}^{q}_{a}(A\vee
B)\rrbracket_{X}.$

By Definition 4.3,

$\llbracket A\vee\mathbf{C}^{q}_{a}B\rrbracket_{X}=\llbracket
A\rrbracket_{X}\cup\llbracket\mathbf{C}_{a}^{q}B\rrbracket_{X}$

Let $f\in$ ($2^{\omega}$)X. There are two possible cases:

  * •

$\mu\big{(}\Pi_{f}(\llbracket B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q$. Since
$\\{f\in$ ($2^{\omega}$)X $|$ $\mu\big{(}\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q\\}$ = ($2^{\omega}$)X,

$\displaystyle\llbracket A\vee\mathbf{C}^{q}_{a}B\rrbracket_{X}$
$\displaystyle=\llbracket
A\rrbracket_{X}\cup\llbracket\mathbf{C}^{q}_{a}B\rrbracket_{X}$
$\displaystyle=\llbracket A\rrbracket_{X}\cup(2^{\omega})^{X}$
$\displaystyle=(2^{\omega})^{X}.$

  * •

$\mu\big{(}\Pi_{f}(\llbracket B\rrbracket_{X\cup\\{a\\}})\big{)}<q$. Since
$\\{f\in(2^{\omega})^{X}\ |\ \mu\big{(}\Pi_{f}(\llbracket
B\rrbracket_{X\cup\\{a\\}})\big{)}\geq q\\}$ = $\emptyset^{X}$,

$\displaystyle\llbracket A\vee\mathbf{C}^{q}_{a}B\rrbracket_{X}$
$\displaystyle=\llbracket
A\rrbracket_{X}\cup\llbracket\mathbf{C}^{q}_{a}B\rrbracket_{X}$
$\displaystyle=\llbracket A\rrbracket_{X}\cup\emptyset^{X}$
$\displaystyle=\llbracket A\rrbracket_{X}.$

Thus,

$\llbracket
A\vee\mathbf{C}^{q}_{a}B\rrbracket_{X}=\begin{cases}(2^{\omega})^{X}\ \
&\text{ if }\mu(\Pi_{f}(\llbracket B\rrbracket_{X\cup\\{a\\}}))\geq q\\\
\llbracket A\rrbracket_{X}\ \ &\text{ otherwise}\end{cases}$

On the other hand,