Let $\rhd_{\textbf{{\L${}_{3}$}}}^{\to}$ be the Set-Set logic determined by
the three-valued logical matrix $\mathbb{M}_{\textbf{{\L${}_{3}$}}}^{\to}$
whose signature contains only $\to$, interpreted as
$\to_{\textrm{{{\L${}_{3}$}}}}$ in this case — the truth table of which we
repeat below for convenience — and whose set of designated values is
$\\{\mathbf{1}\\}$. The reader can easily verify that this matrix is not
monadic, as applications of $\to_{\textrm{{{\L${}_{3}$}}}}$ on the same value
always yield $\mathbf{1}$. As in the previous section, despite this fact, we
will axiomatize this logic in Set-Set.

$\to_{\textrm{{{\L${}_{3}$}}}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
---|---|---|---
$\mathbf{0}$ | $\mathbf{1}$ | $\mathbf{1}$ | $\mathbf{1}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$ | $\mathbf{1}$
$\mathbf{1}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$

######  Definition 5.33.

Let $\mathsf{R}^{\to}_{\textbf{{\L${}_{3}$}}}$ be the Set-Set calculus whose
rule schemas are the following:

$\displaystyle\frac{q}{p\to
q}\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{1,\to}\quad\frac{p_{1}\to
p_{2},p_{1}}{p_{2}}\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{2,\to}\quad\frac{(p_{1}\to
p_{2})\to q_{0}}{p_{2}\to
q_{0}}\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{3,\to}\quad\frac{p_{2}\to
q_{0},p_{1}}{(p_{1}\to p_{2})\to
q_{0}}\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{4,\to}$ $\displaystyle\frac{p_{1}\to
p_{2},p_{2}\to q_{0}}{p_{1}\to
q_{0}}\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{5,\to}\quad\frac{(p_{1}\to p_{2})\to
q_{0},p_{2}\to q_{0}}{p_{1}\to
q_{0},p_{1}}\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{6,\to}$
$\displaystyle\frac{p_{1}\to q_{0}}{p_{1}\to p_{2},q_{\frac{1}{2}}\to
q_{0},q_{\frac{1}{2}}}\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{7,\to}\quad\frac{}{p_{1}\to
p_{2},p_{2}\to q_{0},p_{1}}\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{8,\to}$

######  Theorem 5.34.

$\mathsf{R}^{\to}_{\textbf{{\L${}_{3}$}}}$ is sound for
$\mathbb{M}_{\textbf{{\L${}_{3}$}}}^{\to}$.

###### Proof.

This is routine. ∎

######  Theorem 5.35.

$\mathsf{R}^{\to}_{\textbf{{\L${}_{3}$}}}$ is complete for
$\mathbb{M}_{\textbf{{\L${}_{3}$}}}^{\to}$ and $\\{p\to q\\}$-analytic.

###### Proof.

Let $\Theta:=\\{p\to q\\}$. Suppose that
$\Phi\blacktriangleright_{\mathsf{R}^{\to}_{\textbf{{\L${}_{3}$}}}}^{\Theta}\Psi$,
then, by cut for sets, there is $\Pi\subseteq L_{\Sigma}(P)$ such that
$\Pi\blacktriangleright_{\mathsf{R}^{\to}_{\textbf{{\L${}_{3}$}}}}^{\Theta}{\Pi}^{\mathsf{c}}$,
with $\Phi\subseteq\Pi$ and $\Psi\subseteq{\Pi}^{\mathsf{c}}$. Let
$S:=\mathsf{subf}(\Phi\cup\Psi)\cup\\{\varphi\to\psi\mid\varphi,\psi\in\mathsf{subf}(\Phi\cup\Psi)\\}$.
Then
$T\blacktriangleright_{\mathsf{R}^{\to}_{\textbf{{\L${}_{3}$}}}}^{\Theta}F$
for some partition $(T,F)$ of $S$, with $\Phi\subseteq T$ and $\Psi\subseteq
F$. We consider two cases, defining for each of them a mapping
$v:\mathsf{subf}(\Phi\cup\Psi)\to V_{3}$ and proving that
$v(\varphi\to\psi)=v(\varphi)\to_{\textrm{{{\L${}_{3}$}}}}v(\psi)$:

  * •

(a): for every $\varphi,\psi\in F\cap\mathsf{subf}(\Phi\cup\Psi)$, we have
$\varphi\to\psi\in T$. Let us define $v:\mathsf{subf}(\Phi\cup\Psi)\to V_{3}$
such that

$v(\varphi):=\begin{cases}\mathbf{1}&\text{ if }\varphi\in T\\\
\mathbf{0}&\text{ if }\varphi\in F\\\ \end{cases}$

    * –

if $v(\varphi)=\mathbf{1}$ and $v(\psi)=\mathbf{0}$: by rule
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{2,\to})$, we must have
$\varphi\to\psi\in F$, that is, $v(\varphi\to\psi)=\mathbf{0}$;

    * –

if $v(\varphi\to\psi)=\mathbf{0}$: by
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{1,\to})$, we have $\psi\in F$ and, by
(a), we must have $\varphi\in T$;

    * –

if $v(\varphi)=\mathbf{0}$: by $(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{8,\to})$,
we have that (b): $\varphi\to\psi\in T$ or (c): $\psi\to\varphi\in T$. Case
(b), we are done. Case (c), by $(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{2,\to})$,
we have $\psi\in F$, and then, by (a), we have $\varphi\to\psi\in T$;

    * –

if $v(\psi)=\mathbf{1}$: by rule
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{1,\to})$, we must have
$\varphi\to\psi\in T$;

    * –

if $v(\varphi\to\psi)=\mathbf{1}$: by
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{2,\to})$, we must have either
$\varphi\in F$ or $\psi\in T$.

  * •

there are
$\varphi_{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}},\psi_{\mathbf{0}}\in
F\cap\mathsf{subf}(\Phi\cup\Psi)$ with
$\varphi_{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}}\to\psi_{\mathbf{0}}\in F$. In
this case, let $v:\mathsf{subf}(\Phi\cup\Psi)\to V_{3}$ such that

$v(\varphi):=\begin{cases}\mathbf{1}&\text{ if }\varphi\in T\\\
\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}&\text{ if
}\varphi,\varphi\to\psi_{\mathbf{0}}\in F\\\ \mathbf{0}&\text{ if }\varphi\in
F,\varphi\to\psi_{\mathbf{0}}\in T\\\ \end{cases}$

    * –

if $v(\varphi)=\mathbf{1}$ and $v(\psi)=\mathbf{0}$: we have $\psi\in
F,\psi\to\psi_{\mathbf{0}}\in T$, then, by
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{4,\to})$, we have
$(\varphi\to\psi)\to\psi_{\mathbf{0}}\in T$, and, by
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{1,\to})$, $\varphi\to\psi\in F$, thus
$v(\varphi\to\psi)=\mathbf{0}$;

    * –

if $v(\varphi\to\psi)=\mathbf{0}$: by
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{3,\to})$, we have
$\psi\to\psi_{\mathbf{0}}\in T$ and by
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{2,\to})$, we have $\psi\in F$, thus
$v(\psi)=\mathbf{0}$; by $(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{6,\to})$, we
have either $\varphi\in T$ or $\varphi\to\psi_{\mathbf{0}}\in T$. In the first
case, we are done; the second case leads to an absurd, by
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{7,\to})$, since
$\varphi_{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}}\to\psi_{\mathbf{0}},\psi_{\mathbf{0}}\in
F$;

    * –

if $v(\varphi)=\mathbf{0}$: by rule
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{8,\to})$, we have either
$\varphi\to\psi\in T$ or
$\psi\to\psi_{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}}\in T$. In the first case,
we are done. In the second, we must have $\varphi\to\psi\in T$ by rule
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{7,\to})$;

    * –

if $v(\psi)=\mathbf{1}$: by rule
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{1,\to})$, we have $\varphi\to\psi\in T$;

    * –

if $v(\varphi\to\psi)=\mathbf{1}$: then $\varphi\to\psi\in T$. By
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{2,\to})$, we have either (b):
$\varphi\in F$ or (c): $\psi\in T$. In case (b), by
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{5,\to})$, we have either (d):
$\varphi\to\psi_{\mathbf{0}}\in T$ or (e): $\psi\to\psi_{\mathbf{0}}\in F$.
Case (d), we have $v(\varphi)=\mathbf{0}$, as desired. Case (e), if $\psi\in
T$, we are done, and if $\psi\in F$, we will have
$v(\psi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$, and we are also done. Case
(c), that is, $\psi\in T$, $v(\psi)=\mathbf{1}$ and we are done;

    * –

if $v(\varphi\to\psi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$: then
$\varphi\to\psi,(\varphi\to\psi)\to\psi_{\mathbf{0}}\in F$. Then, by
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{4,\to})$, either (b): $\varphi\in F$ or
(c): $\psi\to\psi_{\mathbf{0}}\in F$. Case (b), by
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{8,\to})$, we have
$\psi\to\psi_{\mathbf{0}}\in T$, and, by
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{2,\to})$, we have $\psi\in F$, meaning
that $v(\psi)=\mathbf{0}$. Moreover, by
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{7,\to})$, we have
$\varphi\to\psi_{\mathbf{0}}\in F$, hence
$v(\varphi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$, as desired. Case (c), by
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{8,\to})$ we have $\varphi\in T$, i.e.
$v(\varphi)=\mathbf{1}$. Also, by
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{1,\to})$ and the fact that
$\varphi\to\psi\in F$, we have $\psi\in F$, and then
$v(\psi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$, as desired;

    * –

if $v(\varphi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ and
$v(\psi)=\mathbf{0}$: then $\varphi,\varphi\to\psi_{\mathbf{0}}\in F$ and
$\psi\in F$ and $\psi\to\psi_{\mathbf{0}}\in T$. By
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{5,\to})$, we have $\varphi\to\psi\in F$,
and, by $(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{6,\to})$, we have
$(\varphi\to\psi)\to\psi_{\mathbf{0}}\in F$, we have
$v(\varphi\to\psi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$.

    * –

if $v(\varphi)=\mathbf{1}$ and
$v(\psi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$: then $\varphi\in T$, $\psi\in
F$ and $\psi\to\psi_{\mathbf{0}}\in T$. By
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{4,\to})$, we have
$(\varphi\to\psi)\to\psi_{\mathbf{0}}\in F$, and, by
$(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{1,\to})$, we have $\varphi\to\psi\in F$,
thus $v(\varphi\to\psi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$.

∎

####  5.2.3 Implicative fragment of Gödel’s logic

The last example in this series of three-valued logics determined by non-
monadic matrices concerns $\rhd_{\textbf{{G3}}}^{\to}$, the Set-Set logic
determined by the three-valued logical matrix
$\mathbb{M}_{\textbf{{G3}}}^{\to}$ — we repeat the interpretation of $\to$
below for convenience. In this case, we will be able to take advantage of the
calculus introduced in the previous subsection in order to obtain the desired
axiomatization.

$\to_{\textbf{{G3}}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
---|---|---|---
$\mathbf{0}$ | $\mathbf{1}$ | $\mathbf{1}$ | $\mathbf{1}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{0}$ | $\mathbf{1}$ | $\mathbf{1}$
$\mathbf{1}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$

######  Definition 5.36.

Let $\mathsf{R}^{\to}_{\textbf{{G3}}}$ be the Set-Set calculus whose rule
schemas are the same as those of $\mathsf{R}^{\to}_{\textbf{{\L${}_{3}$}}}$,
except that we replace $(\mathsf{r}_{\textbf{{\L${}_{3}$}}}^{6,\to})$ by the
following:

$\displaystyle\frac{p_{2}\to q_{0}}{(p_{1}\to p_{2})\to q_{0},p_{1}\to
q_{0}}(\mathsf{r}_{\textbf{{G3}}}^{6,\to})$

######  Theorem 5.37.

$\mathsf{R}^{\to}_{\textbf{{G3}}}$ is sound for
$\mathbb{M}_{\textbf{{G3}}}^{\to}$.

###### Proof.

This is routine. ∎

######  Theorem 5.38.

$\mathsf{R}^{\to}_{\textbf{{G3}}}$ is complete for
$\mathbb{M}_{\textbf{{G3}}}^{\to}$ and $\\{p\to q\\}$-analytic.

###### Proof.

The proof is very similar to the one of Theorem 5.35, differing only in some
sub-cases of the second item:

  * •

if $v(\varphi\to\psi)=\mathbf{0}$: then $\varphi\to\psi\in F$ and
$(\varphi\to\psi)\to\psi_{\mathbf{0}}\in T$. By
$(\mathsf{r}_{\textbf{{G3}}}^{3,\to})$, we have $\psi\to\psi_{\mathbf{0}}\in
T$ and by $(\mathsf{r}_{\textbf{{G3}}}^{2,\to})$, we have $\psi\in F$, thus
$v(\psi)=\mathbf{0}$; also, by $(\mathsf{r}_{\textbf{{G3}}}^{7,\to})$, we have
$\varphi\to\psi_{\mathbf{0}}\in F$. Then, if $\varphi\in T$, we are done, and
if $\varphi\in F$, we have $v(\varphi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$,
as desired.

  * •

if $v(\varphi\to\psi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$: then
$\varphi\to\psi,(\varphi\to\psi)\to\psi_{\mathbf{0}}\in F$. Then, by
$(\mathsf{r}_{\textbf{{G3}}}^{4,\to})$, either (b): $\varphi\in F$ or (c):
$\psi\to\psi_{\mathbf{0}}\in F$. Case (b), by
$(\mathsf{r}_{\textbf{{G3}}}^{8,\to})$, we have $\psi\to\psi_{\mathbf{0}}\in
T$. By $(\mathsf{r}_{\textbf{{G3}}}^{7,\to})$, we have
$\varphi\to\psi_{\mathbf{0}}\in F$, but, by
$(\mathsf{r}_{\textbf{{G3}}}^{6,\to})$, we have
$\varphi\to\psi_{\mathbf{0}}\in T$, an absurd. Case (c), by
$(\mathsf{r}_{\textbf{{G3}}}^{8,\to})$ we have $\varphi\in T$, i.e.
$v(\varphi)=\mathbf{1}$. Also, by $(\mathsf{r}_{\textbf{{G3}}}^{1,\to})$ and
the fact that $\varphi\to\psi\in F$, we have $\psi\in F$, and then
$v(\psi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$, as desired;

  * •

if $v(\varphi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ and
$v(\psi)=\mathbf{0}$: then $\varphi,\varphi\to\psi_{\mathbf{0}}\in F$ and
$\psi\in F$ and $\psi\to\psi_{\mathbf{0}}\in T$. By
$(\mathsf{r}_{\textbf{{G3}}}^{5,\to})$, we have $\varphi\to\psi\in F$, and, by
$(\mathsf{r}_{\textbf{{G3}}}^{6,\to})$, we have
$(\varphi\to\psi)\to\psi_{\mathbf{0}}\in T$, we have
$v(\varphi\to\psi)=\mathbf{0}$.

∎

##  6 Some correspondences between 3-labelled and multiple-conclusion Hilbert-
style calculi

As to the comparison between three-labelled and Set-Set Hilbert-style calculi,
we first observe the following: Set-Set Hilbert-style calculi manipulate sets
of formulas according to the Tarskian postulates (cf. Definition 2.2), so the
structural rules of three-labelled calculi (Identity, Weakening and Cut — see
Section 4) are implicitly assumed. Therefore, we can confine ourselves to
consider logical rules. For simplicity, we will also limit ourselves in this
section to matrices with the single element $\mathbf{1}$ designated, as
adapting the results to the other cases is not a difficult task. The following
shows a correspondence between the generating subprocedures of each formalism.
To allow for a more general presentation, we use the subprocedure of the Set-
Set formalism for the non-deterministic case [31], which is equivalent to the
one we presented in Section 5.16:

######  Theorem 6.1.

Consider the three-valued monadic matrix
$\mathbb{M}:=\langle\mathbf{A},\\{\mathbf{1}\\}\rangle$. For each
$k\in\omega$, $\copyright\in\Sigma^{k}$, and for all
$\nu_{1},\ldots,\nu_{n}\in V_{3}$, the 3-labelled rule

$(\Phi\mid\Psi\mid\Gamma)[\,\nu_{1}:\varphi_{1}\,]\quad\cdots\quad(\Phi\mid\Psi\mid\Gamma)[\,\nu_{n}:\varphi_{n}\,]$
(R)
$(\Phi\mid\Psi\mid\Gamma)[\,\nu:\copyright(\varphi_{1},\ldots,\varphi_{n})\,]$

is generated by the sub-procedure for 3-labelled calculi if, and only if, the
Set-Set rules

$(\mathsf{r}_{1})\frac{\bigcup_{i=1}^{n}\Omega_{\nu_{i}}(\varphi_{i})\cup\Omega_{\bar{y}_{1}}(\copyright(\varphi_{1},\ldots,\varphi_{n}))}{\bigcup_{i=1}^{n}\mho_{\nu_{i}}(\varphi_{i})\cup\mho_{\bar{y}_{1}}(\copyright(\varphi_{1},\ldots,\varphi_{n}))}\qquad(\mathsf{r}_{2})\frac{\bigcup_{i=1}^{n}\Omega_{\nu_{i}}(\varphi_{i})\cup\Omega_{\bar{y}_{2}}(\copyright(\varphi_{1},\ldots,\varphi_{n}))}{\bigcup_{i=1}^{n}\mho_{\nu_{i}}(\varphi_{i})\cup\mho_{\bar{y}_{2}}(\copyright(\varphi_{1},\ldots,\varphi_{n}))}$

are generated by the sub-procedure for Set-Set Hilbert-style calculi in the
non-deterministic setting (cf.[31]), where
$V_{3}=\\{\bar{y}_{1},\bar{y}_{2},\copyright_{\mathbf{A}}(\nu_{1},\ldots,\nu_{n})\\}$.

###### Proof.

From the left to the right, assume that (R) was generated by the sub-procedure
for 3-labelled calculi, meaning that
${\copyright}_{\mathbf{A}}(\nu_{1},\ldots,\nu_{k})=y$. Then the procedure for
generating Set-Set calculi in the non-deterministic setting produces one rule
for each $z\neq{\copyright}_{\mathbf{A}}(\nu_{1},\ldots,\nu_{k})$, whose shape
is given precisely by $(\mathsf{r}_{1})$ and $(\mathsf{r}_{2})$, where
$\\{\bar{y}_{1},\bar{y}_{2}\\}=V_{3}\setminus\\{{\copyright}_{\mathbf{A}}(\nu_{1},\ldots,\nu_{k})\\}$.
The converse direction is similar: if $(\mathsf{r}_{1})$ and
$(\mathsf{r}_{2})$ are produced, then a single rule will be generated by the
3-labelled sub-procedure bearing witness to the fact that
$y={\copyright}_{\mathbf{A}}(\nu_{1},\ldots,\nu_{k})\not\in\\{\bar{y}_{1},\bar{y}_{2}\\}$.
Notice that, in this way, if $\copyright$ is $n$-ary, a single 3-labelled rule
per entry is produced ($3^{n}$ rules at the end), while two Set-Set rules are
produced per entry (so, $2\cdot 3^{n}$ rules) by the Set-Set sub-procedure.
Thus, a 3-labelled rule corresponds to two Set-Set rules (and vice-versa). ∎

######  Example 6.2.

Here we show some correspondences between rules of
$s\ell.{\textbf{{\L${}_{3}$}}}$ and rules of $mc.{\textbf{{\L${}_{3}$}}}$
according with the previous theorem:

  * •

$\Phi,\varphi\mid\Psi\mid\Gamma$
$\neg^{\mathbf{0}}_{\mathbf{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}}}$
$\Phi\mid\Psi\mid\Gamma,\neg\varphi$ corresponds to
$\neg\neg\varphi,\neg\varphi$
$\neg^{\mathbf{0}}_{\mathbf{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}}\mathbf{0}}$
$\neg\varphi,\varphi$ and  $\neg\varphi$
$\neg^{\mathbf{0}}_{\mathbf{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}}\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}}$
$\neg\neg\varphi,\neg\varphi,\varphi$ , and vice-versa.

  * •

$\Phi\mid\Psi,\varphi\mid\Gamma$ $\Phi\mid\Psi\mid\Gamma,\psi$
$\wedge^{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\mathbf{1}}_{\mathbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\nicefrac{{1}}{{2}}}}}$
$\Phi\mid\Psi,\varphi\wedge\psi\mid\Gamma$ corresponds to
$\neg(\varphi\land\psi),\psi$
$\wedge^{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\mathbf{1}}_{\mathbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\nicefrac{{1}}{{2}}}}\mathbf{0}}$
$\varphi\wedge\psi,\neg\varphi,\varphi$

and  $\varphi\land\psi,\psi$
$\wedge^{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\mathbf{1}}_{\mathbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\nicefrac{{1}}{{2}}}}\mathbf{1}}$
$\neg\varphi,\varphi$ , and vice-versa.

  * •

$\Phi,\varphi\mid\Psi\mid\Gamma$ $\Phi\mid\Psi,\psi\mid\Gamma$
$\rightarrow^{\mathbf{0}\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}}_{\mathbf{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}}}$
$\Phi\mid\Psi\mid\Gamma,\varphi\rightarrow\psi$ corresponds to
$\neg(\varphi\rightarrow\psi),\neg\varphi$
$\rightarrow^{\mathbf{0}\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}}_{\mathbf{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}}\mathbf{0}}$
$\varphi\to\psi,\neg\psi,\varphi,\psi$

and  $\neg\varphi$
$\rightarrow^{\mathbf{0}\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}}_{\mathbf{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}}\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}}$
$\varphi\to\psi,\neg(\varphi\rightarrow\psi),\neg\psi,\varphi,\psi$ , and
vice-versa.

The above result just states that, modulo monadicity, both generating
procedures work by similar mechanisms, characterizing the interpretations of
the three-valued matrix at hand. An interesting problem is whether there is an
effective translation between proofs of each generated calculi. The next
results show that, from Set-Set proofs to 3-labelled proofs, we may explore
the fact that Set-Set proofs internalize proof-by-cases [42, Chapter 20], in
order to provide an effective translation. We first show how to translate Set-
Set rules of inference into 3-labelled rules, and then explain how to use the
latter in transforming proofs between these formalisms preserving
$\Theta$-analyticity. From now on, we will write Set-Set rules schematically
(using variables for formulas instead of propositional variables), in order to
ease the comparison with 3-labelled rules.

######  Lemma 6.3.

Let $\mathbf{L}$ be the Set-Set logic determined by the three-valued matrix
$\mathbb{M}:=\langle\mathbf{A},\\{\mathbf{1}\\}\rangle$ and $\mathsf{R}$ be a
Set-Set axiomatization for $\mathbb{M}$. For every _primitive_ rule
$\mathsf{r}:=\frac{\varphi_{1},\ldots,\varphi_{m}}{\psi_{1},\ldots,\psi_{n}}\in\mathsf{R}$,
the 3-sequent
$\varphi_{1},\ldots,\varphi_{m}\mid\varphi_{1},\ldots,\varphi_{m}\mid\psi_{1},\ldots,\psi_{n}$
has a cut-free derivation in $s\ell.{\mathbf{L}}$.

###### Proof.

It follows directly from the facts that $\mathsf{r}$ is a consecution of
$\mathbf{L}$ and that $s\ell.{\mathbf{L}}$ is adequate with respect
$\mathbb{M}$ and cut is admissible in it. ∎

######  Lemma 6.4.

Let $\mathbf{L}$ be the logic determined by the three-valued matrix
$\mathbb{M}:=\langle\mathbf{A},\\{\mathbf{1}\\}\rangle$ and $\mathsf{R}$ be a
Set-Set axiomatization for $\mathbb{M}$. For every _primitive_ rule
$\mathsf{r}\in\mathsf{R}$, the image of the translation $\lfloor\cdot\rfloor$
given by

$\left\lfloor\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
25.5pt\hbox{\vbox{\hbox{\hskip
4.0pt\hbox{$\varphi_{1},\ldots,\varphi_{m}$}\hskip 4.0pt}\vskip
0.04723pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to43.52242pt{\xleaders\hrule\hfill}\lower 1.95277pt\hbox{\hskip
3.0pt$\mathsf{r}$}}\vskip 0.04723pt\nointerlineskip\hbox{\hskip
0.80553pt\hbox{\hbox{\hskip 4.0pt\hbox{$\psi_{1},\ldots,\psi_{n}$}\hskip
4.0pt}}}}}\ignorespaces\right\rfloor$ $:=$
---
$F,\Phi,\psi_{1}\mid F,\Phi,\psi_{1}\mid\Gamma$ $\cdots$ $F,\Phi,\psi_{n}\mid
F,\Phi,\psi_{n}\mid\Gamma$ $\lfloor\mathsf{r}\rfloor$ $F,\Phi\mid
F,\Phi\mid\Gamma$

where $F:=\\{\varphi_{1},\ldots,\varphi_{m}\\}$ is a derivable rule of
$s\ell.{\mathbf{L}}$.

###### Proof.

By Lemma 6.3,
$\varphi_{1},\ldots,\varphi_{m}\mid\varphi_{1},\ldots,\varphi_{m}\mid\psi_{1},\ldots,\psi_{n}$
is derivable in $s\ell.{\mathbf{L}}$. The result easily follows by applying
cuts using this 3-sequent and the 3-sequents in the premises of
$\lfloor\mathsf{r}\rfloor$. ∎

######  Theorem 6.5.

There is an effective procedure to translate $\mathsf{R}$-proofs into proofs
in $s\ell.{\mathbf{L}}$. Moreover, the translation preserves
$\Theta$-analyticity.

###### Proof.

We will prove by induction on the structure of $\mathsf{R}$-derivations
$\mathsf{t}$ that $S(\mathsf{t}):=$ “for all $\Phi,\Psi\subseteq
L_{\Sigma}(P)$, if $\mathsf{t}$ is an $\mathsf{R}$-proof of $(\Phi,\Psi)$,
then $\mathsf{t}$ can be effectively translated into a proof
$\lfloor\mathsf{t}\rfloor$ of the same statement in $s\ell.{\mathbf{L}}$
preserving $\Theta$-analyticity”. For the base case, suppose that $\mathsf{t}$
has a single node labelled with $\Gamma$. Since it is a proof of
$(\Phi,\Psi)$, we must have $\Gamma\subseteq\Phi$ and
$I:={\Gamma}\cap\Psi\neq\varnothing$. Consider an enumeration
$\varphi_{1},\ldots,\varphi_{n},\ldots$ of the formulas in $I$. Then take
$\lfloor\mathsf{t}\rfloor$ to be the tree

Id${}_{\varphi_{1}}$ $\varphi_{1}\mid\varphi_{1}\mid\varphi_{1}$ $W^{\ast}$
$I\mid I\mid I$ $W^{\ast}$ $\Gamma\mid\Gamma\mid\Psi$ $W^{\ast}$
$\Phi\mid\Phi\mid\Psi$

which is clearly a proof of $(\Phi,\Psi)$ in $s\ell.{\mathbf{L}}$ that is
$\Theta$-analytic if $\mathsf{t}$ is $\Theta$-analytic. Suppose now that
$\mathsf{t}$ has its root labelled with $\Gamma$ and has subtrees
$\mathsf{t}_{1},\ldots,\mathsf{t}_{n}$, which resulted from an application of
the rule instance
$\mathsf{r}^{\sigma}:=\frac{\psi_{1},\ldots,\psi_{m}}{\gamma_{1},\ldots,\gamma_{n}}$.
Note that $\mathsf{t}_{i}$ is an $\mathsf{R}$-proof of
$(\Gamma\cup\\{\gamma_{i}\\},\Psi)$. Assume that (IH): $S(\mathsf{t}_{i})$
holds for every $1\leq i\leq n$. Therefore, each $\mathsf{t}_{i}$ has a
translation to a proof $\lfloor\mathsf{t}_{i}\rfloor$ in $s\ell.{\mathbf{L}}$
of the statement $(\Gamma\cup\\{\gamma_{i}\\},\Psi)$. Since
$\Gamma\subseteq\Phi$ and $\\{\psi_{1},\ldots,\psi_{m}\\}\subseteq\Gamma$, the
following tree is the translation we are looking for (recall the definition of
$\lfloor\mathsf{r}\rfloor$ in Lemma 6.4):

$\lfloor\mathsf{t}_{1}\rfloor$
$\Gamma,\gamma_{1}\mid\Gamma,\gamma_{1}\mid\Psi$ $\cdots$
$\lfloor\mathsf{t}_{n}\rfloor$
$\Gamma,\gamma_{n}\mid\Gamma,\gamma_{n}\mid\Psi$ $\lfloor\mathsf{r}\rfloor$
$\Gamma\mid\Gamma\mid\Psi$ $W^{\ast}$ $\Phi\mid\Phi\mid\Psi$

By Lemma 6.3 and the proof of Lemma 6.4, we observe that only formulas in
$\\{\psi_{1},\ldots,\psi_{m}\\}\cup\\{\gamma_{1},\ldots,\gamma_{n}\\}$ are
used in the derivation of the applied instance of $\lfloor\mathsf{r}\rfloor$,
and since all these formulas appeared in labels of the nodes of $\mathsf{t}$,
they are $\Theta$-subformulas of $(\Phi,\Psi)$. By (IH), then, we conclude
that $\lfloor\mathsf{r}\rfloor$ is $\Theta$-analytic. ∎

From 3-labelled proofs to Set-Set proofs, we leave the task for further
research. A starting point would be to impose the monadicity requirement for
the axiomatized matrix and search for a finite collection of Set-Set rules
that capture the application of a 3-labelled rule, using the fact that each of
such rules represent a collection of entries of the interpretation of a
connective of the logical matrix.

##  7 Final considerations

When it comes to the automatic generation of proof systems for propositional
three-valued logics, the formalism of 3-labelled calculi is powerful enough to
deliver finite and analytic systems for any of such logics. The mechanism
behind this general applicability is fairly simple: each truth value has its
own place in the manipulated sequents, in such a way that the meta-
conjunctions and meta-disjunctions that characterize each truth table have a
direct correspondence in terms of 3-labelled logical rules (see [7] for more
details on this matter). Enriching the structure of the sequents, however, may
bring some disadvantages, namely a greater distancing between the rules of the
proof system and the logic being captured, as well as the extra effort in
dealing with the new metalinguistic resources. One of the research lines in
which these aspects may become practical problems is in the combination of
logics: putting two sequent systems together may cause unwanted interactions
in the combined system [15].

An alternative to increasing the metalanguage resides in investing on Hilbert-
style systems, which keep the metalanguage at a minimum, the rules of
inference being just a collection of consecutions of the underlying logic.
When it comes to system generation, proof search and decidability, these
systems have been put aside due to the lack of modularity and analyticity
results. After the works of C. Caleiro and S. Marcelino [31, 14], we learned
that the simple move to Set-Set Hilbert-style systems [42] allows us to get
modular and analytic systems for a wide class of many-valued logics. The price
for abandoning the metalanguage present in 3-sequents is the sufficient
expressiveness requirement (monadicity), which is demanded for the automatic
proof system generation in the Set-Set setting. Summing up, as we have seen in
Section 6, the choice of proof formalism for a given application depends
essentially on a trade-off between the acceptable usage of extra metalanguage
(or the proximity of the rules to the logic of interest) and the complexity of
the formulas present in the rules of inference (cf. Example 6.2).

It is worth emphasizing that every three-valued logic (in the sense of being
determined by a single deterministic three-valued matrix) has a finite Set-Set
axiomatization [42], even though there is no general procedure for producing
it in the case non-monadic matrices (provided we want to use the same language
— if one is allowed to expand the language, the problem is solved [31, Section
4]). The best we can do, for now, is to proceed in an _ad hoc_ manner, as we
did for some fragments of well-known three-valued logics in Subsection 5.2. A
promising line of investigation, therefore, consists in pursuing a general
procedure covering non-monadic cases and delivering analytic Set-Set calculi
over the original language.

Finally, despite the fact that the three-valued logics studied in this chapter
are all determined by single deterministic logical matrices and the generation
procedures were presented for these cases only, such procedures have all been
generalized to (partial) non-deterministic matrices [14, 5]. These are
structures that allow for (possibly empty) sets of truth values as outputs of
the interpretations of the connectives. With partial matrices, for example,
one may capture by single monadic matrices three-valued logics determined by a
family of deterministic three-valued matrices [31, Example 3]. In this way,
taking the study of three-valued logics to partial non-deterministic semantics
is a natural step towards the discovery of new logics and applications.

## References

  * [1] Hugo Albuquerque, Adam Přenosil, and Umberto Rivieccio.  An algebraic view of super-Belnap logics.  Studia Logica, 105(6):1051–1086, December 2017.
  * [2] O. Arieli, A. Avron, and A. Zamansky.  Ideal paraconsistent logics.  Studia Logica, 99(1):31, Aug 2011.
  * [3] F. G. Asenjo.  A calculus of antinomies.  Notre Dame Journal of Formal Logic, 7(1):103 – 105, 1966.
  * [4] Arnon Avron.  Natural 3-valued logics—Characterization and proof theory.  Journal of Symbolic Logic, 56(1):276–294, 1991.
  * [5] Arnon Avron and Beata Konikowska.  Multi-valued Calculi for Logics Based on Non-determinism.  Logic Journal of the IGPL, 13(4):365–387, 07 2005.
  * [6] Arnon Avron and Anna Zamansky.  Gentzen systems for three-valued logics.  In This book. 2022.
  * [7] Matthias Baaz, Fermüller, and Richard Zach.  Labeled calculi and finite-valued logics.  Studia Logica, 61(1):7–33, 1998.
  * [8] Matthias Baaz, Christian G. Fermüller, Arie Ovrutcki, and Richard Zach.  Multilog: A system for axiomatizing many-valued logics.  In LPAR, 1993.
  * [9] Diderik Batens.  Paraconsistent extensional propositional logics.  Logique et Analyse, 23(90/91):195–234, 1980.
  * [10] D.A. Bochvar and Merrie Bergmann.  On a three-valued logical calculus and its application to the analysis of the paradoxes of the classical extended functional calculus.  History and Philosophy of Logic, 2(1-2):87–112, 1981.
  * [11] S. Bonzio, T. Moraschini, and M. Pra Baldi.  Logics of left variable inclusion and płonka sums of matrices.  Archive for Mathematical Logic, 60(1):49–76, Feb 2021.
  * [12] Stefano Bonzio, José Gil-Férez, Francesco Paoli, and Luisa Peruzzi.  On Paraconsistent Weak Kleene Logic: Axiomatisation and Algebraic Analysis.  Studia Logica, 105(2):253–297, 2017.
  * [13] Stefano Bonzio and Michele Pra Baldi.  Containment logics: Algebraic completeness and axiomatization.  Studia Logica, 109(5):969–994, Oct 2021.
  * [14] Carlos Caleiro and Sérgio Marcelino.  Analytic calculi for monadic PNmatrices.  In R. Iemhoff, M. Moortgat, and R. Queiroz, editors, Logic, Language, Information and Computation (WoLLIC 2019), volume 11541 of LNCS, pages 84–98. Springer, 2019.
  * [15] Carlos Caleiro, Sérgio Marcelino, and João Marcos.  Merging fragments of classical logic.  In Clare Dixon and Marcelo Finger, editors, Frontiers of Combining Systems, pages 298–315, Cham, 2017. Springer International Publishing.
  * [16] Carlos Caleiro, Sérgio Marcelino, and Umberto Rivieccio.  Characterizing finite-valuedness.  Fuzzy Sets and Systems, 345:113–125, 2018.
  * [17] Carlos Caleiro, Sérgio Marcelino, and Pedro Filipe.  Infectious semantics and analytic calculi for even more inclusion logics.  In 2020 IEEE 50th International Symposium on Multiple-Valued Logic (ISMVL), pages 224–229, 2020.
  * [18] Walter A. Carnielli, Jo ao Marcos, and Sandra De Amo.  Formal inconsistency and evolutionary databases.  Logic and Logical Philosophy, 8(2):115–152, 2000.
  * [19] Bruno Da Ré, Federico Pailos, and Damian Szmuc.  Theories of truth based on four-valued infectious logics.  Logic Journal of the IGPL, 28(5):712–746, 11 2018.
  * [20] Michael Dummett.  A propositional calculus with denumerable matrix.  The Journal of Symbolic Logic, 24(2):97–106, 1959.
  * [21] J. Michael Dunn.  Algebraic completeness results for R-Mingle and its extensions.  The Journal of Symbolic Logic, 35(1):1–13, 1970.
  * [22] Richard L. Epstein and Itala M.L. D’Ottaviano.  A paraconsistent logic: J3.  In The Semantic Foundations of Logic Volume 1: Propositional Logics, volume 35 of Nijhoff International Philosophy Series, pages 263–287. Springer, Dordrecht, 1990.
  * [23] T.M. Ferguson.  A computational interpretation of conceptivism.  Journal of Applied Non-Classical Logics, 24(4):333–367, 2014.
  * [24] V. K. Finn and Revaz Grigolia.  Nonsense logics and their algebraic properties.  Theoria, 59:207–273, 2008.
  * [25] Josep Font.  Belnap’s Four-valued logic and De Morgan lattices.  Logic Journal of the IGPL, 5:1–29, 05 1997.
  * [26] Josep Font.  Abstract Algebraic Logic - An Introductory Textbook.  College Publications, 04 2016.
  * [27] K. Gödel.  Zum intuitionistischen aussagenkalkül.  Anzeiger der Akademie der Wissenschaften in Wien, 69:65–66, 1932\.
  * [28] Petr Hájek.  Metamathematics of Fuzzy Logic.  Dordrecht, Boston and London: Kluwer Academic Publishers, 1998.
  * [29] Sören Halldén.  The Logic of Nonsense.  Uppsala, Sweden: Upsala Universitets Arsskrift, 1949.
  * [30] S. C. Kleene.  Introduction to metamathematics.  Van Nostrand, 1950.
  * [31] Sérgio Marcelino and Carlos Caleiro.  Axiomatizing non-deterministic many-valued generalized consequence relations.  Synthese, 198(S22):5373–5390, 2019.
  * [32] Joao Marcos.  Semânticas de traduções possíveis.  Master’s thesis, Unicamp, 1999.
  * [33] Sara Negri and Jan Von Plato.  Structural proof theory.  Cambridge university press, 2008.
  * [34] Hiroakira Ono.  Proof Theory and Algebra in Logic.  Short Textbooks in Logic. Springer, Singapore, 2019.
  * [35] K. Palasinska.  Deductive systems and finite axiomatization properties.  1994\.
  * [36] Francesco Paoli and Michele Pra Baldi.  The algebra of three-valued logics.  In This book. 2022.
  * [37] R. Zane Parks.  A note on ${\bf R}$-Mingle and Sobociński’s three-valued logic.  Notre Dame Journal of Formal Logic, 13(2):227 – 228, 1972.
  * [38] Emil L. Post.  Introduction to a general theory of elementary propositions.  American Journal of Mathematics, 43(3):163–185, 1921.
  * [39] G. Priest.  The logic of paradox.  JPL, 8:219–241, 1979.
  * [40] Arthur Norman Prior.  Past, Present, and Future.  Oxford, England: Clarendon Press, 1967.
  * [41] Alexej P. Pynko.  Characterizing Belnap’s logic via De Morgan’s laws.  Mathematical Logic Quarterly, 41(4):442–454, 1995.
  * [42] D. J. Shoesmith and T. J. Smiley.  Multiple-Conclusion Logic.  Cambridge University Press, 1978.
  * [43] B. Sobocinski.  Axiomatization of partial system of three-valued calculus of propositions.  The Journal of Computing Systems, 1:23 – 55, 1972.
  * [44] A. Tarski.  Logic, Semantics, Metamathematics. Papers from 1923 to 1938.  Clarendon Press, Oxford, 1956.  2nd edition by Hackett Pub. Co., Indianapolis, 1983.
  * [45] Alasdair Urquhart.  Basic Many-Valued Logic, pages 249–295.  Springer Netherlands, Dordrecht, 2001.
  * [46] R. Wójcicki.  Theory of logical calculi. Basic theory of consequence operations, volume 199 of Synthese Library.  Reidel, Dordrecht, 1988.
  * [47] Ítala M. L. D´Ottaviano and Richard L. Epstein.  A paraconsistent logic: J3.  Technical report, Institute of Mathematics, Statistics and Scientific Computing, Unicamp, 1987.
  * [48] Jan Łukasiewicz.  O logice trójwartościowej.  Ruch filozoficzny, 5, 1920.
  * [49] Jan Łukasiewicz.  On three-valued logic.  In Selected works by Jan Łukasiewicz. North–Holland, Amsterdam, 1970.