# Adding an Implication to Logics of Perfect Paradefinite Algebras

Vitor Greati
Bernoulli Institute
University of Groningen
Groningen, The Netherlands
<EMAIL_ADDRESS>
& Sérgio Marcelino
SQIG - Instituto de Telecomunicações
Departamento de Matemática - Instituto Superior Técnico
Universidade de Lisboa
Lisboa, Portugal
<EMAIL_ADDRESS>
& João Marcos
Department of Philosophy
UFSC
Santa Catarina, Brazil
<EMAIL_ADDRESS>
& Umberto Rivieccio
Departamento de Lógica, Historia y Filosofía de la Ciencia
Universidad Nacional de Educación a Distancia
Madrid, Spain
<EMAIL_ADDRESS>

###### Abstract

Perfect paradefinite algebras are De Morgan algebras expanded with a
perfection (or classicality) operation. They form a variety that is term-
equivalent to the variety of involutive Stone algebras. Their associated
multiple-conclusion (Set-Set) and single-conclusion (Set-Fmla) order-
preserving logics are non-algebraizable self-extensional logics of formal
inconsistency and undeterminedness determined by a six-valued matrix, studied
in depth by Gomes et al. (2022) from both the algebraic and the proof-
theoretical perspectives. We continue hereby that study by investigating
directions for conservatively expanding these logics with an implication
connective (essentially, one that admits the deduction-detachment theorem). We
first consider logics given by very simple and manageable non-deterministic
semantics whose implication (in isolation) is classical. These, nevertheless,
fail to be self-extensional. We then consider the implication realized by the
relative pseudo-complement over the six-valued perfect paradefinite algebra.
Our strategy is to expand such algebra with this connective and study the
(self-extensional) Set-Set and Set-Fmla order-preserving and
$\top$-assertional logics of the variety induced by the new algebra. We
provide axiomatizations for such new variety and for such logics, drawing
parallels with the class of symmetric Heyting algebras and with Moisil’s
‘symmetric modal logic’. For the Set-Set logic, in particular, the
axiomatization we obtain is analytic. We close by studying interpolation
properties for these logics and concluding that the new variety has the
Maehara amalgamation property.

_Keywords_ paradefinite logics $\cdot$ logics of formal inconsistency and
undeterminedness $\cdot$ implication $\cdot$ Heyting algebras $\cdot$ De
Morgan algebras.

##  1 Introduction

The algebraic structures we now call _involutive Stone algebras_ appear to
have been first considered by Roberto Cignoli and Marta Sagastume along their
investigation of finite-valued Łukasiewicz logics, in connection with
Łukasiewicz-Moisil algebras (Cignoli and Sagastume (1981, 1983)). Formally,
involutive Stone algebras are usually presented as expansions of De Morgan
algebras (whose languages consists of a conjunction $\land$, a disjunction
$\lor$, a negation ${\sim}$ and the lattice bounds $\bot,\top$) in one of the
following two alternative term-equivalent ways (we shall soon see that a third
one has been recently proposed):

  1. 1.

by adding a unary ‘possibility’ operator (usually denoted by $\nabla$ in the
literature);

  2. 2.

by adding an ‘intuitionistic’ (namely, a pseudo-complement) negation (denoted
by $\neg$) satisfying the well-known Stone equation: $\neg x\lor\neg\neg
x\approx\top$.

Though obviously arising as “algebras of logic”, the class of involutive Stone
algebras was not employed as an algebraic semantics for logical systems in the
above-mentioned seminal works; rather, this has been pursued in a series of
recent papers which focused in particular on the logic that preserves the
lattice order of involutive Stone algebras (Cantú (2019); Cantú and Figallo
(2018); Marcelino and Rivieccio (2022); Cantú and Figallo (2022)).

In the paper Gomes et al. (2022), which is the immediate predecessor of the
present one, we built on the observation (made in Cantú and Figallo (2018))
that the logic of involutive Stone algebras may be viewed as a _Logic of
Formal Inconsistency_ in the sense of Marcos (2005a); Carnielli et al. (2007),
and axiomatized it as such. This was possible due to the fact that involutive
Stone algebras may be presented in a third term-equivalent way, namely:

  1. 3.

by adding a unary ‘perfection’ operator (denoted by $\circ$) of the kind
considered in Marcos (2005b).

Reformulated in this language ($\\{\land,\lor,{\sim},{\circ},\bot,\top\\}$),
involutive Stone algebras have been renamed _perfect paradefinite algebras_
(PP-algebras) in Gomes et al. (2022). In that paper we axiomatized the Set-
Fmla logic of order of PP-algebras, called $\mathcal{PP}_{\\!\leq}$, and also
showed that $\mathcal{PP}_{\\!\leq}$ is semantically determined by a finite
matrix based on the six-element algebra (there dubbed $\mathbf{PP_{6}}$) that
generates the class of PP-algebras as a variety. Actually, we developed most
of our results with respect to a Set-Set version of this logic, called
$\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}{}$. The Set-Set axiomatization we
presented for it is analytic, and thus suitable for automated reasoning. We
then used all these results to aid in the study of $\mathcal{PP}_{\\!\leq}$.

In the present paper, further pursuing this approach, we shall focus on the
question of _how to add an implication connective to Set-Set and Set-Fmla
logics associated to PP-algebras_. In an effort to proceed in a systematic
fashion, we shall be guided by the following main principles:

  * •

the resulting system must be conservative over the logics being extended;

  * •

the new connective must indeed qualify as an implication according to some
general standard.

In order to narrow down our search and to eventually converge upon a short
list of candidates, we shall presently consider a third guiding principle as
well, namely:

  * •

the new logic must also qualify as a _logic of order_ of a suitable class of
algebras.

In the present setting, as we shall see, the above principle turns out to be
equivalent to requiring the logic to be _self-extensional_ , or congruential
(see Definition 2.3).

The approach outlined above for the study of implicational extensions is
reminiscent of — indeed, directly inspired by— Avron’s proposal for extending
Belnap’s logic (Avron (2020)), in which two main requirements are entertained:
first, that the new connective should be an implication relative to a given
set of designated elements (condition $(\mathsf{A}1)$ in Subsection 2.4);
second, that the resulting logic should be self-extensional $(\mathsf{A}2)$.
We shall discuss these requirements at length in Section 4, where we show that
in our case there is unfortunately _no implication connective that meets both
of them_ (Theorem 4.1). This is where we shall choose to retain the latter
requirement (self-extensionality) instead of the former, which we find too
restrictive, as we shall also discuss. As this choice still leaves plenty of
room for a large collection of alternative implications, we shall follow two
North Stars: Algebra and Tradition.

Algebra suggests that, for a wide family of logics, a well-behaved implication
connective may be obtained by considering, whenever available, the residuum of
the algebraic operation that realizes the logical conjunction (see e.g.
Galatos et al. (2007)): this leads us to expand the logics of PP-algebras by a
relative pseudo-complement implication, which we shall call a _Heyting
implication_ , for our definition mirrors the usual one for the implication on
Heyting algebras.

Tradition, in the present setting, turns out to point in the same direction as
algebra. In fact, it turns out that a substantial part of the theory of
involutive Stone algebras was already developed, even prior to Cignoli and
Sagastume’s works, in Monteiro (1980), itself a collection of earlier
material. The main subject of Monteiro’s monograph is the class of _symmetric
Heyting algebras_ , providing an algebraic counterpart to Moisil’s _symmetric
modal logic_. These algebras are presented precisely in the traditional
language of involutive Stone algebras (with the $\nabla$ operator which
Monteiro dubs ‘possibility’) enriched with a Heyting implication.

The formal relation between the class of PP-algebras enriched with an
implication that we shall define and Monteiro’s symmetric Heyting algebras is
discussed in detail in Section 7. For the time being, let us conclude these
introductory remarks by mentioning an alternative proposal concerning our main
question — how to add an implication to logics of PP-algebras, one of them
being $\mathcal{PP}_{\\!\leq}$ — which can be retrieved from a recent paper by
Coniglio and Rodrigues (2023). Their purpose is to add a perfection operator
${\circ}$ to the well-known Belnap-Dunn four-valued logic, but the authors
actually start from a logic which is itself a conservative expansion of the
Belnap-Dunn logic with a _classic-like implication_ (in the sense of
Definition 2.11). The resulting logic – dubbed $\mathrm{LET_{K}^{+}}$ – turns
out to be determined by a six-valued matrix that (if we disregard the
implication) coincides with the matrix
$\langle\mathbf{PP_{6}},{{\uparrow}\mathbf{b}}\rangle$ which determines the
logic $\mathcal{PP}_{\\!\leq}$ (see Gomes et al. (2022)). As noted in Coniglio
and Rodrigues (2023, Subsec. 5.1), it follows that the implication-free
fragment of $\mathrm{LET_{K}^{+}}$ coincides with $\mathcal{PP}_{\\!\leq}$.
The implication connective of $\mathrm{LET_{K}^{+}}$ consists thus in a
candidate for expanding $\mathcal{PP}_{\\!\leq}$ with an implication. An
inspection of its truth-table (see Coniglio and Rodrigues (2023, Def. 3.9))
reveals (see also Section 4) that this implication satisfies (with respect to
the designated set ${{\uparrow}\mathbf{b}}$) the first among Avron’s
requirements, $(\mathsf{A}1)$, and therefore destroys self-extensionality (or,
one may say, preserves the non-self-extensional character of paraconsistent
Nelson logic). This leads to an interesting observation, namely, that
$\mathrm{LET_{K}^{+}}$ is determined by a refinement of the non-deterministic
matrix introduced in Section 4, and may be obtained, thus, from the
corresponding logic by adding suitable rules. In this sense, we may say our
approach subsumes that of Coniglio and Rodrigues (2023), at least insofar as
the task of conservatively expanding $\mathcal{PP}_{\\!\leq}$ is concerned.

The paper is organized as follows. After the preliminary sections in which we
fix the notation and basic definitions, we delve into the problem of expanding
the logics of order of PP-algebras with an implication. To that effect, we
first consider in Section 4 adding an implication satisfying at once
$(\mathsf{A}1)$ and $(\mathsf{A}2)$. After proving the impossibility of this
task, we focus on $(\mathsf{A}1)$, which makes the implication qualify as
classic-like. We explore possibilities of doing so using the semantical
framework of non-deterministic logical matrices, providing analytic
axiomatizations for the obtained Set-Set logics, from which we can readily
obtain Set-Fmla axiomatizations for the corresponding Set-Fmla companions.

Next, having observed that the matrix
$\langle\mathbf{PP_{6}},{{\uparrow}\mathbf{b}}\rangle$, which determines
$\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}$ and $\mathcal{PP}_{\\!\leq}$, is
based on an algebra ($\mathbf{PP_{6}}$) that is a finite distributive lattice,
in Section 5 we enrich its language with an operation
$\Rightarrow_{\mathsf{H}}$ which corresponds to the relative pseudo-complement
implication determined by the lattice order. In fact, the six-element Heyting
algebra thus obtained (denoted by
$\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$) turns out to be a symmetric
Heyting algebra in Monteiro’s sense. We then consider the family of all
matrices $\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},D\rangle$ such
that $D$ is a non-empty lattice filter of the lattice reduct of
$\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$. The (Set-Set and Set-Fmla)
logics determined by this family are the order-preserving logics induced by
the variety $\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$,
guaranteed to be self-extensional.

In Section 6, we proceed to axiomatize both the Set-Set and the Set-Fmla
logics thus defined. First focusing on the Set-Set logic, we propose an
axiomatization by a detailed analysis of the algebraic structure of the
matrices and of their designated sets. More than sound and complete, the
calculus turn out to be analytic. From such axiomatization we show how to
extract an axiomatization for the corresponding Set-Fmla logic of order.

In Section 7, we look at the algebraic models that correspond to the Set-Fmla
logics $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ and
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$ (the $\top$-assertional logic
associated to $\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$) within
the general theory of algebraization of logics. We begin by realizing that
both logics are closely related to Moisil’s ‘symmetric modal logic’, whose
algebraic counterpart is the class of symmetric Heyting algebras (Definition
7.1). Indeed, $\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ is (term-equivalent
to) a symmetric Heyting algebra, and the class of algebras providing an
algebraic semantics for both
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ and
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$ is precisely the subvariety
$\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$ of symmetric Heyting
algebras generated by $\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ (Theorem
7.5); an equational presentation for
$\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$ is introduced in
Definition 7.3, and shown to be sound and complete in Theorem 7.4. The
algebraizability of Moisil’s logic (Proposition 7.2) entails that
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$ is also algebraizable; its
equivalent algebraic semantics is precisely
$\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$, and its reduced
matrix models are the matrices of the form
$\langle\mathbf{A},\\{\top\\}\rangle$ with
$\mathbf{A}\in\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$ (Theorem
7.5). On the other hand, $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$
is not algebraizable (Proposition 5.8) but its algebraic counterpart is also
$\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$; the shape of the
reduced matrix models of $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$
is described in Proposition 7.13. We conclude the section by looking at the
subvarieties of $\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$.
There are only three of them (corresponding precisely to the self-extensional
extensions of $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$) which can
be axiomatized by adding the axioms that translate the equations shown in
Corollary 7.11.

In Section 8, we draw some conclusions regarding interpolation for the
implicative extensions of interest, as well as amalgamation for the class of
algebraic models of $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$. Further
paths of investigation are highlighted in Section 9.

##  2 Preliminaries

In this section, we introduce the main concepts related to algebras, logics
and axiomatizations, with particular attention to perfect paradefinite
algebras and their logics. We also fix what we shall understand as an
implication and the selection criteria we will employ in investigating
extensions of a logic by the addition of an implication.

###  2.1 Algebras, languages and logics

A _propositional signature_ is a family
$\Sigma\,{\coloneqq}\,\\{\Sigma_{k}\\}_{k\in\omega}$, where each $\Sigma_{k}$
is a collection of $k$-ary _connectives_. A _$\Sigma$ -multialgebra_ is a
structure $\mathbf{A}\,{\coloneqq}\,\langle A,\cdot^{\mathbf{A}}\rangle$,
where $A$ is a non-empty set called the _carrier_ of $\mathbf{A}$ and, for
each $\copyright\in\Sigma_{k}$, the _multioperation_
$\copyright^{\mathbf{A}}:A^{k}\to\wp(A)$ is the _interpretation_ of
$\copyright$ in $\mathbf{A}$. We say that $\mathbf{A}$ is a _$\Sigma$
-algebra_ (or _deterministic $\Sigma$-multialgebra_) when
$\copyright^{\mathbf{A}}(a_{1},\ldots,a_{k})$ is a singleton for every
$a_{1},\ldots,a_{k}\in A$, $\copyright\in\Sigma_{k}$ and $k\in\omega$. If
$\copyright^{\mathbf{A}}(a_{1},\ldots,a_{k})\neq\varnothing$ for every
$a_{1},\ldots,a_{k}\in A$, $\copyright\in\Sigma_{k}$ and $k\in\omega$, we say
that $\mathbf{A}$ is _total_. Note that the notion of $\Sigma$-algebra matches
the usual notion of algebra in Universal Algebra (cf. Sankappanavar (1987))
(which we will employ throughout the paper without notice). Given
$\Sigma^{\prime}\subseteq\Sigma$ (that is,
$\Sigma^{\prime}_{k}\subseteq\Sigma_{k}$ for all $k\in\omega$), the
_$\Sigma^{\prime}$ -reduct_ of a $\Sigma$-multialgebra $\mathbf{A}$ is the
$\Sigma^{\prime}$-multialgebra over the same carrier of $\mathbf{A}$ that
agrees with $\mathbf{A}$ on the interpretation of the connectives in
$\Sigma^{\prime}$.

A _$\Sigma$ -homomorphism_ between $\Sigma$-multialgebras $\mathbf{A}$ and
$\mathbf{B}$ is a mapping $h:A\to B$ such that
$h(\copyright^{\mathbf{A}}(a_{1},\ldots,a_{k}))\in\copyright^{\mathbf{B}}(h(a_{1}),\ldots,h(a_{k}))$
for all $a_{1},\ldots,a_{k}\in A$, $\copyright\in\Sigma_{k}$ and $k\in\omega$.
Note that for $\Sigma$-algebras this definition coincides with the usual
notion of homomorphism. The collection of $\Sigma$-homomorphisms between two
$\Sigma$-multialgebras $\mathbf{A}$ and $\mathbf{B}$ is denoted by
$\mathsf{Hom}(\mathbf{A},\mathbf{B})$.

Given a denumerable set $P\supseteq\\{p,q,r,s,x,y\\}$ of _propositional
variables_ , the absolutely free $\Sigma$-algebra freely generated by $P$, or
simply the _language_ over $\Sigma$ (generated by $P$), is denoted by
$\mathbf{L}_{\Sigma}(P)$, and its members are called _$\Sigma$ -formulas_. The
collection of all propositional variables occurring in a formula $\varphi\in
L_{\Sigma}(P)$ is denoted by $\mathsf{props}(\varphi)$, and we let
$\mathsf{props}(\Phi)\,{\coloneqq}\,\bigcup_{\varphi\in\Phi}\mathsf{props}(\varphi)$,
for all $\Phi\subseteq L_{\Sigma}(P)$. The elements of
$\mathsf{Hom}(\mathbf{L}_{\Sigma}(P),\mathbf{A})$ will sometimes be referred
to as _valuations on $\mathbf{A}$_. When $\mathbf{A}$ is
$\mathbf{L}_{\Sigma}(P)$, valuations are endomorphisms on
$\mathbf{L}_{\Sigma}(P)$ and are usually dubbed _substitutions_. The set of
all substitutions is denoted by $\mathsf{End}(\mathbf{L}_{\Sigma}(P))$. Given
$h,h^{\prime}\in\mathsf{Hom}(\mathbf{L}_{\Sigma}(P),\mathbf{A})$, we shall say
that _$h^{\prime}$ agrees with $h$ on $\Phi\subseteq L_{\Sigma}(P)$_ provided
that $h^{\prime}(\varphi)=h(\varphi)$ for all $\varphi\in\Phi$. In case
$p_{1},\ldots,p_{k}$ are the only propositional variables ocurring in
$\varphi\in L_{\Sigma}(P)$, we say that $\varphi$ is _$k$ -ary_ and denote by
$\varphi^{\mathbf{A}}$ the $k$-ary multioperation on $A$ such that
$\varphi^{\mathbf{A}}(a_{1},\ldots,a_{k})\,{\coloneqq}\,\\{h(\varphi)\mid
h\in\mathsf{Hom}(\mathbf{L}_{\Sigma}(P),\mathbf{A})\text{ with
}h(p_{i})=a_{i}\text{ for each }1\leq i\leq k\\}$, for all
$a_{1},\ldots,a_{k}\in A$. Also, if $\psi_{1},\ldots,\psi_{k}\in
L_{\Sigma}(P)$, we let $\varphi(\psi_{1},\ldots,\psi_{k})$ denote the formula
$\varphi^{\mathbf{L}_{\Sigma}(P)}(\psi_{1},\ldots,\psi_{k})$. For a set
$\Theta$ of formulas $\varphi(p_{1},\ldots,p_{k})$, we let
$\Theta(\psi_{1},\ldots,\psi_{k})\,{\coloneqq}\,\\{\varphi(\psi_{1},\ldots,\psi_{k})\mid\varphi\in\Theta\\}$.

A  _$\Sigma$ -equation_ is a pair $(\varphi,\psi)$ of $\Sigma$-formulas that
we denote by $\varphi\approx\psi$, and a $\Sigma$-multialgebra $\mathbf{A}$ is
said to _satisfy_ $\varphi\approx\psi$ if $h(\varphi)=h(\psi)$ for every
$h\in\mathsf{Hom}(\mathbf{L}_{\Sigma}(P),\mathbf{A})$. For any given
collection of $\Sigma$-equations, the class of all $\Sigma$-algebras that
satisfy such equations is called a _$\Sigma$ -variety_. An equation is said to
be _valid_ in a given variety if it is satisfied by each algebra in the
variety. The variety generated by a class $\mathsf{K}$ of $\Sigma$-algebras,
denoted by $\mathbb{V}(\mathsf{K})$, is the closure of $\mathsf{K}$ under
homomorphic images, subalgebras and direct products. We denote the latter
operations, respectively, by $\mathbb{H}$, $\mathbb{S}$ and $\mathbb{P}$. We
write $\operatorname{\mathsf{Cng}}\mathbf{A}$ to refer to the collection of
all congruence relations on $\mathbf{A}$, which is known to form a complete
lattice under inclusion.

In what follows, we assume the reader is familiar with basic notations and
terminology of lattice theory (Davey and Priestley (2002)). We denote by
$\Sigma^{\mathsf{bL}}$ the signature containing but two binary connectives,
$\land$ and $\lor$, and two nullary connectives $\top$ and $\bot$, and by
$\Sigma^{\mathsf{DM}}$ the extension of the latter signature by the addition
of a unary connective ${\sim}$. Moreover, we let $\Sigma^{\mathsf{IS}}$ (resp.
$\Sigma^{\mathsf{PP}}$) be the signature obtained from $\Sigma^{\mathsf{DM}}$
by adding the unary connective $\nabla$ (resp. ${\circ}$). We provide below
the definitions and some examples of De Morgan algebras and of involutive
Stone algebras, in order to illustrate some of the notions introduced above.

######  Definition 2.1.

Given a $\Sigma^{\mathsf{DM}}$-algebra whose $\Sigma^{\mathsf{bL}}$-reduct is
a bounded distributive lattice, we say that it constitutes a _De Morgan
algebra_ if it satisfies the equations:  (DM1) ${\sim}{\sim}x\approx x$ (DM2)
${\sim}(x\land y)\approx{\sim}x\lor{\sim}y$

######  Example 1.

Let
$\mathcal{V}_{4}\,{\coloneqq}\,\\{\mathbf{t},\mathbf{b},\mathbf{n},\mathbf{f}\\}$
and let
$\mathbf{DM}_{4}\,{\coloneqq}\,\langle\mathcal{V}_{4},\cdot^{\mathbf{DM}_{4}}\rangle$
be the $\Sigma^{\mathsf{DM}}$-algebra known as the Dunn-Belnap lattice, whose
interpretations for the lattice connectives are those induced by the Hasse
diagram in Figure 1(a), and the interpretation for ${\sim}$ is such that
${\sim}^{\mathbf{DM}_{4}}\mathbf{f}\,{\coloneqq}\,\mathbf{t}$,
${\sim}^{\mathbf{DM}_{4}}\mathbf{t}\,{\coloneqq}\,\mathbf{f}$ and
${\sim}^{\mathbf{DM}_{4}}a\,{\coloneqq}\,a$, for
$a\in\\{\mathbf{n},\mathbf{b}\\}$; as expected, for the nullary connectives,
we have $\top^{\mathbf{DM}_{4}}\;\,{\coloneqq}\,\;\mathbf{t}$ and
$\bot^{\mathbf{DM}_{4}}\;\,{\coloneqq}\,\;\mathbf{f}$. In Figure 1(a), besides
depicting the lattice structure of $\mathbf{DM}_{4}$, we also show its
subalgebras $\mathbf{DM}_{3}$ and $\mathbf{DM}_{2}$, which coincide with the
three-element Kleene algebra and the two-element Boolean algebra. These three
algebras are the only subdirectly irreducible De Morgan algebras (Balbes and
Dwinger, 1975, Sec. XI.2, Thm. 6).

$\mathbf{f}$$\mathbf{b}$$\mathbf{n}$$\mathbf{t}$$\mathbf{n}$$\mathbf{f}$$\mathbf{t}$$\mathbf{f}$$\mathbf{t}$$\mathbf{DM}_{4}$$\mathbf{DM}_{3}$$\mathbf{DM}_{2}$
(a) The subdirectly irreducible De Morgan algebras.

$\mathbf{f}$$\mathbf{b}$$\mathbf{n}$$\mathbf{t}$$\hat{\mathbf{f}}$$\hat{\mathbf{t}}$$\mathbf{n}$$\mathbf{f}$$\mathbf{t}$$\hat{\mathbf{f}}$$\hat{\mathbf{t}}$$\mathbf{f}$$\mathbf{t}$$\hat{\mathbf{f}}$$\hat{\mathbf{t}}$$\hat{\mathbf{f}}$$\mathbf{n}$$\hat{\mathbf{t}}$$\mathbf{IS}_{6}$$\mathbf{IS}_{5}$$\mathbf{IS}_{4}$$\mathbf{IS}_{3}$$\hat{\mathbf{f}}$$\hat{\mathbf{t}}$$\mathbf{IS}_{2}$
(b) The subdirectly irreducible IS-algebras.

Figure 1:

######  Definition 2.2.

Given a $\Sigma^{\mathsf{IS}}$-algebra whose $\Sigma^{\mathsf{DM}}$-reduct is
a De Morgan algebra, we say that it constitutes an _involutive Stone algebra_
(_IS-algebra_) if it satisfies the equations:  (IS1) $\nabla\bot\approx\bot$
(IS2) $x\land\nabla x\approx x$ (IS3) $\nabla(x\land y)\approx\nabla
x\land\nabla y$ (IS4) ${\sim}\nabla x\land\nabla x\approx\bot$

######  Example 2.

Let
$\mathcal{V}_{6}\,{\coloneqq}\,\mathcal{V}_{4}\cup\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$
and let
$\mathbf{IS}_{6}\,{\coloneqq}\,\langle\mathcal{V}_{6},\cdot^{\mathbf{IS}_{6}}\rangle$
be the $\Sigma^{\mathsf{IS}}$-algebra whose lattice structure is depicted in
Figure 1(b) and interprets ${\sim}$ and $\nabla$ as per the following:

${\sim}^{\mathbf{IS}_{6}}a\,{\coloneqq}\,\begin{cases}{\sim}^{\mathbf{DM}_{4}}a&a\in\mathcal{V}_{4}\\\
\hat{\mathbf{f}}&a=\hat{\mathbf{t}}\\\ \hat{\mathbf{t}}&a=\hat{\mathbf{f}}\\\
\end{cases}\qquad\nabla^{\mathbf{IS}_{6}}a\,{\coloneqq}\,\begin{cases}\hat{\mathbf{t}}&a\in\mathcal{V}_{6}\setminus\\{\hat{\mathbf{f}}\\}\\\
\hat{\mathbf{f}}&a=\hat{\mathbf{f}}\\\ \end{cases}$

The subalgebras of $\mathbf{IS}_{6}$ exhibited in Figure 1(b) constitute the
only subdirectly irreducible IS-algebras (Cignoli and Sagastume (1983)).

The notion of _residuation_ in $\Sigma$-algebras will be essential for us
here, as it is tightly connected to the intuitionistic implication. Let
$\mathsf{K}$ be a class of $\Sigma$-algebras, with
$\Sigma\supseteq\Sigma^{\mathsf{bL}}$, whose $\\{\land,\top\\}$-reducts are
meet-semilattices with a greatest element assigned to $\top$. Given
$\mathbf{A}\in\mathsf{K}$, we say that $\copyright$ is the _residuum_ of
$\land$ in $\mathbf{A}$ provided that $a\,\land^{\mathbf{A}}\,b\leq c$ if, and
only if, $a\leq b\,\copyright^{\mathbf{A}}\,c$ for all $a,b,c\in A$. It is
well-known that in classical logic and in intuitionistic logic the implication
plays the role of residuum of conjunction. We will also consider the notion of
_pseudocomplement_ of $a\in A$: this will be defined as the greatest element
$\neg a\in A$ such that $a\land^{\mathbf{A}}\neg a=\bot^{\mathbf{A}}$. When
every element of $\mathbf{A}$ has a pseudocomplement (unique by definition),
$\neg^{\mathbf{A}}$ is called the _pseudocomplement operation_ of
$\mathbf{A}$.

We move now to the logical preliminaries. A _Set-Fmla logic (over $\Sigma$)_
is a consequence relation $\vdash$ on $L_{\Sigma}(P)$ and a _Set-Set logic
(over $\Sigma$)_ is a generalized consequence relation $\rhd$ on
$L_{\Sigma}(P)$ (Humberstone (2011)). The _Set-Fmla companion_ of a given Set-
Set logic $\rhd$ is the Set-Fmla logic $\vdash_{\rhd}$ such that
$\Phi\vdash_{\rhd}\psi$ if, and only if, $\Phi\rhd\\{\psi\\}$. We will write
$\Phi\;{\lhd\rhd}\;\Psi$ when $\Phi\;\rhd\;\Psi$ and $\Psi\;\rhd\;\Phi$; in
that case, we say these sets are _logically equivalent_ (these definitions
apply analogously for Set-Fmla logics). The complement of a given Set-Set
logic $\rhd$ will be denoted by $\smallblacktriangleright$.

Let $\rhd$ and $\rhd^{\prime}$ be Set-Set logics over signatures $\Sigma$ and
$\Sigma^{\prime}$, respectively, with $\Sigma\subseteq\Sigma^{\prime}$. We say
that $\rhd^{\prime}$ _expands_ $\rhd$ when $\rhd^{\prime}\supseteq\rhd$. When
$\Sigma=\Sigma^{\prime}$, we say more simply that $\rhd^{\prime}$ _extends_
$\rhd$. It is worth recalling that the collection of all extensions of a given
logic forms a complete lattice under inclusion. Moreover, we say that
$\rhd^{\prime}$ is a _conservative expansion_ of $\rhd$ when $\rhd^{\prime}$
expands $\rhd$ and, for all $\Phi,\Psi\subseteq L_{\Sigma}(P)$, we have
$\Phi\rhd^{\prime}\Psi$ if, and only if, $\Phi\rhd\Psi$. The _finitary
companion_ of a Set-Set logic $\rhd$ is the Set-Set logic
$\rhd_{\mathsf{fin}}$ such that $\Phi\rhd_{\mathsf{fin}}\Psi$ if, and only if,
there are finite $\Phi^{\prime}\subseteq\Phi$ and $\Psi^{\prime}\subseteq\Psi$
such that $\Phi^{\prime}\rhd\Psi^{\prime}$. These concepts may be adapted to
Set-Fmla logics in the obvious ways.

We call special attention to the notion of self-extensionality, as it will
play an important role in the implicative extensions we consider in this
paper:

######  Definition 2.3.

A logic $\rhd$ over the signature $\Sigma$ is called _self-extensional_ (or
_congruential_) if $\varphi_{i}\,{\lhd\rhd}\,\psi_{i}\text{ implies
}\copyright(\varphi_{1},\ldots,\varphi_{k})\,{\lhd\rhd}\,\copyright(\psi_{1},\ldots,\psi_{k})$,
for all $\copyright\in\Sigma_{k}$ and
$\varphi_{1},\ldots,\varphi_{k},\psi_{1},\ldots,\psi_{k}\in L_{\Sigma}(P)$.
For Set-Fmla logics, just replace ‘$\rhd$’ by ‘$\vdash$’.

A _partial non-deterministic $\Sigma$-matrix_ (or, more simply, _$\Sigma$
-PNmatrix_) $\mathfrak{M}$ is a structure $\langle\mathbf{A},D\rangle$ where
$\mathbf{A}$ is a $\Sigma$-multialgebra and the members of $D\subseteq A$ are
called _designated values_. We will write $\overline{D}$ to refer to
$A{\setminus{}}D$. When $\mathbf{A}$ is a $\Sigma$-algebra, $\mathfrak{M}$ is
called a _$\Sigma$ -matrix_, and coincides with the usual definition of
logical matrix in the literature. A _refinement of $\mathfrak{M}$_ is a
$\Sigma$-PNmatrix obtained from $\mathbf{A}$ by deleting values from some
entries of the interpretations of the connectives in $\mathbf{A}$ (the
resulting interpretations are also said to be _refinements_ of the ones in
$\mathbf{A}$). The mappings in
$\mathsf{Hom}(\mathbf{L}_{\Sigma}(P),\mathbf{A})$ are called _$\mathfrak{M}$
-valuations_. Every $\Sigma$-PNmatrix determines a Set-Set logic
$\rhd_{\mathfrak{M}}$ such that $\Phi\rhd{}_{\mathfrak{M}}\;\Psi$ iff
$h(\Phi)\cap\overline{D}\neq\varnothing$ or $h(\Psi)\cap D\neq\varnothing$ for
all $\mathfrak{M}$-valuations $h$, as well as a Set-Fmla logic
$\vdash_{\mathfrak{M}}$ with $\Phi\vdash_{\mathfrak{M}}\psi$ iff
$h(\Phi)\cap\overline{D}\neq\varnothing$ or $h(\Psi)\in D$ for all
$\mathfrak{M}$-valuations $h$ (notice that $\vdash_{\mathfrak{M}}$ is the Set-
Fmla companion of $\rhd_{\mathfrak{M}}$). Given a Set-Set logic $\rhd$ (resp.
a Set-Fmla logic $\vdash$), if $\rhd\;\subseteq\;\rhd_{\mathfrak{M}}$ (resp.
$\vdash\;\subseteq\;\vdash_{\mathfrak{M}}$), we shall say that $\mathfrak{M}$
_is a matrix model of_ $\rhd$ (resp. $\vdash$), and if the converse also holds
we shall say that $\mathfrak{M}$ _determines_ $\rhd$ (resp. $\vdash$). The
Set-Set (resp. Set-Fmla) logic _determined_ by a class $\mathcal{M}$ of
$\Sigma$-matrices is given by
$\bigcap\\{\rhd_{\mathfrak{M}}\mid\mathfrak{M}\in\mathcal{M}\\}$ (resp.
$\bigcap\\{\vdash_{\mathfrak{M}}\mid\mathfrak{M}\in\mathcal{M}\\}$).

######  Example 3.

The $\Sigma^{\mathsf{DM}}$-matrix
$\langle\mathbf{DM}_{4},{{\uparrow}\mathbf{b}}\rangle$ determines the logic
known as the 4-valued Dunn-Belnap logic (Belnap (1977)), or First-Degree
Entailment (FDE), which we hereby denote by $\mathcal{B}$. Extensions of
$\mathcal{B}$ are known as _super-Belnap logics_ (Rivieccio (2012)).

######  Example 4.

Classical Logic, henceforth denoted by $\mathcal{CL}$, is determined by the
$\Sigma^{\mathsf{DM}}$-matrix $\langle\mathbf{DM}_{2},\\{\mathbf{t}\\}\rangle$
(see Figure 1(a)).

Given a $\Sigma$-matrix $\mathfrak{M}=\langle\mathbf{A},D\rangle$, a
congruence $\theta\in\operatorname{\mathsf{Cng}}\mathbf{A}$ is said to be
_compatible with_ $\mathfrak{M}$ when $b\in D$ whenever both $a\in D$ and
$a\theta b$, for all $a,b\in A$. We denote by $\Omega^{\mathfrak{M}}$ the
_Leibniz congruence_ associated to $\mathfrak{M}$, namely the greatest
congruence of $\mathbf{A}$ compatible with $\mathfrak{M}$. The matrix
${\mathfrak{M}}^{\ast}=\langle\mathbf{A}/\Omega^{\mathfrak{M}},D/\Omega^{\mathfrak{M}}\rangle$
is the _reduced version_ of $\mathfrak{M}$. It is well known that
$\rhd_{\mathfrak{M}}=\rhd_{{\mathfrak{M}}^{\ast}}$ (and thus
$\vdash_{\mathfrak{M}}\;=\;\vdash_{{\mathfrak{M}}^{\ast}}$) and, since every
logic is determined by a class of matrix models, we have that every logic
coincides with the logic determined by its reduced matrix models. As a
shortcut, we call a matrix _reduced_ when it coincides with its own reduced
version (or, equivalently, when its Leibniz congruence is the identity
relation on $A$).

When a $\Sigma$-algebra $\mathbf{A}$ has a lattice structure with underlying
order $\leq$, for any $a\in A$ we write ${{\uparrow}a}$ to refer to the set
$\\{b\in A\mid a\leq b\\}$. For instance, over $\mathbf{IS_{6}}{}$ we may
consider the set
${{\uparrow}\mathbf{b}}=\\{\mathbf{b},\mathbf{t},\hat{\mathbf{t}}\\}$ (see
Figure 1(b)). A _lattice filter_ of a meet-semilattice $\mathbf{A}$ with a top
element $\top^{\mathbf{A}}$ is a subset $D\subseteq A$ with
$\top^{\mathbf{A}}\in D$ and closed under $\land^{\mathbf{A}}$; moreover, $D$
is a _proper_ lattice filter of $\mathbf{A}$ when $D\neq A$. A  _principal
filter_ of $\mathbf{A}$ is a lattice filter of the form ${\uparrow}a$, for
some $a\in A$. Note that, if $\mathbf{A}$ is finite, every lattice filter is
principal. If $\mathbf{A}$ also has a join-semilattice structure, a _prime
filter_ of $\mathbf{A}$ is a proper lattice filter $D$ of $\mathbf{A}$ such
that $a\lor b\in D$ iff $a\in D$ or $b\in D$, for all $a,b\in A$.

###  2.2 Logics associated to classes of (ordered) algebras

Throughout this section, consider a propositional signature
$\Sigma\supseteq\Sigma^{\mathsf{bL}}$. In addition, for a set of
$\Sigma$-formulas $\Phi\,{\coloneqq}\,\\{\varphi_{1},\ldots,\varphi_{n}\\}$,
let $\bigwedge\Phi\,{\coloneqq}\,\varphi_{1}\land\ldots\land\varphi_{n}$ and
$\bigvee\Phi\,{\coloneqq}\,\varphi_{1}\lor\ldots\lor\varphi_{n}$, while, by
convention, let $\bigwedge\varnothing\,{\coloneqq}\,\top$ and
$\bigvee\varnothing\,{\coloneqq}\,\bot$. Moreover, let the _inequality_
$\varphi\leq\psi$ abbreviate the equation $\varphi\approx\varphi\land\psi$.

######  Definition 2.4.

Let $\mathsf{K}$ be a class of $\Sigma$-algebras such that each
$\mathbf{A}\in\mathsf{K}$ has a bounded distributive lattice reduct with
greatest element $\top^{\mathbf{A}}$ and a least element $\bot^{\mathbf{A}}$.
The _order-preserving logic associated to $\mathsf{K}$_, denoted by
$\rhd_{\mathsf{K}}^{\leq}$, is such that
$\Phi\,\rhd_{\mathsf{K}}^{\leq}\,\Psi$ if, and only if, there are finite
$\Phi^{\prime}\subseteq\Phi$ and $\Psi^{\prime}\subseteq\Psi$ such that
$\bigwedge\Phi^{\prime}\leq\bigvee\Psi^{\prime}$ is valid in $\mathsf{K}$.

For this logic, the following characterization in terms of prime filters
applies:

######  Proposition 2.5.

$\rhd_{\mathsf{K}}^{\leq}$ is the finitary companion of the logic determined
by
$\mathcal{M^{{{\uparrow}\lor}}}\,{\coloneqq}\,\\{\langle\mathbf{A},D\rangle\mid\mathbf{A}\in\mathsf{K}\text{
and }D\text{ is a prime filter of $\mathbf{A}$}\\}$.

###### Proof.

From the left to the right, assume that $\Phi\rhd_{\mathsf{K}}^{\leq}\Psi$.
Then (a): the above condition holds for finite $\Phi^{\prime}\subseteq\Phi$
and $\Psi^{\prime}\subseteq\Psi$. Let
$\langle\mathbf{A},D\rangle\in\mathcal{M^{{{\uparrow}\lor}}}$ and
$v\in\mathsf{Hom}(\mathbf{L}_{\Sigma}(P),\mathbf{A})$ be a valuation. Assume
that $v[\Phi^{\prime}]\subseteq D$. Thus $v(\bigwedge\Phi^{\prime})\in D$, as
$D$ is a lattice filter. By (a), we know that $v(\bigwedge\Phi^{\prime})\leq
v(\bigvee\Psi^{\prime})$, so $v(\bigvee\Psi^{\prime})\in D$. Since $D$ is
prime, we must have $v(\psi)\in D$ for some $\psi\in\Psi^{\prime}$ and we are
done.

From the right to the left, assume that (b):
$\Phi\rhd^{\mathsf{f}}_{\mathcal{M}^{{{\uparrow}\lor}}}\Psi$. This consequence
relation is finitary, so
$\Phi^{\prime}\rhd_{\mathcal{M^{{{\uparrow}\lor}}}}\Psi^{\prime}$ for finite
$\Phi^{\prime}\subseteq\Phi$ and $\Psi^{\prime}\subseteq\Psi$. Let
$\mathbf{A}\in\mathsf{K}$ and
$v\in\mathsf{Hom}(\mathbf{L}_{\Sigma}(P),\mathbf{A})$. Let
$a\,{\coloneqq}\,v(\bigwedge\Phi^{\prime})$ (note that $a=\top^{\mathbf{A}}$
if $\Phi^{\prime}=\varnothing$). If $a=\bot^{\mathbf{A}}$, the result is
straightforward. Otherwise, ${{\uparrow}a}$ is a proper filter. Suppose, by
reductio, that $a\not\leq v(\bigvee\Psi^{\prime})$, that is,
$v(\bigvee\Psi^{\prime})\not\in{{\uparrow}a}$. Since $\mathbf{A}$ is
distributive, consider, by the Prime Filter Theorem, the extension of
${{\uparrow}a}$ to a prime filter $D\supseteq{{\uparrow}a}$ such that
$v(\bigvee\Psi^{\prime})\not\in D$. Since $a\leq v(\varphi)$ for each
$\varphi\in\Phi^{\prime}$, we have $v(\varphi)\in{{\uparrow}a}\subseteq D$,
for all $\varphi\in\Phi^{\prime}$ and, by (b), we have $v(\psi)\in D$ for some
$\psi\in\Psi^{\prime}$. Since $v(\psi)\leq v(\bigvee\Psi^{\prime})$, we must
have $v(\bigvee\Psi^{\prime})\in D$. As this leads to a contradiction, we
conclude that $a\leq v(\bigvee\Psi^{\prime})$, as desired.∎

For a variety generated by a single finite distributive lattice, we have this
simpler characterization in terms of a finite family of finite matrices:

######  Proposition 2.6.

Let $\mathsf{K}=\mathbb{V}(\\{\mathbf{B}\\})$, for $\mathbf{B}$ a finite
distributive lattice. Then $\rhd_{\mathsf{K}}^{\leq}$ is determined by
$\mathcal{M}^{{{\uparrow}\lor}}_{\mathsf{fin}}\,{\coloneqq}\,\\{\langle\mathbf{B},D\rangle\mid
D\text{ is a prime filter of $\mathbf{B}$}\\}$.

###### Proof.

As
$\mathcal{M}^{{{\uparrow}}\lor}_{\mathsf{fin}}\subseteq\mathcal{M}^{{{\uparrow}}\lor}$,
we have
$\rhd_{\mathsf{K}}^{\leq}\subseteq\rhd_{\mathcal{M}^{{{\uparrow}}\lor}_{\mathsf{fin}}}$.
Conversely, suppose that (b):
$\Phi\;\,\smallblacktriangleright_{\mathsf{K}}^{\leq}\;\Psi$. Consider finite
$\Phi^{\prime}\subseteq\Phi$ and $\Psi^{\prime}\subseteq\Psi$. We want to show
that
$\Phi^{\prime}\,\smallblacktriangleright_{\mathcal{M}^{{{\uparrow}}\lor}_{\mathsf{fin}}}\Psi^{\prime}$.
By (b), we know that $\bigwedge\Phi^{\prime}\leq\bigvee\Psi^{\prime}$ fails in
$\mathsf{K}$, thus it fails in $\mathbf{B}$, say under a valuation $v$. Let
$b\,{\coloneqq}\,v(\bigwedge\Phi^{\prime})$. So, $b\not\leq
v(\bigvee\Psi^{\prime})$. Note that ${{\uparrow}b}$ must be proper. As
$v(\bigvee\Psi^{\prime})\not\in{{\uparrow}b}$, consider the extension of
${{\uparrow}b}$ to a prime filter $D$, by the Prime Filter Theorem, such that
$v(\bigvee\Psi^{\prime})\not\in D$. Since $\mathbf{B}$ is finite, we have that
$D$ is principal. Clearly, we must have $v(\psi)\not\in D$ for every
$\psi\in\Psi^{\prime}$, as $v(\psi)\leq v(\bigvee\Psi^{\prime})$ and $D$ is
upwards closed, and $\varphi\in D$ for every $\Phi^{\prime}$. Therefore,
$\Phi^{\prime}\,\smallblacktriangleright_{\mathcal{M}^{{{\uparrow}}\lor}_{\mathsf{fin}}}\Psi^{\prime}$,
as desired. ∎

######  Definition 2.7.

Let $\mathsf{K}$ be a class of $\Sigma$-algebras as in Definition 2.4. The
Set-Fmla _order-preserving logic induced by $\mathsf{K}$_, which we denote by
$\vdash_{\mathsf{K}}^{\leq}$, is such that
$\Phi\vdash_{\mathsf{K}}^{\leq}\psi$ if, and only if, there are
$\varphi_{1},\ldots,\varphi_{n}\subseteq\Phi$ ($n\geq 1$) for which
$\bigwedge_{i}\varphi_{i}\leq\psi$ is valid in $\mathsf{K}$.

Note that $\vdash_{\mathsf{K}}^{\leq}$ is the Set-Fmla companion of
$\rhd_{\mathsf{K}}^{\leq}$.

The above logics are particularly interesting for us in view of the following:

######  Proposition 2.8.

$\rhd_{\mathsf{K}}^{\leq}$ and $\vdash_{\mathsf{K}}^{\leq}$ are self-
extensional.

###### Proof.

Directly from Jansana (2006, Sec. 3) and from the fact that
$\vdash_{\mathsf{K}}^{\leq}$ is the Set-Fmla companion of
$\rhd_{\mathsf{K}}^{\leq}$. ∎

We close by defining the $\top$-assertional logics (also known as
1-assertional logics) associated to a class of bounded lattices.

######  Definition 2.9.

Let $\mathsf{K}$ be a class of algebras with a bounded lattice reduct. The
_$\top$ -assertional logics_ $\rhd^{\top}_{\mathsf{K}}$ and
$\vdash^{\top}_{\mathsf{K}}$ correspond respectively to the Set-Set and Set-
Fmla logics determined by the class of matrices
$\\{\langle\mathbf{A},\\{\top^{\mathbf{A}}\\}\rangle\mid\mathbf{A}\in\mathsf{K}\\}$.

Notice that $\vdash^{\top}_{\mathsf{K}}$ is the Set-Fmla companion of
$\rhd^{\top}_{\mathsf{K}}$.

###  2.3 Hilbert-style axiomatizations

Based on Shoesmith and Smiley (1978) and Caleiro and Marcelino (2019), we
define a _symmetrical_ (_Hilbert-style_) _calculus_ $\mathsf{R}$ (or _Set-Set
calculus_, for short) as a collection of pairs
$(\Phi,\Psi)\in\wp{L_{\Sigma}(P)}\times\wp{L_{\Sigma}(P)}$, denoted by
$\frac{\Phi}{\Psi}\,$ and called (_symmetrical_ or Set-Set) _inference rules_
, where $\Phi$ is the _antecedent_ and $\Psi$ is the _succedent_ of the said
rule. We will adopt the convention of omitting curly braces when writing sets
of formulas and leaving a blank space instead of writing $\varnothing$ when
presenting inference rules and statements involving (generalized) consequence
relations. We proceed to define what constitutes a proof in such calculi.

A _bounded rooted tree_ $t$ is a poset
$\langle\mathsf{nds}(t),\mathsf{\leq}^{t}\rangle$ with a single minimal
element $\mathsf{rt}(t)$, the _root_ of $t$, such that, for each _node_
$n\in\mathsf{nds}(t)$, the set $\\{n^{\prime}\in\mathsf{nds}(t)\mid
n^{\prime}\mathsf{\leq}^{t}n\\}$ of _ancestors_ of $n$ (or the _branch_ up to
$n$) is well-ordered under $\mathsf{\leq}^{t}$, and every branch of $t$ has a
maximal element (a _leaf_ of $t$). We may assign a label
$l^{t}(n)\in\wp{L_{\Sigma}(P)}\cup\\{\ast\\}$ to each node $n$ of $t$, in
which case $t$ is said to be _labelled_. Given $\Psi\subseteq L_{\Sigma}(P)$,
a leaf $n$ is _$\Psi$ -closed_ in $t$ when $l^{t}(n)\;=\;\ast$ or
$l^{t}(n)\cap\Psi\neq\varnothing$. The tree $t$ itself is _$\Psi$ -closed_
when all of its leaves are $\Psi$-closed. The immediate successors of a node
$n$ with respect to $\mathsf{\leq}^{t}$ are called the _children_ of $n$ in
$t$.

Let $\mathsf{R}$ be a symmetrical calculus. An _$\mathsf{R}$ -derivation_ is a
labelled bounded rooted tree such that for every non-leaf node $n$ of $t$
there exists a rule of inference
$\mathsf{r}=\frac{\Pi}{\Theta}\,\in\mathsf{R}$ and a substitution $\sigma$
such that $\sigma(\Pi)\subseteq l^{t}(n)$, and the set of children of $n$ is
either (i) $\\{n^{\varphi}\mid\varphi\in\sigma(\Theta)\\}$, in case
$\Theta\neq\varnothing$, where $n^{\varphi}$ is a node labelled with
$l^{t}(n)\cup\\{\varphi\\}$, or (ii) a singleton $\\{n^{\ast}\\}$ with
$l^{t}(n)\;=\;\ast$, in case $\Theta\;=\;\varnothing$. We say that
$\Phi\;\rhd_{\mathsf{R}}\;\Psi$ whenever there is a $\Psi$-closed derivation
$t$ such that $\Phi\;\supseteq\;\mathsf{rt}(t)$; such a tree consists in a
_proof_ that $\Psi$ follows from $\Phi$ in $\mathsf{R}$. As a matter of
simplification when drawing such trees, we usually avoid copying the formulas
inherited from the parent nodes (see Example 5 below). The relation
$\rhd_{\mathsf{R}}$ so defined is a Set-Set logic and, when
$\rhd_{\mathsf{R}}=\rhd_{\mathfrak{M}}$, we say that $\mathsf{R}$
_axiomatizes_ $\rhd_{\mathfrak{M}}$. A rule $\frac{\Phi}{\Psi}\,$ is _sound_
in $\mathfrak{M}$ when $\Phi\;\rhd_{\mathfrak{M}}\;\Psi$. It should be pointed
out that this deductive formalism generalises the conventional (Set-Fmla)
Hilbert-style calculi: the latter corresponds to symmetrical calculi whose
rules have, each, a finite antecedent and a singleton as succedent.

Given $\Lambda\subseteq L_{\Sigma}(P)$, we write
$\Phi\rhd_{\mathsf{R}}^{\Lambda}\Psi$ whenever there is a proof of $\Psi$ from
$\Phi$ using only formulas in $\Lambda$. Given $\Theta,\Xi\subseteq
L_{\Sigma}(P)$, we define the set $\Upsilon^{\Xi}$ of _$\Xi$ -generalized
subformulas of $\Theta$_ as the set
$\mathsf{sub}(\Theta)\cup\\{\sigma(\varphi)\mid\varphi\in\Xi\mbox{ and
}\sigma:P\to\mathsf{sub}(\Theta)\\}$. We say that $\mathsf{R}$ is _$\Xi$
-analytic_ when, for all $\Phi,\Psi\subseteq L_{\Sigma}(P)$, we always have
$\Phi\rhd_{\mathsf{R}}^{\Upsilon^{\Xi}}\Psi$ whenever we have
$\Phi\;\rhd_{\mathsf{R}}\;\Psi$; intuitively, it means that proofs in
$\mathsf{R}$ that $\Psi$ follows from $\Phi$, whenever they exist, do not need
to use more material than subformulas of $\Phi\cup\Psi$ or substitution
instances of the formulas in $\Xi$ built from those same subformulas.

A general method is introduced in Caleiro and Marcelino (2019); Marcelino and
Caleiro (2021) for obtaining analytic calculi (in the sense of analyticity
introduced in the previous paragraph) for logics given by a $\Sigma$-PNmatrix
$\langle\mathbf{A},D\rangle$ whenever a certain expressiveness requirement
(called ‘monadicity’ in Shoesmith and Smiley (1978)) is met: for every $a,b\in
A$, there is a single-variable formula $\mathrm{S}$ such that
$\mathrm{S}^{\mathbf{A}}(a)\in D$ and $\mathrm{S}^{\mathbf{A}}(b)\not\in D$ or
vice-versa. We call such formula a _separator (for $a$ and $b$)_.

The following example illustrates a symmetrical calculus for $\mathcal{B}$
generated by this method, as well as some proofs in this calculus.

######  Example 5.

The matrix $\langle\mathbf{DM}_{4},{\uparrow}\mathbf{b}\rangle$ fulfills the
above expressiveness requirement, with the following set of separators:
$\mathcal{S}\,{\coloneqq}\,\\{p,{\sim}p\\}$. We may therefore apply the method
introduced in Marcelino and Caleiro (2021) to obtain for $\mathcal{B}$ the
following $\mathcal{S}$-analytic axiomatization we call
$\mathsf{R}_{\mathcal{B}}$:

$\frac{}{\top}\,\mathsf{r}_{1}\quad\frac{{\sim}\top}{}\,\mathsf{r}_{2}\quad\frac{}{{\sim}\bot}\,\mathsf{r}_{3}\quad\frac{\bot}{}\,\mathsf{r}_{4}\quad\frac{p}{{\sim}{\sim}p}\,\mathsf{r}_{5}\quad\frac{{\sim}{\sim}p}{p}\,\mathsf{r}_{6}$
$\frac{p\land q}{p}\,\mathsf{r}_{7}\quad\frac{p\land
q}{q}\,\mathsf{r}_{8}\quad\frac{p,q}{p\land
q}\,\mathsf{r}_{9}\quad\frac{{\sim}p}{{\sim}(p\land
q)}\,\mathsf{r}_{10}\quad\frac{{\sim}q}{{\sim}(p\land
q)}\,\mathsf{r}_{11}\quad\frac{{\sim}(p\land
q)}{{\sim}p,{\sim}q}\,\mathsf{r}_{12}$ $\frac{p}{p\lor
q}\,\mathsf{r}_{13}\quad\frac{q}{p\lor q}\,\mathsf{r}_{14}\quad\frac{p\lor
q}{p,q}\,\mathsf{r}_{15}\quad\frac{{\sim}p,{\sim}q}{{\sim}(p\lor
q)}\,\mathsf{r}_{16}\quad\frac{{\sim}(p\lor
q)}{{\sim}p}\,\mathsf{r}_{17}\quad\frac{{\sim}(p\lor
q)}{{\sim}q}\,\mathsf{r}_{18}$

Figure 2 illustrates some proofs in $\mathsf{R}_{\mathcal{B}}$.

${\sim}(p\land
q)$${\sim}p$${\sim}q$${\sim}p\lor{\sim}q$${\sim}p\lor{\sim}q$$\mathsf{r}_{12}$$\mathsf{r}_{13}$$\mathsf{r}_{14}$${\sim}p\lor{\sim}q$${\sim}p$${\sim}q$${\sim}(p\land
q)$${\sim}(p\land
q)$$\mathsf{r}_{15}$$\mathsf{r}_{10}$$\mathsf{r}_{11}$$p\lor\bot$$p$$\bot$*$\mathsf{r}_{15}$$\mathsf{r}_{4}$$p\lor\bot$$p,q$$\mathsf{r}_{13}$

Figure 2: Proofs in $\mathsf{R}_{\mathcal{B}}$ witnessing that ${\sim}(p\land
q)\;{\lhd\rhd}_{\mathcal{B}}\;{\sim}p\lor{\sim}q$ and
$p\lor\bot\;{\lhd\rhd}_{\mathcal{B}}\;p,q$.

###  2.4 Implication connectives and criteria for implicative expansions

In the present study, we will follow some very specific research paths with
the goal of adding an implication to given logics; we will refer to the
resulting logics as _implicative expansions_. First of all, it is important to
define precisely what we mean by an implication connective on Set-Set and Set-
Fmla logics. Throughout this subsection, let $\Sigma$ be an arbitrary
signature with a binary connective $\lor$ and denote by $\Sigma_{\Rightarrow}$
the signature resulting from adding to $\Sigma$ the binary connective
$\Rightarrow$.

######  Definition 2.10.

The connective $\Rightarrow$ is an _implication in a Set-Set logic $\rhd{}$
over $\Sigma_{\Rightarrow}$ _ provided, for all
$\Phi,\Psi,\\{\varphi,\psi\\}\subseteq L_{\Sigma}(P)$, with $\Psi$ finite,

$\Phi,\varphi\rhd\psi,\Psi\text{ if, and only if,
}\Phi\rhd\varphi\Rightarrow\bigvee\\{\psi\\}\cup\Psi.$

Note that the above definition reduces in Set-Fmla to the _deduction-
detachment theorem_ (DDT) that holds, for example, in intuitionistic and
classical logics, and this is indeed what we will take to be an implication in
Set-Fmla, in this paper. What we did above was a suitable generalization of
the DDT for Set-Set logics, using it to abstractly characterize what we expect
of an implication connective (namely, the internalization of the consequence
relation).

Based on the behaviour of implication in classical logic, we also consider the
following stronger notion of implication:

######  Definition 2.11.

The connective $\Rightarrow$ is a _classic-like implication in a Set-Set logic
$\rhd{}$ over $\Sigma_{\Rightarrow}$_ provided, for all
$\Phi,\Psi,\\{\varphi,\psi\\}\subseteq L_{\Sigma}(P)$,

$\Phi,\varphi\rhd\psi,\Psi\text{ if, and only if,
}\Phi\rhd\varphi\Rightarrow\psi,\Psi.$

It should be clear enough that, for logics with a well-behaved disjunction,
classic-like implications are implications in the sense of Definition 2.10.

In this paper, we shall require two minimal criteria on implicative
extensions:

$(\mathsf{I}1)$

The connective being added must qualify as an implication (Definition 2.10);

$(\mathsf{I}2)$

The expansion must be conservative.

We will prove below some facts regarding the connections among the above
notions of implication, residuation and characterizability via a single
PNmatrix.

######  Proposition 2.12.

Let $\Rightarrow^{\mathbf{A}}$ be the residuum of $\land^{\mathbf{A}}$ in each
$\mathbf{A}\in\mathsf{K}$, where $\mathsf{K}$ is a class of
$\Sigma_{\Rightarrow}$-algebras, with
$\Sigma_{\Rightarrow}\supseteq\Sigma^{\mathsf{bL}}$, whose
$\\{\land,\top\\}$-reducts are $\land$-semilattices with a greatest element
assigned to $\top$. Then $\Rightarrow$ is an implication in
$\rhd_{\mathsf{K}}^{\leq}$ (Definition 2.4).

###### Proof.

Let $\Phi,\Psi,\\{\varphi\\}\subseteq L_{\Sigma}(P)$ with
$\Psi\neq\varnothing$ finite. From the left to the right, suppose that
$\Phi,\varphi\rhd_{\mathsf{K}}^{\leq}\Psi$. Then
$\Phi^{\prime}\rhd_{\mathsf{K}}^{\leq}\Psi^{\prime}$, for finite
$\Phi^{\prime}\subseteq\Phi\cup\\{\varphi\\}$ and
$\Psi^{\prime}\subseteq\Psi$, and thus (a):
$\Phi^{\prime\prime},\varphi\rhd_{\mathsf{K}}^{\leq}\Psi^{\prime}$, for
$\Phi^{\prime}\cup\\{\varphi\\}=\Phi^{\prime\prime}\cup\\{\varphi\\}$ and
$\varphi\not\in\Phi^{\prime\prime}$. Let $\mathbf{A}\in\mathsf{K}$. By (a), we
have that $\bigwedge\Phi^{\prime\prime}\land\varphi\leq\bigvee\Psi^{\prime}$
is valid in $\mathbf{A}$, thus
$\bigwedge\Phi^{\prime\prime}\land\varphi\leq\bigvee\Psi$ is valid in
$\mathbf{A}$; hence, by residuation,
$\bigwedge\Phi^{\prime\prime}\leq\varphi\Rightarrow\bigvee\Psi$ is valid in
$\mathbf{A}$, thus
$\Phi\rhd_{\mathsf{K}}^{\leq}\varphi\Rightarrow\bigvee\Psi$. From the right to
the left, suppose that
$\Phi\rhd_{\mathsf{K}}^{\leq}\varphi\Rightarrow\bigvee\Psi$. Then, without
loss of generality, we have that
$\Phi^{\prime}\rhd_{\mathsf{K}}^{\leq}\varphi\Rightarrow\bigvee\Psi$, for some
finite $\Phi^{\prime}\subseteq\Phi$. Let $\mathbf{A}\in\mathsf{K}$. We have
that $\bigwedge\Phi^{\prime}\leq\varphi\Rightarrow(\bigvee\Psi)$ is valid in
$\mathbf{A}$. By residuation, we have
$\bigwedge\Phi^{\prime}\land\varphi\leq\bigvee\Psi$ also valid in
$\mathbf{A}$, from which we easily obtain that
$\Phi,\varphi\rhd_{\mathsf{K}}^{\leq}\Psi$. ∎

Observe that the above result extends to $\vdash_{\mathsf{K}}^{\leq}$ (recall
Definition 2.7) since it is the Set-Fmla companion of
$\rhd_{\mathsf{K}}^{\leq}$. This also looks like the right moment to introduce
intuitionistic-like implications:

######  Definition 2.13.

A _Heyting implication_ in an algebra $\mathbf{A}\in\mathsf{K}$, with
$\mathsf{K}$ as described in Proposition 2.12, is an implication that
corresponds to the residuum of $\land^{\mathbf{A}}$.

Inspired by Avron (2020), we also consider the following additional criteria
to guide our investigations:

$(\mathsf{A}1)$

The expanded logic is determined by the single PNmatrix
$\langle\mathbf{A},D\rangle$, and, for all $a,b\in A$, we have
$a\Rightarrow^{\mathbf{A}}b\subseteq D$ if, and only if, either $a\not\in D$
or $b\in D$.

$(\mathsf{A}2)$

The expanded logic is self-extensional (Definition 2.3).

Note that, for Set-Set logics, the criterion $(\mathsf{A}1)$ is strong to the
point of forcing the referred implication to be classic-like:

######  Proposition 2.14.

Let $\mathfrak{M}\,{\coloneqq}\,\langle\mathbf{A},D\rangle$ be a
$\Sigma_{\Rightarrow}$-PNmatrix. Then $\Rightarrow$ is a classic-like
implication in $\rhd_{\mathfrak{M}}$ if, and only if, $\mathfrak{M}$ satisfies
$(\mathsf{A}1)$.

###### Proof.

We have that
$\Phi,\varphi\,\,\smallblacktriangleright_{\mathfrak{M}}\,\psi,\Psi$ if, and
only if, $v[\Phi\cup\\{\varphi\\}\\}]\subseteq D$ and
$v[\\{\psi\\}\cup\Psi\\}]\subseteq\overline{D}$ for some valuation $v$ if, and
only if, $v[\Phi]\subseteq D$ and $v(\psi)\in\overline{D}$ and
$v(\varphi\Rightarrow\psi)\in\overline{D}$ for some valuation $v$ if, and only
if,
$\Phi\,\,\smallblacktriangleright_{\mathfrak{M}}\,\varphi\Rightarrow\psi,\Psi$.
∎

##  3 Perfect Paradefinite Algebras and their logics

In this section, we present the main definitions concerning perfect
paradefinite algebras and the logics associated to them. Most of the material
come from Gomes et al. (2022), where these objects were first introduced and
investigated.

######  Definition 3.1.

Given a $\Sigma^{\mathsf{PP}}$-algebra whose $\Sigma^{\mathsf{DM}}$-reduct is
a De Morgan algebra, we say that it constitutes a _perfect paradefinite
algebra_ (_PP-algebra_) if it satisfies the equations:

(PP1) ${\circ}{\circ}x\approx\top$ |  (PP2) $\circ x\approx\circ{\sim}x$ |  (PP3) ${\circ}\top\approx\top$ |  (PP4) $x\land{\sim}x\land{\circ}x\approx\bot$
---|---|---|---

(PP5) $\circ(x\land y)\approx(\circ x\lor\circ y)\land(\circ
x\lor{\sim}y)\land(\circ y\lor{\sim}x)$
---

######  Example 6.

An example of PP-algebra is
$\mathbf{PP}_{6}\,{\coloneqq}\,\langle\mathcal{V}_{6},\cdot^{\mathbf{PP}_{6}}\rangle$,
the $\Sigma^{\mathsf{PP}}$-algebra defined as $\mathbf{IS}_{6}$ in Example 2,
differing only in that, instead of containing an interpretation for $\nabla$,
it contains the following interpretation for ${\circ}$:

${\circ}^{\mathbf{PP}_{6}}a\,{\coloneqq}\,\begin{cases}\hat{\mathbf{f}}&a\in\mathcal{V}_{6}{\setminus}\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}\\\
\hat{\mathbf{t}}&a\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}\\\ \end{cases}$

Other examples are the algebras $\mathbf{PP}_{i}$, the subalgebras of
$\mathbf{PP}_{6}$ having, respectively, the same lattice structures of the
algebras $\mathbf{IS}_{i}$, for $2\leq i\leq 5$, exhibited in Figure 1(b).

We denote by $\mathbb{PP}$ the variety of PP-algebras. This variety is term-
equivalent to the variety of involutive Stone algebras (Gomes et al., 2022,
Thm. 3.6) — in particular, $\nabla x\,{\coloneqq}\,x\lor{\sim}{\circ}x$. Also,
it holds that $\mathbb{PP}=\mathbb{V}(\\{\mathbf{PP_{6}}\\})$ (Gomes et al.,
2022, Prop. 3.8). As it occurs with IS-algebras, we may define, in the
language of PP-algebras, a pseudo-complement satisfying the Stone equation; to
that effect, it suffices to set $\neg
x\;\,{\coloneqq}\,\;{\sim}x\land{\circ}x$ (alternatively, one might now set
$\neg x\;\,{\coloneqq}\,\;{\sim}\nabla x$, as usual).

We shall denote by $\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}$ and
$\mathcal{PP}_{\\!\leq}$, respectively, the Set-Set and Set-Fmla order-
preserving logics induced by $\mathbb{PP}$ (cf. Subsection 2.2). In addition,
we shall denote by $\mathcal{PP}_{\top}^{\mathsf{\rhd}}{}$ and
$\mathcal{PP}_{\top}{}$, respectively, the Set-Set and Set-Fmla
$\top$-assertional logics induced by $\mathbb{PP}$. We know that
$\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}{}\;=\;\rhd_{\langle\mathbf{PP_{6}},{{\uparrow}\mathbf{b}}\rangle}$
and thus
$\mathcal{PP}_{\\!\leq}{}\;=\;\vdash_{\langle\mathbf{PP_{6}},{{\uparrow}\mathbf{b}}\rangle}$
(Gomes et al., 2022, Theorem 3.11).

Taking a proof-theoretical perspective, from (Gomes et al., 2022, Cor. 4.3) we
know that $\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}{}$ is axiomatized by a
$\\{p,{\sim}p,{\circ}p\\}$-analytic Set-Set calculus, which we now recall:

######  Definition 3.2.

Let $\mathsf{R}_{\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}}$ be the following
Set-Set calculus:

$\displaystyle\frac{}{\top}\,\mathsf{r}_{1}$
$\displaystyle\frac{{\sim}\top}{}\,\mathsf{r}_{2}$
$\displaystyle\frac{}{{\sim}\bot}\,\mathsf{r}_{3}$
$\displaystyle\frac{\bot}{}\,\mathsf{r}_{4}$
$\displaystyle\frac{p}{{\sim}{\sim}p}\,\mathsf{r}_{5}$
$\displaystyle\frac{{\sim}{\sim}p}{p}\,\mathsf{r}_{6}$
$\displaystyle\frac{p\land q}{p}\,\mathsf{r}_{7}$ $\displaystyle\frac{p\land
q}{q}\,\mathsf{r}_{8}$ $\displaystyle\frac{p,q}{p\land q}\,\mathsf{r}_{9}$
$\displaystyle\frac{{\sim}p}{{\sim}(p\land q)}\,\mathsf{r}_{10}$
$\displaystyle\frac{{\sim}q}{{\sim}(p\land q)}\,\mathsf{r}_{11}$
$\displaystyle\frac{{\sim}(p\land q)}{{\sim}p,{\sim}q}\,\mathsf{r}_{12}$
$\displaystyle\frac{p}{p\lor q}\,\mathsf{r}_{13}$ $\displaystyle\frac{q}{p\lor
q}\,\mathsf{r}_{14}$ $\displaystyle\frac{p\lor q}{p,q}\,\mathsf{r}_{15}$
$\displaystyle\frac{{\sim}p,{\sim}q}{{\sim}(p\lor q)}\,\mathsf{r}_{16}$
$\displaystyle\frac{{\sim}(p\lor q)}{{\sim}p}\,\mathsf{r}_{17}$
$\displaystyle\frac{{\sim}(p\lor q)}{{\sim}q}\,\mathsf{r}_{18}$
$\displaystyle\frac{}{{\circ}\bot}\,\mathsf{r}_{19}$
$\displaystyle\frac{}{{\circ}\top}\,\mathsf{r}_{20}$
$\displaystyle\frac{}{{\circ}{\circ}p}\,\mathsf{r}_{21}$
$\displaystyle\frac{{\circ}p}{{\circ}{\sim}p}\,\mathsf{r}_{22}$
$\displaystyle\frac{{\circ}{\sim}p}{{\circ}p}\,\mathsf{r}_{23}$
$\displaystyle\frac{{\circ}p}{p,{\sim}p}\,\mathsf{r}_{24}$
$\displaystyle\frac{{\circ}p,p,{\sim}p}{}\,\mathsf{r}_{25}$
$\displaystyle\frac{{\circ}p}{{\circ}(p\land q),p}\,\mathsf{r}_{26}$
$\displaystyle\frac{{\circ}q}{{\circ}(p\land q),q}\,\mathsf{r}_{27}$
$\displaystyle\frac{{\circ}(p\land q),q}{{\circ}p}\,\mathsf{r}_{28}$
$\displaystyle\frac{{\circ}(p\land q),p}{{\circ}q}\,\mathsf{r}_{29}$
$\displaystyle\frac{{\circ}p,{\circ}q}{{\circ}(p\land q)}\,\mathsf{r}_{30}$
$\displaystyle\frac{{\circ}(p\land q)}{{\circ}p,{\circ}q}\,\mathsf{r}_{31}$
$\displaystyle\frac{{\circ}p,{\circ}q}{{\circ}(p\lor q)}\,\mathsf{r}_{32}$
$\displaystyle\frac{{\circ}(p\lor q)}{{\circ}p,{\circ}q}\,\mathsf{r}_{33}$
$\displaystyle\frac{{\circ}p,p}{{\circ}(p\lor q)}\,\mathsf{r}_{34}$
$\displaystyle\frac{{\circ}q,q}{{\circ}(p\lor q)}\,\mathsf{r}_{35}$
$\displaystyle\frac{{\circ}(p\lor q)}{{\circ}p,q}\,\mathsf{r}_{36}$
$\displaystyle\frac{{\circ}(p\lor q)}{{\circ}q,p}\,\mathsf{r}_{37}$

In the mentioned paper, the above calculus was transformed into a Set-Fmla
axiomatization for $\mathcal{PP}_{\\!\leq}$, using a technique that we shall
detail and employ in Section 6.

It is perhaps worth calling attention to the contribution played by rules
$\mathsf{r}_{24}$ and $\mathsf{r}_{25}$ in making the perfection operator,
${\circ}$, restore ‘classicality’, as described in the so-called Derivability
Adjustment Theorems (for a semantical perspective, see Marcos (2005b, Sec. 2),
and more specifically Gomes et al. (2022, Thm. 3.29)).

Finally, we have that the $\top$-assertional logics
$\mathcal{PP}_{\top}^{\mathsf{\rhd}}{}$ and $\mathcal{PP}_{\top}{}$ are
determined by a single three-valued matrix. In fact, it can be shown that such
logics are term-equivalent to the three-valued Łukasiewicz logic (in Set-Set
and Set-Fmla, respectively) — where $\nabla
x\,{\coloneqq}\,x\lor{\sim}{\circ}x$, as above.

######  Proposition 3.3 (Gomes, Greati, Marcelino, Marcos, and Rivieccio
(2022, Prop. 3.12)).

$\mathcal{PP}_{\top}^{\mathsf{\rhd}}{}\;=\;\rhd^{\top}_{\mathbb{V}(\mathbf{PP}_{3})}\;=\;\rhd_{\langle\mathbf{PP}_{3},\\{\hat{\mathbf{t}}\\}\rangle}$,
and thus
$\mathcal{PP}_{\top}{}\;=\;\vdash^{\top}_{\mathbb{V}(\mathbf{PP}_{3})}\;=\;\vdash_{\langle\mathbf{PP}_{3},\\{\hat{\mathbf{t}}\\}\rangle}$
(recall the definition of $\mathbf{PP}_{3}$ in Example 6).

We have at this point all the relevant facts about the logics of PP-algebras
we are interested in. Let us move to the main goal of the paper: adding an
implication to them.

##  4 Conservatively expanding $\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}$ and
$\mathcal{PP}_{\\!\leq}$ by adding a classic-like implication to their matrix

The first path we shall consider amounts to modifying the logical matrix of
$\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}$ , namely
$\langle\mathbf{PP_{6}},{{\uparrow}\mathbf{b}}\rangle$, by enriching its
algebra with a new multioperation $\Rightarrow_{\mathsf{A}}$, thus obtaining a
multialgebra $\mathbf{PP_{6}^{\Rightarrow_{\mathsf{A}}}}$ for which both
criteria $(\mathsf{A}1)$ and $(\mathsf{A}2)$ mentioned in Section 1 hold, that
is:

$(\mathsf{A}1)$

$a\Rightarrow_{\mathsf{A}}b\subseteq{{\uparrow}\mathbf{b}}$ if, and only if,
either $a\not\in{{\uparrow}\mathbf{b}}$ or $b\in{{\uparrow}\mathbf{b}}$.

$(\mathsf{A}2)$

The resulting logic
$\rhd_{\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{A}}}},{{\uparrow}\mathbf{b}}\rangle}$
is self-extensional.

This path soon leads to a dead end, since:

######  Theorem 4.1.

There is no multialgebra $\mathbf{PP_{6}^{\Rightarrow_{\mathsf{A}}}}$
simultaneously satisfying conditions $(\mathsf{A}1)$ and $(\mathsf{A}2)$.

###### Proof.

Let $\Rightarrow_{\mathsf{A}}$ be an implication defined in $\mathbf{PP_{6}}$
that satisfies $(\mathsf{A}1)$ and
$\mathfrak{M}^{\Rightarrow_{\mathsf{A}}}\,{\coloneqq}\,\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{A}}}},{{\uparrow}\mathbf{b}}\rangle$.
Then (a): we have
$\rhd_{\mathfrak{M}^{\Rightarrow_{\mathsf{A}}}}\,p\lor(p\Rightarrow\bot)$,
because, for every valuation $v$, either $v(p)\in{{\uparrow}\mathbf{b}}$ — in
which case we have $v(p\lor(p\Rightarrow\bot))\in v(p)\lor
v(p\Rightarrow\bot)\subseteq{{\uparrow}\mathbf{b}}$ as well — or
$v(p)\notin{{\uparrow}\mathbf{b}}$, which gives us $v(p\Rightarrow q)\in
v(p)\Rightarrow v(\bot)\subseteq{{\uparrow}\mathbf{b}}$ by $(\mathsf{A}1)$.

Note that, for a valuation $v$ such that $v(p)=\mathbf{b}$, using
$(\mathsf{A}1)$ we have
$v(p\Rightarrow\bot)\in\mathbf{b}\Rightarrow\hat{\mathbf{f}}\not\subseteq{{\uparrow}\mathbf{b}}$,
which means that $v(p\Rightarrow\bot)$ may take a value in
$\\{\mathbf{n},\mathbf{f},\hat{\mathbf{f}}\\}$. Hence, this being the case,
$v(p\lor(p\Rightarrow\bot))\in\mathbf{b}\lor
v(p\Rightarrow\bot)\in\\{\mathbf{b},\mathbf{t}\\}$, which entails
$v(\circ(p\lor(p\Rightarrow\bot)))=\hat{\mathbf{f}}$. Thus
$\,\smallblacktriangleright_{\mathfrak{M}^{\Rightarrow_{\mathsf{A}}}}\,\circ(p\lor(p\Rightarrow\bot))$.

This prevents the logic from being self-extensional. Indeed, assuming
$(\mathsf{A}2)$, from (a) we would have that $p\lor(p\Rightarrow\bot)$ and
$\top$ are logically equivalent, thus we would be able to conclude that
$\circ(p\lor(p\Rightarrow\bot))$ and $\circ\top$ are logically equivalent too.
Since $\rhd_{\mathfrak{M}^{\Rightarrow_{\mathsf{A}}}}\,\circ\top$, we would
conclude that
$\rhd_{\mathfrak{M}^{\Rightarrow_{\mathsf{A}}}}\,\circ(p\lor(p\Rightarrow\bot))$,
against what we have shown. ∎

In view of the preceding result, we proceed in this section by pursuing
$(\mathsf{A}1)$, thus necessarily admitting non-self-extensional logics. In
the next sections we will instead see some possibilities that arise when we
opt for abandoning $(\mathsf{A}1)$.

The space of binary multioperations over $\mathcal{V}_{6}$ satisfying
$(\mathsf{A}1)$ is finite but very large — to be precise, there are
$(2^{3})^{9}\cdot(2^{3})^{27}$ of them, each choice consisting in a refinement
of the multioperation $\Rightarrow_{\mathsf{full}}$ defined as:

$\Rightarrow_{\mathsf{full}}(a,b)\,{\coloneqq}\,\begin{cases}{{\uparrow}\mathbf{b}}&\text{if
$a\not\in{{\uparrow}\mathbf{b}}$ or $b\in{{\uparrow}\mathbf{b}}$ }\\\
\mathcal{V}_{6}{\setminus}{{\uparrow}\mathbf{b}}&\text{otherwise.}\end{cases}$

Denote by $\mathbf{PP_{6}}^{\\!\\!\Rightarrow_{\mathsf{full}}}$ the
multialgebra obtained from $\mathbf{PP_{6}}$ by expanding its signature with
$\Rightarrow$ and interpreting this connective as
$\Rightarrow_{\mathsf{full}}$. Let
$\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}\,{\coloneqq}\,\langle\mathbf{PP_{6}}^{\Rightarrow_{\mathsf{full}}},{{\uparrow}\mathbf{b}}\rangle$.
We will soon see that the logic induced by this matrix plays an important role
regarding the conservative expansions of
$\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}$ by a classic-like implication; but
let us first present an analytic axiomatization for it.

######  Definition 4.2.

Let $\mathsf{R}_{\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}}$ be the calculus
given by all inference rules in
$\mathsf{R}_{\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}}$ plus the following three
inference rules:

$\frac{q}{p\Rightarrow
q}\,\mathsf{r}_{1}^{\mathcal{CL}}\qquad\frac{}{p,p\Rightarrow
q}\,\mathsf{r}_{2}^{\mathcal{CL}}\qquad\frac{p,p\Rightarrow
q}{q}\,\mathsf{r}_{3}^{\mathcal{CL}}$

In a monadic PNmatrix $\mathfrak{M}\,{\coloneqq}\,\langle\mathbf{A},D\rangle$,
a set $\mathcal{S}_{a}$ of unary formulas _isolates $a\in A$_ in case, for
every $b\neq a\in A$, there is a separator in $\mathcal{S}_{a}$ for $a$ and
$b$. A _discriminator for $\mathfrak{M}$_ is a family
$\\{(\Omega_{a},\mho_{a})\\}_{a\in A}$ such that $\Omega_{a}\cup\mho_{a}$
isolates $a$ and $\mathrm{S}^{\mathbf{A}}(a)\subseteq D$ if
$\mathrm{S}\in\Omega_{a}$, and
$\mathrm{S}^{\mathbf{A}}(a)\subseteq\overline{D}$ if $\mathrm{S}\in\mho_{a}$.
Discriminators play an essential role in the axiomatization of monadic PN-
matrices, as we shall see in the next results.

######  Theorem 4.3.

$\mathsf{R}_{\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}}$ is
$\\{p,{\sim}p,{\circ}p\\}$-analytic and axiomatizes
$\rhd_{\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}}$.

###### Proof.

We consider the axiomatization method presented by Marcelino and Caleiro
(2021, Theorem 3.5 and Theorem 3.12), which can be applied because
$\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}$ is monadic, with same
discriminator as that of $\mathfrak{M}_{6}$ (see Figure 1). The method can be
seen essentially as a process of refining fully indeterministic six-valued
interpretations of the connectives (that is, interpretations where
$\mathcal{V}_{6}$ appears at every entry) by imposing soundness of some
collections of inference rules, until obtaining the desired interpretations
(in our case, the ones of $\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}$). For
the connectives $\land,\lor,{\sim}$ and ${\circ}$, the method produces the
calculus $\mathsf{R}_{\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}}$ after
simplifications (Gomes et al. (2022)). Thus, since the method is modular on
the connectives, we only need to see what happens when we run it on the new
connective $\Rightarrow_{\mathsf{full}}$ and then add the resulting rules to
$\mathsf{R}_{\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}}$. The rules that are
imposed will have the following shape:

$\frac{\Omega_{a}(p),\Omega_{b}(q),\Omega_{c}(p\Rightarrow
q)}{\mho_{a}(p),\mho_{b}(q),\mho_{c}(p\Rightarrow q)}\,$

for each $c\in\mathcal{V}_{6}{\setminus}(a\Rightarrow_{\mathsf{full}}b)$ and
each $a,b\in\mathcal{V}_{6}$, where the sets $\Omega_{d}$ and $\mho_{d}$ for
each $d\in\mathcal{V}_{6}$ are given by the following table:

$d$ | $\Omega_{d}$ | $\mho_{d}$
---|---|---
$\hat{\mathbf{f}}$ | ${\circ}p$ | $p$
$\mathbf{f}$ | ${\sim}p$ | ${\circ}p,p$
$\mathbf{n}$ | $\varnothing$ | $p,{\circ}p,{\sim}p$
$\mathbf{b}$ | $p,{\sim}p$ | ${\circ}p$
$\mathbf{t}$ | $p$ | ${\circ}p,{\sim}p$
$\hat{\mathbf{t}}$ | $p,{\circ}p$ | $\varnothing$
Table 1: Discriminator for $\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}$. They
give, for example, $\Omega_{\mathbf{b}}=\\{p,{\sim}p\\}$ and
$\mho_{\mathbf{n}}=\\{p,{\circ}p,{\sim}p\\}$.

These rules at first do not seem to relate to the three rules for
$\Rightarrow$ in $\mathsf{R}_{\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}}$.
However, we will see now that each of them is a ‘dilution’ of one of the
latter (that is, they are obtained from the latter by adding formulas on the
antecedents and succedents). Then, because these three rules for implication
are sound, it follows trivially that we can use only them and discard its
dilutions without harm for completeness and for analyticity.

First, consider the entries of $a\Rightarrow_{\mathsf{full}}b$ for
$b\in{{\uparrow}\mathbf{b}}$. The values
$c\in\mathcal{V}_{6}{\setminus}(a\Rightarrow_{\mathsf{full}}b)$ are precisely
$\mathbf{n}$, $\mathbf{f}$ and $\hat{\mathbf{f}}$. Then $q\in\Omega_{b}(q)$
and $p\Rightarrow q\in\mho_{c}(p\Rightarrow q)$, thus the above rules are all
dilutions of $\mathsf{r}_{1}^{\mathcal{CL}}$.

Second, consider the entries of $a\Rightarrow_{\mathsf{full}}b$ for
$a\not\in{{\uparrow}\mathbf{b}}$. The values
$c\in\mathcal{V}_{6}{\setminus}(a\Rightarrow_{\mathsf{full}}b)$ are precisely
$\mathbf{n}$, $\mathbf{f}$ and $\hat{\mathbf{f}}$. Then $p\in\mho_{a}(p)$ and
$p\Rightarrow q\in\mho_{c}(p\Rightarrow q)$, thus the above rules are all
dilutions of $\mathsf{r}_{2}^{\mathcal{CL}}$.

Finally, consider the entries of $a\Rightarrow_{\mathsf{full}}b$ for
$a\in{{\uparrow}\mathbf{b}}$ and $b\not\in{{\uparrow}\mathbf{b}}$. The values
$c\in\mathcal{V}_{6}{\setminus}(a\Rightarrow_{\mathsf{full}}b)$ are precisely
$\mathbf{b}$, $\mathbf{t}$ and $\hat{\mathbf{t}}$. Then $p\in\Omega_{a}(p)$,
$p\Rightarrow q\in\Omega_{c}(p\Rightarrow q)$ and $q\in\mho_{b}(q)$, thus the
above rules are all dilutions of $\mathsf{r}_{3}^{\mathcal{CL}}$. ∎

######  Remark 4.4.

The above result could have been obtained by another strategy, observing that
$\rhd_{\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}}$ is induced by the _strict
product_ (Caleiro and Marcelino, 2023, Definition 10) of $\mathfrak{M}_{6}$
and the matrix $\mathfrak{M}_{2}$ over the signature containing only
$\Rightarrow$, in which the algebra has carrier
$\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$ and interprets $\Rightarrow$ as in
classical logic ($a\Rightarrow^{\mathfrak{M}_{2}}b=\hat{\mathbf{f}}$ if, and
only if, $a=\hat{\mathbf{t}}$ and $b=\hat{\mathbf{f}}$), and the designated
set is $\\{\hat{\mathbf{t}}\\}$. By Caleiro and Marcelino (2023, Theorem 12),
this implies that $\rhd_{\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}}$ is the
_disjoint fibring_ of $\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}$ and
$\rhd_{\mathfrak{M}_{2}}$ (that is, the smallest Set-Set logic in the
signature $\Sigma_{\Rightarrow}$ extending both logics). One can then show
that, because both logics have analytic Set-Set axiomatizations, it is enough
to merge both calculi in order to axiomatize their disjoint fibring. As it is
well-known that $\rhd_{\mathfrak{M}_{2}}$ is axiomatized by the
$\\{p\\}$-analytic calculus given by the three rules for implication in
Definition 4.2, the desired result follows.

From the above, we have that
$\rhd_{\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}}$ is special in the sense of
being the smallest conservative expansion of
$\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}$ in which the added implication is
classic-like (cf. Definition 2.11):

######  Proposition 4.5.

Let $\rhd$ be a conservative expansion of
$\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}$ over
$\Sigma^{\mathsf{PP}}_{\Rightarrow}$ in which $\Rightarrow$ is a classic-like
implication. Then
$\rhd_{\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}}\subseteq\rhd$.

###### Proof.

It is easy to see that any classic-like implication must satisfy the three
rules for implication in the calculus for
$\rhd_{\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}}$, and this is all we need
for the present result. ∎

We observe that each proper refinement of $\Rightarrow_{\mathsf{full}}$
produces a proper extension of
$\rhd_{\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}}$. In fact, following again
the axiomatization method in Caleiro and Marcelino (2019), for each such
extension we can use the monadicity of
$\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}$ to obtain Set-Set rules that hold
in it but not in $\mathsf{R}_{\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}}$,
and they will be precisely the rules that need to be added to the latter to
obtain a $\\{p,{\sim}p,{\circ}p\\}$-analytic calculus for these extensions.

######  Proposition 4.6.

Let $\mathfrak{M}$ be obtained from
$\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}$ by refining
$\Rightarrow_{\mathsf{full}}$. Then
$\mathsf{R}_{\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}}$ with the following
rules provide a $\\{p,{\sim}p,{\circ}p\\}$-analytic calculus for
$\mathfrak{M}$:

$\frac{\Omega_{a}(p),\Omega_{b}(q),\Omega_{c}(p\Rightarrow
q)}{\mho_{a}(p),\mho_{b}(q),\mho_{c}(p\Rightarrow q)}\,$

for each
$c\in(a\Rightarrow_{\mathsf{full}}b){\setminus}(a\Rightarrow^{\mathfrak{M}}b)$
and each $a,b\in\mathcal{V}_{6}$.

###### Proof.

Directly from the method in Marcelino and Caleiro (2021, Theorem 3.5 and
Theorem 3.12). ∎

For an example of the latter axiomatization technique in action, if we remove
the value $\mathbf{n}$ from the entry
$\mathbf{b}\Rightarrow_{\mathsf{full}}\hat{\mathbf{f}}$, we axiomatize the
resulting logic by adding the following rule:

$\frac{p,{\sim}p,{\circ}q,{{\sim}}q,}{{\circ}p,q,p\Rightarrow
q,{\sim}(p\Rightarrow q),{\circ}(p\Rightarrow q)}\,,$

which clearly does not hold in $\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}$
under a valuation $v$ with $v(p)=\mathbf{b}$, $v(q)=\hat{\mathbf{f}}$ and
$v(p\Rightarrow q)=\mathbf{n}$, but holds in the new logic precisely because
this valuation was forbidden when we deleted $\mathbf{n}$ from that entry.

As another application of this technique, we show how to axiomatize the logic
$\mathrm{LET_{K}^{+}}$ of Coniglio and Rodrigues (2023) with a
$\\{p,{\sim}p,{\circ}p\\}$-analytic calculus, as it fits precisely in this
setting, that is, it is determined by a refinement of
$\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}$. In fact, its implication is
given by the following truth table:

$\Rightarrow^{\mathrm{LET_{K}^{+}}}$ | $\hat{\mathbf{f}}$ | $\mathbf{f}$ | $\mathbf{n}$ | $\mathbf{b}$ | $\mathbf{t}$ | $\hat{\mathbf{t}}$
---|---|---|---|---|---|---
$\hat{\mathbf{f}}$ | $\hat{\mathbf{t}}$ | $\hat{\mathbf{t}}$ | $\hat{\mathbf{t}}$ | $\hat{\mathbf{t}}$ | $\hat{\mathbf{t}}$ | $\hat{\mathbf{t}}$
$\mathbf{f}$ | $\mathbf{t}$ | $\mathbf{t}$ | $\mathbf{t}$ | $\mathbf{t}$ | $\mathbf{t}$ | $\hat{\mathbf{t}}$
$\mathbf{n}$ | $\mathbf{t}$ | $\mathbf{t}$ | $\mathbf{t}$ | $\mathbf{t}$ | $\mathbf{t}$ | $\hat{\mathbf{t}}$
$\mathbf{b}$ | $\hat{\mathbf{f}}$ | $\mathbf{f}$ | $\mathbf{n}$ | $\mathbf{b}$ | $\mathbf{t}$ | $\hat{\mathbf{t}}$
$\mathbf{t}$ | $\hat{\mathbf{f}}$ | $\mathbf{f}$ | $\mathbf{n}$ | $\mathbf{b}$ | $\mathbf{t}$ | $\hat{\mathbf{t}}$
$\hat{\mathbf{t}}$ | $\hat{\mathbf{f}}$ | $\mathbf{f}$ | $\mathbf{n}$ | $\mathbf{b}$ | $\mathbf{t}$ | $\hat{\mathbf{t}}$

Then, to obtain the desired axiomatization, it is enough to add to
$\mathsf{R}_{\mathfrak{M}^{\Rightarrow_{\mathsf{full}}}}$ the following
inference rules:

$\frac{{\sim}(p\Rightarrow q)}{p}\,\quad\frac{{\sim}(p\Rightarrow
q)}{{\sim}q}\,\quad\frac{p,{\sim}q}{{\sim}(p\Rightarrow
q)}\,\quad\frac{{\circ}(p\Rightarrow
q)}{{\circ}p,{\circ}q}\,\quad\frac{{\circ}(p\Rightarrow q)}{{\circ}p,p,q}\,$
$\frac{{\circ}(p\Rightarrow
q),p}{{\circ}q}\,\quad\frac{{\circ}p}{{\circ}(p\Rightarrow
q),p}\,\quad\frac{p,{\circ}q}{{\circ}(p\Rightarrow
q)}\,\quad\frac{{\circ}q,q}{{\circ}(p\Rightarrow q)}\,$

The attentive reader will notice that they are not quite the same rules as the
ones produced by the recipe in Proposition 4.6. In fact, they are
simplifications thereof, following the streamlining procedures described in
Marcelino and Caleiro (2021). Still, it is not hard to see that these rules
produce the desired refinements of $\Rightarrow_{\mathsf{full}}$ in a similar
way as we did in the previous example.

##  5 Logics of PP-algebras expanded with a Heyting implication

In the light of Theorem 4.1, as we proceed to expand our logic with an
implication we shall necessarily have to drop either $(\mathsf{A}1)$ or
$(\mathsf{A}2)$. In this section we explore the first option, that is, we
stick to $(\mathsf{A}2)$ while dropping $(\mathsf{A}1)$. Having fixed a
(deterministic) implication operator (say, on $\mathbf{PP_{6}}$), a
straightforward way to ensure that the resulting logic will be self-
extensional (cf. Proposition 2.8) is to consider, as in the implication-less
case, the Set-Fmla consequence relation that preserves the lattice order of
$\mathbf{PP_{6}}$ (or, to be more precise, of the resulting class of algebras
augmented with an implication). Indeed, as shown by Jansana (2006, Sec. 3),
under certain assumptions every self-extensional logic turns out to be the
consequence associated to a suitably defined partial order.

We thus shall follow this route, which still leaves us free to choose among
the implication operators for $\mathbf{PP_{6}}$. Since on $\mathbf{PP_{6}}$ we
cannot define a classic-like implication suitable for our purposes — i.e., one
satisfying both $(\mathsf{A}1)$ and $(\mathsf{A}2)$ — we suggest to introduce
a Heyting implication. From an algebraic point of view, such an operator is
readily available. Indeed, since $\mathbf{PP_{6}}$ has a (finite) distributive
lattice reduct, the meet operation has a residuum (we will denote it by
$\Rightarrow_{\mathsf{H}}$), which is precisely the relative pseudo-complement
operation.

######  Definition 5.1.

Let $\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ be the algebra obtained by
expanding $\mathbf{PP_{6}}$ with the operation $\Rightarrow_{\mathsf{H}}$
defined as follows:

$a\Rightarrow_{\mathsf{H}}b\,{\coloneqq}\,\max\\{c\in\mathcal{V}_{6}\mid
a\land^{\mathbf{PP_{6}}}c\leq b\\},\text{ for all $a,b\in\mathcal{V}_{6}$.}$

In accordance with the above definition, the truth-table of the implication in
$\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ looks as follows:

$\Rightarrow_{\mathsf{H}}$ | $\hat{\mathbf{f}}$ | $\mathbf{f}$ | $\mathbf{n}$ | $\mathbf{b}$ | $\mathbf{t}$ | $\hat{\mathbf{t}}$
---|---|---|---|---|---|---
$\hat{\mathbf{f}}$ | $\hat{\mathbf{t}}$ | $\hat{\mathbf{t}}$ | $\hat{\mathbf{t}}$ | $\hat{\mathbf{t}}$ | $\hat{\mathbf{t}}$ | $\hat{\mathbf{t}}$
$\mathbf{f}$ | $\hat{\mathbf{f}}$ | $\hat{\mathbf{t}}$ | $\hat{\mathbf{t}}$ | $\hat{\mathbf{t}}$ | $\hat{\mathbf{t}}$ | $\hat{\mathbf{t}}$
$\mathbf{n}$ | $\hat{\mathbf{f}}$ | $\mathbf{b}$ | $\hat{\mathbf{t}}$ | $\mathbf{b}$ | $\hat{\mathbf{t}}$ | $\hat{\mathbf{t}}$
$\mathbf{b}$ | $\hat{\mathbf{f}}$ | $\mathbf{n}$ | $\mathbf{n}$ | $\hat{\mathbf{t}}$ | $\hat{\mathbf{t}}$ | $\hat{\mathbf{t}}$
$\mathbf{t}$ | $\hat{\mathbf{f}}$ | $\mathbf{f}$ | $\mathbf{n}$ | $\mathbf{b}$ | $\hat{\mathbf{t}}$ | $\hat{\mathbf{t}}$
$\hat{\mathbf{t}}$ | $\hat{\mathbf{f}}$ | $\mathbf{f}$ | $\mathbf{n}$ | $\mathbf{b}$ | $\mathbf{t}$ | $\hat{\mathbf{t}}$

$\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ is obviously (i.e., has a reduct
which is) a Heyting algebra. Furthermore, since it also carries a De Morgan
negation, it may be called a _De Morgan-Heyting algebra_ according to
Sankappanavar (1987), or a _symmetric Heyting algebra_ according to Monteiro
(1980)111Monteiro’s work suggests another natural candidate for an implication
(this one, already term-definable) in $\mathbf{PP_{6}}$. This is the
‘implication faible’ $\Rightarrow_{\mathsf{W}}$ introduced in (Monteiro, 1980,
Ch. IV, Def. 4.1), which can be given by the following term:
$x\Rightarrow_{\mathsf{W}}y:={\sim}x\lor{\sim}{\circ}x\lor y$.. Indeed, since
$\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ (as $\mathbf{PP_{6}}$) also has a
Stone lattice reduct (i.e. a pseudo-complemented distributive lattice
satisfying $\neg x\lor\neg\neg x\approx\top$), we may be a little more
specific, observing that $\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ is also,
in Monteiro’s terminology, a _Stonean symmetric Heyting algebra_ (Monteiro,
1980, Ch. IV, Def. 1.1). These observations will be exploited in Section 7.

######  Remark 5.2.

Before we proceed any further, one may wonder whether we are really adding
something new to $\mathbf{PP_{6}}$. In other words, was the implication
$\Rightarrow_{\mathsf{H}}$ already term-definable in this algebra? The answer
is negative. To see why, observe that $\mathbf{PP_{6}}$ is a subdirectly
irreducible algebra having a unique non-trivial congruence $\theta$, which is
the one that identifies (only) the elements in the set
$\\{\mathbf{t},\mathbf{f},\mathbf{b},\mathbf{n}\\}$. By adding the Heyting
implication, we obtain a simple algebra, in which $\theta$ is no longer a
congruence (indeed, $\mathbf{b}\theta\mathbf{n}$, but it is not the case that
$(\mathbf{b}\Rightarrow_{\mathsf{H}}\mathbf{b})\theta(\mathbf{b}\Rightarrow_{\mathsf{H}}\mathbf{n})$).

Before moving to the logics of order associated to the new algebra, we could
first consider the Set-Set logic determined by
$\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{{\uparrow}\mathbf{b}}\rangle$,
which is guaranteed to conservatively expand
$\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}$ (with the implication
$\Rightarrow_{\mathsf{H}}$ being the residuum of $\land$). Since
$\mathfrak{M}_{6}$ is monadic, we can axiomatize $\Rightarrow_{\mathsf{H}}$
straight away (similarly as we did in the proof of Theorem 4.3) following the
method of Marcelino and Caleiro (2021):

######  Theorem 5.3.

The Set-Set $\Sigma_{\Rightarrow}$-logic induced by $\mathfrak{M}_{6}$
expanded with $\Rightarrow_{\mathsf{H}}$ is axiomatized by the
$\\{p,{\sim}p,{\circ}p\\}$-analytic Set-Set calculus given by
$\mathsf{R}_{\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}}$ plus the following
rules:

$\frac{q}{p\Rightarrow q}\,\qquad\frac{p,p\Rightarrow
q}{q}\,\qquad\frac{{\sim}(p\Rightarrow
q)}{{\sim}q}\,\qquad\frac{{{\sim}}q}{{\sim}(p\Rightarrow q),{{\sim}}p}\,$
$\frac{}{p\Rightarrow q,{\circ}q,p}\,\qquad\frac{p\Rightarrow
q}{{\circ}(p\Rightarrow q),{\sim}q,q}\,\qquad\frac{p\Rightarrow
q,{\circ}q}{{\circ}p,q}\,\qquad\frac{{\sim}(p\Rightarrow
q),{\sim}p}{{\circ}(p\Rightarrow q)}\,$ $\frac{{\sim}p}{{\circ}(p\Rightarrow
q),p}\,\qquad\frac{{\circ}(p\Rightarrow
q),{\circ}p,p}{{\circ}q}\,\qquad\frac{{\circ}(p\Rightarrow
q),p}{{\circ}q,q}\,\qquad\frac{{\circ}p}{p\Rightarrow q,p}\,$
$\frac{{\circ}q}{{\circ}(p\Rightarrow q)}\,\qquad\frac{q}{{\sim}(p\Rightarrow
q),{\circ}(p\Rightarrow q),{\circ}p}\,$

Note however that
$\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{{\uparrow}\mathbf{b}}\rangle$
does not satisfy $(\mathsf{A}1)$: pick for instance
$a\,{\coloneqq}\,\mathbf{f}$ and $b\,{\coloneqq}\,\hat{\mathbf{f}}$. Self-
extensionality $(\mathsf{A}2)$ is also not satisfied. To see why, note that
the formula ${\sim}(p\Rightarrow q)\land{\sim}(q\Rightarrow p)$ and $\bot$ are
logically equivalent. However, $\nabla\bot$ and $\nabla({\sim}(p\Rightarrow
q)\land{\sim}(q\Rightarrow p))$ are not — recall that $\nabla
x\,{\coloneqq}\,x\lor{\sim}{\circ}x$. In fact, the latter and $\bot$ are
logically equivalent, while this does not hold for $\nabla\bot$. To see this,
consider a valuation such that $v(p)=\mathbf{b}$ and $v(q)=\mathbf{n}$. Then
$v(\nabla({\sim}(p\Rightarrow q)\land{\sim}(q\Rightarrow
p)))=\nabla^{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}({\sim}^{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}(\mathbf{b}\Rightarrow^{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}\mathbf{n})\land^{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}{\sim}^{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}(\mathbf{n}\Rightarrow^{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}\mathbf{b}))=\hat{\mathbf{t}}$.
Actually, as we are going to show in Proposition 5.7, there is only one self-
extensional Set-Fmla logic determined by a class of matrices based on the
algebra $\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ and principal filters.

Let us now resume our discussion about the logics of order. Having obtained a
new algebra $\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$, we can consider the
variety it generates, denoted
$\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$, and the order-
preserving logics associated to it. We denote by
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ and
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$, respectively, the Set-
Set and Set-Fmla order-preserving logics associated to
$\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$ (cf. Subsection 2.2
for the precise definitions). By the residuation property, we clearly have
that $\Rightarrow_{\mathsf{H}}$ is an implication in these logics (cf.
Definition 2.10 and Proposition 2.12). Furthermore:

######  Proposition 5.4.

${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ and
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ are conservative
expansions of $\mathcal{PP}_{\\!\leq}^{\mathsf{\rhd}}$ and
$\mathcal{PP}_{\\!\leq}$, respectively. Moreover, they are self-extensional.

###### Proof.

That both logics are conservative expansions of $\mathcal{PP}_{\\!\leq}$
follows directly from their matrix characterizations (Proposition 2.5), while
self-extensionality follows from Proposition 2.8. ∎

We may actually simplify the family of matrices that characterize these logics
(see Proposition 2.5) by removing some redundancies:

######  Proposition 5.5.

The logics ${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ and
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ are determined by the
class of matrices
$\\{\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{{\uparrow}\mathbf{f}}\rangle,\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{{\uparrow}\mathbf{b}}\rangle,\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{{\uparrow}\hat{\mathbf{t}}}\rangle\\}$.
Moreover, all these matrices are reduced.

###### Proof.

We begin by item (1). Any matrix
$\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},D\rangle$ with
$D\neq\mathcal{V}_{6}$ is reduced, because
$\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ is a simple algebra. However, two
of the matrices appearing in Proposition 5.4 may be safely omitted. Obviously
this holds for
$\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{{\uparrow}\hat{\mathbf{f}}}\rangle$,
which defines a trivial logic. Note further that
$\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{{\uparrow}\mathbf{b}}\rangle$
and
$\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{{\uparrow}\mathbf{n}}\rangle$
are isomorphic, and thus determine the same logic; so one of them can also be
omitted. Finally, the matrix with set of designated values
${{\uparrow}\mathbf{t}}$ can be safely omitted as we only need to consider
prime filters. Thus only the matrices listed in the statement remain. Item (2)
follows from the observation that
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ is the Set-Fmla companion
of the two Set-Set order-preserving logics. ∎

There is another Set-Set logic that has
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ as Set-Fmla companion,
namely the one determined by the class of matrices based on the algebra
$\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ having as designated sets the
principal filters of $\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$, which we
denote by ${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$. By a
similar argument as above, we have that
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$ is determined
by the class of matrices
$\\{\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{{\uparrow}\mathbf{f}}\rangle,\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{{\uparrow}\mathbf{b}}\rangle,\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{{\uparrow}\mathbf{t}}\rangle,\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{{\uparrow}\hat{\mathbf{t}}}\rangle\\}$
— that is, the matrices from Proposition 5.5 together with the matrix
$\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{{\uparrow}\mathbf{t}}\rangle$.
In this logic, however, $\Rightarrow$ is not an implication in our sense,
since $\rhd_{\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}(p\lor
q)\Rightarrow(p\lor q)$, but $p\lor
q\,\,\smallblacktriangleright_{{\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}}\,p,q$.
Still, we will include
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$ in our
considerations in view of its close relationship with
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ and because our techniques
will also apply very naturally to it, as we shall see.

The above results do not clarify whether one could find a single matrix to
characterize those logics (as it happens with $\mathbf{PP_{6}}$): the next
result rules out this possibility.

######  Theorem 5.6.

The logic $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$ is not
determined by a single logical matrix. The same holds also for the logics
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ and
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$.

###### Proof.

Since the two Set-Set logics share the same Set-Fmla companion
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}$, it is enough to prove
that the latter is not determined by a single logical matrix. For that, we use
the fact that a Set-Fmla logic that fails the property of _cancellation_ fails
to be determined by a single logical matrix (Wójcicki (1988); Shoesmith and
Smiley (1978)). A $\Sigma$-logic $\vdash$ respects cancellation when
$\Phi,\\{\Psi_{i}:i\in I\\}\vdash\varphi$ implies $\Phi\vdash\varphi$ for all
$\\{\varphi\\},\Phi,\Psi_{i}\subseteq L_{\Sigma}(P)$, $i\in I$, such that

  1. 1.

$\mathsf{props}(\Phi\cup\\{\varphi\\})\cap\mathsf{props}(\bigcup_{i\in
I}\Psi_{i})=\varnothing$

  2. 2.

$\mathsf{props}(\Psi_{i})\cap\mathsf{props}(\Psi_{j})=\varnothing$, $i\neq j$

  3. 3.

for all $i\in I$, we have $\Psi_{i}\not\vdash\psi$ for some $\psi\in
L_{\Sigma}(P)$.

Consider now $I=\\{1\\}$, $\Phi=\varnothing$, $\Psi_{1}=\\{p\land{\sim}p\land
q\land{\sim}q\land{\sim}{\circ}(p\Rightarrow q)\\}$ and
$\varphi=r\lor{\sim}r$. Conditions (1) and (2) are obviously satisfied.
Condition (3) is satisfied too, just consider the matrix
$\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{{\uparrow}\mathbf{f}}\rangle$
to see that
$\Psi_{1}\not\vdash_{{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}}\bot$.
Moreover, we have clearly that
$\not\vdash_{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}r\lor{\sim}r$
(it suffices to consider the matrix
$\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{{\uparrow}\mathbf{b}}\rangle$).
Finally, one can check that $p\land{\sim}p\land
q\land{\sim}q\land{\sim}{\circ}(p\Rightarrow
q)\vdash_{{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}}r\lor{\sim}r$. ∎

As earlier anticipated, we now proceed to show that
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ is actually the only
self-extensional Set-Fmla logic we can have when semantics of classes of
matrices based on the algebra $\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ and
principal filters are concerned.

######  Proposition 5.7.

For $\mathcal{V}\subseteq\mathcal{V}_{6}$, let $\vdash_{\mathcal{V}}$ be the
Set-Fmla logic determined by
$\left\\{\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{\uparrow}a\rangle\mid
a\in\mathcal{V}\right\\}$. If the logic $\vdash_{\mathcal{V}}$ is self-
extensional, then
$\vdash_{\mathcal{V}}\,=\,{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$.

###### Proof.

By Jansana (2006, Thm. 3.7), the finitary self-extensional extensions of
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ are in a one-to-one
correspondence with the subvarieties of
$\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$. The matrices in
$\\{\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{\uparrow}a\rangle\mid
a\in\mathcal{V}\\}$ are reduced models of $\vdash_{\mathcal{V}}$, implying
that $\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}$ belongs to the subvariety
$\mathsf{K}\subseteq\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$
associated with $\vdash_{\mathcal{V}}$. Then
$\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})\subseteq\mathsf{K}$,
so $\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})=\mathsf{K}$, and
thus
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}\,=\,\vdash_{\mathcal{V}}$.
∎

Adopting the terminology of Jansana (2006), we may say that
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ is _semilattice-based_
relative to $\land$ and to
$\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$. This observation
allows us to obtain further information: for instance, we know by Jansana
(2006, Thm. 3.12) that the class of algebra reducts of reduced matrices for
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ is precisely
$\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$. Semilattice-based
logics are often non-algebraizable but have an algebraizable companion, i.e.
an extension that shares the same algebraic models. We establish this for
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ below.

######  Proposition 5.8.

${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ is equivalential but not
algebraizable. The following is a set of equivalence formulas for it:

$\Xi(x,y)\,{\coloneqq}\,\\{x\Rightarrow y,y\Rightarrow x,\circ(x\Rightarrow
y),\circ(y\Rightarrow x)\\}$

or, equivalently (setting $\Delta x:=x\land{\circ}x$),

$\Xi(x,y)\,{\coloneqq}\,\\{\Delta(x\Rightarrow y),\Delta(y\Rightarrow x)\\}.$

###### Proof.

To prove that ${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ is
equivalential, it suffices to verify that the following conditions are met
(see Font (2016, Thm. 6.60)):

  1. 1.

$\vdash_{{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}}\Xi(x,x)$

  2. 2.

$x,\Xi(x,y)\vdash_{{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}}y$

  3. 3.

$\Xi(x,y)\vdash_{{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}}\Xi(\circ
x,\circ y)$ and
$\Xi(x,y)\vdash_{{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}}\Xi({\sim}x,{\sim}y)$

  4. 4.

$\Xi(x_{1},y_{1}),\Xi(x_{2},y_{2})\vdash_{{\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}}\Xi(x_{1}\copyright
x_{2},y_{1}\copyright y_{2})$ for every binary connective $\copyright$ in the
signature.

The verification of the above conditions is straightforward from the matrix
characterization of ${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$.
Now, if ${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ were
algebraizable, then the set of designated elements would be equationally
definable on every reduced matrix (see Font (2016, Def. 6.90)). But this is
not the case, because the matrices
$\\{\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},{{\uparrow}a}\rangle\mid
a\in\mathcal{V}_{6}\setminus\\{\hat{\mathbf{f}}\\}\\}$, all based on the same
algebra, are all reduced, and have distinct sets of designated elements. ∎

The algebraizable companion of
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ is the
$\top$-assertional logic associated to the variety
$\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$, which we denote by
$\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$. The reduced models of this
logic are all matrices of the form
$\langle\mathbf{A},\\{\top^{\mathbf{A}}\\}\rangle$, where $\mathbf{A}$ is an
algebra in $\mathbb{V}(\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}})$. One
easily verifies that $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$
satisfies the following rules — any of them being in fact sufficient to
distinguish $\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\top}$ from
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ (given that they are
sound in the former but not in the latter):

$\frac{p}{\Delta p}\qquad\frac{p}{\circ p}\qquad\frac{p\Rightarrow
q}{{\sim}q\Rightarrow{\sim}p}\qquad\frac{p,\ p\Rightarrow_{\mathsf{W}}q}{q}$

where $p\Rightarrow_{\mathsf{W}}q\,{\coloneqq}\,{\sim}p\lor{\sim}{\circ}p\lor
q$ and $\Delta p\,{\coloneqq}\,p\land{\circ}p$.

###  5.1 Characterizability by single finite PNmatrices

We saw in Theorem 5.6 that the logics we introduced in this section are not
characterized by any single logical matrix. In this subsection, we will
demonstrate the power of partial non-deterministic matrices by showing that
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$ and
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ are characterized
by a single finite PNmatrix. In consequence,
${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ will be characterized by
either of them. The essential idea is that the collections of matrices that
characterize these logics can be packaged into a single structure using
partiality.

The construction we will present makes use of the notion of total components
of a $\Sigma$-PNmatrix, which we now proceed to introduce. Let
$\mathfrak{M}\,{\coloneqq}\,\langle\mathbf{A},D\rangle$ be a
$\Sigma$-PNmatrix. For $X\subseteq A$, denote by $\mathfrak{M}_{X}$ the
$\Sigma$-PNmatrix $\langle\mathbf{A}_{X},D\cap X\rangle$, where
$\mathbf{A}_{X}\,{\coloneqq}\,\langle A\cap X,\cdot^{\mathbf{A}_{X}}\rangle$
is a $\Sigma$-multialgebra such that
$\copyright^{\mathbf{A}_{X}}(a_{1},\ldots,a_{k})\,{\coloneqq}\,\copyright^{\mathbf{A}}(a_{1},\ldots,a_{k})\cap
X$ for all $a_{1},\ldots,a_{k}\in X$, $k\in\omega$ and
$\copyright\in\Sigma_{k}$. This PNmatrix is called _the restriction of
$\mathfrak{M}$ to $X$_. We say that $X\neq\varnothing$ is a _total component_
of $\mathfrak{M}$ whenever $\mathfrak{M}_{X}$ is total. A total component $X$
is _maximal_ if adding any other value to $X$ leads to a component that is not
total. Denote by $\mathbb{T}(\mathfrak{M})$ the collection of maximal total
components of $\mathfrak{M}$. Then we have that
$\rhd_{\mathfrak{M}}={\rhd_{\\{\mathfrak{M}_{X}\mid
X\in\mathbb{T}(\mathfrak{M})\\}}}$ (Caleiro and Marcelino (2023)). The latter
observation is key to us: the matrices induced by the maximal total components
of the PNmatrices we will construct are be precisely the ones in the classes
that determine the logics
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$ and
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$.

We display below diagrams of the four matrices that determine the logic
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$ (in each case,
the sets of designated elements are highlighted with an ellipse).

$\mathbf{f}$$\mathbf{b}$$\mathbf{n}$$\mathbf{t}$$\hat{\mathbf{f}}$$\hat{\mathbf{t}}$

$\mathbf{f}$$\mathbf{b}$$\mathbf{n}$$\mathbf{t}$$\hat{\mathbf{f}}$$\hat{\mathbf{t}}$

$\mathbf{f}$$\mathbf{b}$$\mathbf{n}$$\mathbf{t}$$\hat{\mathbf{f}}$$\hat{\mathbf{t}}$

$\mathbf{f}$$\mathbf{b}$$\mathbf{n}$$\mathbf{t}$$\hat{\mathbf{f}}$$\hat{\mathbf{t}}$

Below we depict the structure of the PNmatrix $\mathfrak{M}_{\mathsf{up}}$ we
propose for this logic, whose principle of construction is the combination of
the above matrices, such that each of them consists of a total component of
the PNmatrix. Note: There is nothing special about the dashed edge, it is
pictured as dashed only because it crosses other edges.

${\mathfrak{M}_{\mathsf{up}}}$${{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\hat{\mathbf{t}}}}}}$${{\mathbf{t}^{-}}}$${{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{t}^{+}}}}}$${{\mathbf{b}^{-}}}$${{\mathbf{n}^{-}}}$${{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{b}^{+}}}}}$${{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{n}^{+}}}}}$${{\mathbf{f}^{-}}}$${{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{f}^{+}}}}}$${\hat{\mathbf{f}};}$

We try to make the above idea clearer in the following pictures, which show
how to identify each of the four matrices inside $\mathfrak{M}_{\mathsf{up}}$.

${{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\hat{\mathbf{t}}}}}}$${{{{\mathbf{t}^{-}}}}}$${{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{t}^{+}}}}}$${{{{\mathbf{b}^{-}}}}}$${{{{\mathbf{n}^{-}}}}}$${{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{b}^{+}}}}}$${{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{n}^{+}}}}}$${{{{\mathbf{f}^{-}}}}}$${{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{f}^{+}}}}}$${\hat{\mathbf{f}}}$

${{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\hat{\mathbf{t}}}}}}$${{{{\mathbf{t}^{-}}}}}$${{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{t}^{+}}}}}$${{{{\mathbf{b}^{-}}}}}$${{\mathbf{n}^{-}}}$${{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{b}^{+}}}}}$${{{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{n}^{+}}}}}}}$${{\mathbf{f}^{-}}}$${{{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{f}^{+}}}}}}}$${\hat{\mathbf{f}}}$

${{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\hat{\mathbf{t}}}}}}$${{{{\mathbf{t}^{-}}}}}$${{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{t}^{+}}}}}$${{\mathbf{b}^{-}}}$${{\mathbf{n}^{-}}}$${{{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{b}^{+}}}}}}}$${{{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{n}^{+}}}}}}}$${{\mathbf{f}^{-}}}$${{{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{f}^{+}}}}}}}$${\hat{\mathbf{f}}}$

${{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\hat{\mathbf{t}}}}}}$${{\mathbf{t}^{-}}}$${{{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{t}^{+}}}}}}}$${{\mathbf{b}^{-}}}$${{\mathbf{n}^{-}}}$${{{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{b}^{+}}}}}}}$${{{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{n}^{+}}}}}}}$${{\mathbf{f}^{-}}}$${{{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathbf{f}^{+}}}}}}}$${\hat{\mathbf{f}}}$

The PNmatrix for ${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$,
which we dub $\mathfrak{M}_{\leq}$, is essentially the same, the only
difference being the absence of the dashed line.

After this informal presentation of the general approach, we proceed to a
precise definition of the PNmatrices $\mathfrak{M}_{\mathsf{up}}$ and
$\mathfrak{M}_{\leq}$, and prove that they indeed determine, respectively, the
logics ${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$ and
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$.

######  Definition 5.9.

Let
$\mathcal{V}_{10}\,{\coloneqq}\,\\{\hat{\mathbf{f}},\mathbf{f}^{-},\mathbf{n}^{-},\mathbf{b}^{-},\mathbf{t}^{-},\mathbf{f}^{+},\mathbf{n}^{+},\mathbf{b}^{+},\mathbf{t}^{+},\hat{\mathbf{t}}\\}$
and
$D\,{\coloneqq}\,\\{\mathbf{f}^{+},\mathbf{n}^{+},\mathbf{b}^{+},\mathbf{t}^{+},\hat{\mathbf{t}}\\}\subseteq\mathcal{V}_{10}$.
Consider the ternary relations $\mathsf{inc}_{\mathsf{up}}(a,b,c)$ and
$\mathsf{inc}_{\leq}(a,b,c)$ on $\mathcal{V}_{10}$ defined as follows:

$\displaystyle\mathsf{inc}_{\mathsf{up}}(a,b,c)$ iff $\displaystyle
X\subseteq\\{a,b,c\\}\text{, for some
}X\in\\{\\{d^{-},d^{+}\\}:d\in\\{\mathbf{f},\mathbf{n},\mathbf{b},\mathbf{t}\\}\\}\cup$
$\displaystyle\qquad\\{\\{\mathbf{b}^{-},\mathbf{f}^{+}\\},\\{\mathbf{n}^{-},\mathbf{f}^{+}\\},\\{\mathbf{b}^{+},\mathbf{t}^{-}\\},\\{\mathbf{n}^{+},\mathbf{t}^{-}\\},\\{\mathbf{n}^{+},\mathbf{b}^{+},\mathbf{f}^{-}\\}\\}$
$\displaystyle\mathsf{inc}_{\leq}(a,b,c)$ iff $\displaystyle
X\subseteq\\{a,b,c\\}\text{, for some
}X\in\\{\\{d^{-},d^{+}\\}:d\in\\{\mathbf{f},\mathbf{n},\mathbf{b},\mathbf{t}\\}\\}\cup$
$\displaystyle\qquad\\{\\{\mathbf{b}^{-},\mathbf{f}^{+}\\},\\{\mathbf{n}^{-},\mathbf{f}^{+}\\},\\{\mathbf{b}^{+},\mathbf{t}^{-}\\},\\{\mathbf{n}^{+},\mathbf{t}^{-}\\},\\{\mathbf{n}^{+},\mathbf{b}^{+},\mathbf{f}^{-}\\},\\{\mathbf{n}^{-},\mathbf{b}^{-},\mathbf{t}^{+}\\}\\}$

Consider also the function
$f:\mathcal{V}_{10}\to\\{\hat{\mathbf{f}},\mathbf{f},\mathbf{n},\mathbf{b},\mathbf{t},\hat{\mathbf{t}}\\}$
given by $f(\hat{\mathbf{f}})\,{\coloneqq}\,\hat{\mathbf{f}}$,
$f(\hat{\mathbf{t}})\,{\coloneqq}\,\hat{\mathbf{t}}$,
$f(a^{i})\,{\coloneqq}\,a$ for
$a\in\\{\mathbf{f},\mathbf{n},\mathbf{b},\mathbf{t}\\}$. We define the
PNmatrices
$\mathfrak{M}_{\mathsf{up}}\,{\coloneqq}\,{\langle\mathbf{A}_{\mathsf{up}},D\rangle}$
and $\mathfrak{M}_{\leq}\,{\coloneqq}\,{\langle\mathbf{A}_{\leq},D\rangle}$,
with
$\mathbf{A}_{\mathsf{up}}\,{\coloneqq}\,\langle\mathcal{V}_{10},\cdot_{\mathsf{up}}\rangle$
and
$\mathbf{A}_{\leq}\,{\coloneqq}\,\langle\mathcal{V}_{10},\cdot_{\leq}\rangle$
such that

  * •

for $\copyright\in\\{{\sim},{\circ}\\}$,

$\displaystyle\copyright_{\mathsf{up}}(a)$
$\displaystyle\,{\coloneqq}\,\\{b\in\mathcal{V}_{10}:\copyright_{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}(f(a))=f(b),\text{
not }\mathsf{inc}_{\mathsf{up}}(a,a,b)\\}$ $\displaystyle\copyright_{\leq}(a)$
$\displaystyle\,{\coloneqq}\,\\{b\in\mathcal{V}_{10}:\copyright_{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}(f(a))=f(b),\text{
not }\mathsf{inc}_{\leq}(a,a,b)\\}$

  * •

for $\copyright\in\\{\land,\lor,\Rightarrow\\}$,

$\displaystyle\copyright_{\mathsf{up}}(a,b)$
$\displaystyle\,{\coloneqq}\,\\{c\in\mathcal{V}_{10}:\copyright_{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}(f(a),f(b))=f(c),\text{
not }\mathsf{inc}_{\mathsf{up}}(a,b,c)\\}$
$\displaystyle\copyright_{\leq}(a,b)$
$\displaystyle\,{\coloneqq}\,\\{c\in\mathcal{V}_{10}:\copyright_{\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}}}(f(a),f(b))=f(c),\text{
not }\mathsf{inc}_{\leq}(a,b,c)\\}$

######  Proposition 5.10.

${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$ is determined
by ${\mathfrak{M}_{\mathsf{up}}}$ and
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ is determined by
${\mathfrak{M}_{\leq}}$.

###### Proof.

We have that if $\\{a,b,c\\}\subseteq X$ and
$\mathsf{inc}_{\mathsf{up}}(a,b,c)$ then $X$ is not contained in a total
component of $\mathfrak{M}_{\mathsf{up}}$. In fact,

  * •

if $b_{1},b_{2}\in X$ with

$\\{b_{1},b_{2}\\}\in\\{\\{a^{-},a^{+}\\}:a\in\\{\mathbf{f},\mathbf{n},\mathbf{b},\mathbf{t}\\}\\}\cup\\{\\{\mathbf{b}^{-},\mathbf{f}^{+}\\},\\{\mathbf{n}^{-},\mathbf{f}^{+}\\},\\{\mathbf{b}^{+},\mathbf{t}^{-}\\},\\{\mathbf{n}^{+},\mathbf{t}^{-}\\}\\}$

then $b_{1}\land_{\mathsf{up}}b_{2}=\varnothing$.

  * •

if $\\{\mathbf{n}^{+},\mathbf{b}^{+},\mathbf{f}^{-}\\}\subseteq X$, then
$\mathbf{n}^{+}\land_{\mathsf{up}}\mathbf{b}^{+}=\\{\mathbf{f}^{+}\\}$ and
$\mathbf{f}^{-}\land_{\mathsf{up}}\mathbf{f}^{+}=\varnothing$.

The maximal total components of $\mathfrak{M}_{\mathsf{up}}$ are

$\mathbb{T}({\mathfrak{M}_{\mathsf{up}}})=\\{\\{\hat{\mathbf{f}},\mathbf{f}^{-},\mathbf{n}^{-},\mathbf{b}^{-},\mathbf{t}^{-},\hat{\mathbf{t}}\\},\\{\hat{\mathbf{f}},\mathbf{f}^{-},\mathbf{n}^{-},\mathbf{b}^{-},\mathbf{t}^{+},\hat{\mathbf{t}}\\},\\{\hat{\mathbf{f}},\mathbf{f}^{-},\mathbf{n}^{-},\mathbf{b}^{+},\mathbf{t}^{+},\hat{\mathbf{t}}\\},\\{\hat{\mathbf{f}},\mathbf{f}^{+},\mathbf{n}^{+},\mathbf{b}^{+},\mathbf{t}^{+},\hat{\mathbf{t}}\\}\\}$

since for every $X\in\mathbb{T}({\mathfrak{M}_{\mathsf{up}}})$ and every
$a,b,c\in X$ we have that $\mathsf{inc}_{\mathsf{up}}(a,b,c)$ is not the case.
Thus the restriction of $\mathfrak{M}_{\mathsf{up}}$ to $X$ is isomorphic to
(that is, it is the same up to renaming of truth values) some matrix with set
of designated values $D_{X}={{\uparrow}a}$ for $a\in\mathcal{V}_{6}$. The
isomorphism is given by the restriction of $f$ to $X$.

Similarly, the maximal total components of $\mathfrak{M}_{\leq}$ are

$\mathbb{T}({\mathfrak{M}_{\leq}})=\\{\\{\hat{\mathbf{f}},\mathbf{f}^{-},\mathbf{n}^{-},\mathbf{b}^{-},\mathbf{t}^{-},\hat{\mathbf{t}}\\},\\{\hat{\mathbf{f}},\mathbf{f}^{-},\mathbf{n}^{-},\mathbf{b}^{+},\mathbf{t}^{+},\hat{\mathbf{t}}\\},\\{\hat{\mathbf{f}},\mathbf{f}^{+},\mathbf{n}^{+},\mathbf{b}^{+},\mathbf{t}^{+},\hat{\mathbf{t}}\\}\\}$

This is so because $\mathsf{inc}_{\leq}(a,b,c)$ iff
$\mathsf{inc}_{\mathsf{up}}(a,b,c)$ or
$\\{\mathbf{n}^{-},\mathbf{b}^{-},\mathbf{t}^{+}\\}\subseteq X$, and the fact
that if $\\{\mathbf{n}^{-},\mathbf{b}^{-},\mathbf{t}^{+}\\}\subseteq X$ then
$X$ is not in a total component of $\mathfrak{M}_{\leq}$, since
$\mathbf{n}^{-}\lor_{\mathsf{up}}\mathbf{b}^{-}=\\{\mathbf{t}^{-}\\}$ and
$\mathbf{t}^{-}\land_{\mathsf{up}}\mathbf{t}^{+}=\varnothing$.∎

##  6 Hilbert-style axiomatizations

Our goal here is to present analytic Set-Set Hilbert-style axiomatizations for
the implicative extensions
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$ and
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$, as well as a Set-
Fmla axiomatization for ${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$.
Unfortunately, the PNmatrices from the previous section do not allow us to
extract automatically an analytic Set-Set calculus for the corresponding
logics using the technology of Caleiro and Marcelino (2019), employed in Gomes
et al. (2022) and in the previous sections of the present paper, in view of
the following:

######  Proposition 6.1.

Neither $\mathfrak{M}_{\leq}$ nor $\mathfrak{M}_{\leq}$ is monadic.

###### Proof.

Note that no unary formula can separate $\mathbf{n}^{+}$ from
$\mathbf{b}^{+}$, nor $\mathbf{n}^{-}$ from $\mathbf{b}^{-}$. Indeed, one can
show inductively on the structure of a unary formula $\varphi(p)$ that, given
valuations $v_{a}$, $v_{b}$ such that $v_{a}(p)=a^{s}$ and $v_{b}(p)=b^{s}$
for $s\in\\{+,-\\}$, we have that
$v_{x}(\varphi)\in\\{\hat{\mathbf{f}},x^{s},\hat{\mathbf{t}}\\}$, and either
$v_{a}(\varphi)=v_{b}(\varphi)$ or $v_{a}(\varphi)=a^{s}$ and
$v_{b}(\varphi)=b^{s}$. ∎

We need, therefore, to delve into specific details of the logical matrices
introduced above, and extract what is important to characterize their
algebraic and logical structures in terms of formulas and Set-Set rules of
inference. We will do that and obtain analytic axiomatizations for the Set-Set
logics and then, taking advantage of the fact that in
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ we have a
disjunction (a notion we will soon make precise), we will convert the calculus
for ${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$ into a Set-Fmla
axiomatization for ${\mathcal{PP}^{\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$.

###  6.1 Analytic axiomatizations for
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$ and
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$

We begin by the analytic Set-Set axiomatizations. What follows is a succession
of definitions introducing groups of rules of inference that capture
particular aspects of the collections of logical matrices determining
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\mathsf{up}}}$ and
${\mathcal{PP}^{\rhd,\Rightarrow_{\mathsf{H}}}_{\\!\leq}}$. We check the
soundness of each of them and ultimately arrive to the desired completeness
results. Throughout the proofs, we will make use of the following
abbreviations:

######  Definition 6.2.

Set ${\uparrow}p\,{\coloneqq}\,{\circ}({\sim}p\Rightarrow p)$ and
${\downarrow}p\,{\coloneqq}\,{\circ}(p\Rightarrow{\sim}p)$.

Note that the above definitions introduce new connectives by means of
abbreviations, so we have
${\mathsf{sub}}({\uparrow}p)=\\{p,{\sim}p,{\sim}p\Rightarrow
p,{\circ}({\sim}p\Rightarrow p)\\}$ (the case of
${\mathsf{sub}}({\downarrow}p)$ is similar).

######  Definition 6.3.

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

$\frac{}{{\uparrow}p,{\downarrow}p}\,\mathsf{r}^{\Diamond}_{{\uparrow}\mathsf{or}{\downarrow}}\qquad\frac{}{{\circ}(p\Rightarrow
p)}\,\mathsf{r}_{\mathsf{id}}^{\Diamond}\qquad\frac{{\circ}(p\Rightarrow
q),{\circ}(q\Rightarrow r)}{{\circ}q,{\circ}(p\Rightarrow
r)}\,\mathsf{r}_{\mathsf{trans}}^{\Diamond}$

$\frac{}{{\downarrow}p,{\circ}q,{\circ}(q\Rightarrow
p)}\,\mathsf{r}^{\Diamond}_{\leq\mathbf{t}}\qquad\frac{}{{\uparrow}p,{\circ}(p\Rightarrow
q)}\,\mathsf{r}^{\Diamond}_{\geq\mathbf{f}}$

$\frac{{\uparrow}p,{\circ}(p\Rightarrow
q)}{{\circ}p,{\uparrow}q}\,\mathsf{r}^{\Diamond}_{\mathsf{incclass}_{1}}\qquad\frac{{\downarrow}q,{\circ}(p\Rightarrow
q)}{{\circ}q,{\downarrow}p}\,\mathsf{r}^{\Diamond}_{\mathsf{incclass}_{2}}\qquad\frac{{\uparrow}p,{\downarrow}q,{\circ}(p\Rightarrow
q)}{{\circ}q,{\circ}(q\Rightarrow
p)}\,\mathsf{r}^{\Diamond}_{\mathsf{incclass}_{3}}$

$\frac{{\downarrow}p,{\uparrow}r}{{\circ}p,{\circ}(p\Rightarrow
q),{\circ}(p\Rightarrow r),{\circ}(q\Rightarrow
r)}\,\mathsf{r}^{\Diamond}_{\mathsf{just}_{2}}$

######  Proposition 6.4.

The rules of $\mathsf{R}_{\Diamond}$ are sound for any matrix
$\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},D\rangle$ with $D$
containing $\hat{\mathbf{t}}$ and not containing $\hat{\mathbf{f}}$.

###### Proof.

We proceed rule by rule.

$\mathsf{r}^{\Diamond}_{{\uparrow}\mathsf{or}{\downarrow}}$:

If $v({\uparrow}p)\notin D$, then $v({\uparrow}p)=\hat{\mathbf{f}}$, so
$v(p)=\mathbf{f}$ and thus $v({\downarrow}p)=\hat{\mathbf{t}}\in D$.

${\mathsf{r}^{\Diamond}_{\mathsf{id}}}$:

Clearly, $v({\circ}(p\Rightarrow p))=\hat{\mathbf{t}}\in D$.

$\mathsf{r}^{\Diamond}_{\mathsf{trans}}$:

If $v({\circ}q)\notin D$, we have $v(q)\neq\hat{\mathbf{f}}$, hence
$v({\circ}(p\Rightarrow q))=\hat{\mathbf{t}}$ and $v({\circ}(q\Rightarrow
r))=\hat{\mathbf{t}}$, thus $v(p)\leq v(q)\leq v(r)$, and therefore
$v({\circ}(p\Rightarrow r))=\hat{\mathbf{t}}$.

$\mathsf{r}^{\Diamond}_{\leq\mathbf{t}}$:

If $v({\downarrow}p)\notin D$, then $v(p)=\mathbf{t}$. If $v({\circ}q)\notin
D$, then $\mathbf{f}\leq v(q)\leq\mathbf{t}$ and therefore
$v({\circ}(q\Rightarrow p))=\hat{\mathbf{t}}$.

$\mathsf{r}^{\Diamond}_{\geq\mathbf{f}}$:

If $v({\uparrow}p)\notin D$ then $v(p)=\mathbf{f}$ and therefore
$v({\circ}(p\Rightarrow q))=\hat{\mathbf{t}}$.

$\mathsf{r}^{\Diamond}_{\mathsf{incclass}_{1}}$:

If $v({\uparrow}p)\in D$ and $v({\circ}p)\notin D$ then
$v(p)\in\\{\mathbf{b},\mathbf{n},\mathbf{t}\\}$ and if $v({\circ}(p\Rightarrow
q))\in D$ then
$v(q)\in\\{\hat{\mathbf{f}},\mathbf{b},\mathbf{n},\mathbf{t},\hat{\mathbf{t}}\\}$
and therefore $v({\uparrow}q)=\hat{\mathbf{t}}\in D$.

$\mathsf{r}^{\Diamond}_{\mathsf{incclass}_{2}}$:

If $v({\downarrow}q)\in D$ and $v({\circ}q)\notin D$ then
$v(q)\in\\{\mathbf{f},\mathbf{b},\mathbf{n}\\}$ and if $v({\circ}(p\Rightarrow
q))\in D$ then
$v(p)\in\\{\hat{\mathbf{f}},\mathbf{f},\mathbf{b},\mathbf{n}\\}$ and therefore
$v({\downarrow}p)=\hat{\mathbf{t}}\in D$.

$\mathsf{r}^{\Diamond}_{\mathsf{incclass}_{3}}$:

If $v({\uparrow}p),v({\downarrow}q)\in D$ and $v({\circ}q)\notin D$ then
$v(p)\neq\mathbf{f}$ and $v(q)\in\\{\mathbf{f},\mathbf{b},\mathbf{n}\\}$.
Further, if $v({\circ}(p\Rightarrow q))\in D$ then $v(p)\leq v(q)$ and so
$v(q\Rightarrow p)\in D$.

$\mathsf{r}^{\Diamond}_{\mathsf{just}_{2}}$:

If $v({\downarrow}p),v({\uparrow}r)\in D$ and $v({\circ}p)\notin D$ then
$v(p)\in\\{\mathbf{f},\mathbf{b},\mathbf{n}\\}$ and $v(r)\neq\mathbf{f}$. If
$v({\circ}(p\Rightarrow q)),v({\circ}(p\Rightarrow q))\not\in D$, then
$v(p\Rightarrow q),v(q\Rightarrow
r)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$. Then
$v(p),v(q),v(r)\in\\{\mathbf{b},\mathbf{n}\\}$. Hence, either $v(p)=v(q)$, in
which case $v(p\Rightarrow q)=\hat{\mathbf{t}}\in D$, or $v(q)=v(r)$, in which
case $v(q\Rightarrow r)=\hat{\mathbf{t}}\in D$ (both cases contradicting the
assumptions) or $v(p)=v(r)$, in which case $v(p\Rightarrow
r)=\hat{\mathbf{t}}\in D$, as desired. ∎

######  Definition 6.5.

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

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

######  Proposition 6.6.

The rules of $\mathsf{R}_{\Rightarrow}$ 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}^{\Rightarrow}_{1}$:

If $v({\circ}q)\in D$ then $v(q)\in\\{\hat{\mathbf{t}},\hat{\mathbf{f}}\\}$,
hence $v({\circ}(p\Rightarrow q))\in D$.

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

If $v(q)\in D$, then $v(q)\geq a$ and by analysing the table of
$\Rightarrow_{\mathsf{H}}$ we conclude that $v(p\Rightarrow q)\geq v(q)\geq a$
and thus $v(p\Rightarrow q)\in D$.

$\mathsf{r}^{\Rightarrow}_{3}$:

If $v(p),v(p\Rightarrow q)\in D$ then $v(p)\geq a$ and $v(p\Rightarrow q)\geq
a$, and by analysing the table of $\Rightarrow_{\mathsf{H}}$ we conclude that
$v(q)\geq a$ and thus $v(q)\in D$.

$\mathsf{r}^{\Rightarrow}_{4}$:

If $v({\circ}p),v(p)\in D$ and $v({\circ}q)\not\in D$, then
$v(p)=\hat{\mathbf{t}}$ and
$v(q)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$ and $v(p\Rightarrow
q)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$, so
$v({\circ}(p\Rightarrow q))=\hat{\mathbf{f}}\not\in D$.

$\mathsf{r}^{\Rightarrow}_{5}$:

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

$\mathsf{r}^{\Rightarrow}_{6}$:

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

$\mathsf{r}^{\Rightarrow}_{7}$:

If $v({\uparrow}q)\in D$, then $v(q)\neq\mathbf{f}$. But then $v(p\Rightarrow
q)\neq\mathbf{f}$, and $v({\uparrow}(p\Rightarrow q))=\hat{\mathbf{t}}$.

$\mathsf{r}^{\Rightarrow}_{8}$:

Similar to the proof for $\mathsf{r}^{\Rightarrow}_{7}$.

$\mathsf{r}^{\Rightarrow}_{9}$:

If $v({\circ}(p\Rightarrow(q\Rightarrow p)))\not\in D$, then
$v(p\Rightarrow(q\Rightarrow
p))\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$. Then
$v(p)\in\\{\mathbf{b},\mathbf{n},\mathbf{t},\hat{\mathbf{t}}\\}$ and
$v(q\Rightarrow p)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$. So,
$v(q)\in\\{\mathbf{b},\mathbf{n},\mathbf{t},\hat{\mathbf{t}}\\}$ and
$v(p)\in\\{\mathbf{b},\mathbf{n},\mathbf{t}\\}$. If $v(p)=\mathbf{b}$ and
$v(q\Rightarrow p)=\mathbf{b}$, then $v(p\Rightarrow(q\Rightarrow
p))=\hat{\mathbf{t}}$. If $v(p)=\mathbf{n}$, the proof is similar. If
$v(p)=\mathbf{t}$, then $v(q\Rightarrow p)=\hat{\mathbf{t}}$ or
$v(q)=\hat{\mathbf{t}}$. In all cases we reach a contradiction.

$\mathsf{r}^{\Rightarrow}_{10}$, $\mathsf{r}^{\Rightarrow}_{11}$:

If $v(p),v({\circ}p)\notin D$, then $v(p)=\hat{\mathbf{f}}$, thus
$v(p\Rightarrow q)=v({\circ}(p\Rightarrow q))=\hat{\mathbf{t}}\in D$.

$\mathsf{r}^{\Rightarrow}_{12}$:

If $v({\circ}q)\in D$ and $v(q)\not\in D$, then $v(q)=\hat{\mathbf{f}}$. If
$v({\circ}p)\not\in D$, then
$v(p)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$. But then
$v(p\Rightarrow q)=\mathbf{f}\not\in D$.

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

If $v({\circ}(p\Rightarrow q))\in D$, then $v(p\Rightarrow
q)\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$. Further, if $v({\circ}q)\not\in
D$, then $v(q)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$, thus
$v(p\Rightarrow q)=\hat{\mathbf{t}}$.

$\mathsf{r}^{\Rightarrow}_{14}$:

If $v({\circ}(p\Rightarrow q))\not\in D$, we have $v(p\Rightarrow
q)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$. If
$v({\downarrow}p)\not\in D$, then $v(p)=\mathbf{t}$, and $v(p\Rightarrow
q)=v(q)$, and we are done.

$\mathsf{r}^{\Rightarrow}_{15}$:

If $v({\circ}p)\not\in D$, then
$v(p)\in\\{\mathbf{b},\mathbf{n},\mathbf{t}\\}$. If $v({\uparrow}q)\not\in D$,
then $v(q)=\mathbf{f}$. Thus $v(p\Rightarrow
q)\in\\{\mathbf{b},\mathbf{n},\mathbf{f}\\}$, so $v({\circ}(p\Rightarrow
q))=\hat{\mathbf{f}}$.

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

If $v({\circ}p)\not\in D$ and $v({\downarrow}p)\in D$, then
$v(p)\in\\{\mathbf{f},\mathbf{b},\mathbf{n}\\}$ and $v(p\Rightarrow
q)\neq\mathbf{f}$, and thus $v({\uparrow}(p\Rightarrow q))=\hat{\mathbf{t}}$.

$\mathsf{r}^{\Rightarrow}_{17}$:

If $v({\circ}p)\not\in D$, then
$v(p)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$. Thus
$v(p\Rightarrow q)\neq\mathbf{t}$, so $v({\downarrow}(p\Rightarrow
q))=\hat{\mathbf{t}}$.

$\mathsf{r}^{\Rightarrow}_{18}$:

If $v({\uparrow}p)\in D$ and $v({\circ}p)\not\in D$, then
$v(p)\in\\{\mathbf{b},\mathbf{n},\mathbf{t}\\}$. If $v({\uparrow}q)\not\in D$,
then $v(q)=\mathbf{f}$. If $v(p)=\mathbf{b}$, then $v(p\Rightarrow
q)=\mathbf{n}$, and then $v(p\Rightarrow(p\Rightarrow q))=\mathbf{n}$.
Similarly, we have $v(p\Rightarrow(p\Rightarrow q))=\mathbf{b}$ if
$v(p)=\mathbf{n}$. If $v(p)=\mathbf{t}$, then $v(p\Rightarrow q)=\mathbf{f}$,
and $v(p\Rightarrow(p\Rightarrow q))=\mathbf{f}$. In any case,
$v({\circ}(p\Rightarrow(p\Rightarrow q)))=\hat{\mathbf{f}}$.

$\mathsf{r}^{\Rightarrow}_{19}$:

If $v({\circ}(p\Rightarrow q))\not\in D$, we have $v(p\Rightarrow
q)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$. If $v({\uparrow}q)\in
D$, we have $v(q)\neq\mathbf{f}$. The case $v(p\Rightarrow q)=\mathbf{f}$ is
impossible. If $v(p\Rightarrow q)=\mathbf{b}$, we have $v(q)=\mathbf{b}$, and
clearly $v({\circ}((p\Rightarrow q)\Rightarrow q))=\hat{\mathbf{t}}$. The case
$v(p\Rightarrow q)=\mathbf{n}$ is similar as the previous case. If
$v(p\Rightarrow q)=\mathbf{t}$, then $v(p)=\hat{\mathbf{t}}$, thus
$v({\circ}((p\Rightarrow q)\Rightarrow q))=\hat{\mathbf{t}}$. ∎

######  Definition 6.7.

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

$\frac{{\circ}p}{p,{\sim}p}\,\mathsf{r}^{\sim}_{1}\qquad\frac{{\circ}p,p,{\sim}p}{}\,\mathsf{r}^{\sim}_{2}\qquad\frac{{\circ}p}{{\circ}{\sim}p}\,\mathsf{r}^{\sim}_{3}\qquad\frac{{\circ}{\sim}p}{{\circ}p}\,\mathsf{r}^{\sim}_{4}$

$\frac{{\uparrow}{\sim}p}{{\downarrow}p}\,\mathsf{r}^{\sim}_{5}\qquad\frac{{\downarrow}{\sim}p}{{\uparrow}p}\,\mathsf{r}^{\sim}_{6}\qquad\frac{{\downarrow}p}{{\uparrow}{\sim}p}\,\mathsf{r}^{\sim}_{7}\qquad\frac{{\uparrow}p}{{\downarrow}{\sim}p}\,\mathsf{r}^{\sim}_{8}$

######  Proposition 6.8.

The rules of $\mathsf{R}_{\sim}$ 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}^{\sim}_{1}}$:

If $v({\circ}p)\in D$ and $v(p)\notin D$ then $v(p)=\hat{\mathbf{f}}$ and
$v({\sim}p)=\hat{\mathbf{t}}\in D$.

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

If $v(p),v({\circ}p)\in D$ then $v(p)=\hat{\mathbf{t}}$ and
$v({\sim}p)=\hat{\mathbf{f}}\notin D$.

${\mathsf{r}^{\sim}_{3}}$:

If $v({\circ}p)\in D$ then
$v(p),v({\sim}p)\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$ and so
$v({\circ}{\sim}p)=\hat{\mathbf{t}}\in D$.

$\mathsf{r}^{\sim}_{4}$:

If $v({\circ}{\sim}p)\in D$ then
$v({\sim}p),v(p)\in\\{\hat{\mathbf{f}},\hat{\mathbf{t}}\\}$ and so
$v({\circ}p)=\hat{\mathbf{t}}\in D$.

${{\mathsf{r}^{\sim}_{5}}}$:

If $v({\downarrow}p)\notin D$ then $v(p)=\mathbf{t}$, so
$v({\sim}p)=\mathbf{f}$ and hence $v({\uparrow}{\sim}p)=\hat{\mathbf{f}}\notin
D$.

${\mathsf{r}^{\sim}_{6}}$:

If $v({\uparrow}p)\notin D$ then $v(p)=\mathbf{f}$, so $v({\sim}p)=\mathbf{t}$
and hence $v({\downarrow}{\sim}p)=\hat{\mathbf{f}}\notin D$.

${\mathsf{r}^{\sim}_{7}}$:

If $v({\downarrow}p)\in D$ then $v(p)\neq\mathbf{t}$, hence
$v({\sim}p)\neq\mathbf{f}$ and so $v({\uparrow}{\sim}p)=\hat{\mathbf{t}}\in
D$.

${\mathsf{r}^{\sim}_{8}}$:

If $v({\uparrow}p)\in D$ then $v(p)\neq\mathbf{f}$, hence
$v({\sim}p)\neq\mathbf{t}$ and so $v({\downarrow}{\sim}p)=\hat{\mathbf{t}}\in
D$.∎

######  Definition 6.9.

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

$\frac{}{{\circ}{\circ}p}\,\mathsf{r}_{{\circ}}$

######  Proposition 6.10.

The rules of $\mathsf{R}_{\circ}$ are sound for any matrix
$\langle\mathbf{PP_{6}^{\Rightarrow_{\mathsf{H}}}},D\rangle$ with
$\hat{\mathbf{t}}\in D$.

###### Proof.

Easily, $v(\circ\circ p)=\hat{\mathbf{t}}\in D$. ∎

######  Definition 6.11.

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

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

######  Proposition 6.12.

The rules of $\mathsf{R}_{\land}$ 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}^{\land}_{1}$:

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

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

It follows because principal filters are closed under meets.

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

If $v(p\land q)\geq a$, then from $v(p)\geq v(p\land q)$ and $v(q)\geq
v(p\land q)$ we have that $v(p),v(q)\in D$.

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

If $v({\circ}q)\not\in D$, then
$v(q)\in\\{\mathbf{f},\mathbf{b},\mathbf{n},\mathbf{t}\\}$. If