$v({\circ}(p\land q))\in D$, then $v(p\land
q)\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$. Thus if $v(p\land
q)=\hat{\mathbf{t}}$, then $v(p)=v(q)=\hat{\mathbf{t}}$, absurd. Otherwise, we
must have $v(p)=\hat{\mathbf{f}}$. The proof is similar for the other rule.

$\mathsf{r}^{\land}_{5}$,$\mathsf{r}^{\land}_{9}$:

If $v({\circ}p)\in D$, then $v(p)\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$.
Then either $v(q\Rightarrow(p\land q))=v(q\Rightarrow q)=\hat{\mathbf{t}}$ or
$v(q\Rightarrow(p\land q))\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$. In both
cases we are done. The proof is similar for the other rule.

$\mathsf{r}^{\land}_{6}$, $\mathsf{r}^{\land}_{10}$:

We have that $v(p\land q)\leq v(p)$ and $v(p\land q)\leq v(q)$ hence
$v((p\land q)\Rightarrow q)=v({\circ}((p\land q)\Rightarrow q))=v((p\land
q)\Rightarrow p)=v({\circ}((p\land q)\Rightarrow p))=\hat{\mathbf{t}}\in D$.

$\mathsf{r}^{\land}_{11}$, $\mathsf{r}^{\land}_{12}$:

If $v({\circ}p)\in D$ and $v(p)\notin D$, or $v({\circ}q)\in D$ and
$v(q)\notin D$, then either $v(p)=\hat{\mathbf{f}}$ or
$v(q)=\hat{\mathbf{f}}$. In any case we have that $v(p\land
q)=\hat{\mathbf{f}}$ and $v({\circ}(p\land q))=\hat{\mathbf{t}}\in D$.

$\mathsf{r}^{\land}_{13}$:

If $v({\circ}(p\land q))\in D$, then $v(p\land
q)\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$. If
$v(p)=v(q)=\hat{\mathbf{t}}$, clearly
$v({\circ}p)=v({\circ}q)=\hat{\mathbf{t}}$. If $v(p)=\hat{\mathbf{f}}$, then
$v({\circ}p)=\hat{\mathbf{t}}$. Analogously if $v(q)=\hat{\mathbf{f}}$.

$\mathsf{r}^{\land}_{14}$, $\mathsf{r}^{\land}_{15}$:

Suppose ${\circ}(p\Rightarrow q)\in D$. Then either $v(q)=\hat{\mathbf{f}}$,
in which case $v((p\lor q)\Rightarrow q),v((q\lor p)\Rightarrow
q)\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$ and thus $v({\circ}((p\lor
q)\Rightarrow q))=v({\circ}((q\lor p)\Rightarrow q))=\hat{\mathbf{t}}\in D$;
or $v(p)\leq v(q)$, and so $v(p\lor q)=v(q\lor p)=v(q)$, hence
$v({\circ}((p\lor q)\Rightarrow q))=v({\circ}((q\lor p)\Rightarrow
q))=\hat{\mathbf{t}}\in D$.

$\mathsf{r}^{\land}_{16}$:

If $v({\circ}p)\not\in D$ and $v({\downarrow}p)\in D$, then
$v(p)\in\\{\mathbf{f},\mathbf{b},\mathbf{n}\\}$. If $v({\uparrow}(p\land
q))\in D$, then $v(p\land q)\neq\mathbf{f}$. We may safely focus on cases in
which $v(p)\neq v(q)$. If $v(p)=\mathbf{f}$, then $v(p\Rightarrow
q)\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$. If $v(p)=\mathbf{b}$, we have
$v(q)\not\in\\{\mathbf{f},\mathbf{b},\mathbf{n}\\}$ from the above
assumptions, and this gives $v(p\Rightarrow
q)\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$. Similarly if $v(p)=\mathbf{n}$.
∎

######  Definition 6.13.

Let $\mathsf{R}_{\lor}$ be the Set-Set calculus given by the following
inference rules:

$\frac{{\circ}p,{\circ}q}{{\circ}(p\lor
q)}\,\mathsf{r}_{1}^{\lor}\qquad\frac{{\circ}p,p\lor
q}{p,q}\,\mathsf{r}_{2}^{\lor}\qquad\frac{q}{p\lor
q}\,\mathsf{r}_{3}^{\lor}\qquad\frac{{\circ}(p\lor
q)}{p,{\circ}q}\,\mathsf{r}_{4}^{\lor}\qquad\frac{}{{\circ}(q\Rightarrow(p\lor
q))}\,\mathsf{r}_{5}^{\lor}$ $\frac{{\circ}p}{p,{\circ}((p\lor q)\Rightarrow
q)}\,\mathsf{r}_{6}^{\lor}\qquad\frac{p}{p\lor
q}\,\mathsf{r}_{7}^{\lor}\qquad\frac{{\circ}(p\lor
q)}{q,{\circ}p}\,\mathsf{r}_{8}^{\lor}\qquad\frac{}{{\circ}(p\Rightarrow(p\lor
q))}\,\mathsf{r}_{9}^{\lor}$ $\frac{{\circ}q}{q,{\circ}((p\lor q)\Rightarrow
p)}\,\mathsf{r}_{10}^{\lor}\qquad\frac{p,{\circ}p}{{\circ}(p\lor
q)}\,\mathsf{r}_{11}^{\lor}\qquad\frac{q,{\circ}q}{{\circ}(p\lor
q)}\,\mathsf{r}_{12}^{\lor}\qquad\frac{{\circ}(p\lor
q)}{{\circ}p,{\circ}q}\,\mathsf{r}_{13}^{\lor}$ ${\circ}((p\lor q)\Rightarrow
q){\circ}(p\Rightarrow q)\qquad\frac{{\circ}(q\Rightarrow p)}{{\circ}((p\lor
q)\Rightarrow
p)}\,\mathsf{r}_{15}^{\lor}\qquad\frac{{\uparrow}q,{\downarrow}(p\lor
q)}{{\circ}p,{\circ}(p\Rightarrow q)}\,\mathsf{r}_{16}^{\lor}$

######  Proposition 6.14.

The rules of $\mathsf{R}_{\lor}$ are sound for any matrix
$\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},D\rangle$ with
$D={{\uparrow}a}$ for some $a>\hat{\mathbf{f}}$.

###### Proof.

We proceed rule by rule.

$\mathsf{r}_{1}^{\lor}$:

If $v({\circ}p),v({\circ}q)\in D$, then
$v(p),v(q)\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$, thus $v(p\lor
q)\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$, and we are done.

$\mathsf{r}_{2}^{\lor}$:

If $v({\circ}p)\in D$ and $v(p)\not\in D$, $v(p)=\hat{\mathbf{f}}$. Then
$v(p\lor q)=v(q)$ and we are done.

$\mathsf{r}_{3}^{\lor}$, $\mathsf{r}_{7}^{\lor}$:

As $v(q)\leq v(p\lor q)$, if $v(q)\in D$, then $v(p\lor q)\in D$. Similarly
for the other rule.

$\mathsf{r}_{4}^{\lor}$, $\mathsf{r}_{8}^{\lor}$:

If $v({\circ}(p\lor q))\in D$, then $v(p\lor
q)\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$. If $v({\circ}q)\not\in D$,
$v(q)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$. Then
$v(p)=\hat{\mathbf{t}}$. Similarly for the other rule.

$\mathsf{r}_{5}^{\lor}$, $\mathsf{r}_{9}^{\lor}$:

We have that $v(p\lor q)\geq v(p)$ and $v(p\lor q)\geq v(q)$, hence
$v(q\Rightarrow(p\lor q))=v({\circ}(q\Rightarrow(p\lor
q)))=v(p\Rightarrow(p\lor q))=v({\circ}(p\Rightarrow(p\lor
q)))=\hat{\mathbf{t}}\in D$.

$\mathsf{r}_{6}^{\lor}$, $\mathsf{r}_{10}^{\lor}$:

If $v({\circ}p)\in D$ and $v(p)\notin D$ then $v(p)=\hat{\mathbf{f}}$ and
$v(p\lor q)=v(q)$, so $v((p\lor q)\Rightarrow q)=\hat{\mathbf{t}}$. Similarly
if $v({\circ}q)\in D$ and $v(q)\notin D$.

$\mathsf{r}_{11}^{\lor}$, $\mathsf{r}_{12}^{\lor}$:

If $v(p),v({\circ}p)\in D$, or $v(q),v({\circ}q)\in D$, then either
$v(p)=\hat{\mathbf{t}}$ or $v(q)=\hat{\mathbf{t}}$. In any case we have that
$v(p\lor q)=v({\circ}(p\lor q))=\hat{\mathbf{t}}\in D$.

$\mathsf{r}_{13}^{\lor}$:

If $v({\circ}p),v({\circ}q)\not\in D$, we have
$v(p),v(q)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$, thus $v(p\lor
q)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$, and $v({\circ}(p\lor
q))\not\in D$.

$\mathsf{r}_{14}^{\lor}$, $\mathsf{r}_{15}^{\lor}$:

Suppose ${\circ}(p\Rightarrow q)\in D$. Then either $v(q)=\hat{\mathbf{f}}$,
in which case $v((p\lor q)\Rightarrow q),v((q\lor p)\Rightarrow
q)\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$ and thus $v({\circ}((p\lor
q)\Rightarrow q))=v({\circ}((q\lor p)\Rightarrow q))=\hat{\mathbf{t}}\in D$;
or $v(p)\leq v(q)$, so $v(p\lor q)=v(q\lor p)=v(q)$, hence $v({\circ}((p\lor
q)\Rightarrow q))=v({\circ}((q\lor p)\Rightarrow q))=\hat{\mathbf{t}}\in D$.

$\mathsf{r}_{16}^{\lor}$:

If $v({\circ}p)\not\in D$ and $v({\uparrow}q)\in D$,
$v(p)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$ and
$v(q)\neq\mathbf{f}$. If $v(p)=v(q)$, we are done, so suppose $v(p)\neq v(q)$.
If $v({\downarrow}(p\lor q))\in D$, then $v(p\lor q)\neq\mathbf{t}$. If
$v(p)=\mathbf{f}$, then $v(p\Rightarrow
q)\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$, and we are done. If
$v(p)=\mathbf{b}$, the only non-obvious case is $v(q)=\mathbf{n}$, but this is
impossible as $v(p\lor q)\neq\mathbf{t}$. If $v(p)=\mathbf{n}$, the proof is
similar as the previous case. If $v(p)=\mathbf{t}$, the only non-obvious cases
are if $v(q)\in\\{\mathbf{b},\mathbf{n}\\}$, but they are impossible again
because $v(p\lor q)\neq\mathbf{t}$. ∎

######  Definition 6.15.

Let $\mathsf{R}_{\bot\top}$ be the Set-Set calculus given by the following
inference rules:

$\frac{}{\top}\,\mathsf{r}_{1}^{\top}\qquad\frac{}{{\circ}\top}\,\mathsf{r}_{2}^{\top}\qquad\frac{\bot}{}\,\mathsf{r}_{1}^{\bot}\qquad\frac{}{{\circ}\bot}\,\mathsf{r}_{2}^{\bot}$

######  Proposition 6.16.

The rules of $\mathsf{R}_{\top\bot}$ are sound for any matrix
$\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},D\rangle$ with
$D={{\uparrow}a}$ for some $a>\hat{\mathbf{f}}$.

###### Proof.

Obvious. ∎

The final rules we introduce encode the differences between the logics
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$ and
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$.

######  Definition 6.17.

Consider the following inference rules:

$\frac{p,{\downarrow}p,q}{{\circ}p,{\circ}(p\Rightarrow
q),{\circ}r,r}\,\mathsf{r}_{D_{\land}}\qquad\frac{p,{\circ}(p\Rightarrow
q)}{{\circ}q,q}\,\mathsf{r}_{D_{\leq}}\qquad\frac{r,{\uparrow}q}{{\downarrow}r,{\circ}(p\Rightarrow
q),p,q}\,\mathsf{r}_{D\neq{\uparrow}\mathbf{t}}$

######  Proposition 6.18.

In the matrix $\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},D\rangle$:
(i) the rules $\mathsf{r}_{D_{\land}}$ and $\mathsf{r}_{D_{\leq}}$ are sound
when $D={\uparrow}a$ for $a>\hat{\mathbf{f}}$; (ii) the rule
$\mathsf{r}_{D\neq{\uparrow}\mathbf{t}}$ is sound when $D$ is a prime filter;
(iii) the rule $\mathsf{r}_{D\neq{\uparrow}\mathbf{t}}$ is not sound when
$D={\uparrow}\mathbf{t}$.

###### Proof.

For items (i) and (ii), we prove soundness rule by rule.

$\mathsf{r}_{D_{\land}}$:

If $v({\circ}(p\Rightarrow q))\not\in D$, then $v(p\Rightarrow
q)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$. From that and the
assumption that $v({\circ}p)\not\in D$ and $v({\downarrow}p)\in D$, we have
$v(p)\in\\{\mathbf{b},\mathbf{n}\\}$. Also, we obtain
$v(q)\in\\{\mathbf{f},\mathbf{n},\mathbf{b}\\}$. Suppose $v(p),v(q)\in D$. If
$v(q)=\mathbf{f}$, then $D={\uparrow}\mathbf{f}$, and supposing
$v({\circ}r)\not\in D$, we have $v(r)\in D$. If $v(q)=\mathbf{b}$, we must
have $v(p)=\mathbf{n}$. Then again $D={\uparrow}\mathbf{f}$, for the same
reason as before. The case of $v(q)=\mathbf{n}$ is analogous.

$\mathsf{r}_{D_{\leq}}$:

If $v({\circ}(p\Rightarrow q))\in D,v(p)\geq a$ and $v(\circ q)<a$, then
$v({\circ}(p\Rightarrow q))=\hat{\mathbf{t}}$.

$\mathsf{r}_{D\neq{\uparrow}\mathbf{t}}$:

If $v({\downarrow}r)\not\in D$, we have $v(r)=\mathbf{t}$. If
$v({\uparrow}q)\in D$, we have $v(q)\neq\mathbf{f}$. If
$v({\circ}(p\Rightarrow q))\not\in D$, we have $v(p\Rightarrow
q)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$. This gives
$v(p)\in\\{\mathbf{b},\mathbf{n},\mathbf{t}\\}$ and
$v(q)\in\\{\mathbf{b},\mathbf{n},\mathbf{t}\\}$. We only consider the cases
$v(p)\neq v(q)$. If $v(p)=\mathbf{b}$, then $v(q)=\mathbf{n}$, and supposing
$v(p),v(q)\not\in D$, given that $D$ is prime we must have
$D={\uparrow}\hat{\mathbf{t}}$, and $v(r)\not\in D$. If $v(p)=\mathbf{n}$, the
proof is similar to the previous case. If $v(p)=\mathbf{t}$, again we have
$D={\uparrow}\hat{\mathbf{t}}$, and we are done.

For item (iii), a valuation $v$ such that $v(r)=\mathbf{t}$, $v(p)=\mathbf{n}$
and $v(q)=\mathbf{b}$ shows that $\mathsf{r}_{D\neq{\uparrow}\mathbf{t}}$ is
not sound when $D={\uparrow}\mathbf{t}$. ∎

We are ready to define our Set-Set axiomatizations and prove the desired
completeness results.

######  Definition 6.19.

From the previous definitions, let

  1. 1.

$\mathsf{R}_{\mathsf{up}}\,{\coloneqq}\,\mathsf{R}_{\Diamond}\cup\mathsf{R}_{D}\cup\mathsf{R}_{\Rightarrow}\cup\mathsf{R}_{\circ}\cup\mathsf{R}_{\sim}\cup\mathsf{R}_{\land}\cup\mathsf{R}_{\lor}\cup\mathsf{R}_{\top\bot}\cup\\{\mathsf{r}_{D_{\land}},\mathsf{r}_{D_{\leq}}\\}$;

  2. 2.

$\mathsf{R}_{\leq}\,{\coloneqq}\,\mathsf{R}_{\mathsf{up}}\cup\\{\mathsf{r}_{D\neq{\uparrow}\mathbf{t}}\\}$.

######  Theorem 6.20.

$\mathsf{R}_{\mathsf{up}}$ axiomatizes
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$and
$\mathsf{R}_{\leq}$ axiomatizes
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$. Moreover, both
$\mathsf{R}_{\mathsf{up}}$ and $\mathsf{R}_{\leq}$ are $\Theta$-analytic
calculi, for $\Theta\,{\coloneqq}\,\\{p,{\circ}p,{\circ}(p\Rightarrow
q),{\uparrow}p,{\downarrow}p\\}$.

###### Proof.

That
$\rhd_{\mathsf{R}_{\mathsf{up}}}\subseteq{\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$
and
$\rhd_{\mathsf{R}_{\leq}}\subseteq{\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$
(i.e. soundness) follows easily using the previous propositions. To check
completeness for
$\mathsf{R}\in\\{\mathsf{R}_{\mathsf{up}},\mathsf{R}_{\leq}\\}$ we need to
show that from $\Phi\not\rhd_{\mathsf{R}}\Psi$ we can find a valuation over
the algebra $\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ and a principal
filter that testifies it. Let
$\Lambda\,{\coloneqq}\,{\mathsf{sub}}(\Phi\cup\Psi)$. Recall that from
$\Phi\not\rhd_{\mathsf{R}}\Psi$, by cut for sets, there is a partition
$(\Omega,\overline{\Omega})$ of $\Theta(\Lambda)$ such that
$\Omega\not\rhd_{\mathsf{R}}\,\overline{\Omega}$. We will build a partial
valuation $f$ on $\Lambda$ and show that for its extension to the whole
language it holds that $f(\Lambda\cap\Omega)\subseteq D$ and
$f(\Lambda\cap\overline{\Omega})\subseteq\mathcal{V}_{6}{\setminus}D$ for
suitable $D$ (either principal or prime depending on the case). Further,
analyticity will follow from the fact that we will be using only instances of
the rules in $\mathsf{R}$ with formulas in $\Lambda$, thus only formulas in
$\Theta(\Lambda)\,{\coloneqq}\,\\{\psi^{\sigma}:\psi\in\Theta,\sigma:\\{p,q\\}\to\Lambda\\}$
will appear along this proof.

Let

$\displaystyle\Lambda_{\hat{\mathbf{f}}}$
$\displaystyle\,{\coloneqq}\,\\{\varphi\in\Lambda:\varphi\in\overline{\Omega},{\circ}\varphi\in\Omega\\}$
$\displaystyle\Lambda_{\hat{\mathbf{t}}}$
$\displaystyle\,{\coloneqq}\,\\{\varphi\in\Lambda:\varphi,{\circ}\varphi\in\Omega\\}$
$\displaystyle\Lambda_{\Diamond}$
$\displaystyle\,{\coloneqq}\,\\{\varphi\in\Lambda:{\circ}\varphi\in\overline{\Omega}\\}$
$\displaystyle\Lambda_{\mathbf{t}}$
$\displaystyle\,{\coloneqq}\,\\{\varphi\in\Lambda_{\Diamond}:{\downarrow}\varphi\in\overline{\Omega}\\}$
$\displaystyle\Lambda_{\mathbf{f}}$
$\displaystyle\,{\coloneqq}\,\\{\varphi\in\Lambda_{\Diamond}:{\uparrow}\varphi\in\overline{\Omega}\\}$
$\displaystyle\Lambda_{\mathsf{mid}}$
$\displaystyle\,{\coloneqq}\,\\{\varphi\in\Lambda_{\Diamond}:{\uparrow}\varphi,{\downarrow}\varphi\in\Omega\\}$

In what follows, consider the relation
$\equiv_{\Diamond}\,\subseteq\Lambda_{\Diamond}\times\Lambda_{\Diamond}$ given
by $\varphi\equiv_{\Diamond}\psi$ if, and only if,
${\circ}(\varphi\Rightarrow\psi),{\circ}(\psi\Rightarrow\varphi)\in\Omega$.

######  Lemma 6.21.

From $\mathsf{R}^{\Diamond}\subseteq\mathsf{R}$, we obtain that

  1. 1.

$\Lambda_{\Diamond}=\Lambda_{\mathbf{f}}\cup\Lambda_{\mathbf{t}}\cup\Lambda_{\mathsf{mid}}$
;

  2. 2.

the relation $\equiv_{\Diamond}$ is an equivalence relation that partitions
$\Lambda_{\Diamond}$ into at most four equivalence classes. In particular,
each set $\Lambda_{\mathbf{f}}$ and $\Lambda_{\mathbf{t}}$ consists of
formulas corresponding to a single $\equiv_{\Diamond}$-class, and if
$\Lambda_{\mathsf{mid}}\neq\varnothing$ then it is partitioned into exactly
two $\equiv_{\Diamond}$-classes, which we name $\Lambda_{\mathbf{b}}$ and
$\Lambda_{\mathbf{n}}$, such that, for $\varphi,\psi\in\Lambda_{\mathsf{mid}}$
and $a\in\\{\mathbf{b},\mathbf{n}\\}$, $\varphi,\psi\in\Lambda_{a}$ if, and
only if, ${\circ}(\varphi\Rightarrow\psi)\in\Omega$;

  3. 3.

for $\varphi\in\Lambda_{a}$ and $\psi\in\Lambda_{b}$ with
$a,b\in\\{\mathbf{f},\mathbf{n},\mathbf{b},\mathbf{t}\\}$, $a\leq b$ if, and
only if, ${\circ}(\varphi\Rightarrow\psi)\in\Omega$.

###### Proof.

Note that since $\Omega\cap\overline{\Omega}=\varnothing$ we have that
$\Lambda_{a}\cap\Lambda_{b}=\varnothing$ for $a\neq b$ and
$a,b\in\\{\mathbf{f},\mathbf{t},\mathsf{mid},\hat{\mathbf{t}},\hat{\mathbf{f}}\\}$.
By $\mathsf{r}^{\sim}_{{\uparrow}\mathsf{or}{\downarrow}}$ we know that
$\Lambda_{\Diamond}=\Lambda_{\mathbf{f}}\cup\Lambda_{\mathbf{t}}\cup\Lambda_{\mathsf{mid}}$,
and this is item (1).

For all that follows, recall that ${\circ}\varphi\in\overline{\Omega}$ for any
$\varphi\in\Lambda_{\Diamond}$, by definition of $\Lambda_{\Diamond}$. That
$\equiv_{\Diamond}$ is an equivalence relation follows by the fact that the
definition is symmetric and the presence of the rules
$\mathsf{r}_{\mathsf{id}}$ and $\mathsf{r}_{\mathsf{trans}}$.

We show now that formulas in $\Lambda_{\mathbf{t}}$ and $\Lambda_{\mathbf{f}}$
correspond to the same $\equiv_{\Diamond}$-class. If
$\varphi,\psi\in\Lambda_{\mathbf{t}}$, then
${\downarrow}\varphi,{\downarrow}\psi\in\overline{\Omega}$ and by
$\mathsf{r}^{\Diamond}_{\leq\mathbf{t}}$ we obtain that
$\varphi\equiv_{\Diamond}\psi$. Similarly, if
$\varphi,\psi\in\Lambda_{\mathbf{f}}$, then
${\uparrow}\varphi,{\uparrow}\psi\in\overline{\Omega}$ and by
$\mathsf{r}^{\Diamond}_{\geq\mathbf{f}}$ we obtain that
$\varphi\equiv_{\Diamond}\psi$.

We will show that there are subsets of $\Lambda_{\mathsf{mid}}$ corresponding
to a partition of this set. Our candidates are just the classes
$[\varphi]_{\equiv_{\Diamond}}$. They are clearly disjoint and their union
yields $\Lambda_{\mathsf{mid}}$, so it is enough to show that they are all
subsets of $\Lambda_{\mathsf{mid}}$. In fact, if
$\psi\in[\varphi]_{\equiv_{\mathsf{\Diamond}}}$, we have
${\circ}\psi\in\overline{\Omega}$ and
${\circ}(\varphi\Rightarrow\psi),{\circ}(\psi\Rightarrow\varphi)\in\Omega$.
Then we obtain ${\circ}\psi\in\overline{\Omega}$ and
${\uparrow}\psi,{\downarrow}\psi\in\Omega$ by the rules
$\mathsf{r}^{\Diamond}_{\mathsf{incclass}_{1}}$ and
$\mathsf{r}^{\Diamond}_{\mathsf{incclass}_{2}}$. Moreover, for
$\varphi,\psi\in\Lambda_{\mathsf{mid}}$, we have that
${\circ}(\varphi\Rightarrow\psi)\in\Omega$ if, and only if,
$\varphi\equiv_{\Diamond}\psi$. The difficult direction is left-to-right, and
it follows by $\mathsf{r}^{\Diamond}_{\mathsf{incclass}_{3}}$.

Still, $\Lambda_{\mathsf{mid}}$ might be partitioned into more than two
$\equiv_{\Diamond}$-equivalence classes. We avoid this with the rule
$\mathsf{r}^{\sim}_{\mathsf{just}_{2}}$, which, together with the fact proved
in the previous paragraph, forbids the existence of more than two
$\equiv_{\Diamond}$-equivalence classes in $\Lambda_{\mathsf{mid}}$.

Finally, for item (3), let $\varphi\in\Lambda_{a}$ and $\psi\in\Lambda_{b}$
with $a,b\in\\{\mathbf{f},\mathbf{n},\mathbf{b},\mathbf{t}\\}$. From left-to-
right, suppose that $a\leq b$. We want to prove
${\circ}(\varphi\Rightarrow\psi)\in\Omega$. Note that we cannot have
$a=\mathbf{b}$ and $b=\mathbf{n}$, nor $a=\mathbf{n}$ and $b=\mathbf{b}$. The
only cases we need to consider, then, are:

  1. 1.

If $a=b$, we already have that each $\Lambda_{c}$, with
$c\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$ forms an
$\equiv_{\Diamond}$-class, so ${\circ}(\varphi\Rightarrow\psi)\in\Omega$ by
the definition of $\equiv_{\Diamond}$.

  2. 2.

If $a=\mathbf{f}$, we obtain ${\circ}(\varphi\Rightarrow\psi)\in\Omega$ by
$\mathsf{r}^{\Diamond}_{\geq\mathbf{f}}$.

  3. 3.

If $b=\mathbf{t}$, we obtain ${\circ}(\varphi\Rightarrow\psi)\in\Omega$ by
$\mathsf{r}^{\Diamond}_{\leq\mathbf{t}}$.

From right-to-left, work contrapositively. Suppose that $a\not\leq b$. We want
to conclude that ${\circ}(\varphi\Rightarrow\psi)\in\overline{\Omega}$. We
only need to consider the following cases:

  1. 1.

If $a=\mathbf{t}$, we have $b<\mathbf{t}$. Thus ${\downarrow}\psi\in\Omega$.
By $\mathsf{r}^{\Diamond}_{\mathsf{incclass}_{2}}$, we have
${\circ}(\varphi\Rightarrow\psi)\in\overline{\Omega}$.

  2. 2.

If $a=\mathbf{b}$ or $a=\mathbf{n}$, and $b=\mathbf{f}$, we obtain
${\circ}(\varphi\Rightarrow\psi)\in\overline{\Omega}$ by
$\mathsf{r}^{\Diamond}_{\mathsf{incclass}_{1}}$.

  3. 3.

If $\\{a,b\\}=\\{\mathbf{b},\mathbf{n}\\}$, we have that
${\circ}(\varphi\Rightarrow\psi),{\circ}(\psi\Rightarrow\varphi)\in\overline{\Omega}$
by the definition of the sets $\Lambda_{\mathbf{b}}$ and
$\Lambda_{\mathbf{n}}$.

Note that in this proof the mentioned rules were instantiated only with
formulas in $\Lambda$ and all such instances have their formulas in
$\Theta(\Lambda)$.∎

Our candidate for partial valuation is $f:\Lambda\to\mathcal{V}_{6}$ given by
$f(\varphi)\,{\coloneqq}\,a$ if $\varphi\in\Lambda_{a}$. One can check without
difficulty that this function is well defined (as a matter of fact, the sets
$\Lambda_{a}$ defined above are pairwise disjoint). We will prove that $f$ is
indeed the desired valuation using a succession of lemmas. Let us begin with
proving that $f$ is a partial homomorphism.

######  Lemma 6.22.

Suppose $\mathsf{R}_{\Rightarrow},\mathsf{R}_{\Diamond}\subseteq\mathsf{R}$.
If $\\{\varphi,\psi,\varphi\Rightarrow\psi\\}\subseteq\Lambda$, then
$f(\varphi\Rightarrow\psi)=f(\varphi)\Rightarrow_{\mathsf{H}}f(\psi)$.

###### Proof.

By cases on the values of $f(\varphi)$ and $f(\psi)$:

  1. 1.

If $f(\psi)=\hat{\mathbf{t}}$, we have ${\circ}\psi,\psi\in\Omega$. We want
$f(\varphi\Rightarrow\psi)=\hat{\mathbf{t}}$, which follows from
$\mathsf{r}_{1}^{\Rightarrow}$ and $\mathsf{r}_{2}^{\Rightarrow}$.

  2. 2.

If $f(\varphi)=\hat{\mathbf{t}}$, we have ${\circ}\varphi,\varphi\in\Omega$
and proceed by cases on the value of $f(\psi)$. Note that we want to show that
$f(\varphi\Rightarrow\psi)=f(\psi)$:

    1. (a)

The case $f(\psi)=\hat{\mathbf{t}}$ was already covered.

    2. (b)

If $f(\psi)=\hat{\mathbf{f}}$, it follows from $\mathsf{r}_{1}^{\Rightarrow}$
and $\mathsf{r}_{3}^{\Rightarrow}$.

    3. (c)

If $f(\psi)=\mathbf{t}$, it follows from $\mathsf{r}_{4}^{\Rightarrow}$ and
$\mathsf{r}_{5}^{\Rightarrow}$.

    4. (d)

If $f(\psi)=\mathbf{f}$, it follows from $\mathsf{r}_{4}^{\Rightarrow}$ and
$\mathsf{r}_{6}^{\Rightarrow}$.

    5. (e)

If $f(\psi)\in\\{\mathbf{b},\mathbf{n}\\}$, it follows by
$\mathsf{r}_{4}^{\Rightarrow}$, $\mathsf{r}_{7}^{\Rightarrow}$ and
$\mathsf{r}_{8}^{\Rightarrow}$ that
$f(\varphi\Rightarrow\psi)\in\\{\mathbf{b},\mathbf{n}\\}$. Then, by
$\mathsf{r}_{9}^{\Rightarrow}$ and Lemma 6.21 we have
$f(\varphi\Rightarrow\psi)=f(\psi)$.

  3. 3.

If $f(\varphi)=\hat{\mathbf{f}}$, we have ${\circ}\varphi\in\Omega$ and
$\varphi\in\overline{\Omega}$. We obtain that
$f(\varphi\Rightarrow\psi)=\hat{\mathbf{t}}$ by
$\mathsf{r}_{10}^{\Rightarrow}$ and $\mathsf{r}_{11}^{\Rightarrow}$.

  4. 4.

If $f(\psi)=\hat{\mathbf{f}}$, the case
$f(\varphi)\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$ was already treated, so
we consider $f(\varphi)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$
and want to prove $f(\varphi\Rightarrow\psi)=\hat{\mathbf{f}}$. From the
available information, we have that ${\circ}\psi\in\Omega$,
$\psi\in\overline{\Omega}$, ${\circ}\varphi\in\overline{\Omega}$. Then for any
of the possibilities for $f(\varphi)$, the result follows by
$\mathsf{r}_{1}^{\Rightarrow}$ and $\mathsf{r}_{12}^{\Rightarrow}$.

  5. 5.

In case
$f(\varphi),f(\psi)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$, we
make intensive use of Lemma 6.21.

    1. (a)

If $f(\varphi)\leq f(\psi)$, we want to show
$f(\varphi\Rightarrow\psi)=\hat{\mathbf{t}}$. By Lemma 6.21, we already have
${\circ}(\varphi\Rightarrow\psi)\in\Omega$. The result then follows by
$\mathsf{r}^{\Rightarrow}_{13}$.

    2. (b)

If $f(\psi)\leq f(\varphi)$ and $f(\varphi)\not\leq f(\psi)$, we have
${\circ}(\varphi\Rightarrow\psi)\in\overline{\Omega}$ and
${\circ}(\psi\Rightarrow\varphi)\in\Omega$ by Lemma 6.21, and consider the
following subcases:

      1. i.

If $f(\varphi)=\mathbf{t}$, we want $f(\varphi\Rightarrow\psi)=f(\psi)$, which
follows by $\mathsf{r}_{9}^{\Rightarrow}$ and $\mathsf{r}_{14}^{\Rightarrow}$.

      2. ii.

If $f(\varphi)\in\\{\mathbf{n},\mathbf{b}\\}$ and $f(\psi)=\mathbf{f}$, we
want $f(\varphi\Rightarrow\psi)=\mathbf{b}$. This follows from by
$\mathsf{r}^{\Rightarrow}_{15}$, $\mathsf{r}^{\Rightarrow}_{16}$,
$\mathsf{r}^{\Rightarrow}_{17}$ and $\mathsf{r}^{\Rightarrow}_{18}$. The first
two force $f(\varphi\Rightarrow\psi)\in\\{\mathbf{b},\mathbf{n}\\}$, while the
third forces $f(\varphi)\neq f(\varphi\Rightarrow\psi)$.

    3. (c)

Otherwise, $\\{f(\varphi),f(\psi)\\}=\\{\mathbf{b},\mathbf{n}\\}$, thus we
want $f(\varphi\Rightarrow\psi)=f(\psi)$, which is achieved by
$\mathsf{r}^{\Rightarrow}_{9}$ and $\mathsf{r}^{\Rightarrow}_{19}$ together
with Lemma 6.21.

Note that in this proof the mentioned rules were instantiated only with
formulas in $\Lambda$ and all such instances have their formulas in
$\Theta(\Lambda)$.∎

######  Lemma 6.23.

Suppose $\mathsf{R}_{\sim},\mathsf{R}_{\Diamond}\subseteq\mathsf{R}$. If
$\\{\varphi,{\sim}\varphi\\}\subseteq\Lambda$, then
$f({\sim}\varphi)={\sim}^{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}(f(\varphi))$.

###### Proof.

By cases on the value of $f(\varphi)$, to show that
$f({\sim}\varphi)={\sim}^{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}(f(\varphi))$:

  1. 1.

If $f(\varphi)=\hat{\mathbf{t}}$, then $\varphi,{\circ}\varphi\in\Omega$, so
${\sim}\varphi\in\overline{\Omega}$ and ${\circ}{\sim}\varphi\in\Omega$ by
$\mathsf{r}^{\sim}_{2}$ and $\mathsf{r}^{\sim}_{3}$.

  2. 2.

If $f(\varphi)=\hat{\mathbf{f}}$, then ${\circ}\varphi\in\Omega$ and
$\varphi\in\overline{\Omega}$, so ${\sim}\varphi\in\Omega$ and
${\circ}{\sim}\varphi\in\Omega$ by $\mathsf{r}_{1}^{\sim}$ and
$\mathsf{r}_{3}^{\sim}$.

  3. 3.

If $f(\varphi)=\mathbf{t}$, then ${\circ}\varphi\in\overline{\Omega}$ and
${\downarrow}\varphi\in\overline{\Omega}$. Thus, by $\mathsf{r}^{\sim}_{4}$
and $\mathsf{r}^{\sim}_{5}$ we have that
${\circ}{\sim}\varphi\in\overline{\Omega}$ and
${\uparrow}{\sim}\varphi\in\overline{\Omega}$.

  4. 4.

If $f(\varphi)=\mathbf{f}$, then ${\circ}{\sim}\varphi\in\overline{\Omega}$
and ${\uparrow}\varphi\in\overline{\Omega}$. Thus by $\mathsf{r}^{\sim}_{4}$
and $\mathsf{r}^{\sim}_{6}$ we have ${\circ}{\sim}\varphi\in\overline{\Omega}$
and ${\downarrow}{\sim}\varphi\in\overline{\Omega}$.

  5. 5.

If $f(\varphi)\in\\{\mathbf{b},\mathbf{n}\\}$, then
${\circ}\varphi\in\overline{\Omega}$ and
${\uparrow}\varphi,{\downarrow}\varphi\in\Omega$. By $\mathsf{r}^{\sim}_{4}$,
$\mathsf{r}^{\sim}_{7}$ and $\mathsf{r}^{\sim}_{8}$, we have
${\circ}{\sim}\varphi\in\overline{\Omega}$ and
${\uparrow}{\sim}\varphi,{\downarrow}{\sim}\varphi\in\Omega$. This gives us
that $f({\sim}\varphi)\in\\{\mathbf{b},\mathbf{n}\\}$. Also, since we have
${\circ}(\varphi\Rightarrow{\sim}\varphi)={\downarrow}\varphi\in\Omega$, we
must have $f({\sim}\varphi)=f(\varphi)$ by Lemma 6.21.

Note that in this proof the mentioned rules were instantiated only with
formulas in $\Lambda$ and all such instances have their formulas in
$\Theta(\Lambda)$. ∎

######  Lemma 6.24.

Suppose $\mathsf{R}_{\circ}\subseteq\mathsf{R}$. If
$\\{\varphi,{\circ}\varphi\\}\subseteq\Lambda$, then
$f({\circ}\varphi)={\circ}^{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}(f(\varphi))$.

###### Proof.

Note that by $\mathsf{r}_{1}^{\circ}$ we always have
${\circ}{\circ}\varphi\in\Omega$. Hence, if
$f(\varphi)\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$, then
${\circ}\varphi\in\Omega$ and thus
$f({\circ}\varphi)=\hat{\mathbf{t}}={\circ}^{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}(f(\varphi))$.
If $f(\varphi)\notin\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$, then
${\circ}\varphi\in\overline{\Omega}$, thus
$f({\circ}\varphi)=\hat{\mathbf{f}}={\circ}^{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}(f(\varphi))$.
∎

######  Lemma 6.25.

Suppose $\mathsf{R}_{\land},\mathsf{R}_{\Diamond}\subseteq\mathsf{R}$. If
$\\{\varphi,\psi,\varphi\land\psi\\}\subseteq\Lambda$, then
$f(\varphi\land\psi)=f(\varphi)\land^{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}\\!\\!f(\psi)$.

###### Proof.

We proceed by cases on the values of $f(\varphi)$ and $f(\psi)$:

  1. 1.

If $f(\varphi)=\hat{\mathbf{t}}$, we have ${\circ}\varphi,\varphi\in\Omega$.
We want $f(\varphi\land\psi)=f(\psi)$.

    1. (a)

If $f(\psi)=\hat{\mathbf{t}}$, we have ${\circ}\psi,\psi\in\Omega$. Then we
have ${\circ}(\varphi\land\psi),\varphi\land\psi\in\Omega$ by
$\mathsf{r}_{1}^{\land}$ and $\mathsf{r}_{2}^{\land}$.

    2. (b)

If $f(\psi)=\hat{\mathbf{f}}$, we have ${\circ}\psi\in\Omega$ and
$\psi\in\overline{\Omega}$. Then we have ${\circ}(\varphi\land\psi)\in\Omega$
and $\varphi\land\psi\in\overline{\Omega}$ by $\mathsf{r}_{1}^{\land}$ and
$\mathsf{r}_{3}^{\land}$.

    3. (c)

If $f(\psi)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$, we have
${\circ}\psi\in\overline{\Omega}$ and that
$f(\varphi\land\psi)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$ by
$\mathsf{r}_{4}^{\land}$. Then we have that
${\circ}(\psi\Rightarrow(\varphi\land\psi)),{\circ}((\varphi\land\psi)\Rightarrow\psi)\in\Omega$
by $\mathsf{r}_{5}^{\land}$ and $\mathsf{r}_{6}^{\land}$. This, together with
Lemma 6.21, gives the desired result.

  2. 2.

If $f(\psi)=\hat{\mathbf{t}}$, the argument is very similar to the previous
one. The case $f(\varphi)=\hat{\mathbf{t}}$ was already covered.

    1. (a)

If $f(\varphi)=\hat{\mathbf{f}}$, we have ${\circ}\varphi\in\Omega$ and
$\varphi\in\overline{\Omega}$. Then we have
${\circ}(\varphi\land\psi)\in\Omega$ and
$\varphi\land\psi\in\overline{\Omega}$ by $\mathsf{r}_{1}^{\land}$ and
$\mathsf{r}_{7}^{\land}$.

    2. (b)

If $f(\varphi)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$, we have
${\circ}\varphi\in\overline{\Omega}$ and also that
$f(\varphi\land\psi)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$, in
view of $\mathsf{r}_{8}^{\land}$. Then we have that
${\circ}(\varphi\Rightarrow(\varphi\land\psi)),{\circ}((\varphi\land\psi)\Rightarrow\varphi)\in\Omega$
by $\mathsf{r}_{9}^{\land}$ and $\mathsf{r}_{10}^{\land}$. Then, by Lemma
6.21, we obtain the desired result.

  3. 3.

If $f(\varphi)=\hat{\mathbf{f}}$, we have ${\circ}\varphi\in\Omega$ and
$\varphi\in\overline{\Omega}$. By $\mathsf{r}_{11}^{\land}$ and
$\mathsf{r}_{7}^{\land}$, we have ${\circ}(\varphi\land\psi)\in\Omega$ and
$\varphi\land\psi\in\overline{\Omega}$, as desired.

  4. 4.

If $f(\psi)=\hat{\mathbf{f}}$, the argument is similar as above, and follows
by $\mathsf{r}_{12}^{\land}$ and $\mathsf{r}_{3}^{\land}$.

  5. 5.

If $f(\varphi),f(\psi)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$,
we have ${\circ}\varphi,{\circ}\psi\in\overline{\Omega}$. Thus we have
${\circ}(\varphi\land\psi)\in\overline{\Omega}$ by $\mathsf{r}_{13}^{\land}$
and thus
$f(\varphi\land\psi)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$, as
desired. Consider then the following cases:

    1. (a)

If $f(\varphi)\leq f(\psi)$, we want to obtain
$f(\varphi\land\psi)=f(\varphi)$. By Lemma 6.21, it is enough to conclude
${\circ}(\varphi\Rightarrow(\varphi\land\psi)),{\circ}((\varphi\land\psi)\Rightarrow\varphi)\in\Omega$,
which follows by $\mathsf{r}_{10}^{\land}$ and $\mathsf{r}_{14}^{\land}$.

    2. (b)

If $f(\psi)\leq f(\varphi)$, we want to obtain $f(\varphi\land\psi)=f(\psi)$.
Similarly as in the previous item, by Lemma 6.21, it is enough to conclude
${\circ}(\psi\Rightarrow(\varphi\land\psi)),{\circ}((\varphi\land\psi)\Rightarrow\psi)\in\Omega$,
which follows by $\mathsf{r}_{15}^{\land}$ and $\mathsf{r}_{6}^{\land}$.

    3. (c)

Otherwise, we have $f(\varphi),f(\psi)\in\\{\mathbf{b},\mathbf{n}\\}$ and
$f(\varphi)\neq f(\psi)$. Note that by Lemma 6.21 we obtain
${\circ}(\varphi\Rightarrow\psi)\in\overline{\Omega}$. We want to obtain here
$f(\varphi\land\psi)=\mathbf{f}$, that is, we want to have
${\uparrow}(\varphi\lor\psi)\in\overline{\Omega}$, which is achieved by
$\mathsf{r}_{16}^{\land}$.

Note that the mentioned rules were instantiated only with formulas in
$\Lambda$ and all such instances have their formulas in $\Theta(\Lambda)$.∎

######  Lemma 6.26.

Suppose $\mathsf{R}_{\lor},\mathsf{R}_{\Diamond}\subseteq\mathsf{R}$. If
$\\{\varphi,\psi,\varphi\lor\psi\\}\subseteq\Lambda$, then
$f(\varphi\lor\psi)=f(\varphi)\lor^{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}\\!\\!f(\psi)$.

###### Proof.

We proceed by cases on the values of $f(\varphi)$ and $f(\psi)$:

  1. 1.

If $f(\varphi)=\hat{\mathbf{f}}$, we know that $\varphi\in\overline{\Omega}$
and ${\circ}\varphi\in{\Omega}$. We want to obtain that
$f(\varphi\lor\psi)=f(\psi)$, since
$f(\psi)=\hat{\mathbf{f}}\lor^{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}\\!\\!f(\psi)$.

    1. (a)

If $f(\psi)=\hat{\mathbf{f}}$, the result follows by $\mathsf{r}_{1}^{\lor}$
and $\mathsf{r}_{2}^{\lor}$.

    2. (b)

If $f(\psi)=\hat{\mathbf{t}}$, the result follows by $\mathsf{r}_{1}^{\lor}$
and $\mathsf{r}_{3}^{\lor}$.

    3. (c)

If $f(\psi)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$, we have
${\circ}\psi\in\overline{\Omega}$ and that
$f(\varphi\lor\psi)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$ by
$\mathsf{r}_{4}^{\lor}$. Then we have that
${\circ}(\psi\Rightarrow(\varphi\lor\psi)),{\circ}((\varphi\lor\psi)\Rightarrow\psi)\in\Omega$
by $\mathsf{r}_{5}^{\lor}$ and $\mathsf{r}_{6}^{\lor}$, which, with Lemma
6.21, gives the desired result.

  2. 2.

If $f(\psi)=\hat{\mathbf{f}}$, we know that $\psi\in\overline{\Omega}$ and
${\circ}\psi\in{\Omega}$. We want to obtain that
$f(\varphi\lor\psi)=f(\varphi)$, since
$f(\varphi)=f(\varphi)\lor^{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}\hat{\mathbf{f}}$.

    1. (a)

The case $f(\varphi)=\hat{\mathbf{f}}$ was covered already.

    2. (b)

If $f(\varphi)=\hat{\mathbf{t}}$, the result follows by
$\mathsf{r}_{1}^{\lor}$ and $\mathsf{r}_{7}^{\lor}$.

    3. (c)

If $f(\varphi)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$, we have
${\circ}\varphi\in\overline{\Omega}$ and that
$f(\varphi\lor\psi)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$ in
view of $\mathsf{r}_{8}^{\lor}$. So we have that
${\circ}(\varphi\Rightarrow(\varphi\lor\psi)),{\circ}((\varphi\lor\psi)\Rightarrow\varphi)\in\Omega$
by $\mathsf{r}_{9}^{\lor}$ and $\mathsf{r}_{10}^{\lor}$. By Lemma 6.21, then,
we obtain the desired result.

  3. 3.

If either $f(\varphi)=\hat{\mathbf{t}}$ or $f(\psi)=\hat{\mathbf{t}}$, we know
that either ${\circ}\varphi,\varphi\in\Omega$ or ${\circ}\psi,\psi\in\Omega$.
In any case, we obtain ${\circ}(\varphi\lor\psi),\varphi\lor\psi\in\Omega$ by
$\mathsf{r}_{11}^{\lor}$, $\mathsf{r}_{7}^{\lor}$, $\mathsf{r}_{12}^{\lor}$
and $\mathsf{r}_{3}^{\lor}$, and therefore
$f(\varphi\lor\psi)=\hat{\mathbf{t}}$, as desired.

  4. 4.

If $f(\varphi),f(\psi)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$,
we know that ${\circ}\varphi,{\circ}\psi\in\overline{\Omega}$, and so
${\circ}(\varphi\lor\psi)\in\overline{\Omega}$, by $\mathsf{r}_{13}^{\lor}$,
thus $f(\varphi\lor\psi)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$.
Consider now the following cases:

    1. (a)

If $f(\varphi)\leq f(\psi)$, we want to obtain $f(\varphi\lor\psi)=f(\psi)$.
By Lemma 6.21, we know that ${\circ}(\varphi\Rightarrow\psi)\in\Omega$. But
then ${\circ}(\psi\Rightarrow(\varphi\lor\psi))$,
${\circ}((\varphi\lor\psi)\Rightarrow\psi)\in\Omega$, by
$\mathsf{r}_{5}^{\lor}$ and $\mathsf{r}_{14}^{\lor}$, which gives us the
desired result by Lemma 6.21 again.

    2. (b)

If $f(\psi)\leq f(\varphi)$, we want to obtain
$f(\varphi\lor\psi)=f(\varphi)$. By Lemma 6.21, we know that
${\circ}(\psi\Rightarrow\varphi)\in\Omega$. But then
${\circ}(\varphi\Rightarrow(\varphi\lor\psi))$,
${\circ}((\varphi\lor\psi)\Rightarrow\varphi)\in\Omega$, by
$\mathsf{r}_{9}^{\lor}$ and $\mathsf{r}_{15}^{\lor}$, which gives us the
desired result by Lemma 6.21 again.

    3. (c)

Otherwise, we have $f(\varphi),f(\psi)\in\\{\mathbf{b},\mathbf{n}\\}$ and
$f(\varphi)\neq f(\psi)$. Note that by Lemma 6.21 we obtain
${\circ}(\varphi\Rightarrow\psi)\in\overline{\Omega}$. We want to obtain here
$f(\varphi\lor\psi)=\mathbf{t}$, that is, we want to have
${\downarrow}(\varphi\lor\psi)\in\overline{\Omega}$, and this is achieved by
$\mathsf{r}_{16}^{\lor}$.

Note that the mentioned rules were instantiated only with formulas in
$\Lambda$ and all such instances have their formulas in $\Theta(\Lambda)$.∎

######  Lemma 6.27.

Suppose $\mathsf{R}_{\top\bot}\subseteq\mathsf{R}$. If $\top\in\Lambda$, then
$f(\top)=\hat{\mathbf{t}}$; if $\bot\in\Lambda$, then
$f(\bot)=\hat{\mathbf{f}}$.

###### Proof.

Obvious from the rules of $\mathsf{R}_{\top\bot}$ and the definition of $f$. ∎

######  Lemma 6.28.

If
$\\{\mathsf{r}_{D_{\land}},\mathsf{r}_{D_{\leq}}\\},\mathsf{R}_{\Diamond}\subseteq\mathsf{R}$,
we have $f[\Omega\cap\Lambda]={\uparrow}a\cap f[\Lambda]$ for some
$a>\hat{\mathbf{f}}$; and if we also have
$\mathsf{r}_{D\neq{\uparrow}\mathbf{t}}\in\mathsf{R}$, then
$f[\Omega\cap\Lambda]={\uparrow}a\cap f[\Lambda]$ for some
$\hat{\mathbf{f}}<a\neq\mathbf{t}$.

###### Proof.

First of all, we show that, for
$\varphi_{1},\ldots,\varphi_{n}\in\Omega\cap\Lambda$, if
$\bigwedge_{i}f(\varphi_{i})\in f[\Lambda]$, then
$\bigwedge_{i}f(\varphi_{i})\in f[\Omega\cap\Lambda]$. By induction on $n$,
consider the base case $n=2$. The cases $f(\varphi)\leq f(\psi)$ and
$f(\psi)\leq f(\varphi)$ are obvious, as $f(\varphi)\land f(\psi)$ will
coincide either with $f(\varphi)$ or with $f(\psi)$ and they are in
$f[\Omega\cap\Lambda]$ by assumption. The tricky case thus is when
$\\{f(\varphi),f(\psi)\\}=\\{\mathbf{b},\mathbf{n}\\}$. Suppose that for some
$\theta\in\Lambda$ we have $f(\theta)=f(\varphi)\land f(\psi)=\mathbf{f}$.
Then, by $\mathsf{r}_{D_{\land}}$, we must have $\theta\in\Omega$, and so
$f(\theta)=\mathbf{f}\in f[\Omega\cap\Lambda]$. In the inductive step, suppose
that $b\,{\coloneqq}\,(f(\varphi_{1})\land\ldots\land f(\varphi_{n}))\land
f(\varphi_{n+1})\in f[\Lambda]$, for
$\varphi_{1},\ldots,\varphi_{n+1}\in\Omega\cap\Lambda$. Then either
$b=(f(\varphi_{1})\land\ldots\land f(\varphi_{n}))$, $b=f(\varphi_{n+1})$ or
$b=\mathbf{f}$ and $\\{f(\varphi_{1})\land\ldots\land
f(\varphi_{n}),f(\varphi_{n+1})\\}=\\{\mathbf{b},\mathbf{n}\\}$. In the first
case, use the induction hypothesis. The second case is obvious. For the third,
use $\mathsf{r}_{D_{\land}}$ as we did in the base case.

Second, we show that, for $\varphi\in\Omega\cap\Lambda$ and $\psi\in\Lambda$,
if $f(\varphi)\leq f(\psi)$, then $\psi\in\Omega$. By cases on the value of
$f(\varphi)$ (note that $f(\varphi)\neq\mathbf{f}$ as $\varphi\in\Omega$):

  1. 1.

If $f(\varphi)=\hat{\mathbf{t}}$, we must have $f(\psi)=\hat{\mathbf{t}}$,
thus $\psi\in\Omega$.

  2. 2.

If $f(\varphi)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$, we have
either $f(\psi)=\hat{\mathbf{t}}$, and thus $\psi\in\Omega$, or
$f(\psi)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$. In that case,
by Lemma 6.21, we have ${\circ}(\varphi\Rightarrow\psi)\in\Omega$. Then
$\psi\in\Omega$ follows by $\mathsf{r}_{D_{\leq}}$.

Let $a\,{\coloneqq}\,\bigwedge f[\Omega\cap\Lambda]$. Clearly,
$a\neq\hat{\mathbf{f}}$. Since $a\leq b$ for each $b\in f[\Omega\cap\Lambda]$,
we must have $f[\Omega\cap\Lambda]\subseteq{\uparrow}a\cap f[\Lambda]$. It
remains to show that ${\uparrow}a\cap f[\Lambda]\subseteq
f[\Omega\cap\Lambda]$. Suppose that there is
$\theta\in\overline{\Omega}\cap\Lambda$ such that (a): $a\leq f(\theta)$. By
cases:

  1. 1.

If $f(\theta)\leq f(\varphi)$ for all $\varphi\in\Omega\cap\Lambda$, then
$f(\theta)=a$, and thus $\theta\in\Omega$ by the first claim we proved above.

  2. 2.

If $f(\theta)\not\leq f(\psi)$ for some $\psi\in\Omega$, we have the following
subcases:

    1. (a)

If $f(\psi)<f(\theta)$, by the second claim we proved above we must have
$\theta\in\Omega\cap\Lambda$.

    2. (b)

If $f(\psi)\not\leq f(\theta)$, we have $f(\psi)=\mathbf{b}$ and
$f(\theta)=\mathbf{n}$ or vice-versa. By (a), we have
$a\in\\{\mathbf{f},\mathbf{n}\\}$. The case $a=\mathbf{n}$ was treated in (1),
so we only consider $a=\mathbf{f}$. This means that either
$\mathbf{b},\mathbf{n}\in f[\Omega\cap\Lambda]$ or $\mathbf{f}\in
f[\Omega\cap\Lambda]$, and the result follows from the second claim proved
above.

Now, in case the rule $\mathsf{r}_{D\neq{\uparrow}\mathbf{t}}$ is present in
the calculus, we are able to show that if $\varphi,\psi\in\Omega\cap\Lambda$
and $f(\varphi)\lor f(\psi)\in f[\Omega\cap\Lambda]$, then either
$f(\varphi)\in f[\Omega\cap\Lambda]$ or $f(\psi)\in f[\Omega\cap\Lambda]$,
which essentially excludes the possibility of $a=\mathbf{t}$. Suppose that for
$\theta\in\Lambda$, $f(\theta)=f(\varphi)\lor f(\psi)\in
f[\Omega\cap\Lambda]$. Then either $f(\theta)=f(\varphi)$, or
$f(\theta)=f(\psi)$ or $f(\theta)=\mathbf{t}$ and
$\\{f(\varphi),f(\psi)\\}=\\{\mathbf{b},\mathbf{n}\\}$. The first two cases
are obvious. The third one follows because the rule
$\mathsf{r}_{D\neq{\uparrow}\mathbf{t}}$ forces $\varphi\in\Omega$ in this
situation.

Note that the mentioned rules were instantiated only with formulas in
$\Lambda$ and all such instances have their formulas in $\Theta(\Lambda)$.∎

The above lemmas show that $f$ is a partial homomorphism over
$\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ (which can of course be extended
to a full homomorphism) and, in view of the above lemma, by considering a set
of designated values of the form ${\uparrow}a$ for appropriate $a$ we obtain a
countermodel for
$\Phi\rhd_{{\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}}\Psi$
or for
$\Phi\rhd_{{\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}}\Psi$ as
desired.∎

###  6.2 Set-Fmla axiomatization for
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$

The Set-Set calculus developed in the preceding subsection for the logic
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ induces a Set-Fmla
logic for its Set-Fmla companion
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$. We begin by defining
this calculus, then indicate why it is complete for
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$.

######  Definition 6.29.

Let $\mathsf{R}$ be a Set-Set calculus. We define $\mathsf{R}^{\lor}$ as the
Set-Fmla calculus

$\left\\{\frac{p}{p\lor q},\frac{p\lor q}{q\lor p},\frac{p\lor(q\lor
r)}{(p\lor q)\lor
r}\right\\}\cup\left\\{\mathsf{r}^{\lor}\mid\mathsf{r}\in\mathsf{R}\right\\}$

where $\mathsf{r}^{\lor}$ is $\frac{\varnothing}{\varphi}$ if
$\mathsf{r}=\frac{\varnothing}{\varphi}$, $\frac{\Phi\lor
p_{0}}{(\bigvee\Psi)\lor p_{0}}$ if $\mathsf{r}=\frac{\Phi}{\Psi}$, and
$\frac{\Phi\lor p_{0}}{p_{0}}$ if $\mathsf{r}=\frac{\Phi}{\varnothing}$, for
$p_{0}$ is a propositional variable not occurring in the rules that belong to
$\mathsf{R}$.

Using the above recipe is straightforward, and this gives the reason why we
decided to not spell out the whole axiomatization here. Before introducing the
completeness result, we define what it means for a Set-Fmla logic to have a
disjunction. A Set-Fmla logic $\vdash$ over $\Sigma$ _has a disjunction_
provided that $\Phi,\varphi\lor\psi\;\vdash\;\phi$ if, and only if,
$\Phi,\varphi\;\vdash\;\phi$ and $\Phi,\psi\;\vdash\;\phi$ (for $\lor$ a
binary connective in $\Sigma$). The completeness result is immediate from the
fact that ${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ has a
disjunction, in view of the following result:

######  Lemma 6.30 (Shoesmith and Smiley (1978, Thm. 5.37)).

Let $\mathsf{R}$ be a Set-Set calculus over a signature containing a binary
connective $\lor$. If $\vdash_{\mathsf{R}}$ has a disjunction, then
$\vdash_{\mathsf{R}^{\lor}}\;=\;\vdash_{\mathsf{R}}$.

From this it immediately follows that:

######  Theorem 6.31.

$\vdash_{\mathsf{R}_{\leq}^{\lor}}={\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$.

##  7 Algebraic study of $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$
and $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$

In this section we look at the class of algebras that corresponds to
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ and
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$ according to the general
theory of algebraization of logics (Font (2016)). In order to facilitate the
exposition, here we will write a $\Sigma$-algebra
$\mathbf{A}\,{\coloneqq}\,\langle A,\cdot^{\mathbf{A}}\rangle$ as $\langle
A;\copyright_{1}^{\mathbf{A}},\ldots,\copyright_{n}^{\mathbf{A}}\rangle$, with
$\copyright_{i}\in\Sigma$ for each $1\leq i\leq n$. We will further omit the
superscript $\mathbf{A}$ from the interpretations of the connectives whenever
there is no risk of confusion.

We begin by recalling that, as observed earlier, the algebra
$\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ is a symmetric Heyting algebra in
Monteiro’s sense.

######  Definition 7.1 (Monteiro (1980, Def. 1.2, p. 61)).

A _symmetric Heyting algebra (SHA)_ is a
$\Sigma^{\mathsf{DM}}_{\Rightarrow}$-algebra $\langle
A;\land,\lor,\Rightarrow,{\sim},\bot,\top\rangle$ such that:

  1. (i)

$\langle A;\land,\lor,\Rightarrow,\bot,\top\rangle$ is a Heyting algebra.

  2. (ii)

$\langle A;\land,\lor,{\sim},\bot,\top\rangle$ is a De Morgan algebra.

As mentioned earlier, SHAs are alternatively known as _De Morgan-Heyting
algebras_ in the terminology introduced by Sankappanavar (1987). The logical
counterpart of SHAs is Moisil’s ‘symmetric modal logic’, which is the
expansion of the Hilbert-Bernays positive logic (the conjunction-disjunction-
implication fragment of intuitionistic logic) by the addition of a De Morgan
negation. One might expect Moisil’s logic to be closely related to
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$. In fact, as we shall see,
the logic $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$ considered earlier
(the $\top$-assertional companion of
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$) may be viewed as an
axiomatic extension of Moisil’s logic; whereas we may obtain
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ from Moisil’s logic
provided we extend it by appropriate axioms but also drop the _contraposition_
rule schema ($\mathsf{r}^{\mathsf{M}}_{12}$ below). The following is a
Hilbert-style calculus for Moisil’s logic (see Monteiro (1980, p. 60)):

$\frac{}{p\Rightarrow(q\Rightarrow
p)}\,\mathsf{r}^{\mathsf{M}}_{1}\quad\frac{}{(p\Rightarrow(q\Rightarrow
r))\Rightarrow((p\Rightarrow q)\Rightarrow(p\Rightarrow
r))}\,\mathsf{r}^{\mathsf{M}}_{2}$ $\frac{}{(p\land q)\Rightarrow
p}\,\mathsf{r}^{\mathsf{M}}_{3}\quad\frac{}{(p\land q)\Rightarrow
q}\,\mathsf{r}^{\mathsf{M}}_{4}\quad\frac{}{(p\Rightarrow
q)\Rightarrow((p\Rightarrow r)\Rightarrow(p\Rightarrow(q\land
r)))}\,\mathsf{r}^{\mathsf{M}}_{5}$ $\frac{}{p\Rightarrow(p\lor
q)}\,\mathsf{r}^{\mathsf{M}}_{6}\quad\frac{}{q\Rightarrow(p\lor
q)}\,\mathsf{r}^{\mathsf{M}}_{7}\quad\frac{}{(p\Rightarrow
r)\Rightarrow((q\Rightarrow r)\Rightarrow((p\lor q)\Rightarrow
r))}\,\mathsf{r}^{\mathsf{M}}_{8}$
$\frac{}{p\Rightarrow{\sim}{\sim}p}\,\mathsf{r}^{\mathsf{M}}_{9}\quad\frac{}{{\sim}{\sim}p\Rightarrow
p}\,\mathsf{r}^{\mathsf{M}}_{10}$ $\frac{p,p\Rightarrow
q}{q}\,\mathsf{r}^{\mathsf{M}}_{11}\quad\frac{p\Rightarrow
q}{{\sim}q\Rightarrow{\sim}p}\,\mathsf{r}^{\mathsf{M}}_{12}$

The Lindenbaum-Tarski algebras of Moisil’s logic are precisely the symmetric
Heyting algebras (see Monteiro (1980, Thm. 2.3, p. 62)). Using this result, it
is easy to obtain the following:

######  Proposition 7.2.

Moisil’s logic is algebraizable (in the sense of Blok and Pigozzi (1989)) with
the same translations as positive logic (namely, equivalence formulas
$\\{x\Rightarrow y,y\Rightarrow x\\}$ and defining equation $x\approx\top$).
Its equivalent algebraic semantics is the variety of symmetric Heyting
algebras.

Having verified that $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$ is an
axiomatic extension of Moisil’s logic (see our axiomatization below), we will
immediately obtain that $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$ is
algebraizable with the translations mentioned in the preceding proposition;
the equivalent algebraic semantics of
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$ is then bound to be a
sub(quasi)variety of SHAs. To obtain
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$ from the above
axiomatizations of Moisil’s logic, we need to add the following axioms (we use
$\neg p$ as an abbreviation of $p\Rightarrow{\sim}(p\Rightarrow p)$ and
${\circ}p$ as an abbreviation of $\neg p\lor\neg{\sim}p)$):

$\frac{}{\neg p\Rightarrow{\sim}\neg\neg
p}\,\mathsf{r}^{\top}_{1}\qquad\frac{}{{\sim}\neg\neg p\Rightarrow\neg
p}\,\mathsf{r}^{\top}_{2}$ $\frac{}{({{\circ}(p_{1}\Rightarrow
p_{2})\land{\circ}(p_{2}\Rightarrow
p_{3})})\Rightarrow({{\circ}p_{1}\lor{\circ}p_{4}\lor{\circ}(p_{4}\Rightarrow
p_{3})}\lor{\circ}(p_{3}\Rightarrow p_{2})\lor{\circ}(p_{2}\Rightarrow
p_{1}))}\,\mathsf{r}^{\top}_{3}$

This axiomatization should be compared with the equational presentation given
in Definition 7.3, and the claimed completeness of the axiomatization will
follow from Theorems 7.4 and 7.5. Definition 7.3(2) matches
$\mathsf{r}^{\top}_{3}$. Definition 7.3(1) says that the algebra has a PP-
algebra reduct: as observed in Marcelino and Rivieccio (2022, p. 3150), for an
algebra that has a pseudo-complement negation (as all symmetric Heyting
algebras do), it is sufficient to impose the equation ${\sim}\neg\neg
x\approx\neg x$ to obtain an involutive Stone algebra (i.e., modulo the
language, a PP-algebra); clearly the equation ${\sim}\neg\neg x\approx\neg x$
corresponds, via algebraizability, to $\mathsf{r}^{\top}_{1}$ and
$\mathsf{r}^{\top}_{2}$.

One can also show that $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ may
be obtained from the preceding axiomatization by taking as axioms all the
valid formulas while dropping the contraposition rule of Moisil’s logic (see,
e.g., Bou et al. (2011, p.11)).

We proceed to obtain further information on the subclass of symmetric Heyting
algebras that are models of $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$
and $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$. Monteiro (1980)
carried out an extensive study of symmetric Heyting (and related) algebras;
independently, some of Monteiro’s results were rediscovered and a number of
new ones obtained in Sankappanavar (1987). From these works we shall recall
only the few lemmas needed for our purposes.

The following example is of special relevance to us because, as we shall see,
the symmetric Heyting algebras we are mostly interested in have the shape
described therein:

######  Example 7 (Sankappanavar (1987), p. 568).

Let $\mathbf{D}$ be a finite De Morgan algebra and let $\mathbf{C}^{+}_{n}$
and $\mathbf{C}^{-}_{n}$ be two $n$-element chains, which we view as lattices.
Denoting $C^{+}_{n}\,{\coloneqq}\,\\{c_{1},\ldots,c_{n}\\}$, with
$c_{1}<\ldots<c_{n}$, let
$C^{-}_{n}\,{\coloneqq}\,\\{{\sim}c_{1},\ldots,{\sim}c_{n}\\}$, with
${\sim}c_{n}<\ldots<{\sim}c_{1}$. Consider the ordinal sum of these lattices,
$\mathbf{D}^{\mathbf{C}}:=\mathbf{C}^{-}_{n}\oplus\mathbf{D}\oplus\mathbf{C}^{+}_{n}$,
in which the order and the De Morgan negation are defined as follows: for all
$d\in D$ and $c_{i}\in C^{+}_{n}$, we let ${\sim}c_{i}<d<c_{i}$ and
${\sim}^{\mathbf{D}^{\mathbf{C}}}d={\sim}^{\mathbf{D}}d$. Then,
$\mathbf{D}^{\mathbf{C}}$ is a finite De Morgan algebra, and can therefore be
endowed with the Heyting implication determined by the order, turning it into
a symmetric Heyting algebra.

We now proceed to the axiomatization of
$\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$. First, we define an
equational class $\mathbb{PP}^{\Rightarrow_{\mathsf{H}}}$, then we show that
it coincides with $\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$.

######  Definition 7.3.

Let $\mathbf{A}\,{\coloneqq}\,\langle
A;\land,\lor,\Rightarrow,{\sim},{\circ},\bot,\top\rangle$ be a symmetric
Heyting algebra expanded with an operation ${\circ}$. We say that $\mathbf{A}$
is in the class $\mathbb{PP}^{\Rightarrow_{\mathsf{H}}}$ if the following
conditions are satisfied:

  1. (i)

The reduct $\langle A;\land,\lor,{\circ},{\sim},\bot,\top\rangle$ is a PP-
algebra.

  2. (ii)

$\mathbf{A}$ satisfies the following equation:

${{\circ}(x_{1}\Rightarrow x_{2})\land{\circ}(x_{2}\Rightarrow
x_{3})}\leq{{\circ}x_{1}\lor{\circ}x_{4}\lor{\circ}(x_{4}\Rightarrow
x_{3})}\lor{\circ}(x_{3}\Rightarrow x_{2})\lor{\circ}(x_{2}\Rightarrow
x_{1}).$

Our next aim is to check the following results:

######  Theorem 7.4.

$\mathbb{PP}^{\Rightarrow_{\mathsf{H}}}$ is the variety (and the quasi-
variety) generated by $\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$.

######  Theorem 7.5.

$\mathbb{PP}^{\Rightarrow_{\mathsf{H}}}$ is the equivalent algebraic semantics
of the algebraizable logic $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$.

We shall prove the above by relying on a few lemmas which also have an
independent interest, in that they throw some light on the structures of
symmetric Heyting algebras in general and of algebras in
$\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$ in particular.

Adopting Monteiro’s notation, we use $\Delta x:=\neg{\sim}x$, where $\neg
x:=x\Rightarrow{\sim}(x\Rightarrow x)$ as abbreviations (recall that, on every
algebra having a PP-algebra reduct (Gomes et al. (2022)), one may take
${\circ}x\,{\coloneqq}\,\neg x\lor\Delta x$ and $\Delta
x\,{\coloneqq}\,x\land{\circ}x$). In
$\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$, we have:

$\neg^{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}(a)=\begin{cases}\hat{\mathbf{t}}&\text{if
}a=\hat{\mathbf{f}},\\\
\hat{\mathbf{f}}&\text{otherwise.}\end{cases}\quad\text{and}\quad\Delta^{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}(a)=\begin{cases}\hat{\mathbf{t}}&\text{
if }a=\hat{\mathbf{t}},\\\ \hat{\mathbf{f}}&\text{ otherwise.}\end{cases}$

Given a SHA $\mathbf{A}$ and a subset $F\subseteq A$, we shall say that $F$ is
a _filter_ if it is a non-empty lattice filter of the bounded lattice reduct
of $\mathbf{A}$. A filter $F$ will be called _regular_ if $\Delta a\in F$
whenever $a\in F$, for all $a\in A$. For example, the algebra
$\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ has only one proper regular
filter, namely the singleton $\\{\hat{\mathbf{t}}\\}$. On every SHA, the
regular filters form a closure system (hence, a complete lattice) and may be
characterized in a number of alternative ways (see e.g. Monteiro (1980, Thm.
4.3, p. 75, and Thm. 4.11, p. 80)). In particular, it can be shown that
regular filters coincide with the lattice filters $F$ that further satisfy the
contraposition rule, that is: ${\sim}b\Rightarrow{\sim}a\in F$ whenever
$a\Rightarrow b\in F$. By the algebraizability of Moisil’s logic, this
observation yields the following result, which Sankappanavar proved in a more
general (and purely algebraic) context:

######  Lemma 7.6 (Sankappanavar (1987), Thm. 3.3).

The lattice of congruences of each SHA $\mathbf{A}$ is isomorphic to the
lattice of regular filters on $\mathbf{A}$.

We now focus on a subvariety of SHAs (to which
$\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ obviously belongs) where regular
filter generation admits a particularly simple description. As we will see,
the following equation will play a key role:

$\Delta\Delta x\approx\Delta x$ ($\Delta$-idemp)

######  Lemma 7.7 (Monteiro (1980, Thm. 4.17, p. 82)).

Let $\mathbf{A}$ be a SHA that satisfies ($\Delta$-idemp) and let $B\subseteq
A$. The regular filter $F(B)$ generated by $B$ is given by:

$F(B)\,{\coloneqq}\,\\{a\in A:\Delta(a_{1}\land\ldots\land a_{n})\leq a\text{
for some }a_{1},\ldots,a_{n}\in B\\}.$

######  Lemma 7.8 (Sankappanavar (1987, Cor. 4.8)).

Let $\mathbf{A}$ be a SHA that satisfies ($\Delta$-idemp). The following are
equivalent:

  1. (i)

$\mathbf{A}$ is directly indecomposable.

  2. (ii)

$\mathbf{A}$ is subdirectly irreducible.

  3. (iii)

$\mathbf{A}$ is simple.

The subvariety of SHAs defined by the equation ($\Delta$-idemp) is dubbed
$\mathbb{SDH}_{1}$ by Sankappanavar (1987), who observes that it is a
discriminator222Note that this notion of discriminator variety is unrelated to
the above-mentioned discriminator for a monadic matrix (see Theorem 4.3).
variety (see Burris and Sankappanavar (2011, Def. IV.9.3)). This entails that
$\mathbb{PP}^{\Rightarrow_{\mathsf{H}}}$ is also a discriminator variety. The
discriminator term for $\mathbb{PP}^{\Rightarrow_{\mathsf{H}}}$ is the
following:

$t(x,y,z):=(\Delta(x\Leftrightarrow y)\land
z)\lor({\sim}\Delta(x\Leftrightarrow y)\land x)$

where $x\Leftrightarrow y\,{\coloneqq}\,(x\Rightarrow y)\land(y\Rightarrow
x)$. To see this, consider Theorem 7.4 and note that on
$\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ we have, for all
$c,d\in\mathcal{V}_{6}$,

$\Delta^{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}(c\Leftrightarrow
d)=\begin{cases}\hat{\mathbf{t}}&\text{ if }c=d,\\\ \hat{\mathbf{f}}&\text{
otherwise.}\end{cases}$

Recall that every variety of algebras is generated by its subdirectly
irreducible members, which in our case (since
$\mathbb{PP}^{\Rightarrow_{\mathsf{H}}}\subseteq\mathbb{SDH}_{1}$) are simple,
by Lemma 7.8. By Lemma 7.6, this means that every such algebra $\mathbf{A}$
with a top element $\top$ has (as we have seen of
$\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$) a unique non-trivial regular
filter, namely the singleton $\\{\top\\}$. The following is now the main lemma
we need:

######  Lemma 7.9.

Every simple algebra $\mathbf{A}\in\mathbb{PP}^{\Rightarrow_{\mathsf{H}}}$ is
(isomorphic to) a subalgebra of $\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$.

###### Proof.

In the proof we shall use the equations $\Delta x\leq x$ and $\Delta(x\lor
y)=\Delta x\lor\Delta y$, which can be easily verified in
$\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$. If $\mathbf{A}$ is simple, then
$\mathbf{A}$ has only one non-trivial congruence, corresponding to the regular
filter $\\{\top\\}$ — which in this case must be prime, as we now argue. In
fact, since $\mathbf{A}$ satisfies $\Delta\Delta x\approx\Delta x$, we have
$\Delta a=\bot$ whenever $a\neq\top$. For, otherwise, the regular filter
$F(a)=\\{b\in A:\Delta a\leq b\\}$ would be proper (Lemma 7.7). Now, assume
$a_{1}\lor a_{2}=\top$ for some $a_{1},a_{2}\in A$. We have $\Delta(a_{1}\lor
a_{2})=\Delta a_{1}\lor\Delta a_{2}=\top=\Delta\top$. Thus, if
$a_{1}\neq\top$, then $\Delta a_{1}=\bot$ and $a_{2}\geq\Delta
a_{2}=\bot\lor\Delta a_{2}=\Delta a_{1}\lor\Delta a_{2}=\top$, so
$a_{2}=\top$. Thus $\\{\top\\}$ is a prime filter (entailing, since
$\mathbf{A}$ has a De Morgan algebra reduct, that $\\{\bot\\}$ is a prime
ideal); hence the last elements of $\mathbf{A}$ form a chain $C^{+}$, and the
first elements of $\mathbf{A}$ form a chain $C^{-}$. This means that
$\mathbf{A}$ has the shape described in Example 7, except that it need not be
finite.

Let $D:=A-\\{\bot,\top\\}$. We claim that any chain of elements in $D$ must
have length at most $3$. To see this, notice that, for all $a\in A$, we have
$a\in D$ if, and only if, ${\circ}a=\bot$. In fact, for $a\in D$, we have
$\neg a=\bot=\Delta a$, so ${\circ}a=\neg a\lor\Delta a=\bot$. Notice also
that, for $a_{1},a_{2}\in D$, we have ${\circ}(a_{1}\Rightarrow a_{2})=\bot$
if (and only if) $a_{1}\not\leq a_{2}$.

Now assume, by way of contradiction, that there are elements
$a_{1},a_{2},a_{3},a_{4}\in D$ such that $a_{1}<a_{2}<a_{3}<a_{4}$, forming a
four-element chain. Then the inequality in the second item of Definition 7.3
would fail, for we would have:

${{\circ}(a_{1}\Rightarrow a_{2})\land{\circ}(a_{2}\Rightarrow
a_{3})}={\circ}\top\land{\circ}\top=\top\not\leq\bot={\circ}a_{1}\lor{\circ}a_{4}\lor{\circ}(a_{4}\Rightarrow
a_{3})\lor{\circ}(a_{3}\Rightarrow a_{2})\lor{\circ}(a_{2}\Rightarrow a_{1}).$

Thus, all chains in $D$ have at most three elements. Hence, as $\mathbf{A}$ is
a distributive lattice, it is easy to verify that $\mathbf{A}$ must be finite,
with a coatom (call it $\mathbf{t}$) and an atom $\mathbf{f}$. This easily
entails that $\mathbf{A}$ must be isomorphic to one of the subalgebras of
$\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$. ∎

Theorem 7.4 is now an immediate corollary of Lemma 7.9:
$\mathbb{PP}^{\Rightarrow_{\mathsf{H}}}$ is both the variety and the
quasivariety generated by $\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ (for
the latter statement, see e.g. Clark and Davey (1998, Thm. 1.3.6.ii)). We are
now ready to prove the following:

######  Theorem 7.10.

The variety $\mathbb{PP}^{\Rightarrow_{\mathsf{H}}}$ is the equivalent
algebraic semantics of the algebraizable logic
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$.

###### Proof.

We know from the algebraizability of Moisil’s logic (with respect to all SHAs)
that $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$ is algebraizable, with
the same translations, with respect to a sub(quasi)variety of SHAs which is
axiomatized by the equations that translate the new axioms. Recalling that the
equation $\neg x\approx{\sim}\neg\neg x$ guarantees that a Heyting algebra has
an involutive Stone algebra reduct (see Cignoli and Sagastume (1983, Remark
2.2)), is easy to verify that the translations of the new axioms are indeed
equivalent to the equations introduced in Definition 7.3. ∎

Another consequence of Lemma 7.9 which has a logical impact is the following.
Recall that the universes of subalgebras of
$\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ are the same as those of
$\mathbf{PP_{6}}$, minus the five-element chain. Let us denote the
corresponding algebras by
$\mathbf{PP_{4}^{\Rightarrow_{\mathsf{H}}}},\mathbf{PP_{3}^{\Rightarrow_{\mathsf{H}}}}$
and $\mathbf{PP_{2}^{\Rightarrow_{\mathsf{H}}}}$.

######  Corollary 7.11.

The (proper, non-trivial) subvarieties of
$\mathbb{PP}^{\Rightarrow_{\mathsf{H}}}$ are precisely the following (the
axiomatizations are obtained by adding the mentioned equations to the
axiomatization of $\mathbb{PP}^{\Rightarrow_{\mathsf{H}}}$):

  1. 1.

$\mathbb{V}(\mathbf{PP_{4}^{\Rightarrow_{\mathsf{H}}}})$, axiomatized by the
equation $x\land{\sim}x\leq y\lor{\sim}y$.

  2. 2.

$\mathbb{V}(\mathbf{PP_{3}^{\Rightarrow_{\mathsf{H}}}})$, axiomatized by
$x\lor(x\Rightarrow(y\lor\neg y))\approx\top$.

  3. 3.

$\mathbb{V}(\mathbf{PP_{2}^{\Rightarrow_{\mathsf{H}}}})$, axiomatized by
$x\lor{\sim}x\approx\top$.

Note that $\mathbb{V}(\mathbf{PP_{4}^{\Rightarrow_{\mathsf{H}}}})$ and
$\mathbb{V}(\mathbf{PP_{3}^{\Rightarrow_{\mathsf{H}}}})$ are incomparable,
while $\mathbb{V}(\mathbf{PP_{2}^{\Rightarrow_{\mathsf{H}}}})$, which is (up a
choice of language) just the variety of Boolean algebras, is included in both
of them.

###### Proof.

All claims are established by easy computations. The main observation we need
is that, by Jónsson’s Lemma (see Burris and Sankappanavar (2011, Cor.
IV.6.10)), for
$\mathbf{A}\in\\{\mathbf{PP_{4}^{\Rightarrow_{\mathsf{H}}}},\mathbf{PP_{3}^{\Rightarrow_{\mathsf{H}}}},\mathbf{PP_{2}^{\Rightarrow_{\mathsf{H}}}}\\}$,
the subdirectly irreducible (here meaning simple) algebras in each
$\mathbb{V}(\mathbf{A})$ are in $\mathbb{H}\mathbb{S}(\mathbf{A})$, and
$\mathbb{H}\mathbb{S}(\mathbf{A})=\mathbb{S}(\mathbf{A})$. ∎

By Theorem 7.10, the logic $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$ is
complete with respect to the class of all matrices
$\langle\mathbf{A},\\{\top^{\mathbf{A}}\\}\rangle$ such that
$\mathbf{A}\in\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$. But, by
Theorem 7.4, we know that the single matrix
$\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},\\{\hat{\mathbf{t}}\\}\rangle$
suffices. Thus:

######  Proposition 7.12.

$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$ is determined by
$\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},\\{\hat{\mathbf{t}}\\}\rangle$.

This observation may be used to verify the following equivalence, which holds
for all $\Phi\cup\\{\varphi\\}\subseteq L_{\Sigma}(P)$:

$\Phi\vdash_{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}}\varphi\quad\text{
if, and only if,
}\quad\Delta\Phi\vdash_{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}\varphi$

where $\Delta\Phi:=\\{\Delta\psi:\psi\in\Phi\\}$. From the latter, relying on
the DDT for $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$, we can obtain
the DDT for $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$: for all
$\Phi,\\{\varphi,\psi\\}\subseteq L_{\Sigma}(P)$,

$\Phi,\varphi\vdash_{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}}\psi\quad\text{
iff
}\quad\Phi\vdash_{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}}\Delta\varphi\Rightarrow\psi.$

The class of algebraic reducts of reduced matrices for
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ is also
$\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$. In fact, it can be
shown that $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ is complete
with respect to the class of all matrices $\langle\mathbf{A},D\rangle$ with
$\mathbf{A}\in\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$ and $D$
a non-empty lattice filter of $\mathbf{A}$. The reduced models of
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ may be characterized as
follows:

######  Proposition 7.13.

Given $\mathbf{A}\in\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$,
we have that a matrix $\langle\mathbf{A},D\rangle$ is a reduced model of
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ if, and only if, $D$ is a
lattice filter that contains exactly one regular filter (namely
$\\{\top^{\mathbf{A}}\\}$).

###### Proof.

We shall prove both implications by contraposition. Assume first that
$\langle\mathbf{A},D\rangle$ is not reduced. Then, by the characterization of
the Leibniz congruence given in Proposition 5.8, there are elements $a,b\in A$
such that $a\neq b$ and

$\Delta(a\Rightarrow b),\Delta(b\Rightarrow a)\in D.$

Assuming $a\not\leq b$, we have $a\Rightarrow b\neq\top$. Recall that the
regular filter generated by the element $a\Rightarrow b$ is

$F(\\{a\Rightarrow b\\})=\\{c\in A:\Delta(a\Rightarrow b)\leq c\\}.$

From the assumption $\Delta(a\Rightarrow b)\in D$, we have $F(\\{a\Rightarrow
b\\})\subseteq D$. So $D$ contains a regular filter distinct from
$\\{\top\\}$.

Conversely, assume $D$ contains a regular filter $F\neq\\{\top\\}$. Then there
is $a\in F$ such that $a<\top$. This means that
$\Delta(a\Rightarrow\top)=\Delta\top=\top\in F$ and (since $F$ is regular)
$\Delta(\top\Rightarrow a)=\Delta a\in F$. Then, by the characterization of
Proposition 5.8, the pair $(a,\top)$ is identified by the Leibniz congruence
of $D$, which would make $\langle\mathbf{A},D\rangle$ not reduced. ∎

##  8 On interpolation for
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ and
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$, and amalgamation for
$\mathbb{PP}^{\Rightarrow_{\mathsf{H}}}$

We begin by defining three basic notions of interpolation according to the
terminology of Czelakowski and Pigozzi (1998, Def. 3.1). In this section we
will focus only in Set-Fmla logics, since this is the framework in which the
properties of interpolation are commonly formulated and investigated in the
literature.

######  Definition 8.1.

A Set-Fmla $\Sigma$-logic $\vdash$ has the

  1. 1.

_extension interpolation property_ (EIP) if having $\Phi,\Psi\vdash\varphi$
implies that there is $\Pi\subseteq
L_{\Sigma}(\mathsf{props}({\Psi\cup\\{\varphi\\})})$ such that
$\Phi\vdash\psi$ for all $\psi\in\Pi$ and $\Pi,\Psi\vdash\varphi$.

  2. 2.

_Craig interpolation property_ (CIP) if, whenever
$\mathsf{props}(\Phi)\cap\mathsf{props}(\varphi)\neq\varnothing$, having
$\Phi\vdash\varphi$ implies that there is $\Pi\subseteq
L_{\Sigma}(\mathsf{props}({\Phi})\cap\mathsf{props}(\varphi))$ such that
$\Phi\vdash\psi$ for all $\psi\in\Pi$ and $\Pi\vdash\varphi$.

  3. 3.

_Maehara interpolation property_ (MIP) if, whenever
$\mathsf{props}(\Phi)\cap\mathsf{props}({\Psi\cup\\{\varphi\\})}\neq\varnothing$,
having $\Phi,\Psi\vdash\varphi$ implies that there is $\Pi\subseteq
L_{\Sigma}(\mathsf{props}(\Phi)\cap\mathsf{props}({\Psi\cup\\{\varphi\\})})$
such that $\Phi\vdash\psi$ for all $\psi\in\Pi$ and $\Pi,\Psi\vdash\varphi$.

Note that the (MIP) implies the (CIP) — just take $\Psi=\varnothing$. It also
implies the (EIP) when the logic has theses (that is, formulas $\varphi$ such
that $\varnothing\vdash\varphi$) on a single variable and every formula
without variables is logically equivalent to some constant in the signature.
Note that for the logics ${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$
and $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$ both conditions hold
good.

Let us see now which of these interpolation properties the logic
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ satisfies. For what
follows, we recall that this logic satisfies the _deduction-detachment
theorem_ (DDT) with respect to the connective $\Rightarrow$, that is, we have
$\Phi,\varphi\vdash_{{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}}\psi$
if, and only if,
$\Phi\vdash_{{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}}\varphi\Rightarrow\psi$.

######  Theorem 8.2.

The logic ${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ has the (EIP)
but does not have the (CIP) nor the (MIP).

###### Proof.

Since ${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ is finitary, we
may consider only finite candidates for $\Psi$ and $\Pi$. To see that
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ has (EIP), assume that
$\Phi,\Psi\vdash_{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}\varphi$.
The property is satisfied if we choose
$\Pi\,{\coloneqq}\,\\{\bigwedge\Psi\Rightarrow\varphi\\}$, since
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ has the DDT.

Given that (MIP) implies (CIP), it is enough to show that the latter fails.
First of all, note that $(p\land{\sim}p\land
q\land{\sim}q\land{\sim}{\circ}(p\Rightarrow q))\lor
s\vdash_{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}(r\lor{\sim}r)\lor
s$ (recall the proof of Theorem 5.6). Based on the definition of (CIP), let
$\Phi\,{\coloneqq}\,\\{(p\land{\sim}p\land
q\land{\sim}q\land{\sim}{\circ}(p\Rightarrow q))\lor s\\}$ and
$\varphi\,{\coloneqq}\,(r\lor{\sim}r)\lor s$. Note that
$\mathsf{props}(\Phi)\cap\mathsf{props}(\varphi)=\\{s\\}$. Assume there is
such $\Pi$, then $\psi(s)\,{\coloneqq}\,\bigwedge\Pi$ is a formula with a
single variable $s$. We will see now that we cannot have both (i)
$\Phi\vdash_{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}\psi(s)$ and
(ii)
$\psi(s)\vdash_{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}\varphi$.
Let us fix $v(p)\,{\coloneqq}\,\mathbf{b}$, $v(q)\,{\coloneqq}\,\mathbf{n}$,
$v(r)\,{\coloneqq}\,\mathbf{b}$ and $v(s)\,{\coloneqq}\,\hat{\mathbf{f}}$ thus
making $v(\Phi)=\\{\mathbf{f}\\}$ and $v(\varphi)=\mathbf{b}$. Note that
$v(\psi)\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$. Hence, if
$v(\psi)=\hat{\mathbf{f}}$, then (i) fails, and, if
$v(\psi)=\hat{\mathbf{t}}$, (ii) fails.∎

Let us now take a look at the situation for
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}}$. Recall from Proposition
7.12 that this logic is determined by the single matrix
$\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},\\{\hat{\mathbf{t}}\\}\rangle$.

######  Theorem 8.3.

The logic ${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}}$ has the (EIP),
the (CIP) and the (MIP).

###### Proof.

It is enough to show it has the (MIP). Since
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$ is finitary, it suffices to
consider finite sets. Given
$\Phi,\Psi\vdash_{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}}\varphi$, let
$\mathsf{props}(\Phi)\cap\mathsf{props}(\Psi\cup\\{\varphi\\})=\\{p_{1},\ldots,p_{k}\\}\neq\varnothing$.
Consider
$\mathcal{U}\,{\coloneqq}\,\\{v\in\mathsf{Hom}(L_{\Sigma}(\\{p_{1},\ldots,p_{k}\\}),\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})\mid
v(\Phi)=\hat{\mathbf{t}}\\}$. For each $v\in\mathcal{U}$ and $1\leq i\leq k$,
let

$\displaystyle\varphi^{v}_{i}(p)$
$\displaystyle\,{\coloneqq}\,\begin{cases}p\land{\circ}p&\mbox{ if
}v(p_{i})=\hat{\mathbf{t}}\\\ {\sim}{\downarrow}p&\mbox{ if
}v(p_{i})=\mathbf{t}\\\
{\uparrow}p\land{\downarrow}p\land{\sim}{\circ}p&\mbox{ if
}v(p_{i})\in\\{\mathbf{b},\mathbf{n}\\}\\\ {\sim}{\uparrow}p&\mbox{ if
}v(p_{i})=\mathbf{f}\\\ {\sim}p\land{\circ}p&\mbox{ if
}v(p_{i})=\hat{\mathbf{f}}\end{cases}$ $\displaystyle I^{v}_{\mathbf{b}}$
$\displaystyle\,{\coloneqq}\,\\{i:v(p_{i})=\mathbf{b}\\}$ $\displaystyle
J^{v}_{\mathbf{n}}$ $\displaystyle\,{\coloneqq}\,\\{j:v(p_{j})=\mathbf{n}\\}$

and

$\displaystyle\psi_{v}$ $\displaystyle\,{\coloneqq}\,\bigwedge_{1\leq i\leq
k}\varphi^{v}_{i}(p_{i})\land\bigwedge_{i\in I_{\mathbf{b}}^{v},j\in
J_{\mathbf{n}}^{v}}{\sim}{\circ}(p_{i}\Rightarrow p_{j})$ $\displaystyle\phi$
$\displaystyle\,{\coloneqq}\,\bigvee_{v\in\mathcal{U}}\psi_{v}$

If we set $\equiv\;\subseteq\mathcal{V}_{6}\times\mathcal{V}_{6}$ such that
$a\equiv b$ iff $a=b$ or $\\{a,b\\}=\\{\mathbf{b},\mathbf{n}\\}$ we obtain
that, for all
$v^{\prime}\in\mathsf{Hom}(\mathbf{L}_{\Sigma}(P),\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$,

$v^{\prime}(\varphi^{v}_{i}(p))=\begin{cases}\hat{\mathbf{t}}&\text{if
}v^{\prime}(p)\equiv v(p_{i})\\\ \hat{\mathbf{f}}&\text{otherwise.}\\\
\end{cases}$

Thus, if $v^{\prime}(\psi_{v})=\hat{\mathbf{t}}$ then $v(p_{i})\equiv
v^{\prime}(p_{i})$ for every $1\leq i\leq k$.

Let us show that
$\phi\vdash_{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}}\varphi$. For
every
$v^{\prime}\in\mathsf{Hom}(\mathbf{L}_{\Sigma}(P),\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$
such that $v^{\prime}(\phi)=\hat{\mathbf{t}}$, there is $v\in\mathcal{U}$ such
that $v(p_{i})\equiv v^{\prime}(p_{i})$ for every $1\leq i\leq k$. Also,
$\\{\mathbf{b},\mathbf{n}\\}=\\{v(p_{i}),v(p_{j})\\}$ if, and only if,
$\\{\mathbf{b},\mathbf{n}\\}=\\{v^{\prime}(p_{i}),v^{\prime}(p_{j})\\}$, and
therefore $v(\psi)=v^{\prime}(\psi)$ for every $\psi$ such that
$\mathsf{props}(\psi)\subseteq\\{p_{1},\ldots,p_{k}\\}$. Thus, without loss of
generality, we proceed considering that $v(p_{i})=v^{\prime}(p_{i})$ for
$1\leq i\leq k$.

Considering
$v^{\prime\prime}\in\mathsf{Hom}(\mathbf{L}_{\Sigma}(P),\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$
such that

$v^{\prime\prime}(p)\,{\coloneqq}\,\begin{cases}v(p)&p\in
P{\setminus}\mathsf{props}(\Phi)\\\
v^{\prime}(p)&p\in\mathsf{props}(\Phi){\setminus}\\{p_{1},\ldots,p_{k}\\}\end{cases}$

we have that $v^{\prime\prime}(\Phi)=v^{\prime\prime}(\Psi)=\hat{\mathbf{t}}$,
thus from
$\Phi,\Psi\vdash_{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}}\varphi$ we
conclude that $v^{\prime\prime}(\varphi)=v^{\prime}(\psi)=\hat{\mathbf{t}}$
and therefore
$\phi\vdash_{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}}\varphi$. Finally,
to see that $\Phi\vdash_{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}}\phi$,
note that if $v(\Phi)=\\{\hat{\mathbf{t}}\\}$ then, by definition,
$v\in\mathcal{U}$ and therefore $v(\psi_{v})=v(\phi)=\hat{\mathbf{t}}$.∎

######  Remark 8.4.

Recall that, in the previous section, we presented the DDT for
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$, which demands a different
(derived) connective to play the role of $\Rightarrow$. This could also have
been used to prove the (EIP) for this logic.

When a Set-Fmla logic satisfies some of the above interpolation properties and
we know it is algebraizable, the class of algebras corresponding to the
equivalent algebraic semantics satisfies so-called ‘amalgamation properties’.
We will focus here on two of such properties, the _Maehara amalgamation
property_ (MAP) and the _flat amalgamation property_ (FAP), as they are the
ones corresponding respectively to the interpolation properties (MIP) and
(CIP) entertained above.

We need some preliminary concepts before formulating such properties. Let
$\mathsf{K}$ be a class of $\Sigma$-algebras and
$\mathbf{A},\mathbf{B}\in\mathsf{K}$. If $\mathbf{A}$ is a subalgebra of
$\mathbf{B}$ and $S\subseteq B$, $\mathbf{B}$ is said to be a _$\mathsf{K}$
-free extension of $\mathbf{A}$ over $S$_ if for every
$\mathbf{C}\in\mathsf{K}$, every homomorphism $h:\mathbf{A}\to\mathbf{C}$ and
every $f:S\to C$, there is a unique homomorphism $g:\mathbf{B}\to\mathbf{C}$
such that $g\upharpoonleft A=h$ and $g\upharpoonleft S=f$, where
$\upharpoonleft$ denotes domain restriction. Write
$f:\mathbf{A}\rightarrowtail\mathbf{B}$ to denote that $f$ is an injective
homomorphism, and $f:\mathbf{A}\hookrightarrow\mathbf{B}$ to denote that $f$
is a _free injection over $\mathsf{K}$_, meaning that $f$ is an injection and
$f(\mathbf{B})$ is a _$\mathsf{K}$ -free extension_ of $\mathbf{B}$ over some
set $S$ of elements.

######  Definition 8.5 (Czelakowski and Pigozzi (1998), Def. 5.2).

A class of algebras $\mathsf{K}$ has the

  1. 1.

_Maehara amalgamation property_ (MAP) when, for all
$\mathbf{A},\mathbf{B},\mathbf{C}\in\mathsf{K}$, and all homomorphisms
$f:\mathbf{C}\rightarrowtail\mathbf{A}$ and $g:\mathbf{C}\to\mathbf{B}$, there
exists $\mathbf{D}\in\mathsf{K}$ and homomorphisms $h:\mathbf{A}\to\mathbf{D}$
and $k:\mathbf{B}\rightarrowtail\mathbf{D}$ such that $hf=kg$.

  2. 2.

_flat amalgamation property_ (FAP) when for all
$\mathbf{A},\mathbf{B},\mathbf{C}\in\mathsf{K}$, and all homomorphisms
$f:\mathbf{C}\rightarrowtail\mathbf{A}$ and
$g:\mathbf{C}\hookrightarrow\mathbf{B}$, there exists
$\mathbf{D}\in\mathsf{K}$ and homomorphisms
$h:\mathbf{A}\hookrightarrow\mathbf{D}$ and
$k:\mathbf{B}\rightarrowtail\mathbf{D}$ such that $hf=kg$.

######  Theorem 8.6.

$\mathbb{PP}^{\Rightarrow_{\mathsf{H}}}$ has the (MAP) and the (FAP).

###### Proof.

By Theorem 7.5, we know that $\mathbb{PP}^{\Rightarrow_{\mathsf{H}}}$ is the
equivalent algebraic semantics of
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$. We just saw that this logic
satisfies (MIP) and (CIP), thus, by (Czelakowski and Pigozzi, 1998, Cor. 5.27
and Cor. 5.29), $\mathbb{PP}^{\Rightarrow_{\mathsf{H}}}$ satisfies (MAP) and
(FAP). ∎

##  9 Conclusions and future work

In the present paper we have initiated the study of implicative expansions of
logics of perfect paradefinite algebras by considering classic-like and
Heyting implications, both in the Set-Set and in the Set-Fmla framework. We
investigated semantical characterizations (via classes of algebras and logical
matrices) as well as proof-theoretical ones (via Set-Set and Set-Fmla Hilbert-
style calculi) of these extensions. For the extensions with a Heyting
implication, in particular, the new connective introduced many challenges for
not allowing the logic to be characterized by any single logical matrix; we
proved, however, that it can be characterized by a single finite PNmatrix.
Over such extensions we also studied properties of interpolation and
amalgamation for the corresponding algebraic models. We indicate below a few
directions that we believe could prove worthwhile pursuing in future research.

#### Alternative expansions of the logics of PP-algebras.

In Section 4 we have briefly considered other logics that may be obtained by
conservatively adding an implication to the logics of PP-algebras
$\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}$ and $\mathcal{PP}_{\\!\leq}$. We did
not explore these alternatives much further, preferring instead (from Section
5 onward) to focus our attention on logics having a more straightforward
connection to existing frameworks (Moisil’s logic and symmetric Heyting
algebras). Nevertheless, we feel that such alternative systems may deserve
further study, and the connection we noted with the recent work by Coniglio
and Rodrigues (2023) provides further motivation for this project.
Additionally, it would be interesting to systematically investigate the logics
determined by refinements of the PNmatrix $\mathfrak{M}_{\mathsf{up}}$,
providing axiomatizations, classifying them within the hierarchies of
algebraic logic (e.g., which among them are algebraizable?) and studying the
corresponding classes of algebras as done in Section 7 for
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$. Lastly, further enlarging
the scope, one might ask whether condition $(\mathsf{A}1)$ could be relaxed,
perhaps requiring the new implication to be axiomatized by the usual inference
rules for Heyting implications (rather than classic-like implications, which
correspond to $(\mathsf{A}1)$, as we have seen). In this way we could
circumvent the limitation of Theorem 4.1 exploring alternative self-
extensional expansions of the logics of PP-algebras.

#### Extensions of $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$.

Our preliminary investigations suggest that the landscape of extensions of the
base logics considered in the present paper is quite interesting and complex.
Concerning the _finitary_ Set-Fmla extensions of
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ we may affirm the
following:

  * •

By (Jansana, 2006, Thm. 3.7), the finitary Set-Fmla self-extensional
extensions of ${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ are in
one-to-one correspondence with the subvarieties of
$\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$. Thus, by Corollary
7.11, there are only three of them, all of them axiomatic (none being
conservative expansions over $\mathcal{PP}_{\\!\leq}$). These logics may be
axiomatized, relatively to
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$, by adding the axioms
corresponding to the equations in Corollary 7.11, to wit:

    1. 1.

the logic of $\mathbb{V}(\mathbf{PP_{4}^{\Rightarrow_{\mathsf{H}}}})$ is
axiomatized by $(p\land{\sim}p)\Rightarrow(q\lor{\sim}q)$;

    2. 2.

the logic of $\mathbb{V}(\mathbf{PP_{3}^{\Rightarrow_{\mathsf{H}}}})$ by
$p\lor(p\Rightarrow(q\lor\neg q))$; and

    3. 3.

the logic of $\mathbb{V}(\mathbf{PP_{2}^{\Rightarrow_{\mathsf{H}}}})$, which
is (up to the choice of language) just classical logic, by $p\lor{\sim}p$.

  * •

The number of all the axiomatic Set-Fmla extensions of
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ (which are obviously
finitary) is larger but also finite, for each axiomatic extension may be be
characterized by the submatrices of the original matrices that satisfy the
axioms333 This result can be easily established using (Caleiro and Marcelino,
2021, Prop. 3.1) together with the observation that the total components of
the PNmatrix $\mathfrak{M}_{\mathsf{up}}$ are deterministic; thus, the
submatrices of $\mathfrak{M}_{\mathsf{up}}$ which are images of valuations
that satisfy every instance of an axiom are sound with respect to that
particular axiom..

  * •

As we have seen, the assertional logic
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$ is itself a (non-axiomatic,
non-self-extensional) extension of
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$. Algebraizability of
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$ (Theorem 7.5) entails that
its axiomatic Set-Fmla extensions are in one-to-one correspondence with the
subvarieties of $\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$, so
again we can conclude that there are only three of them.

  * •

In contrast to the preceeding results, we conjecture that it may be possible
to construct countably many distinct (non-axiomatic) Set-Fmla finitary
extensions of $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$. By
algebraizability, this would tell us that the variety
$\mathbb{PP}^{\Rightarrow_{\mathsf{H}}}$ has at least countably many sub-
quasivarieties.

Now considering the Set-Set extensions of
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$, we can say the
following:

  * •

Similarly to the Set-Fmla setting, all _axiomatic_ Set-Set extensions of
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$ are
characterized by the sets of (sub)matrices in
$\\{\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{\uparrow}a\rangle\mid
a\in\mathcal{V}\\}$ that satisfy the corresponding axioms, hence their
cardinality is also finite. Their Set-Fmla companions are obtained by adding
the same axioms to $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$.

  * •

In consequence, there are _at least_ three self-extensional Set-Set extensions
of ${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$, namely, the
ones determined by the matrices which satisfy the corresponding axioms. (There
may be more, but each of them will have as Set-Fmla fragment one of the three
self-extensional Set-Fmla extensions of
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ mentioned earlier.)

  * •

The methods used in the previous sections may be used to obtain analytic Set-
Set axiomatizations for all the logics determined by sets of (sub)matrices in
$\\{\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{\uparrow}a\rangle\mid
a\in\mathcal{V}\\}$.

The preceding considerations suggest that a complete description of the
lattice of all extensions of our base logics is well beyond the scope of the
present work, and will have to be pursued in further research. We summarize
such research path in terms of the following couple of problems:

######  Problem 1.

Describe the lattice of all (Set-Fmla) extensions of
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ and the lattice of all
(Set-Set) extensions of
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$.

######  Problem 2.

Same as the preceding one, but restricting one’s attention to the sublattices
consisting of all the Set-Fmla (Set-Set) extensions of
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$ (of its Set-Set companion
determined by the matrix
$\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{{\uparrow}\hat{\mathbf{t}}}\rangle$).
Due to the algebraizability of
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$, for finitary Set-Fmla logics
the problem may be rephrased as: describe the lattice of all subquasivarieties
of $\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$.

#### Fragments of the language of
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$.

A close inspection of the methods employed in the previous sections to
axiomatize $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ and its Set-Set
companions suggests that these may also be applied so as to obtain analytic
axiomatizations for the logics corresponding to those fragments of the
language over the connectives in
$\\{\land,\lor,\Rightarrow,{\sim},{\circ},\bot,\top\\}$ that are sufficiently
rich to express an appropriate set of separators. Some of these, we believe,
have intrinsic logical and algebraic interest, and may deserve further study.
Let us single out, for instance, the fragments corresponding to the
connectives $\\{\Rightarrow,{\circ}\\}$, $\\{\Rightarrow,\Delta\\}$ (recall
that $\Delta x:={\sim}x\Rightarrow{\sim}(x\Rightarrow x)$) and
$\\{\Rightarrow,{\sim}\\}$. The first of them may be of interest as a minimal
Logic of Formal Inconsistency, while the second could be studied in the
setting of implication fragments of modal systems. The study of the third
could lead to an interesting generalization of Monteiro’s results on symmetric
Heyting algebras and their logic.

## Acknowledgments

Vitor Greati acknowledges support from the FWF project P33548. Sérgio
Marcelino’s research was done under the scope of project FCT/MCTES through
national funds and when applicable co-funded by EU under the project
UIDB/50008/2020.

## References

  * Avron [2020] A. Avron.  The normal and self-extensional extension of Dunn-Belnap logic.  _Logica Universalis_ , 14(3):281–296, 2020.  doi:10.1007/s11787-020-00254-1.
  * Balbes and Dwinger [1975] R. Balbes and P. Dwinger.  _Distributive Lattices_.  University of Missouri Press, 1975.  ISBN 0826201636,9780826201638.
  * Belnap [1977] N. D. Belnap.  A useful four-valued logic.  In _Modern Uses of Multiple-Valued Logic_ , pages 5–37. Springer Netherlands, Dordrecht, 1977.  ISBN 978-94-010-1161-7.  doi:10.1007/978-94-010-1161-7_2.
  * Blok and Pigozzi [1989] W. J. Blok and D. Pigozzi.  Algebraizable logics.  _Memoirs of the American Mathematical Society_ , 396, 1989.
  * Bou et al. [2011] F. Bou, F. Esteva, J. Maria Font, A. J. Gil, L. Godo, A. Torrens, and V. Verdú.  Logics preserving degrees of truth from varieties of residuated lattices.  _Journal of Logic and Computation_ , 22(3):661–665, 03 2011.  ISSN 0955-792X.  doi:10.1093/logcom/exr003.
  * Burris and Sankappanavar [2011] S. Burris and H. P. Sankappanavar.  _A Course in Universal Algebra_.  Springer, 2011.
  * Caleiro and Marcelino [2019] C. Caleiro and S. 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.  doi:10.1007/978-3-662-59533-6_6.
  * Caleiro and Marcelino [2021] C. Caleiro and S. Marcelino.  On axioms and rexpansions.  In O. Arieli and A. Zamansky, editors, _Arnon Avron on Semantics and Proof Theory of Non-Classical Logics_ , volume 21 of _Outstanding Contributions to Logic_. Springer, 2021.  doi:10.1007/978-3-030-71258-7_3.
  * Caleiro and Marcelino [2023] C. Caleiro and S. Marcelino.  Modular many-valued semantics for combined logics.  _The Journal of Symbolic Logic_ , pages 1–54, Apr. 2023.  doi:10.1017/jsl.2023.22.
  * Cantú [2019] L. M. Cantú.  Sobre la lógica que preserva grados de verdad asociada a las Álgebras de Stone involutivas.  Master’s thesis, Universidad Nacional del Sur, Bahía Blanca, Argentina, 2019.
  * Cantú and Figallo [2018] L. M. Cantú and M. Figallo.  On the logic that preserves degrees of truth associated to involutive Stone algebras.  _Logic Journal of the IGPL_ , 28(5):1000–1020, 11 2018.  ISSN 1367-0751.  doi:10.1093/jigpal/jzy071.
  * Cantú and Figallo [2022] L. M. Cantú and M. Figallo.  Cut-free sequent-style systems for a logic associated to involutive Stone algebras.  _Journal of Logic and Computation_ , page to appear, 09 2022.  ISSN 0955-792X.  doi:10.1093/logcom/exac061.
  * Carnielli et al. [2007] W. A. Carnielli, M. E. Coniglio, and J. Marcos.  Logics of Formal Inconsistency.  In D. Gabbay and F. Guenthner, editors, _Handbook of Philosophical Logic_ , volume 14, pages 1–93. Springer, 2nd edition, 2007.  doi:10.1007/978-1-4020-6324-4_1.
  * Cignoli and Sagastume [1981] R. Cignoli and M. Sagastume.  The lattice structure of some Łukasiewicz algebras.  _Algebra Universalis_ , 13(1):315–328, Dec 1981.  ISSN 1420-8911.  doi:10.1007/BF02483844.
  * Cignoli and Sagastume [1983] R. Cignoli and M. Sagastume.  Dualities for some De Morgan algebras with operators and Łukasiewicz algebras.  _Journal of the Australian Mathematical Society. Series A. Pure Mathematics and Statistics_ , 34(3):377–393, 1983.  doi:10.1017/S1446788700023806.
  * Clark and Davey [1998] D. M. Clark and B. A. Davey.  _Natural Dualities for the Working Algebraist_.  Cambridge, 1998.
  * Coniglio and Rodrigues [2023] M. E. Coniglio and A. Rodrigues.  On six-valued logics of evidence and truth expanding Belnap-Dunn four-valued logic.  _Studia Logica_ , page to appear, 2023.
  * Czelakowski and Pigozzi [1998] J. Czelakowski and D. Pigozzi.  _Models, Algebras, and Proofs_ , chapter Amalgamation and Interpolation in Abstract Algebraic Logic.  Taylor & Francis, 1998.
  * Davey and Priestley [2002] B. A. Davey and H. A. Priestley.  _Introduction to Lattices and Order_.  Cambridge University Press, 2nd edition, 2002.  ISBN 0521784514,9780521784511.
  * Font [2016] J. M. Font.  _Abstract Algebraic Logic: An introductory textbook_.  College Publications, 04 2016.  ISBN 978-1-84890-207-7.
  * Galatos et al. [2007] N. Galatos, P. Jipsen, T. Kowalski, and H. Ono.  _Residuated lattices: an algebraic glimpse at substructural logics_ , volume 151 of _Studies in Logic and the Foundations of Mathematics_.  Elsevier, 2007.
  * Gomes et al. [2022] J. Gomes, V. Greati, S. Marcelino, J. Marcos, and U. Rivieccio.  On logics of perfect paradefinite algebras.  _Electronic Proceedings in Theoretical Computer Science_ , 357:56–76, Apr. 2022.  doi:10.4204/eptcs.357.5.
  * Humberstone [2011] L. Humberstone.  _The Connectives_.  MIT Press, 2011.
  * Jansana [2006] R. Jansana.  Selfextensional logics with a conjunction.  _Studia Logica_ , 84(1):63–104, Sep 2006.  ISSN 1572-8730.  doi:10.1007/s11225-006-9003-z.
  * Marcelino and Caleiro [2021] S. Marcelino and C. Caleiro.  Axiomatizing non-deterministic many-valued generalized consequence relations.  _Synthese_ , 198:5373–5390, 2021.  ISSN 1573-0964.  doi:10.1007/s11229-019-02142-8.
  * Marcelino and Rivieccio [2022] S. Marcelino and U. Rivieccio.  Logics of involutive Stone algebras.  _Soft Computing_ , 26:3147–3160, 2022.
  * Marcos [2005a] J. Marcos.  _Logics of Formal Inconsistency_.  PhD thesis, Unicamp, Brazil & IST, Portugal, 2005a.  URL https://www.math.tecnico.ulisboa.pt/~jmarcos/Thesis/.
  * Marcos [2005b] J. Marcos.  Nearly every normal modal logic is paranormal.  _Logique et Analyse_ , 48:279–300, 01 2005b.
  * Monteiro [1980] A. Monteiro.  Sur les algèbres de Heyting symétriques.  _Portugaliae Mathematica_ , 39(1-4):1–237, 1980.  URL http://eudml.org/doc/115416.
  * Rivieccio [2012] U. Rivieccio.  An infinity of super-Belnap logics.  _Journal of Applied Non-Classical Logics_ , 22(4):319–335, 2012.  doi:10.1080/11663081.2012.737154.
  * Sankappanavar [1987] H. P. Sankappanavar.  Heyting algebras with a dual lattice endomorphism.  _Zeitschrift fur mathematische Logik und Grundlagen der Mathematik_ , 33(6):565–573, 1987.  doi:10.1002/malq.19870330610.
  * Shoesmith and Smiley [1978] D. J. Shoesmith and T. J. Smiley.  _Multiple-Conclusion Logic_.  Cambridge University Press, 1978.
  * Wójcicki [1988] R. Wójcicki.  _Theory of Logical Calculi_.  Synthese Library. Springer, Dordrecht, 1 edition, 1988.  ISBN 978-90-277-2785-5.  doi:10.1007/978-94-015-6942-2.