Adding an implication to logics of perfect paradefinite algebras

Abstract

Perfect paradefinite algebras are De Morgan algebras expanded with an operation that allows for the full behavior of classical negation to be restored. They form a variety that is term-equivalent to the variety of involutive Stone algebras. Their associated multiple-conclusion (Set-Set) and single-conclusion () order-preserving logics are non-algebraizable self-extensional logics of formal inconsistency and undeterminedness determined by a six-valued matrix. We studied these logics extensively in Gomes et al. ((2022). Electronic Proceedings in Theoretical Computer Science 357 56–76.) from both the algebraic and the proof-theoretical perspectives. In the present paper, we continue 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 the language of the latter algebra with this connective and study the (self-extensional) Set-Set and order-preserving and $\top$-assertional logics of the variety induced by the resulting 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 order-preserving Set-Set logic, in particular, we obtain a Set-Set axiomatization that is analytic. We close by studying interpolation properties for these logics and concluding that the new variety has the Maehara amalgamation property.

1. Introduction

The algebraic structures we now call involutive Stone algebras appear to have been first considered by Roberto Cignoli and Marta Sagastume along with 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 consist 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, 2022; Marcelino and Rivieccio 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 discussed in Marcos (2005b).

Reformulated in this language (i.e., $\{ \land, \lor, {\sim },{\circ }, \bot, \top \}$ ), involutive Stone algebras have been renamed perfect paradefinite algebras (PP-algebras) in Gomes et al. (2022). In the latter paper we axiomatized the 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 }^{{\rhd }}{}$ . The Set-Set axiomatization we presented for it is analytic and thus suitable for automated reasoning. We then used all those 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 logics associated with 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 the 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 (see Definitions 3, 4 and general results on self-extensional logics in Jansana 2006, Section 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 $(\textsf{A}1)$ in Subsection 2.4); second, that the resulting logic should be self-extensional $(\textsf{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 20). 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 standard one for the implication on Heyting algebras.

Tradition, in the present setting, happens to point in the same direction as algebra. In fact, it turns out that a substantial part of the theory of involutive Stone algebras had already been 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 the present 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). The purpose of the latter is to add a “classicality” 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 13). The resulting logic – dubbed ${\textrm{LET}_{\textrm{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 ${\textrm{LET}_{\textrm{K}}^{+}}$ coincides with $\mathcal{PP}_{\!\leq }$ . The implication connective of ${\textrm{LET}_{\textrm{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, $(\textsf{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 ${\textrm{LET}_{\textrm{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.

Our 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 $(\textsf{A}1)$ and $(\textsf{A}2)$ . After proving the impossibility of this task, we focus first on $(\textsf{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 axiomatizations for the corresponding companions.

Next, turning our focus to $(\textsf{A}2)$ , and having observed that the matrix $\langle \mathbf{PP_6},{{\uparrow }{\mathbf{b}}} \rangle$ , which determines $\mathcal{PP}_{\!\leq }^{{\rhd }}$ and $\mathcal{PP}_{\!\leq }$ , is based on an algebra (i.e., $\mathbf{PP_6}$ ) that is a finite distributive lattice, in Section 5 we enrich its language with an operation $\Rightarrow _{\textsf{H}}$ that 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 _{\textsf{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 _{\textsf{H}}}}, D \rangle$ such that $D$ is a non-empty lattice filter of the lattice reduct of $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ . The (Set-Set and ) logics determined by this family are the order-preserving logics induced by the variety $\mathbb{V}(\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}})$ , guaranteed to be self-extensional.

In Section 6, we proceed to axiomatize both the Set-Set and the logics thus defined. First focusing on the Set-Set logic, we present an axiomatization after a detailed analysis of the algebraic structure of the matrices and of their designated sets. The calculus we present is not only sound and complete, but also analytic. From such axiomatization, moreover, we show how to extract an axiomatization for the corresponding logic of order.

In Section 7, we look at the algebraic models that correspond to the logics $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ and $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ (the $\top$ -assertional logic associated with $\mathbb{V}(\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}})$ ) within the general theory of algebraization of logics. We begin by observing that both logics are closely related to Moisil’s “symmetric modal logic,” whose algebraic counterpart is the class of symmetric Heyting algebras (Definition 70). Indeed, $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ is (term-equivalent to) a symmetric Heyting algebra, and the class of algebras providing an algebraic semantics for both $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ and $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ is precisely the subvariety $\mathbb{V}(\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}})$ of symmetric Heyting algebras generated by $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ (Theorem 78); an equational presentation for $\mathbb{V}(\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}})$ is introduced in Definition 72, and shown to be sound and complete in Theorem 77. The algebraizability of Moisil’s logic (Proposition 71) entails that $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ is also algebraizable; its equivalent algebraic semantics is precisely $\mathbb{V}(\mathbf{PP_6^{\Rightarrow _{\textsf{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 _{\textsf{H}}}})$ (Theorem 78). On the other hand, $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ is not algebraizable (Proposition 36) but its algebraic counterpart is also $\mathbb{V}(\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}})$ ; the shape of the reduced matrix models of $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ is described in Proposition 81. We conclude the section by looking at the subvarieties of $\mathbb{V}(\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}})$ . There are only three of them (corresponding precisely to the self-extensional extensions of $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ ) which can be axiomatized by adding the axioms that translate the equations shown in Corollary 79.

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 _{\textsf{H}}}_\top$ . Further directions 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 expansions of a logic by the addition of an implication.

2.1 Algebras, languages, and logics

A propositional signature is a family $\Sigma \,{:=}\, \{\Sigma _k\}_{k \in \omega }$ , where each $\Sigma _k$ is a collection of $k$ -ary connectives. A $\Sigma$ -multialgebra is a structure $\mathbf{A} \,{:=}\, \langle A, \cdot ^{\mathbf{A}} \rangle$ , where $A$ is a non-empty set called the carrier of $\mathbf{A}$ and, for each $\unicode{x00A9} \in \Sigma _k$ , the multioperation $\unicode{x00A9}^{\mathbf{A}} : A^k \to \wp (A)$ is the interpretation of $\unicode{x00A9}$ in $\mathbf{A}$ . We say that $\mathbf{A}$ is a $\Sigma$ -algebra (or deterministic $\Sigma$ -multialgebra) when $\unicode{x00A9}^{\mathbf{A}}(a_1,\ldots, a_k)$ is a singleton for every $a_1,\ldots, a_k \in A$ , $\unicode{x00A9} \in \Sigma _k$ and $k \in \omega$ . If $\unicode{x00A9}^{\mathbf{A}}(a_1,\ldots, a_k) \neq \varnothing$ for every $a_1,\ldots, a_k \in A$ , $\unicode{x00A9} \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). Given $\Sigma ^\prime \subseteq \Sigma$ (i.e., $\Sigma ^\prime _k \subseteq \Sigma _k$ for all $k \in \omega$ ), the $\Sigma '$ -reduct of a $\Sigma$ -multialgebra $\mathbf{A}$ is the $\Sigma '$ -multialgebra over the same carrier of $\mathbf{A}$ that agrees with $\mathbf{A}$ on the interpretation of the connectives in $\Sigma '$ .

A $\Sigma$ -homomorphism between $\Sigma$ -multialgebras $\mathbf{A}$ and $\mathbf{B}$ is a mapping $h : A \to B$ such that $h(\unicode{x00A9}^{\mathbf{A}}(a_1,\ldots, a_k)) \in \unicode{x00A9}^{\mathbf{B}}(h(a_1),\ldots, h(a_k))$ for all $a_1,\ldots, a_k \in A$ , $\unicode{x00A9} \in \Sigma _k$ and $k \in \omega$ . Note that for $\Sigma$ -algebras this definition coincides with the usual notion of homomorphism. The collection of all $\Sigma$ -homomorphisms between two $\Sigma$ -multialgebras $\mathbf{A}$ and $\mathbf{B}$ is denoted by $\textsf{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 subformulas of a formula $\varphi$ is denoted by $\textsf{sub}(\varphi )$ and we let $\textsf{sub}(\Phi ) \,{:=}\, \bigcup _{\varphi \in \Phi }\textsf{sub}(\varphi )$ , for all $\Phi \subseteq L_{\Sigma }(P)$ . Similarly, the collection of all propositional variables occurring in $\varphi \in L_{\Sigma }(P)$ is denoted by $\textsf{props}(\varphi )$ , and we let $\textsf{props}(\Phi ) \,{:=}\, \bigcup _{\varphi \in \Phi }\textsf{props}(\varphi )$ , for all $\Phi \subseteq L_{\Sigma }(P)$ . The elements of $\textsf{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 $\textsf{End}(\mathbf{L}_{\Sigma }(P))$ . Given $h,h' \in \textsf{Hom}(\mathbf{L}_{\Sigma }(P), \mathbf{A})$ , we shall say that $h'$ agrees with $h$ on $\Phi \subseteq L_{\Sigma }(P)$ provided that $h'(\varphi )=h(\varphi )$ for all $\varphi \in \Phi$ . In case $p_1,\ldots, p_k$ are the only propositional variables occurring 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) \,{:=}\, \{ h(\varphi ) : h \in \textsf{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 resulting from substituting each $p_i$ in $\varphi$ by $\psi _i$ , for all $1 \leq i \leq k$ . For a set $\Theta$ of formulas $\varphi (p_1,\ldots, p_k)$ , we let $\Theta (\psi _1,\ldots, \psi _k) \,{:=}\, \{ \varphi (\psi _1,\ldots, \psi _k) : \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 \textsf{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 $\textsf{K}$ of $\Sigma$ -algebras, denoted by $\mathbb{V}(\textsf{K})$ , is the closure of $\textsf{K}$ under homomorphic images, subalgebras and direct products. We denote the latter operations, respectively, by $\mathbb{H}$ , $\mathbb{S}$ and $\mathbb{P}$ . We write $\textsf{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 ^{\textsf{bL}}$ the signature containing but two binary connectives, $\land$ and $\lor$ , and two nullary connectives $\top$ and $\bot$ , and by $\Sigma ^{\textsf{DM}}$ the extension of the latter signature by the addition of a unary connective $\sim$ . Moreover, by adding the unary connective $\nabla$ to $\Sigma ^{\textsf{DM}}$ we obtain a signature we shall call $\Sigma ^{\textsf{IS}}$ , and by adding instead the unary connective $\circ$ we obtain a signature we shall call $\Sigma ^{\textsf{PP}}$ . 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 1. Given a $\Sigma ^{\textsf{DM}}$ -algebra whose $\Sigma ^{\textsf{bL}}$ -reduct is a bounded distributive lattice, we say that it constitutes a De Morgan algebra if it satisfies the equations:

\begin{align*} \mathbf{(DM1)} \; {\sim }{\sim } x \approx x \qquad \mathbf{(DM2)} \; {\sim } (x \land y) \approx{\sim } x \lor{\sim } y \end{align*}

Example 1. Let $\mathcal{V}_4 \,{:=}\, \{{\mathbf{t}},{\mathbf{b}},{\mathbf{n}},{\mathbf{f}}\}$ and let $\mathbf{DM}_4 \,{:=}\, \langle \mathcal{V}_4, \cdot ^{\mathbf{DM}_4} \rangle$ be the $\Sigma ^{\textsf{DM}}$ -algebra known as the Dunn-Belnap lattice, whose interpretations for the lattice connectives are those induced by the Hasse diagram in Fig. 1(a), and the interpretation for $\sim$ is such that ${\sim }^{\mathbf{DM}_4}{\mathbf{f}} \,{:=}\,{\mathbf{t}}$ , ${\sim }^{\mathbf{DM}_4}{\mathbf{t}} \,{:=}\,{\mathbf{f}}$ and ${\sim }^{\mathbf{DM}_4} a \,{:=}\, a$ , for $a \in \{{\mathbf{n}},{\mathbf{b}}\}$ ; as expected, for the nullary connectives, we have $\top ^{\mathbf{DM}_4} \;\,{:=}\,\;{\mathbf{t}}$ and $\bot ^{\mathbf{DM}_4} \;\,{:=}\,\;{\mathbf{f}}$ . In Fig. 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).

Definition 2. Given a $\Sigma ^{\textsf{IS}}$ -algebra whose $\Sigma ^{\textsf{DM}}$ -reduct is a De Morgan algebra, we say that it constitutes an involutive Stone algebra (IS-algebra) if it satisfies the equations:

\begin{align*} \textbf{(IS1)} \; \nabla \bot \approx \bot \quad \textbf{(IS2)} \; x \land \nabla x \approx x\quad \textbf{(IS3)} \; \nabla (x \land y) \approx \nabla x \land \nabla y\quad \textbf{(IS4)} \; {\sim }\nabla x \land \nabla x \approx \bot \end{align*}

Example 2. Let $\mathcal{V}_6 \,{:=}\, \mathcal{V}_4 \cup \{{\hat{\mathbf{f}}},{\hat{\mathbf{t}}}\}$ and let $\mathbf{IS}_6 \,{:=}\, \langle \mathcal{V}_6, \cdot ^{\mathbf{IS}_6} \rangle$ be the $\Sigma ^{\textsf{IS}}$ -algebra whose lattice structure is depicted in Fig. 1(b) and interprets $\sim$ and $\nabla$ as per the following:

\begin{equation*} {\sim }^{\mathbf {IS}_6} a \,{:=}\, \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 \,{:=}\, \begin {cases} {\hat {\mathbf {t}}} & a \in \mathcal {V}_6\setminus \{{\hat {\mathbf {f}}}\}\\ {\hat {\mathbf {f}}} & a = {\hat {\mathbf {f}}}\\ \end {cases} \end{equation*}

The subalgebras of $\mathbf{IS}_6$ exhibited in Fig. 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 $\textsf{K}$ be a class of $\Sigma$ -algebras, with $\Sigma \supseteq \Sigma ^{\textsf{bL}}$ , whose $\{ \land, \top \}$ -reducts are meet-semilattices with a greatest element assigned to $\top$ . Given $\mathbf{A} \in \textsf{K}$ , we say that $\unicode{x00A9}$ is the residuum of $\land$ in $\mathbf{A}$ provided that $a \,\land ^{\mathbf{A}}\, b \leq c$ if, and only if, $a \leq b \,\unicode{x00A9}^{\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 pseudo-complement 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 pseudo-complement (unique by definition), we may think of $\neg ^{\mathbf{A}}$ as a unary operation, known as the pseudo-complement operation of $\mathbf{A}$ .

Figure 1. The subdirectly irreducible De Morgan (a) and the subdirectly irreducible IS-algebras (b).

We move now to the logical preliminaries. A 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 companion of a given Set-Set logic $\rhd$ is the 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$ ; that being the case, we say these sets are logically equivalent. We will adopt the convention of omitting curly braces when writing sets of formulas in statements involving (generalized) consequence relations. The complement of a given Set-Set logic $\rhd$ , that is, $(\wp L_{\Sigma }(P) \times \wp L_{\Sigma }(P)){\setminus }\rhd$ , will be denoted by $\blacktriangleright _{}$ .

Let $\rhd$ and $\rhd '$ be Set-Set logics over signatures $\Sigma$ and $\Sigma '$ , respectively, with $\Sigma \subseteq \Sigma '$ . We say that $\rhd '$ expands $\rhd$ when $\rhd ' \supseteq \rhd$ . When $\Sigma = \Sigma '$ , we say more simply that $\rhd '$ extends $\rhd$ . It is worth recalling that the collection of all extensions of a given logic forms a complete lattice under inclusion. We say that $\rhd '$ is a conservative expansion of $\rhd$ when $\rhd '$ expands $\rhd$ and, for all $\Phi, \Psi \subseteq L_{\Sigma }(P)$ , we have $\Phi \rhd ' \Psi$ if, and only if, $\Phi \rhd \Psi$ . The finitary companion of a Set-Set logic $\rhd$ is the Set-Set logic $\rhd _{\textsf{fin}}$ such that $\Phi \rhd _{\textsf{fin}} \Psi$ if, and only if, there are finite $\Phi ' \subseteq \Phi$ and $\Psi ' \subseteq \Psi$ such that $\Phi ' \rhd \Psi '$ . The latter concepts may be straightforwardly adapted to logics.

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 3. A logic $\rhd$ over the signature $\Sigma$ is called self-extensional (or congruential) if logical equivalence is compatible with each connective in the signature, that is, for every $\unicode{x00A9} \in \Sigma _k$ , it is the case that $\unicode{x00A9}(\varphi _1,\ldots, \varphi _k) \,{\lhd \rhd } \, \unicode{x00A9}(\psi _1,\ldots, \psi _k)$ whenever $\varphi _i \,{\lhd \rhd } \, \psi _i$ for every $1\leq i \leq k$ . For 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 $\textsf{Hom}(\mathbf{L}_{\Sigma }(P), \mathbf{A})$ are called $\mathfrak{M}$ -valuations. Every $\Sigma$ -PNmatrix determines a 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 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 companion of $\rhd _{\mathfrak{M}}$ ). Given a logic $\rhd$ (resp. a 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 (resp. ) logic determined by a class $\mathcal{M}$ of $\Sigma$ -matrices is given by $\bigcap \{\rhd _{\mathfrak{M}} : \mathfrak{M} \in \mathcal{M}\}$ (resp. $\bigcap \{\vdash _{\mathfrak{M}} : \mathfrak{M} \in \mathcal{M}\}$ ).

Example 3. The $\Sigma ^{\textsf{DM}}$ -matrix $\langle \mathbf{DM}_4, \{{\mathbf{b}},{\mathbf{t}} \} \rangle$ determines the logic known as the 4-valued Dunn-Belnap logic (Belnap 1977 ), or First-Degree Entailment, 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 ^{\textsf{DM}}$ -matrix $\langle \mathbf{DM}_2, \{{\mathbf{t}}\} \rangle$ (see Fig. 1(a)).

Given a $\Sigma$ -matrix $\mathfrak{M} = \langle \mathbf{A}, D \rangle$ , a congruence $\theta \in \textsf{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 with $\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 : 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 Fig. 1B). We may employ the same notation to write the designated set of a $\Sigma$ -matrix having a lattice as underlying algebra. 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 with classes of (ordered) algebras

Throughout this section, consider a propositional signature $\Sigma \supseteq \Sigma ^{\textsf{bL}}$ . In addition, for a set of $\Sigma$ -formulas $\Phi \,{:=}\, \{ \varphi _1,\ldots, \varphi _n \}$ , let $\bigwedge \Phi \,{:=}\, \varphi _1 \land \ldots \land \varphi _n$ and $\bigvee \Phi \,{:=}\, \varphi _1 \lor \ldots \lor \varphi _n$ , while, by convention, let $\bigwedge \varnothing \,{:=}\, \top$ and $\bigvee \varnothing \,{:=}\, \bot$ . Moreover, let the inequality $\varphi \leq \psi$ abbreviate the equation $\varphi \approx \varphi \land \psi$ .

Definition 4. Let $\textsf{K}$ be a class of $\Sigma$ -algebras such that each $\mathbf{A} \in \textsf{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 with $\textsf{K}$ , denoted by $\rhd _{\textsf{K}}^{\leq }$ , is such that $\Phi \, \rhd _{\textsf{K}}^{\leq } \, \Psi$ if, and only if, there are finite $\Phi '\subseteq \Phi$ and $\Psi '\subseteq \Psi$ such that $\bigwedge \Phi ' \leq \bigvee \Psi '$ is valid in $\textsf{K}$ .

For any order-preserving logic $\rhd _{\textsf{K}}^{\leq }$ associated with an appropriate class $\textsf{K}$ of algebras, the following characterization in terms of prime filters applies:

Proposition 5. $\rhd _{\textsf{K}}^{\leq }$ is the finitary companion of the logic determined by $ \mathcal{M^{{{\uparrow }\lor }}} \,{:=}\, \{ \langle \mathbf{A}, D \rangle : \mathbf{A} \in \textsf{K}\text{ and } D \text{ is a prime filter of $\mathbf{A}$}\}$ .

Proof. To start with, assume that $\Phi \rhd _{\textsf{K}}^{\leq }\Psi$ . So, (i) there are finite $\Phi '\subseteq \Phi$ and $\Psi '\subseteq \Psi$ such that $\Phi '\rhd _{\textsf{K}}^{\leq }\Psi '$ . Let $\langle \mathbf{A}, D \rangle \in \mathcal{M^{{{\uparrow }\lor }}}$ and $v \in \textsf{Hom}(\mathbf{L}_{\Sigma }(P), \mathbf{A})$ be a valuation. Assume that $v[\Phi '] \subseteq D$ . Thus $v(\bigwedge \Phi ') \in D$ , as $D$ is a lattice filter. By (i), we know that $v(\bigwedge \Phi ') \leq v(\bigvee \Psi ')$ , so $v(\bigvee \Psi ') \in D$ . Since $D$ is prime, we must have $v(\psi ) \in D$ for some $\psi \in \Psi '$ and we are done.

Conversely, assume that (ii) follows from in the finitary companion of $\rhd_{\mathcal{M}^{{{\uparrow }\lor }}}$ . Thus $\Phi ' \rhd _{\mathcal{M^{{{\uparrow }\lor }}}} \Psi '$ for finite $\Phi '\subseteq \Phi$ and $\Psi '\subseteq \Psi$ . Let $\mathbf A \in \textsf{K}$ and $v \in \textsf{Hom}(\mathbf{L}_{\Sigma }(P), \mathbf{A})$ . Let $a \,{:=}\, v(\bigwedge \Phi ')$ (note that $a = \top ^{\mathbf{A}}$ if $\Phi ' = \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 ')$ , that is, $v(\bigvee \Psi ') \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 ') \not \in D$ . Since $a \leq v(\varphi )$ for each $\varphi \in \Phi '$ , we have $v(\varphi ) \in{{\uparrow }a} \subseteq D$ , for all $\varphi \in \Phi '$ and, by (ii), we have $v(\psi ) \in D$ for some $\psi \in \Psi '$ . Since $v(\psi ) \leq v(\bigvee \Psi ')$ , we must have $v(\bigvee \Psi ') \in D$ . As this leads to a contradiction, we conclude that $a \leq v(\bigvee \Psi ')$ , 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 6. Let $\textsf{K} = \mathbb{V}(\{ \mathbf{B}\})$ , for $\mathbf{B}$ a finite distributive lattice. Then $\rhd _{\textsf{K}}^{\leq }$ is determined by $ \mathcal{M}^{{{\uparrow }\lor }}_{\textsf{fin}} \,{:=}\, \{ \langle \mathbf{B}, D \rangle : D \text{ is a prime filter of $\mathbf{B}$}\}$ .

Proof. As $\mathcal{M}^{{{\uparrow }}\lor }_{\textsf{fin}} \subseteq \mathcal{M}^{{{\uparrow }}\lor }$ , we have $\rhd _{\textsf{K}}^{\leq } \subseteq \rhd _{\mathcal{M}^{{{\uparrow }}\lor }_{\textsf{fin}}}$ . Conversely, suppose that $\Phi \; \,\blacktriangleright _{\textsf{K}}^{\leq } \; \Psi$ . Consider finite $\Phi ' \subseteq \Phi$ and $\Psi ' \subseteq \Psi$ . We want to show that $\Phi ' \,\blacktriangleright _{\mathcal{M}^{{{\uparrow }}\lor }_{\textsf{fin}}} \Psi '$ . By the hypothesis, we know that $\bigwedge \Phi ' \leq \bigvee \Psi '$ fails in $\textsf{K}$ , thus it fails in $\mathbf{B}$ , say under a valuation $v$ . Let $b \,{:=}\, v(\bigwedge \Phi ')$ . So, $b \not \leq v(\bigvee \Psi ')$ . Note that ${\uparrow }b$ must be proper. As $v(\bigvee \Psi ') \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 ') \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 '$ , as $v(\psi ) \leq v(\bigvee \Psi ')$ and $D$ is upwards closed, and $v(\varphi ) \in D$ for every $\varphi \in \Phi '$ . Therefore, $\Phi ' \,\blacktriangleright _{\mathcal{M}^{{{\uparrow }}\lor }_{\textsf{fin}}} \Psi '$ , as desired.

Definition 7. Let $\textsf{K}$ be a class of $\Sigma$ -algebras as in Definition 4 . The order-preserving logic induced by $\textsf{K}$ , which we denote by $\vdash _{\textsf{K}}^{\leq }$ , is such that $\Phi \vdash _{\textsf{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 $\textsf{K}$ .

Notice that $\vdash _{\textsf{K}}^{\leq }$ is the companion of $\rhd _{\textsf{K}}^{\leq }$ .

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

Proposition 8. $\rhd _{\textsf{K}}^{\leq }$ and $\vdash _{\textsf{K}}^{\leq }$ are self-extensional.

Proof. Directly from Jansana (2006, Sec. 3) and from the fact that $\vdash _{\textsf{K}}^{\leq }$ is the companion of $\rhd _{\textsf{K}}^{\leq }$ .

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

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

Notice that $\vdash ^{\top }_{\textsf{K}}$ is the companion of $\rhd ^\top _{\textsf{K}}$ .

2.3 Hilbert-style axiomatizations

Based on Shoesmith and Smiley (1978) and Caleiro and Marcelino (2019), we define a symmetrical (Hilbert-style) calculus $\textsf{R}$ (or 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 ) 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 finite bounded rooted tree $t$ is a finite poset $\langle \textsf{nds}(t), {\leq }^t \rangle$ with a single minimal element $\textsf{rt}(t)$ , the root of $t$ , such that, for each node $n \in \textsf{nds}(t)$ , the set $\{n' \in \textsf{nds}(t) : n' {\leq }^t n \}$ of ancestors of $n$ (or the branch up to $n$ ) is linearly ordered under ${\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 labeled. 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 ${\leq }^t$ are called the children of $n$ in $t$ .

Figure 2. Graphical representation of $\textsf{R}$ -derivations, where $\textsf{R}$ is a system. The dashed edges and blank circles represent other branches that may exist in the derivation. We usually omit the formulas inherited from the parent node, exhibiting only the ones introduced by the applied rule of inference. Recall that, in both cases, we must have $\Pi \subseteq \Phi$ .

Let $\textsf{R}$ be a symmetrical calculus. An $\textsf{R}$ -derivation is a finite labeled bounded rooted tree such that for every non-leaf node $n$ of $t$ there exists a rule of inference $\textsf{r} = \frac{\Pi }{\Theta } \in \textsf{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 : \varphi \in \sigma (\Theta )\}$ , in case $\Theta \neq \varnothing$ , where $n^\varphi$ is a node labeled with $l^{t}(n) \cup \{\varphi \}$ , or (ii) a singleton $\{n^\ast \}$ with $l^{t}(n^\ast )\;=\;\ast$ , in case $\Theta \;=\;\varnothing$ . Such node $n$ is said to be expanded by an application of $\textsf r$ . Fig. 2 illustrates the general shape of $\textsf{R}$ -derivations. We say that $\Phi \; \rhd _{\textsf{R}}\; \Psi$ whenever there is a $\Psi$ -closed derivation $t$ such that $\Phi \;\supseteq \;\textsf{rt}(t)$ ; such a tree consists in a proof that $\Psi$ follows from $\Phi$ in $\textsf{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, where we display some proof trees). The relation $\rhd _{\textsf{R}}$ so defined is a logic and, when $\rhd _{\textsf{R}} = \rhd$ , we say that $\textsf{R}$ axiomatizes $\rhd$ . It is worth emphasizing that we restrict ourselves to finite derivations because we are interested in finitary logics, but in general they could be infinite and cover also non-finitary logics (cf. Marcelino and Caleiro 2021, Figure 1, for an example). A rule $\frac{\Phi }{\Psi }$ is sound in a PNmatrix $\mathfrak{M}$ when $\Phi \;\rhd _{\mathfrak{M}}\;\Psi$ . It should be pointed out that this proof formalism generalizes the conventional () Hilbert-style calculi: the latter corresponds to symmetrical calculi whose rules have, each, a finite antecedent and a singleton as succedent.

Remark 10. Observe that any application of a rule of inference that creates a node labeled with the same set of formulas as the label of the node being expanded is superfluous (cf. Greati 2022, Prop. 35); in this way, loops in these derivations may be readily averted.

The process of building an $\textsf{R}$ -derivation, in principle, does not necessarily terminate, since there may be infinitely many rule instances that are applicable. We now introduce a notion of analyticity that allows a limit to be set on the search space in such a way that this process is guaranteed to finish. Given $\Lambda \subseteq L_{\Sigma }(P)$ , we write $\Phi \rhd _{\textsf{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 $\textsf{sub}(\Theta ) \cup \{ \sigma (\varphi ) : \varphi \in \Xi \mbox{ and } \sigma : P \to \textsf{sub}(\Theta )\}$ . We say that $\textsf{R}$ is $\Xi$ -analytic when, for all $\Phi, \Psi \subseteq L_{\Sigma }(P)$ , we always have $\Phi \rhd _{\textsf{R}}^{\Upsilon ^\Xi } \Psi$ whenever we have $\Phi \;\rhd _{\textsf{R}}\;\Psi$ ; intuitively, it means that proofs in $\textsf{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 the subformulas of $\Phi \cup \Psi$ . Searching for proofs in a finite $\Xi$ -analytic calculus is then guaranteed to terminate because (i) due to analyticity, there are finitely many rule instances to be considered when expanding a node and (ii) in view of Remark 10, loops may always be averted.

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 $\textrm{S}$ such that $\textrm{S}^{\mathbf{A}}(a) \in D$ and $\textrm{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-mentioned expressiveness requirement, with the following set of separators: $\mathcal{S} \,{:=}\, \{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 $\textsf{R}_{\mathcal{B}}$ :

\begin{equation*} \frac {}{\top }\,\textsf {r}_1 \quad \frac {\sim \top }{} \, {\textsf {r}_2} \quad \frac {}{\sim \bot }\, \textsf {r}_3 \quad \frac {\bot }{}\, \textsf {r}_4 \quad \frac {p}{\sim \sim p}\, \textsf {r}_5 \quad \frac {\sim \sim p}{p}\, \textsf {r}_6 \end{equation*}

\begin{equation*} \frac {p \land q}{p}\, \textsf {r}_7 \quad \frac {p \land q}{q}\, \textsf {r}_8 \quad \frac {p, q}{p \land q}\, \textsf {r}_9 \quad \frac {\sim p}{\sim (p \land q)}\, \textsf {r}_{10} \quad \frac {\sim q}{\sim (p \land q)}\, \textsf {r}_{11} \quad \frac {\sim (p \land q)}{\sim p, \sim q}\, \textsf {r}_{12} \end{equation*}

\begin{equation*} \frac {p}{p \lor q}\, \textsf {r}_{13} \quad \frac {q}{p \lor q}\,\textsf {r}_{14} \quad \frac {p \lor q}{p, q}\, \textsf {r}_{15} \quad \frac {\sim p, \sim q}{\sim (p \lor q)}\, \textsf {r}_{16} \quad \frac {\sim (p \lor q)}{\sim p}\,\textsf {r}_{17} \quad \frac {\sim (p \lor q)}{\sim q}\, \textsf {r}_{18} \end{equation*}

Fig. 3 illustrates proofs in $\textsf{R}_{\mathcal{B}}$ .

Remark 11. Avron et al. (2007) employed essentially the same sufficient expressiveness condition – further discussed in Caleiro and Marcos (2012)– as the one described above to provide cut-free sequent calculi for logics determined by finite non-deterministic matrices. In this work, we focus, instead, on Hilbert-style systems for their proximity with the logics being axiomatized (rules are simply consequence statements involving an antecedent and a succedent), which facilitates the algebraic study thereof. On what concerns the underlying decision procedures, we emphasize that analytic calculi admit straightforward (in general exponential-time) proof-search procedures.

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 and 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$ . In what follows, let $\bigvee \{ \psi _1,\ldots, \psi _m \} \,{:=}\, \psi _1 \lor (\psi _2 \lor \ldots (\ldots \lor \psi _n)\ldots )$ .

Figure 3. Proofs in $\textsf{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, r$ .

Definition 12. The connective $\Rightarrow$ is an implication in a logic $\rhd{}$ over $\Sigma _\Rightarrow$ provided, for all $\Phi, \{ \psi _1,\ldots, \psi _m \}, \{ \varphi, \psi \} \subseteq L_{\Sigma }(P)$ ,

\begin{equation*} \Phi, \varphi \rhd \psi, \psi _1,\ldots, \psi _m \text { if, and only if, } \Phi \rhd \varphi \Rightarrow \left (\bigvee \{\psi, \psi _1,\ldots, \psi _m \}\right ). \end{equation*}

Note that the above definition reduces in 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 , in this paper. That is, $\vdash$ has the DDT with respect to $\Rightarrow$ in case $\Phi, \varphi \vdash \psi$ if, and only if, $\Phi \vdash \varphi \Rightarrow \psi$ for all $\Phi, \{ \varphi, \psi \} \subseteq L_{\Sigma }(P)$ . What we did above was a convenient generalization of the DDT for logics, using it to abstractly characterize what we expect of an implication connective (namely, an internalization of the consequence relation that allows formulas to be discharged from the antecedent).

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

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

\begin{equation*} \Phi, \varphi \rhd \psi, \Psi \text { if, and only if, } \Phi \rhd \varphi \Rightarrow \psi, \Psi . \end{equation*}

It should be clear enough that, for logics $\rhd$ with $\lor$ satisfying $p \rhd p \lor q$ ; $q \rhd p \lor q$ ; and $p \lor q \rhd p,q$ , classic-like implications are implications in the sense of Definition 12. The converse, however, might not hold (see Remark 32).

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

1. $(\textsf{I}1)$ The connective being added must qualify as an implication (Definition 12);

2. $(\textsf{I}2)$ The expansion must be conservative.

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

Proposition 14. Let $\Rightarrow ^{\mathbf{A}}$ be the residuum of $\land ^{\mathbf{A}}$ in each $\mathbf{A} \in \textsf{K}$ , where $\textsf{K}$ is a class of $\Sigma _\Rightarrow$ -algebras, with $\Sigma _\Rightarrow \supseteq \Sigma ^{\textsf{bL}}$ , whose $\{ \land, \top \}$ -reducts are $\land$ -semilattices with a greatest element assigned to $\top$ . Then $\Rightarrow$ is an implication in $\rhd _{\textsf{K}}^{\leq }$ (recall Definition 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 _{\textsf{K}}^{\leq } \Psi$ . Then $\Phi ' \rhd _{\textsf{K}}^{\leq } \Psi '$ , for finite $\Phi ' \subseteq \Phi \cup \{ \varphi \}$ and $\Psi ' \subseteq \Psi$ , and thus ( $\star$ ) $\Phi '',\varphi \rhd _{\textsf{K}}^{\leq } \Psi '$ , for $\Phi ' \cup \{ \varphi \} = \Phi '' \cup \{ \varphi \}$ and $\varphi \not \in \Phi ''$ . Let $\mathbf{A} \in \textsf{K}$ . By ( $\star$ ), we have that $\bigwedge \Phi '' \land \varphi \leq \bigvee \Psi '$ is valid in $\mathbf{A}$ , thus $\bigwedge \Phi '' \land \varphi \leq \bigvee \Psi$ is valid in $\mathbf{A}$ ; hence, by residuation, $\bigwedge \Phi '' \leq \varphi \Rightarrow \bigvee \Psi$ is valid in $\mathbf{A}$ , thus $\Phi \rhd _{\textsf{K}}^{\leq } \varphi \Rightarrow \bigvee \Psi$ . From the right to the left, suppose that $\Phi \rhd _{\textsf{K}}^{\leq } \varphi \Rightarrow \bigvee \Psi$ . Then, by definition, we have that $\Phi ' \rhd _{\textsf{K}}^{\leq } \varphi \Rightarrow \bigvee \Psi$ , for some finite $\Phi ' \subseteq \Phi$ . Let $\mathbf{A} \in \textsf{K}$ . We have that $\bigwedge \Phi ' \leq \varphi \Rightarrow \bigvee \Psi$ is valid in $\mathbf{A}$ . By residuation, we have $\bigwedge \Phi ' \land \varphi \leq \bigvee \Psi$ also valid in $\mathbf{A}$ , from which we easily obtain that $\Phi, \varphi \rhd _{\textsf{K}}^{\leq } \Psi$ .

Observe that the above result extends to $\vdash _{\textsf{K}}^{\leq }$ (recall Definition 7) since it is the companion of $\rhd _{\textsf{K}}^{\leq }$ . This also looks like the right moment to introduce intuitionistic-like implications:

Definition 15. A Heyting implication in an algebra $\mathbf{A} \in \textsf{K}$ , with $\textsf{K}$ as described in Proposition 14 , 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:

1. $(\textsf{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$ .

2. $(\textsf{A}2)$ The expanded logic is self-extensional (Definition 3).

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

Proposition 16. Let $\mathfrak{M} \,{:=}\, \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 $(\textsf{A}1)$ .

Proof. We have that $\Phi, \varphi \, \,\blacktriangleright _{\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 \,\,\blacktriangleright _{\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 with them. Most of the materials come from Gomes et al. (2022), where these objects were first introduced and investigated.

Definition 17. Given a $\Sigma ^{\textsf{PP}}$ -algebra whose $\Sigma ^{\textsf{DM}}$ -reduct is a De Morgan algebra, we say that it constitutes a perfect paradefinite algebra (PP-algebra) if it satisfies the equations:

\begin{align*} & \mathbf{(PP1)}\;{\circ }{\circ } x \approx \top \qquad \mathbf{(PP2)} \circ x \approx \circ{\sim } x \qquad \mathbf{(PP3)}\;{\circ } \top \approx \top \qquad \mathbf{(PP4)}\; x \land{\sim } x \land{\circ } x \approx \bot \\ & \mathbf{(PP5)} \circ (x \land y) \approx (\circ x \lor \circ y) \land (\circ x \lor{\sim } y) \land (\circ y \lor{\sim } x) \end{align*}

Example 6. An example of PP-algebra is $\mathbf{PP}_6 \,{:=}\, \langle \mathcal{V}_6, \cdot ^{\mathbf{PP}_6} \rangle$ , the $\Sigma ^{\textsf{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$ :

\begin{equation*} {\circ }^{\mathbf {PP}_6} a \,{:=}\, \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} \end{equation*}

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 Fig. 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 \,{:=}\, 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 \;\,{:=}\,\;{\sim } x \land{\circ } x$ (alternatively, one might simply set $\neg x \;\,{:=}\,\;{\sim }\nabla x$ , as usual).

We shall denote by $\mathcal{PP}_{\!\leq }^{{\rhd }}$ and $\mathcal{PP}_{\!\leq }$ , respectively, the and order-preserving logics induced by $\mathbb{PP}$ (cf. Subsection 2.2). In addition, we shall denote by $\mathcal{PP}_{\top }^{{\rhd }}{}$ and $\mathcal{PP}_\top{}$ , respectively, the and $\top$ -assertional logics induced by $\mathbb{PP}$ . We know that $\mathcal{PP}_{\!\leq }^{{\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). We will sometimes refer to as

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

Definition 18. Let $\textsf{R}_{\mathcal{PP}_{\!\leq }^{{\rhd }}}$ be the calculus containing the rules in Example 5 together with the following rules:

\begin{align*} \frac{}{\circ \bot }\, \textsf{r}_{19} && \frac{}{\circ \top }\, \textsf{r}_{20} && \frac{}{\circ \circ p}\, \textsf{r}_{21} && \frac{\circ p }{\circ \sim p}\, \textsf{r}_{22} && \frac{\circ \sim p }{\circ p}\, \textsf{r}_{23} && \frac{\circ p}{p, \sim p}\, \textsf{r}_{24} && \frac{\circ p, p, \sim p}{}\,\textsf{r}_{25} \end{align*}

\begin{align*} \frac{\circ p}{\circ (p \land q), p}\, \textsf{r}_{26} && \frac{\circ q}{\circ (p \land q), q}\, \textsf{r}_{27} && \frac{\circ (p \land q), q}{\circ p}\, \textsf{r}_{28} && \frac{\circ (p \land q), p}{\circ q}\, \textsf{r}_{29} && \frac{\circ p, \circ q}{\circ (p \land q)}\, \textsf{r}_{30} && \frac{\circ (p \land q)}{\circ p, \circ q}\, \textsf{r}_{31} \end{align*}

\begin{align*} \frac{\circ p, \circ q}{\circ (p \lor q)}\, \textsf{r}_{32} && \frac{\circ (p \lor q)}{\circ p, \circ q}\, \textsf{r}_{33} && \frac{\circ p, p}{\circ (p \lor q)}\, \textsf{r}_{34} && \frac{\circ q, q}{\circ (p \lor q)}\, \textsf{r}_{35} && \frac{\circ (p \lor q)}{\circ p, q}\, \textsf{r}_{36} && \frac{\circ (p \lor q)}{\circ q, p}\, \textsf{r}_{37} \end{align*}

In the mentioned paper, the above calculus was transformed into a 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 $\textsf{r}_{24}$ and $\textsf{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 }^{{\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 and , respectively) – in a language containing a “possibility” operator definable by setting $\nabla x \,{:=}\, x \lor{\sim }{\circ } x$ , as above.

Proposition 19 (Gomes et al. 2022, Prop. 3.12). $\mathcal{PP}_{\top }^{{\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 }^{{\rhd }}$ and $\mathcal{PP}_{\!\leq }$ by Adding a Classic-Like Implication to Their Matrix

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

1. $(\textsf{A}1)$ $a \Rightarrow _{\textsf{A}} b \subseteq{{\uparrow }{\mathbf{b}}}$ if, and only if, either $a \not \in{{\uparrow }{\mathbf{b}}}$ or $b \in{{\uparrow }{\mathbf{b}}}$ .

2. $(\textsf{A}2)$ The resulting logic $\rhd _{\langle \mathbf{PP_6^{\Rightarrow _{\textsf{A}}}},{{\uparrow }{\mathbf{b}}} \rangle }$ is self-extensional.

This path soon leads to a dead end, since:

Theorem 20. There is no multialgebra $\mathbf{PP_6^{\Rightarrow _{\textsf{A}}}}$ simultaneously satisfying conditions $(\textsf{A}1)$ and $(\textsf{A}2)$ .

Proof. Let $\Rightarrow _{\textsf{A}}$ be an implication defined in $\mathbf{PP_6}$ that satisfies $(\textsf{A}1)$ and $\mathfrak{M}^{\Rightarrow _{\textsf{A}}} \,{:=}\, \langle \mathbf{PP_6^{\Rightarrow _{\textsf{A}}}},{{\uparrow }{\mathbf{b}}} \rangle$ . Then, ( $\star$ ) we have $\rhd _{\mathfrak{M}^{\Rightarrow _{\textsf{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 \bot ) \in v(p ) \Rightarrow v(\bot ) \subseteq{{\uparrow }{\mathbf{b}}}$ by $(\textsf{A}1)$ .

Note that, for a valuation $v$ such that $v(p) ={\mathbf{b}}$ , using $(\textsf{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 $\,\blacktriangleright _{\mathfrak{M}^{\Rightarrow _{\textsf{A}}}} \, {\circ} (p \lor (p \Rightarrow \bot ))$ .

This prevents the logic from being self-extensional. Indeed, assuming $(\textsf{A}2)$ , from ( $\star$ ) 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 _{\textsf{A}}}} \, {\circ} \top$ , we would conclude that $\rhd _{\mathfrak{M}^{\Rightarrow _{\textsf{A}}}} \, \circ (p \lor (p \Rightarrow \bot ))$ , against what we have shown.

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

The space of binary multioperations over $\mathcal{V}_6$ satisfying $(\textsf{A}1)$ is finite but very large, consisting of total refinements¹ of the multioperation $\Rightarrow _{\textsf{A1}}$ defined as:

\begin{equation*} \Rightarrow _{\textsf {A1}}(a, b) \,{:=}\, \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} \end{equation*}

Denote by $\mathbf{PP_6}^{\!\!\Rightarrow _{\textsf{A1}}}$ the multialgebra obtained from $\mathbf{PP_6}$ by expanding its signature with $\Rightarrow$ and interpreting this connective as $\Rightarrow _{\textsf{A1}}$ . Let $\mathfrak{M}^{\Rightarrow _{\textsf{A1}}} \,{:=}\, \langle \mathbf{PP_6}^{\Rightarrow _{\textsf{A1}}},{{\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 }^{{\rhd }}$ by a classic-like implication; but let us first present an analytic axiomatization for it.

Definition 21. Let $\textsf{R}_{\mathfrak{M}^{\Rightarrow _{\textsf{A1}}}}$ be the calculus given by all inference rules in $\textsf{R}_{\mathcal{PP}_{\!\leq }^{{\rhd }}}$ plus the following three inference rules:

\begin{equation*} \frac {q}{p\Rightarrow q}\, \textsf {r}_1^{\mathcal {CL}} \qquad \frac {}{p, p\Rightarrow q}\, \textsf {r}_2^{\mathcal {CL}} \qquad \frac {p, p\Rightarrow q}{q}\, \textsf {r}_3^{\mathcal {CL}} \end{equation*}

Remark 22. The rule $\textsf{r}_2^{\mathcal{CL}}$ is responsible for the classicality of $\Rightarrow$ in $\textsf{R}_{\mathfrak{M}^{\Rightarrow _{\textsf{A1}}}}$ . One may observe, in particular, that in the presence of this rule, the connective defined by setting $\neg p := p \Rightarrow \bot$ satisfies the “law of excluded middle” ( $p \lor \neg p$ is provable).

In a PNmatrix $\mathfrak{M} \,{:=}\, \langle \mathbf{A}, D \rangle$ , a set $\mathcal{S}_a$ of unary formulas is said to isolate $a \in A$ if for every $b \neq a \in A$ there is in $\mathcal{S}_a$ a separator 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$ , where $\textrm{S}^{\mathbf{A}}(a) \subseteq D$ whenever $\textrm{S} \in \Omega _{a}$ , and $\textrm{S}^{\mathbf{A}}(a) \subseteq \overline D$ whenever $\textrm{S} \in \mho _{a}$ . We say that a PNmatrix is monadic in case there is a discriminator for it. Discriminators play an essential role in the axiomatization of monadic PNmatrices, as we shall see in the following results.

Theorem 23. $\textsf{R}_{\mathfrak{M}^{\Rightarrow _{\textsf{A1}}}}$ is $\{ p,{\sim }p,{\circ }p \}$ -analytic and axiomatizes $\rhd _{\mathfrak{M}^{\Rightarrow _{\textsf{A1}}}}$ .

Proof. We consider the axiomatization method presented by Marcelino and Caleiro (2021, Theorems 3.5 and 3.12), which can be applied because $\mathfrak{M}^{\Rightarrow _{\textsf{A1}}}$ is monadic, with the same discriminator as that of $\mathfrak{M}_6$ (see Table 1). The method can be seen essentially as a process of refining fully indeterministic six-valued interpretations of the connectives (i.e., 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 _{\textsf{A1}}}$ ). For the connectives $\land, \lor, {\sim }$ and $\circ$ , the method produces the calculus $\textsf{R}_{\mathcal{PP}_{\!\leq }^{{\rhd }}}$ after some simplifications (Gomes et al. 2022). Thus, since the method is modular on the connectives, we only need to check what happens when we run it on the new connective $\Rightarrow _{\textsf{A1}}$ and then add the resulting rules to $\textsf{R}_{\mathcal{PP}_{\!\leq }^{{\rhd }}}$ . The rules that are imposed will have the following shape:

\begin{equation*} \frac {\Omega _{a}(p),\Omega _{b}(q),\Omega _{c}(p \Rightarrow q)}{\mho _{a}(p), \mho _{b}(q), \mho _{c}(p \Rightarrow q)} \end{equation*}

for each $c \in \mathcal{V}_6{\setminus } (a \Rightarrow _{\textsf{A1}} 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 in Table 1:

Table 1. Discriminator for $\mathfrak{M}^{\Rightarrow _{\textsf{A1}}}$ . 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 $\textsf{R}_{\mathfrak{M}^{\Rightarrow _{\textsf{A1}}}}$ . However, we will see below that each of them is a “dilution” of one of the latter (i.e., 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 _{\textsf{A1}} b$ for $b \in{{\uparrow }{\mathbf{b}}}$ . The values $c \in \mathcal{V}_6{\setminus } (a \Rightarrow _{\textsf{A1}} 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 $\textsf{r}_1^{\mathcal{CL}}$ .

Second, consider the entries of $a \Rightarrow _{\textsf{A1}} b$ for $a \not \in{{\uparrow }{\mathbf{b}}}$ . The values $c \in \mathcal{V}_6{\setminus } (a \Rightarrow _{\textsf{A1}} 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 $\textsf{r}_2^{\mathcal{CL}}$ .

Finally, consider the entries of $a \Rightarrow _{\textsf{A1}} b$ for $a \in{{\uparrow }{\mathbf{b}}}$ and $b \not \in{{\uparrow }{\mathbf{b}}}$ . The values $c \in \mathcal{V}_6{\setminus } (a \Rightarrow _{\textsf{A1}} 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 $\textsf{r}_3^{\mathcal{CL}}$ .

Remark 24. For a discriminator in the language of involutive Stone algebras, check Cantú and Figallo (2022, Prop. 4.3).

Remark 25. The above result could have been obtained by another strategy, observing that $\rhd _{\mathfrak{M}^{\Rightarrow _{\textsf{A1}}}}$ 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 _{\textsf{A1}}}}$ is the disjoint fibring of $\mathcal{PP}_{\!\leq }^{{\rhd }}$ and $\rhd _{\mathfrak{M}_2}$ (i.e., the smallest logic in the signature $\Sigma _\Rightarrow$ extending both logics). One can then show that, because both logics have analytic 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 21, the desired result follows.

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

Proposition 26. Let $\rhd$ be a conservative expansion of $\mathcal{PP}_{\!\leq }^{{\rhd }}$ over $\Sigma ^{\textsf{PP}}_\Rightarrow$ in which $\Rightarrow$ is a classic-like implication. Then $\rhd _{\mathfrak{M}^{\Rightarrow _{\textsf{A1}}}} \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 _{\textsf{A1}}}}$ , and this is all we need for the present result.

We observe that each proper refinement of $\Rightarrow _{\textsf{A1}}$ produces a proper extension of $\rhd _{\mathfrak{M}^{\Rightarrow _{\textsf{A1}}}}$ . 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 _{\textsf{A1}}}$ to obtain rules that hold in it but not in $\textsf{R}_{\mathfrak{M}^{\Rightarrow _{\textsf{A1}}}}$ , 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 27. Let $\mathfrak{M}$ be obtained from $\mathfrak{M}^{\Rightarrow _{\textsf{A1}}}$ by refining $\Rightarrow _{\textsf{A1}}$ . Then $\textsf{R}_{\mathfrak{M}^{\Rightarrow _{\textsf{A1}}}}$ with the following rules provide a $\{ p,{\sim }p,{\circ }p \}$ -analytic calculus for $\mathfrak{M}$ :

\begin{equation*} \frac {\Omega _{a}(p), \Omega _{b}(q), \Omega _{c}(p \Rightarrow q) }{\mho _{a}(p), \mho _{b}(q), \mho _{c}(p \Rightarrow q) } \end{equation*}

for each $c \in (a \Rightarrow _{\textsf{A1}} 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, Theorems 3.5 and 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 _{\textsf{A1}}{\hat{\mathbf{f}}}$ , we axiomatize the resulting logic by adding the following rule:

\begin{equation*} \frac {p, \sim p, \circ q }{\circ p, q, p \Rightarrow q, \sim (p \Rightarrow q), \circ (p \Rightarrow q)}, \end{equation*}

which clearly does not hold in $\mathfrak{M}^{\Rightarrow _{\textsf{A1}}}$ 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 ${\textrm{LET}_{\textrm{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 _{\textsf{A1}}}$ . In fact, its implication is given by the following truth table:

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

\begin{equation*} \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} \end{equation*}

\begin{equation*} \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)} \end{equation*}

The attentive reader will notice that they are not quite the same rules as the ones produced by the recipe in Proposition 27. In fact, they are simplifications thereof, following the streamlining procedures described in Marcelino and Caleiro (2021). Still, it is not hard to confirm that these rules produce the desired refinements of $\Rightarrow _{\textsf{A1}}$ 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 20, as we proceed to expand our logic with an implication we shall necessarily have to drop either $(\textsf{A}1)$ or $(\textsf{A}2)$ . In this section we explore the first option, that is, we stick to $(\textsf{A}2)$ while dropping $(\textsf{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 8) is to consider, as in the implication-less case, the 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), when a conjunction is present, every self-extensional logic turns out to be the consequence associated with a suitably defined partial order. We shall thus 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 – that is one satisfying both $(\textsf{A}1)$ and $(\textsf{A}2)$ – we suggest introducing 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 _{\textsf{H}}$ ), which is precisely the relative pseudo-complement operation.

Definition 28. Let $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ be the algebra obtained by expanding $\mathbf{PP_6}$ with the operation $\Rightarrow _{\textsf{H}}$ defined as follows:

\begin{equation*} a \Rightarrow _{\textsf {H}} b \,{:=}\, \max \{ c \in \mathcal {V}_6 : a \land ^{\mathbf {PP_6}} c \leq b \}, \text { for all $a,b \in \mathcal {V}_6$.} \end{equation*}

In accordance with the above definition, the truth table of the implication in $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ looks as follows:

$\mathbf{PP_6^{\Rightarrow _{\textsf{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).² Indeed, since $\mathbf{PP_6^{\Rightarrow _{\textsf{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 bit more specific, observing that $\mathbf{PP_6^{\Rightarrow _{\textsf{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 29. 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 _{\textsf{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 single 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 _{\textsf{H}}{\mathbf{b}}) \theta ({\mathbf{b}} \Rightarrow _{\textsf{H}}{\mathbf{n}})$ ).

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

Theorem 30. The $\Sigma _\Rightarrow$ -logic induced by $\mathfrak{M}_6$ expanded with $\Rightarrow _{\textsf{H}}$ is axiomatized by the $\{ p,{\sim }p,{\circ }p \}$ -analytic calculus given by $\textsf{R}_{\mathcal{PP}_{\!\leq }^{{\rhd }}}$ plus the following rules:

\begin{equation*} \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} \end{equation*}

\begin{equation*} \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)} \end{equation*}

\begin{equation*} \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} \end{equation*}

\begin{equation*} \frac {\circ q}{\circ (p \Rightarrow q)} \qquad \frac {q}{\sim (p \Rightarrow q),\circ (p \Rightarrow q),\circ p} \end{equation*}

Note however that $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}},{{\uparrow }{\mathbf{b}}} \rangle$ does not satisfy $(\textsf{A}1)$ : pick for instance $a \,{:=}\,{\mathbf{f}}$ and $b \,{:=}\,{\hat{\mathbf{f}}}$ . As for $(\textsf{A}2)$ , we note that self-extensionality also fails. To see why, consider the formula $\varphi :={\sim } (p \Rightarrow q) \land{\sim } (q \Rightarrow p )$ , and recall that $\nabla x \,{:=}\, x \lor{\sim }{\circ } x$ . While it is clear that both $\varphi$ and $\nabla \bot$ are logically equivalent to $\bot$ , the same does not hold for $\nabla \varphi$ . 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 _{\textsf{H}}}}}({\sim }^{\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}} ({\mathbf{b}} \Rightarrow ^{\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}}{\mathbf{n}}) \land ^{\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}}{\sim }^{\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}} ({\mathbf{n}} \Rightarrow ^{\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}}{\mathbf{b}} )) ={\hat{\mathbf{t}}}$ . It follows that $\varphi \;{\lhd \rhd } \;\bot$ holds good, while $\nabla \varphi \;{\lhd \rhd } \;\nabla \bot$ does not hold. In fact, as we are going to show in Proposition 35, there is only one self-extensional logic determined by a class of matrices based on the algebra $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ and principal filters.

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

Proposition 31. $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\!\leq }$ and $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ are conservative expansions of $\mathcal{PP}_{\!\leq }^{{\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 6), while self-extensionality follows from Proposition 8.

Remark 32. Observe that $p \lor q \rhd _{{\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\!\leq }}} p, q$ (by the above proposition), while $\,\blacktriangleright _{{\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\!\leq }}} (p \lor q) \Rightarrow p, q$ (take a valuation $v$ such that $v(p) :={\mathbf{b}}$ and $v(q) :={\mathbf{n}}$ ), showing that $\Rightarrow _{\textsf{H}}$ is not a classic-like implication in $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\!\leq }$ (recall Definition 13). This is one of the main reasons for which we chose Definition 12 as a more general notion of implication in instead of the one in Definition 13.

We may actually improve Proposition 31 by removing some redundancies from the classes of matrices that characterize the logics thereby considered:

Proposition 33. The logics $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\!\leq }$ and $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ are determined by the class of matrices $\{ \langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}},{{\uparrow }{\mathbf{f}}} \rangle, \langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}},{{\uparrow }{\mathbf{b}}} \rangle, \langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}},{{\uparrow }{\hat{\mathbf{t}}}} \rangle \}$ . Moreover, all the latter matrices are reduced.

Proof. Note that any matrix $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}, D \rangle$ with $D \neq \mathcal{V}_6$ is reduced, because $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ is a simple algebra. Regarding $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\!\leq }$ , we observe that two of the matrices appearing in Proposition 6 may be safely omitted. Obviously this holds for $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}},{{\uparrow }{\hat{\mathbf{f}}}} \rangle$ , which defines a trivial logic. Note further that $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}},{{\uparrow }{\mathbf{b}}} \rangle$ and $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}},{{\uparrow }{\mathbf{n}}} \rangle$ are isomorphic, and thus determine the same logic; so one of them may also be omitted. Finally, note that the matrix with set of designated values ${\uparrow }{\mathbf{t}}$ is not considered as we only need to take prime filters into account. Thus only the matrices listed in the statement remain. Regarding $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ , the result follows from the observation that $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ is the companion of the order-preserving logics.

There is another logic that has $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ as companion, namely the one determined by the class of matrices based on the algebra $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ having as designated sets the principal filters of $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ . We shall denote this logic by $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\textsf{up}}$ . By a similar argument to the one above, we see that $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\textsf{up}}$ is determined by the class of matrices $\{ \langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}},{{\uparrow }{\mathbf{f}}} \rangle, \langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}},{{\uparrow }{\mathbf{b}}} \rangle, \langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}},{{\uparrow }{\mathbf{t}}} \rangle, \langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}},{{\uparrow }{\hat{\mathbf{t}}}} \rangle \}$ – that is, the matrices from Proposition 33 together with the matrix $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}},{{\uparrow }{\mathbf{t}}} \rangle$ . In this logic, however, $\Rightarrow$ is not an implication in our sense, since $\rhd _{\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\textsf{up}}} (p \lor q) \Rightarrow (p \lor q)$ , but $p \lor q \, \,\blacktriangleright _{{\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\textsf{up}}}}\, p,q$ . Still, we will include $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\textsf{up}}$ in our next considerations in view of its close relationship with $\mathcal{PP}^{\Rightarrow _{\textsf{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 $\mathcal{PP}_{\!\leq }$ ): the next result rules out this possibility.

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

Proof. Since the two logics share the same companion $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ , it is enough to prove that the latter is not determined by a single logical matrix. To that effect, we use the fact that any logic $\vdash$ that is determined by a single logical matrix respects the so-called uniformity property (cf. Wójcicki 1969), according to which $\Phi, \Psi \vdash \varphi$ implies $\Phi \vdash \varphi$ for all $\Phi \cup \Psi \cup \{ \varphi \} \subseteq L_{\Sigma }(P)$ such that (1) $\textsf{props}(\Phi \cup \{ \varphi \}) \cap \textsf{props}(\Psi ) = \varnothing$ and (2) $\Psi \not \vdash \psi$ for some $\psi \in L_{\Sigma }(P)$ .

Consider now $\Phi := \varnothing$ , $\Psi := \{ p \land{\sim } p \land q \land{\sim } q \land{\sim }{\circ }(p \Rightarrow q) \}$ and $\varphi := r \lor{\sim } r$ . Condition (1) is obviously satisfied. To see that condition (2) is also satisfied, one may consider the matrix $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}},{{\uparrow }{\mathbf{f}}} \rangle$ , and to see that $\not \vdash _{\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }} r \lor{\sim } r$ it suffices to consider the matrix $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}},{{\uparrow }{\mathbf{b}}} \rangle$ . Yet, one may now use the semantics of the order-preserving logic associated with $\mathbb{V}(\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}})$ to confirm that $p \land{\sim } p \land q \land{\sim } q \land{\sim }{\circ }(p \Rightarrow q) \vdash _{{\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }}} r \lor{\sim } r$ .

As earlier anticipated, we now proceed to show that $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ is actually the only self-extensional logic determined by a class of matrices based on the algebra $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ and principal filters.

Proposition 35. For $ \mathcal{V} \subseteq \mathcal{V}_6$ , let $\vdash _{\mathcal{V}}$ be the logic determined by $\left \{ \langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}},{\uparrow } a \rangle : a \in \mathcal{V} \right \}$ . If the logic $\vdash _{\mathcal{V}}$ is self-extensional, then $\vdash _{\mathcal{V}} \, = \,{\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }}$ .

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

Adopting the terminology of Jansana (2006), we may say that $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ is semilattice-based relative to $\land$ and to $\mathbb{V}(\mathbf{PP_6^{\Rightarrow _{\textsf{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 _{\textsf{H}}}_{\!\leq }$ is precisely $\mathbb{V}(\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}})$ . Semilattice-based logics are often non-algebraizable but have an algebraizable companion, that is, an extension that shares the same algebraic models. We establish this for $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ below.

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

\begin{equation*}\Xi (x,y) \,{:=}\, \{ x \Rightarrow y, y \Rightarrow x, \circ (x \Rightarrow y), \circ (y \Rightarrow x) \}\end{equation*}

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

\begin{equation*}\Xi (x,y) \,{:=}\, \{ \Delta (x \Rightarrow y), \Delta (y \Rightarrow x) \}. \end{equation*}

Proof. To prove that $\mathcal{PP}^{\Rightarrow _{\textsf{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 _{\textsf{H}}}_{\!\leq }}} \Xi (x,x)$

2. 2. $x, \Xi (x,y) \vdash _{{\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }}} y$

3. 3. $\Xi (x,y) \vdash _{{\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }}} \Xi ( \circ x, \circ y)$ and $\Xi (x,y) \vdash _{{\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }}} \Xi ({\sim } x,{\sim } y)$

4. 4. $\Xi (x_1,y_1), \Xi (x_2,y_2) \vdash _{{\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }}} \Xi ( x_1 \unicode{x00A9} x_2, y_1 \unicode{x00A9} y_2)$ for every binary connective $\unicode{x00A9}$ ; in the signature.

The verification of the above conditions is straightforward from the matrix characterization of $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ . Now, if $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ were algebraizable, then each set of designated elements would be equationally definable on the corresponding reduced matrix (see Font 2016, Def. 6.90). But this is not the case, because the matrices $\{ \langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}},{{\uparrow }a} \rangle : 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 _{\textsf{H}}}_{\!\leq }$ is the $\top$ -assertional logic associated with the variety $\mathbb{V}(\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}})$ , which we denote by $\mathcal{PP}^{\Rightarrow _{\textsf{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 _{\textsf{H}}}})$ . One easily verifies that $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ satisfies the following rules – any of them being in fact sufficient to distinguish $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ from $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ (given that they are sound in the former but not in the latter):

\begin{equation*} \frac {p} {\Delta p} \qquad \frac {p} {\circ p} \qquad \frac {p \Rightarrow q } {{\sim } q \Rightarrow {\sim } p} \qquad \frac {p, \ p \Rightarrow _{\textsf {W}} q } {q} \end{equation*}

where $p \Rightarrow _{\textsf{W}} q \,{:=}\,{\sim } p \lor{\sim }{\circ } p \lor q$ and $\Delta p \,{:=}\, p \land{\circ } p$ .

5.1 Characterizability by single finite PNmatrices

We saw in Theorem 34 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 both $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\textsf{up}}$ and $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\!\leq }$ are characterized by single finite PNmatrices. In consequence, $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ will be characterized by either of these matrices. 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} \,{:=}\, \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 \,{:=}\, \langle A \cap X, \cdot ^{\mathbf{A}_X} \rangle$ is a $\Sigma$ -multialgebra such that $\unicode{x00A9}^{\mathbf{A}_X}(a_1,\ldots, a_k) \,{:=}\, \unicode{x00A9}^{\mathbf{A}}(a_1,\ldots, a_k) \cap X$ for all $a_1,\ldots, a_k \in X$ , $k \in \omega$ and $\unicode{x00A9} \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 : 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 precisely the ones in the classes that determine the logics $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\textsf{up}}$ and $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\!\leq }$ .

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

Below we depict the structure of the PNmatrix $\mathfrak{M}_{\textsf{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.

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}_{\textsf{up}}$ .

The PNmatrix for $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{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}_{\textsf{up}}$ and $\mathfrak{M}_{\leq }$ , and prove that they indeed determine, respectively, the logics $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\textsf{up}}$ and $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\!\leq }$ .

Definition 37. Let $\mathcal{V}_{10} \,{:=}\, \{{\hat{\mathbf{f}}},{\mathbf{f}}^-,{\mathbf{n}}^-,{\mathbf{b}}^-,{\mathbf{t}}^-,{\mathbf{f}}^+,{\mathbf{n}}^+,{\mathbf{b}}^+,{\mathbf{t}}^+,{\hat{\mathbf{t}}}\}$ and $D \,{:=}\, \{{\mathbf{f}}^+,{\mathbf{n}}^+,{\mathbf{b}}^+,{\mathbf{t}}^+,{\hat{\mathbf{t}}}\} \subseteq \mathcal{V}_{10}$ . Consider the predicates $\textsf{inc}_{\textsf{up}}$ and $\textsf{inc}_{\leq }$ over $\wp (\mathcal{V}_{10})$ , where $\textsf{inc}_{\textsf{up}}(X)$ (resp. $\textsf{inc}_{\leq }(X)$ ) means that $X$ is not contained in the image of valuations over $\mathfrak{M}_{\textsf{up}}$ (resp. $\mathfrak{M}_{\leq }$ ), and can be defined as follows:

\begin{align*} \textsf{inc}_{\textsf{up}}(X) & \text{ iff }\\ &X\supseteq Y\text{, for some }Y\in \{\{d^-,d^+\}:d\in \{{\mathbf{f}},{\mathbf{n}},{\mathbf{b}},{\mathbf{t}}\}\}\cup \\ &\qquad \{\{{\mathbf{b}}^-,{\mathbf{f}}^+\}, \{{\mathbf{n}}^-,{\mathbf{f}}^+\},\{{\mathbf{b}}^+,{\mathbf{t}}^-\}, \{{\mathbf{n}}^+,{\mathbf{t}}^-\}, \{{\mathbf{n}}^+,{\mathbf{b}}^+,{\mathbf{f}}^-\}\} \end{align*}

\begin{align*} {\textsf{inc}_{\leq }(X)}& \text{ iff }\\ &X\supseteq Y\text{, for some }Y\in \{\{d^-,d^+\}:d\in \{{\mathbf{f}},{\mathbf{n}},{\mathbf{b}},{\mathbf{t}}\}\}\cup \\ &\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}}^+\}\} \end{align*}

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

• • for $\unicode{x00A9} \in \{{\sim },{\circ }\}$ ,

  \begin{align*} \unicode{x00A9}_{\textsf{up}}(a)& \,{:=}\, \{b\in \mathcal{V}_{10}:\unicode{x00A9}_{\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}}(g(a))=g(b) \text{ and not }{\textsf{inc}_{\textsf{up}}(\{ a,b \})}\}\\ \unicode{x00A9}_\leq (a)&\,{:=}\,\{b\in \mathcal{V}_{10}: \unicode{x00A9}_{\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}}(g(a))=g(b) \text{ and not }{\textsf{inc}_{\leq }(\{a,b\})} \} \end{align*}

• • for $\unicode{x00A9}\in \{\land, \lor, \Rightarrow \}$ ,

  \begin{align*} \unicode{x00A9}_{\textsf{up}}(a,b)& \,{:=}\, \{c\in \mathcal{V}_{10}: \unicode{x00A9}_{\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}}(g(a),g(b))=g(c) \text{ and not }{\textsf{inc}_{\textsf{up}}(\{a,b,c\})}\}\\ \unicode{x00A9}_{\leq }(a,b)&\,{:=}\,\{c\in \mathcal{V}_{10}: \unicode{x00A9}_{\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}}(g(a),g(b))=g(c)\text{ and not }{\textsf{inc}_{\leq }(\{a,b,c\})} \} \end{align*}

Proposition 38. $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\textsf{up}}$ is determined by $\mathfrak{M}_{\textsf{up}}$ and $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\!\leq }$ is determined by $\mathfrak{M}_{\leq }$ .

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

• • if $b_1,b_2\in X$ with

  \begin{equation*}\{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}}^-\}\}\end{equation*}
  then $b_1\land _{\textsf{up}} b_2=\varnothing$ .

• • if $\{{\mathbf{n}}^+,{\mathbf{b}}^+,{\mathbf{f}}^-\}\subseteq X$ , then ${\mathbf{n}}^+\land _{\textsf{up}}{\mathbf{b}}^+=\{{\mathbf{f}}^+\}$ and ${\mathbf{f}}^-\land _{\textsf{up}}{\mathbf{f}}^+=\varnothing$ .

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

\begin{equation*}\mathbb {T}({\mathfrak {M}_{\textsf {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}}}\}\}\end{equation*}

since for every $X\in \mathbb{T}({\mathfrak{M}_{\textsf{up}}})$ and every $a,b,c\in X$ we have that $\textsf{inc}_{\textsf{up}}(\{a,b,c\})$ is not the case. Thus, the restriction of $\mathfrak{M}_{\textsf{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 $g$ to $X$ .

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

\begin{equation*}\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}}}\}\}\end{equation*}

This is so because $\textsf{inc}_{\leq }(\{a,b,c\})$ iff $\textsf{inc}_{\textsf{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 _{\textsf{up}}{\mathbf{b}}^-=\{{\mathbf{t}}^-\}$ and ${\mathbf{t}}^-\land _{\textsf{up}}{\mathbf{t}}^+=\varnothing$ .

6. Hilbert-Style Axiomatizations

Our goal in this section is to present analytic Hilbert-style axiomatizations for the implicative expansions $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\textsf{up}}$ and $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\!\leq }$ , as well as a axiomatization for $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ . Unfortunately, the PNmatrices from the previous section do not allow us to extract automatically an analytic 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 39. Neither $\mathfrak{M}_\leq$ nor $\mathfrak{M}_{\textsf{up}}$ 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 rules of inference. We will do that and obtain analytic axiomatizations for the logics and then, taking advantage of the fact that in $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\!\leq }$ we have a disjunction (a notion we will soon make precise), we will convert the calculus for $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\!\leq }$ into a axiomatization for $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ .

6.1 Analytic axiomatizations for $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\textsf{up}}$ and $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\!\leq }$

We begin by the analytic 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 _{\textsf{H}}}_{\textsf{up}}$ and $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\!\leq }$ . We check the soundness of each of them and ultimately arrive at the desired completeness results. Throughout the proofs, we will make use of the following abbreviations:

Definition 40. Set ${\uparrow } p \,{:=}\,{\circ }({\sim } p\Rightarrow p)$ and ${\downarrow } p \,{:=}\,{\circ }(p\Rightarrow{\sim } p)$ .

By way of an example, the truth tables of the above-derived connectives interpreted in $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ are given in Table 2. A key feature of these connectives is that they characterize the values $\mathbf{f}$ and $\mathbf{t}$ in the following sense: for each valuation $v$ over $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}, D\rangle$ , $v({\uparrow } p) \not \in D$ iff $v(p) ={\mathbf{f}}$ and $v({\downarrow } p) \not \in D$ iff $v(p) ={\mathbf{t}}$ , for $D$ containing $\hat{\mathbf{t}}$ and not containing $\hat{\mathbf{f}}$ .

Table 2. Truth tables of the connectives $\uparrow$ and $\downarrow$ interpreted in $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$

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

Definition 41. Let $\textsf{R}_{\Diamond }$ be the calculus given by the following inference rules:

\begin{equation*} \frac {}{{\uparrow } p,{\downarrow } p}\, \textsf {r}^\Diamond _{{\uparrow }\textsf {or}{\downarrow }} \qquad \frac {}{\circ (p\Rightarrow p)}\, {\textsf {r}_{\textsf {id}}^{\Diamond }}\qquad \frac {\circ (p\Rightarrow q),\circ (q\Rightarrow r)}{\circ q,\circ (p\Rightarrow r)}\,\textsf {r}_{\textsf {trans}}^\Diamond \end{equation*}

\begin{equation*}\frac {}{{\downarrow } p,\circ q,\circ ( q\Rightarrow p)}\, \textsf {r}^\Diamond _{\leq \mathbf {t}} \qquad \frac {}{{\uparrow } p,\circ ( p\Rightarrow q)}\,\textsf {r}^\Diamond _{\geq \mathbf {f}} \end{equation*}

\begin{equation*}\frac {{\uparrow } p,\circ (p\Rightarrow q)}{\circ p,{\uparrow } q}\, \textsf {r}^\Diamond _{\textsf {incclass}_1} \qquad \frac {{\downarrow } q,\circ (p\Rightarrow q)}{\circ q,{\downarrow } p}\, \textsf {r}^\Diamond _{\textsf {incclass}_2} \qquad \frac {{\uparrow } p,{\downarrow } q,\circ (p\Rightarrow q)}{\circ q,\circ (q\Rightarrow p)}\, \textsf {r}^\Diamond _{\textsf {incclass}_3} \end{equation*}

\begin{equation*} \frac {{\downarrow } p,{\uparrow } r}{\circ p,\circ (p\Rightarrow q),\circ ( p\Rightarrow r),\circ (q\Rightarrow r)}\, \textsf {r}^\Diamond _{\textsf {just}_2} \end{equation*}

Proposition 42. The rules of $\textsf{R}_\Diamond$ are sound for any matrix $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}, D \rangle$ with $D$ containing $\hat{\mathbf{t}}$ and not containing $\hat{\mathbf{f}}$ .

Proof. We proceed rule by rule.

1. $\textsf{r}^\Diamond _{{\uparrow }\textsf{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$ .

2. $\textsf{r}^\Diamond _{\textsf{id}}$ : Clearly, $v({\circ }(p\Rightarrow p))={\hat{\mathbf{t}}}\in D$ .

3. $\textsf{r}^\Diamond _{\textsf{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}}}$ .

4. $\textsf{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}}}$ .

5. $\textsf{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}}}$ .

6. $\textsf{r}^\Diamond _{\textsf{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$ .

7. $\textsf{r}^\Diamond _{\textsf{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$ .

8. $\textsf{r}^\Diamond _{\textsf{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$ .

9. $\textsf{r}^\Diamond _{\textsf{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 43. Let $\textsf{R}_{\Rightarrow }$ be the calculus given by the following inference rules:

\begin{equation*} \frac {\circ q}{\circ (p \Rightarrow q)}\,\textsf {r}^\Rightarrow _1 \qquad \frac {q}{p \Rightarrow q}\, \textsf {r}^\Rightarrow _2 \qquad \frac {p, p \Rightarrow q}{q}\, \textsf {r}^\Rightarrow _3 \qquad \frac {\circ p, p,\circ (p \Rightarrow q)}{\circ q}\, \textsf {r}^\Rightarrow _4 \qquad \frac {\circ p, p,{\downarrow }(p \Rightarrow q)}{{\downarrow } q}\, \textsf {r}^\Rightarrow _5 \end{equation*}

\begin{equation*} \frac {\circ p, p,{\uparrow }(p \Rightarrow q)}{{\uparrow } q}\, \textsf {r}^\Rightarrow _6 \quad \frac {{\uparrow } q}{{\uparrow }(p \Rightarrow q)}\, \textsf {r}^\Rightarrow _7 \qquad \frac {{\downarrow } q}{{\downarrow }(p \Rightarrow q)}\, \textsf {r}^\Rightarrow _8 \qquad \frac {}{\circ (q \Rightarrow (p \Rightarrow q))}\, \textsf {r}^\Rightarrow _9 \quad \frac {\circ p}{p,\circ (p \Rightarrow q)}\, \textsf {r}^\Rightarrow _{10} \end{equation*}

\begin{equation*} \frac {\circ p}{p, p \Rightarrow q}\, \textsf {r}^\Rightarrow _{11} \qquad \frac {\circ q,p \Rightarrow q}{q,\circ p}\, \textsf {r}^\Rightarrow _{12} \qquad \frac {\circ (p \Rightarrow q)}{\circ q, p\Rightarrow q}\, \textsf {r}^\Rightarrow _{13} \qquad \frac {}{{\downarrow } p, \circ (p \Rightarrow q), \circ ((p \Rightarrow q) \Rightarrow q)}\, \textsf {r}^\Rightarrow _{14} \end{equation*}

\begin{equation*} \frac {{\uparrow } p,\circ (p\Rightarrow q)}{\circ p,{\uparrow } q}\, \textsf {r}^\Rightarrow _{15} \qquad \frac {{\downarrow } p}{\circ p,{\uparrow }(p\Rightarrow q)}\, \textsf {r}^\Rightarrow _{16} \qquad \frac {}{\circ p,{\downarrow }(p\Rightarrow q)}\, \textsf {r}^\Rightarrow _{17} \end{equation*}

\begin{equation*} \frac {{\uparrow } p, \circ (p \Rightarrow (p \Rightarrow q))}{\circ p,{\uparrow } q}\, \textsf {r}^\Rightarrow _{18} \qquad \frac {{\uparrow } q}{\circ (p\Rightarrow q),\circ ((p \Rightarrow q) \Rightarrow q)}\, \textsf {r}^\Rightarrow _{19} \end{equation*}

Proposition 44. The rules of $\textsf{R}_\Rightarrow$ are sound for any matrix $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}, D \rangle$ with $D ={{\uparrow }a}$ for some $a \gt{\hat{\mathbf{f}}}$ .

Proof. We proceed rule by rule.

1. $\textsf{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$ .

2. $\textsf{r}^{\Rightarrow }_{2}$ : If $v(q)\in D$ , then $v(q)\geq a$ and by analyzing the table of $\Rightarrow _{\textsf{H}}$ we conclude that $v(p\Rightarrow q)\geq v(q)\geq a$ and thus $v(p \Rightarrow q)\in D$ .

3. $\textsf{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 analyzing the table of $\Rightarrow _{\textsf{H}}$ we conclude that $v(q)\geq a$ and thus $v(q)\in D$ .

4. $\textsf{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$ .

5. $\textsf{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.

6. $\textsf{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.

7. $\textsf{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}}}$ .

8. $\textsf{r}^{\Rightarrow }_{8}$ : Similar to the proof for $\textsf{r}^{\Rightarrow }_{7}$ .

9. $\textsf{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.

10. $\textsf{r}^{\Rightarrow }_{10}$ , $\textsf{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$ .

11. $\textsf{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$ .

12. $\textsf{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}}}$ .

13. $\textsf{r}^{\Rightarrow }_{14}$ : 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}}}$ .

14. $\textsf{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}}}$ .

15. $\textsf{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}}}$ .

16. $\textsf{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}}$ , and so $v({\downarrow }(p \Rightarrow q)) ={\hat{\mathbf{t}}}$ .

17. $\textsf{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}}}$ .

18. $\textsf{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 to 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 45. Let $\textsf{R}_{{\sim }}$ be the calculus given by the following inference rules:

\begin{equation*}\frac {\circ p}{p, \sim p}\, \textsf {r}^\sim_1\qquad \frac {\circ p,p, \sim p}{}\,\textsf {r}^\sim_2\qquad \frac {\circ p}{\circ \sim p}\, \textsf {r}^\sim_3\qquad \frac {\circ \sim p}{\circ p}\, \textsf {r}^\sim_4 \end{equation*}

\begin{equation*}\frac {{\uparrow } \sim p}{{\downarrow } p}\, {\textsf {r}^\sim_5}\qquad \frac {{\downarrow } \sim p}{{\uparrow } p}\, \textsf {r}^\sim_6\qquad \frac {{\downarrow } p}{{\uparrow } \sim p}\, \textsf {r}^\sim_7\qquad \frac {{\uparrow } p}{{\downarrow } \sim p}\, \textsf {r}^\sim_8 \end{equation*}

Proposition 46. The rules of $\textsf{R}_{\sim }$ are sound for any matrix $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}, D \rangle$ with $D ={{\uparrow }a}$ for some $a\gt{\hat{\mathbf{f}}}$ .

Proof. We proceed rule by rule.

1. $\textsf{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$ .

2. $\textsf{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$ .

3. $\textsf{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$ .

4. $\textsf{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$ .

5. ${\textsf{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$ .

6. $\textsf{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$ .

7. $\textsf{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$ .

8. $\textsf{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 47. Let $\textsf{R}_{{\circ }}$ be the calculus given by the following inference rule:

\begin{equation*}\frac {}{{\circ}{\circ} p}\, \textsf {r}_{\circ } \end{equation*}

Proposition 48. The rules of $\textsf{R}_{\circ }$ are sound for any matrix $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}, D \rangle$ with ${\hat{\mathbf{t}}} \in D$ .

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

Definition 49. Let $\textsf{R}_{\land }$ be the calculus given by the following inference rules:

\begin{equation*} \frac {\circ p,\circ q}{\circ (p \land q)}\, \textsf {r}^{\land }_1 \qquad \frac {p,q}{p\land q}\, \textsf {r}^{\land }_2 \qquad \frac {p \land q}{q}\,\textsf {r}^{\land }_3 \qquad \frac {p, \circ (p \land q)}{\circ q}\, \textsf {r}^{\land }_4 \qquad \frac {\circ p}{\circ (q \Rightarrow (p \land q))}\, \textsf {r}^{\land }_5 \end{equation*}

\begin{equation*} \frac {}{\circ ((p \land q) \Rightarrow q)}\, \textsf {r}^{\land }_6 \qquad \frac {p \land q}{p}\, \textsf {r}^{\land }_7 \qquad \frac {q, \circ (p \land q)}{\circ p}\, \textsf {r}^{\land }_8 \qquad \frac {\circ q}{\circ (p \Rightarrow (p \land q))}\, \textsf {r}^{\land }_9 \end{equation*}

\begin{equation*} \frac {}{\circ ((p \land q) \Rightarrow p)}\, \textsf {r}^{\land }_{10} \qquad \frac {\circ p}{p,\circ (p \land q)}\, \textsf {r}^{\land }_{11} \qquad \frac {\circ q}{q,\circ (p \land q)}\, \textsf {r}^{\land }_{12} \qquad \frac {\circ (p \land q)}{\circ p, \circ q}\, \textsf {r}^{\land }_{13} \end{equation*}

\begin{equation*} \frac {\circ (p \Rightarrow q)}{\circ (p \Rightarrow (p \land q))}\, \textsf {r}^{\land }_{14} \qquad \frac {\circ (q \Rightarrow p)}{\circ (q \Rightarrow (p \land q))}\, \textsf {r}^{\land }_{15} \qquad \frac {{\downarrow } p,{\uparrow }(p \land q)}{\circ p,\circ (p \Rightarrow q)}\, \textsf {r}^{\land }_{16} \end{equation*}

Proposition 50. The rules of $\textsf{R}_\land$ are sound for any matrix $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}, D \rangle$ with $D ={{\uparrow }a}$ for some $a\gt{\hat{\mathbf{f}}}$ .

Proof. We proceed rule by rule:

1. $\textsf{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}}}$ .

2. $\textsf{r}^{\land }_{2}$ : Soundness follows from the fact that principal filters are closed under meets.

3. $\textsf{r}^{\land }_{3}$ , $\textsf{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$ .

4. $\textsf{r}^{\land }_{4}$ , $\textsf{r}^{\land }_{8}$ : If $v({\circ } q) \not \in D$ , then $v(q) \in \{{\mathbf{f}},{\mathbf{b}},{\mathbf{n}},{\mathbf{t}} \}$ . If $v({\circ }(p \land q)) \in D$ , then $v(p \land q) \in \{{\hat{\mathbf{f}}},{\hat{\mathbf{t}}} \}$ . Thus if $v(p \land q) ={\hat{\mathbf{t}}}$ , then $v(p) = v(q) ={\hat{\mathbf{t}}}$ , absurd. Otherwise, we must have $v(p) ={\hat{\mathbf{f}}}$ . The proof is analogous for the other rule.

5. $\textsf{r}^{\land }_{5}$ , $\textsf{r}^{\land }_{9}$ : If $v({\circ } p) \in D$ , then $v(p) \in \{{\hat{\mathbf{f}}},{\hat{\mathbf{t}}} \}$ . Then either $v(q \Rightarrow (p \land q)) = v(q \Rightarrow q) ={\hat{\mathbf{t}}}$ or $v(q \Rightarrow (p \land q)) \in \{{\hat{\mathbf{f}}},{\hat{\mathbf{t}}} \}$ . In both cases, we are done. The proof is analogous to the other rule.

6. $\textsf{r}^{\land }_{6}$ , $\textsf{r}^{\land }_{10}$ : We have that $v(p\land q)\leq v(p)$ and $v(p\land q)\leq v(q)$ hence $v((p\land q)\Rightarrow q)=v({\circ }((p\land q)\Rightarrow q))=v((p\land q)\Rightarrow p)=v({\circ }((p\land q)\Rightarrow p))={\hat{\mathbf{t}}}\in D$ .

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

8. $\textsf{r}^{\land }_{13}$ : If $v({\circ }(p \land q)) \in D$ , then $v(p \land q) \in \{{\hat{\mathbf{f}}},{\hat{\mathbf{t}}} \}$ . If $v(p) = v(q) ={\hat{\mathbf{t}}}$ , clearly $v({\circ } p) = v({\circ } q) ={\hat{\mathbf{t}}}$ . If $v(p) ={\hat{\mathbf{f}}}$ , then $v({\circ } p) ={\hat{\mathbf{t}}}$ . Analogously if $v(q) ={\hat{\mathbf{f}}}$ .

9. $\textsf{r}^{\land }_{14}$ , $\textsf{r}^{\land }_{15}$ : Suppose ${\circ }(p\Rightarrow q)\in D$ . Then either $v(q)={\hat{\mathbf{f}}}$ , in which case $v(p \Rightarrow (p \land q))\in \{{\hat{\mathbf{f}}},{\hat{\mathbf{t}}}\}$ and thus $v({\circ }(p \Rightarrow (p\land q)))={\hat{\mathbf{t}}}\in D$ ; or $v(p)\leq v(q)$ , and so $v(p\land q)=v(p)$ , hence $v({\circ }(p\Rightarrow (p\land q)))={\hat{\mathbf{t}}}\in D$ . The proof for $\textsf{r}^{\land }_{15}$ is similar.

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

Definition 51. Let $\textsf{R}_{\lor }$ be the calculus given by the following inference rules:

\begin{equation*} \frac {\circ p,\circ q}{\circ (p \lor q)}\, \textsf {r}_1^{\lor } \qquad \frac {\circ p, p \lor q}{p, q}\, \textsf {r}_2^{\lor } \qquad \frac {q}{p \lor q}\, \textsf {r}_3^{\lor } \qquad \frac {\circ (p \lor q)}{p, \circ q}\, \textsf {r}_4^{\lor } \qquad \frac {}{\circ (q \Rightarrow (p \lor q))}\, \textsf {r}_5^{\lor } \end{equation*}

\begin{equation*} \frac {\circ p}{p, \circ ((p \lor q) \Rightarrow q)}\, \textsf {r}_6^{\lor } \qquad \frac {p}{p \lor q}\, \textsf {r}_7^{\lor } \qquad \frac {\circ (p \lor q)}{q,\circ p}\, \textsf {r}_8^{\lor } \qquad \frac {}{\circ (p \Rightarrow (p \lor q))}\, \textsf {r}_9^{\lor } \end{equation*}

\begin{equation*} \frac {\circ q}{q, \circ ((p \lor q) \Rightarrow p)}\, \textsf {r}_{10}^{\lor } \qquad \frac {p,\circ p}{\circ (p\lor q)}\, \textsf {r}_{11}^{\lor } \qquad \frac {q,\circ q}{\circ (p\lor q)}\, \textsf {r}_{12}^{\lor }\qquad \frac {\circ (p \lor q)}{\circ p, \circ q}\, \textsf {r}_{13}^{\lor } \end{equation*}

\begin{equation*} \frac {\circ (p \Rightarrow q)}{\circ ((p \lor q) \Rightarrow q)}\, \textsf {r}_{14}^{\lor }\qquad \frac {\circ (q \Rightarrow p)}{\circ ((p \lor q) \Rightarrow p)}\, \textsf {r}_{15}^{\lor } \qquad \frac {{\uparrow } q, {\downarrow }(p \lor q)} {\circ p,\circ (p \Rightarrow q)}\, \textsf {r}_{16}^{\lor } \end{equation*}

Proposition 52. The rules of $\textsf{R}_\lor$ are sound for any matrix $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}, D \rangle$ with $D ={{\uparrow }a}$ for some $a\gt{\hat{\mathbf{f}}}$ .

Proof. We proceed rule by rule.

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

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

3. $\textsf{r}_3^\lor$ , $\textsf{r}_7^\lor$ : As $v(q) \leq v(p \lor q)$ , if $v(q) \in D$ , then $v(p \lor q) \in D$ . Similarly for the other rule.

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

5. $\textsf{r}_5^\lor$ , $\textsf{r}_9^\lor$ : We have that $v(p\lor q)\geq v(p)$ and $v(p\lor q)\geq v(q)$ , hence $v(q\Rightarrow (p\lor q))= v({\circ }(q\Rightarrow (p\lor q)))=v(p\Rightarrow (p\lor q))= v({\circ }(p\Rightarrow (p\lor q)))={\hat{\mathbf{t}}} \in D$ .

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

7. $\textsf{r}_{11}^\lor$ , $\textsf{r}_{12}^\lor$ : If $v(p),v({\circ } p)\in D$ , or $v(q),v({\circ } q)\in D$ , then either $v(p)={\hat{\mathbf{t}}}$ or $v(q)={\hat{\mathbf{t}}}$ . In any case we have that $v(p\lor q)=v({\circ }(p\lor q))={\hat{\mathbf{t}}}\in D$ .

8. $\textsf{r}_{13}^\lor$ : If $v({\circ } p),v({\circ } q) \not \in D$ , we have $v(p),v(q) \in \{{\mathbf{f}},{\mathbf{b}},{\mathbf{n}},{\mathbf{t}} \}$ , thus $v(p \lor q) \in \{{\mathbf{f}},{\mathbf{b}},{\mathbf{n}},{\mathbf{t}} \}$ , and $v({\circ }(p \lor q)) \not \in D$ .

9. $\textsf{r}_{14}^\lor$ , $\textsf{r}_{15}^\lor$ : Suppose ${\circ }(p\Rightarrow q)\in D$ . Then either $v(q)={\hat{\mathbf{f}}}$ , in which case $v((p\lor q)\Rightarrow q)\in \{{\hat{\mathbf{f}}},{\hat{\mathbf{t}}}\}$ and thus $v({\circ }((p\lor q)\Rightarrow q))={\hat{\mathbf{t}}}\in D$ ; or $v(p)\leq v(q)$ , so $v(p\lor q)=v(q)$ , hence $v({\circ }((p\lor q)\Rightarrow q))={\hat{\mathbf{t}}}\in D$ . The proof for $\textsf{r}_{15}^\lor$ is similar.

10. $\textsf{r}_{16}^\lor$ : If $v({\circ } p) \not \in D$ and $v({\uparrow } q) \in D$ , $v(p) \in \{{\mathbf{f}},{\mathbf{b}},{\mathbf{n}},{\mathbf{t}} \}$ and $v(q) \neq{\mathbf{f}}$ . If $v(p) = v(q)$ , we are done, so suppose $v(p) \neq v(q)$ . If $v({\downarrow }(p \lor q)) \in D$ , then $v(p \lor q) \neq{\mathbf{t}}$ . If $v(p) ={\mathbf{f}}$ , then $v(p \Rightarrow q) \in \{{\hat{\mathbf{f}}},{\hat{\mathbf{t}}} \}$ , and we are done. If $v(p) ={\mathbf{b}}$ , the only non-obvious case is $v(q) ={\mathbf{n}}$ , but this is impossible as $v(p \lor q) \neq{\mathbf{t}}$ . If $v(p) ={\mathbf{n}}$ , the proof is similar to the previous case. If $v(p) ={\mathbf{t}}$ , the only non-obvious cases are those in which $v(q) \in \{{\mathbf{b}},{\mathbf{n}} \}$ ; yet they are impossible, again, because $v(p \lor q) \neq{\mathbf{t}}$ .

Definition 53. Let $\textsf{R}_{\bot \top }$ be the calculus given by the following inference rules:

\begin{equation*} \frac {}{\top }\,\textsf {r}_1^\top \qquad \frac {}{\circ \top }\, \textsf {r}_2^\top \qquad \frac {\bot }{}\, \textsf {r}_1^\bot \qquad \frac {}{\circ \bot }\, \textsf {r}_2^\bot \end{equation*}

Proposition 54. The rules of $\textsf{R}_{\top \bot }$ are sound for any matrix $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}, D \rangle$ with $D ={{\uparrow }a}$ for some $a\gt{\hat{\mathbf{f}}}$ .

Proof. Obvious.

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

Definition 55. Consider the following inference rules:

\begin{equation*} \frac {p, {\downarrow } p, q}{\circ p,\circ (p \Rightarrow q),\circ r, r}\, \textsf {r}_{D_\land } \qquad \frac {p,\circ (p \Rightarrow q)}{\circ q, q}\, \textsf {r}_{D_\leq } \qquad \frac {r,{\uparrow } q}{{\downarrow } r, \circ (p\Rightarrow q),p,q}\, \textsf {r}_{D\neq {\uparrow } {\mathbf {t}}} \end{equation*}

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

Proof. We first check items (i) and (ii):

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

2. $\textsf{r}_{D_\leq }$ : If $v({\circ }(p\Rightarrow q)) \in D, v(p)\geq a$ and $v(\circ q) \lt a$ , then $v({\circ }(p\Rightarrow q))={\hat{\mathbf{t}}}$ .

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

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

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

Definition 57. Using the previous definitions, we set the two following collection of rules:

1. 1. $\textsf{R}_{\textsf{up}} \,{:=}\,\textsf{R}_\Diamond \cup \textsf{R}_D\cup \textsf{R}_\Rightarrow \cup \textsf{R}_{\circ }\cup \textsf{R}_{\sim } \cup \textsf{R}_\land \cup \textsf{R}_\lor \cup \textsf{R}_{\top \bot } \cup \{\textsf{r}_{D_\land },\textsf{r}_{D_\leq }\}$ ;

2. 2. $\textsf{R}_{\leq }\,{:=}\,\textsf{R}_{\textsf{up}} \cup \{\textsf{r}_{D\neq{\uparrow }{\mathbf{t}}}\}$ .

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

Proof. From the previous propositions, it easily follows that $\rhd _{\textsf{R}_{\textsf{up}}}\subseteq{\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\textsf{up}}}$ and $\rhd _{\textsf{R}_{\leq }}\subseteq{\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\!\leq }}$ , thus guaranteeing soundness of the proposed axiomatizations. To check completeness for $\textsf{R}\in \{\textsf{R}_{\textsf{up}},\textsf{R}_{\leq }\}$ we need to show that each consequence statement of the form $\Phi \blacktriangleright_{\textsf{R}} \Psi$ is witnessed by some valuation and some principal filter over the algebra $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ . Let $\Lambda \,{:=}\,{\textsf{sub}}(\Phi \cup \Psi )$ . Recall that from $\Phi \blacktriangleright_{\textsf{R}}\Psi$ , by cut for sets, there is a partition $(\Omega, \overline{\Omega })$ of $\Theta (\Lambda )$ such that $\Omega \blacktriangleright_{\textsf{R}} \,\overline{\Omega }$ . Lemmas 59–66, below, will give us material to show how a partial valuation $f$ on $\Lambda$ may be extended to the whole language to such an effect that we will have $f(\Lambda \cap \Omega )\subseteq D$ and $f(\Lambda \cap \overline{\Omega })\subseteq \mathcal{V}_6{\setminus }D$ for some suitable $D$ (either principal or prime, depending on the case). Further, analyticity will follow from the fact that we will be using only instances of the rules in $\textsf{R}$ with formulas in $\Lambda$ , thus only formulas in $\Theta (\Lambda ) \,{:=}\, \{\psi ^\sigma :\psi \in \Theta \text{ and }\sigma :\{p,q\}\to \Lambda \}$ will appear along this proof.

The following abbreviations will be helpful in what follows. Let

\begin{align*} \Lambda _{{\hat{\mathbf{f}}}}& \,{:=}\,\{\varphi \in \Lambda : \varphi \in \overline{\Omega }\text{ and }{\circ } \varphi \in \Omega \} \\ \Lambda _{{\hat{\mathbf{t}}}}&\,{:=}\,\{\varphi \in \Lambda : \varphi, {\circ } \varphi \in \Omega \} \\ \Lambda _{\Diamond }&\,{:=}\,\{\varphi \in \Lambda :{\circ } \varphi \in \overline{\Omega } \}\\ \Lambda _{\mathbf{t}}&\,{:=}\,\{\varphi \in \Lambda _{\Diamond }:{\downarrow } \varphi \in \overline{\Omega } \}\\ \Lambda _{\mathbf{f}}&\,{:=}\, \{\varphi \in \Lambda _{\Diamond }:{\uparrow } \varphi \in \overline{\Omega } \}\\ \Lambda _{\textsf{mid}}&\,{:=}\,\{\varphi \in \Lambda _{\Diamond }:{\uparrow }\varphi, {\downarrow } \varphi \in \Omega \} \end{align*}

We will also consider the relation $\equiv _\Diamond \,\subseteq \Lambda _\Diamond \times \Lambda _\Diamond$ given by $\varphi \equiv _\Diamond \psi$ if, and only if, ${\circ }(\varphi \Rightarrow \psi ),{\circ }(\psi \Rightarrow \varphi )\in \Omega$ .

Lemma 59. From $\textsf{R}^\Diamond \subseteq \textsf{R}$ , we obtain that

1. 1. $\Lambda _\Diamond =\Lambda _{\mathbf{f}}\cup \Lambda _{\mathbf{t}}\cup \Lambda _{\textsf{mid}}$ ;

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

3. 3. for $\varphi \in \Lambda _a$ and $\psi \in \Lambda _b$ with $a,b\in \{{\mathbf{f}},{\mathbf{n}},{\mathbf{b}},{\mathbf{t}}\}$ , we have $a \leq b$ if, and only if, ${\circ }(\varphi \Rightarrow \psi )\in \Omega$ .

Proof. Note that since $\Omega \cap \overline{\Omega }=\varnothing$ we have that $\Lambda _a\cap \Lambda _b=\varnothing$ for $a\neq b$ and $a,b\in \{{\mathbf{f}},{\mathbf{t}},\textsf{mid},{\hat{\mathbf{t}}},{\hat{\mathbf{f}}}\}$ . By $\textsf{r}^{\sim }_{{\uparrow }\textsf{or}{\downarrow }}$ we know that $\Lambda _\Diamond = \Lambda _{\mathbf{f}}\cup \Lambda _{\mathbf{t}}\cup \Lambda _{\textsf{mid}}$ , and this takes care of item (1).

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

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

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

Still, $\Lambda _{\textsf{mid}}$ might be partitioned into more than two $\equiv _\Diamond$ -equivalence classes. We avoid this with the rule $\textsf{r}^{\sim }_{\textsf{just}_2}$ , which, together with the fact proved in the previous paragraph, prevents the existence of more than two $\equiv _\Diamond$ -equivalence classes in $\Lambda _{\textsf{mid}}$ . This concludes the proof of item (2).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   2. b. If $f(\psi ) ={\hat{\mathbf{f}}}$ , it follows from $\textsf{r}_1^\Rightarrow$ and $\textsf{r}_3^\Rightarrow$ .

   3. c. If $f(\psi ) ={\mathbf{t}}$ , it follows from $\textsf{r}_4^\Rightarrow$ and $\textsf{r}_5^\Rightarrow$ .

   4. d. If $f(\psi ) ={\mathbf{f}}$ , it follows from $\textsf{r}_4^\Rightarrow$ and $\textsf{r}_6^\Rightarrow$ .

   5. e. If $f(\psi ) \in \{{\mathbf{b}},{\mathbf{n}} \}$ , it follows by $\textsf{r}_4^\Rightarrow$ , $\textsf{r}_7^\Rightarrow$ and $\textsf{r}_8^\Rightarrow$ that $f(\varphi \Rightarrow \psi ) \in \{{\mathbf{b}},{\mathbf{n}} \}$ . Then, by $\textsf{r}_9^\Rightarrow$ and Lemma 59 we have $f(\varphi \Rightarrow \psi ) = f(\psi )$ .

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

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

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

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

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

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

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

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

Lemma 61. Suppose $\textsf{R}_{\sim }, \textsf{R}_\Diamond \subseteq \textsf{R}$ . If $\{\varphi, {\sim }\varphi \} \subseteq \Lambda$ , then $f({\sim }\varphi )={\sim }^{\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}}(f(\varphi ))$ .

Proof. We reason by cases on the value of $f(\varphi )$ :

1. 1. If $f(\varphi )={\hat{\mathbf{t}}}$ , then $\varphi, {\circ } \varphi \in \Omega$ , so ${\sim } \varphi \in \overline{\Omega }$ and ${\circ }{\sim } \varphi \in \Omega$ by $\textsf{r}^{\sim }_2$ and $\textsf{r}^{\sim }_3$ .

2. 2. If $f(\varphi )={\hat{\mathbf{f}}}$ , then ${\circ } \varphi \in \Omega$ and $\varphi \in \overline{\Omega }$ , so ${\sim } \varphi \in \Omega$ and ${\circ }{\sim } \varphi \in \Omega$ by $\textsf{r}_1^{\sim }$ and $\textsf{r}_3^{\sim }$ .

3. 3. If $f(\varphi )={\mathbf{t}}$ , then ${\circ }\varphi \in \overline \Omega$ and ${\downarrow } \varphi \in \overline{\Omega }$ . Thus, by $\textsf{r}^{\sim }_4$ and $\textsf{r}^{\sim }_5$ we have that ${\circ }{\sim }\varphi \in \overline \Omega$ and ${\uparrow }{\sim } \varphi \in \overline{\Omega }$ .

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

5. 5. If $f(\varphi ) \in \{{\mathbf{b}},{\mathbf{n}} \}$ , then ${\circ } \varphi \in \overline \Omega$ and ${\uparrow } \varphi, {\downarrow } \varphi \in \Omega$ . By $\textsf{r}^{\sim }_4$ , $\textsf{r}^{\sim }_7$ and $\textsf{r}^{\sim }_8$ , we have ${\circ }{\sim }\varphi \in \overline \Omega$ and ${\uparrow }{\sim }\varphi, {\downarrow }{\sim }\varphi \in \Omega$ . This gives us that $f({\sim } \varphi ) \in \{{\mathbf{b}},{\mathbf{n}} \}$ . Also, since we have ${\circ }(\varphi \Rightarrow{\sim }\varphi ) ={\downarrow } \varphi \in \Omega$ , we must have $f({\sim } \varphi ) = f(\varphi )$ by Lemma 59.

Lemma 62. Suppose $\textsf{R}_{\circ } \subseteq \textsf{R}$ . If $\{\varphi, {\circ }\varphi \} \subseteq \Lambda$ , then $f({\circ }\varphi )={\circ }^{\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}}(f(\varphi ))$ .

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

Lemma 63. Suppose $\textsf{R}_\land, \textsf{R}_\Diamond \subseteq \textsf{R}$ . If $\{\varphi, \psi, \varphi \land \psi \} \subseteq \Lambda$ , then $f(\varphi \land \psi )=f(\varphi )\land ^{\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}}\!\! f(\psi )$ .

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

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

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

   2. b. If $f(\psi ) ={\hat{\mathbf{f}}}$ , we have ${\circ }\psi \in \Omega$ and $\psi \in \overline{\Omega }$ . Then we have ${\circ }(\varphi \land \psi ) \in \Omega$ and $\varphi \land \psi \in \overline{\Omega }$ by $\textsf{r}_1^\land$ and $\textsf{r}_3^\land$ .

   3. c. If $f(\psi ) \in \{{\mathbf{f}},{\mathbf{b}},{\mathbf{n}},{\mathbf{t}} \}$ , we have ${\circ }\psi \in \overline \Omega$ and that $f(\varphi \land \psi ) \in \{{\mathbf{f}},{\mathbf{b}},{\mathbf{n}},{\mathbf{t}} \}$ by $\textsf{r}_4^\land$ . Then we have that ${\circ }(\psi \Rightarrow (\varphi \land \psi )),{\circ }((\varphi \land \psi ) \Rightarrow \psi ) \in \Omega$ by $\textsf{r}_5^\land$ and $\textsf{r}_6^\land$ . This, together with Lemma 59, gives the desired result.

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

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

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

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

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

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

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

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

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

Lemma 64. Suppose $\textsf{R}_\lor, \textsf{R}_\Diamond \subseteq \textsf{R}$ . If $\{\varphi, \psi, \varphi \lor \psi \} \subseteq \Lambda$ , then $f(\varphi \lor \psi )=f(\varphi )\lor ^{\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}}\!\! f(\psi )$ .

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

1. 1. If $f(\varphi )={\hat{\mathbf{f}}}$ , we know that $\varphi \in \overline \Omega$ and ${\circ } \varphi \in{\Omega }$ . We want to obtain that $f(\varphi \lor \psi )=f(\psi )$ , since $f(\psi ) ={\hat{\mathbf{f}}} \lor ^{\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}}\!\! f(\psi )$ .

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

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

   3. c. If $f(\psi ) \in \{{\mathbf{f}},{\mathbf{b}},{\mathbf{n}},{\mathbf{t}} \}$ , we have ${\circ }\psi \in \overline \Omega$ and we know that $f(\varphi \lor \psi ) \in \{{\mathbf{f}},{\mathbf{b}},{\mathbf{n}},{\mathbf{t}} \}$ by $\textsf{r}_4^\lor$ . Then we have that ${\circ }(\psi \Rightarrow (\varphi \lor \psi )),{\circ }((\varphi \lor \psi ) \Rightarrow \psi ) \in \Omega$ by $\textsf{r}_5^\lor$ and $\textsf{r}_6^\lor$ , which, together with Lemma 59, gives the desired result.

2. 2. If $f(\psi )={\hat{\mathbf{f}}}$ , we know that $\psi \in \overline \Omega$ and ${\circ } \psi \in{\Omega }$ . We want to obtain that $f(\varphi \lor \psi )=f(\varphi )$ , since $f(\varphi ) = f(\varphi ) \lor ^{\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}}{\hat{\mathbf{f}}}$ .

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

   2. b. If $f(\varphi )={\hat{\mathbf{t}}}$ , the result follows by $\textsf{r}_1^\lor$ and $\textsf{r}_7^\lor$ .

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

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

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

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

   2. b. If $f(\psi ) \leq f(\varphi )$ , we reason analogously to the previous item, but now using $\textsf{r}_9^\lor$ and $\textsf{r}_{15}^\lor$ .

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

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

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

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

Proof. First of all, we show that (I): for $\varphi _1, \ldots, \varphi _n \in \Omega \cap \Lambda$ , if $\bigwedge _i f(\varphi _i) \in f[\Lambda ]$ , then $\bigwedge _i f(\varphi _i) \in f[\Omega \cap \Lambda ]$ . By induction on $n$ , consider the base case $n = 2$ . The cases $f(\varphi ) \leq f(\psi )$ and $f(\psi ) \leq f(\varphi )$ are obvious, as $f(\varphi ) \land f(\psi )$ will coincide either with $f(\varphi )$ or with $f(\psi )$ and they are in $f[\Omega \cap \Lambda ]$ by assumption. The tricky case thus is when $\{ f(\varphi ),f(\psi ) \} = \{{\mathbf{b}},{\mathbf{n}} \}$ . Suppose that for some $\theta \in \Lambda$ we have $f(\theta ) = f(\varphi ) \land f(\psi ) ={\mathbf{f}}$ . Then, by $\textsf{r}_{D_\land }$ , we must have $\theta \in \Omega$ , and so $f(\theta ) ={\mathbf{f}} \in f[\Omega \cap \Lambda ]$ . In the inductive step, suppose that $b \,{:=}\, (f(\varphi _1) \land \ldots \land f(\varphi _n)) \land f(\varphi _{n+1}) \in f[\Lambda ]$ , for $\varphi _1,\ldots, \varphi _{n+1} \in \Omega \cap \Lambda$ . Then either (i) $b = (f(\varphi _1) \land \ldots \land f(\varphi _n))$ , or (ii) $b = f(\varphi _{n+1})$ , or (iii) $b ={\mathbf{f}}$ and $\{f(\varphi _1) \land \ldots \land f(\varphi _n),f(\varphi _{n+1})\} = \{{\mathbf{b}},{\mathbf{n}} \}$ . In case (i), we use the induction hypothesis. Case (ii) is obvious. As for case (iii), we use $\textsf{r}_{D_\land }$ as we did in the base case.

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

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

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

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

1. 1. If $f(\theta ) \leq f(\varphi )$ for all $\varphi \in \Omega \cap \Lambda$ , then $f(\theta ) = a$ , and thus $\theta \in \Omega$ by (I).

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

   1. a. If $f(\psi ) \lt f(\theta )$ , by (II) we must have $\theta \in \Omega \cap \Lambda$ .

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

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

We are now finally ready to go back to the completeness proof we were working on before going through the above series of auxiliary results. Note that the above lemmas show that $f$ is a partial homomorphism over $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ (which can of course be extended to a full homomorphism) and, in view of the above lemmas, by considering a set of designated values of the form ${\uparrow } a$ for appropriate $a$ we obtain a countermodel for $\Phi \rhd _{{\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\textsf{up}}}} \Psi$ or for $\Phi \rhd _{{\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\!\leq }}}\Psi$ as desired. This finishes the proof of Theorem 58.

6.2 axiomatization for $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$

The calculus developed in the preceding subsection for the logic $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\!\leq }$ induces a logic for its companion $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ . We begin by defining this calculus, then indicate why it is complete for $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ . In what follows, given a set of formulas $\Phi$ , let $\Phi \lor \psi \,{:=}\, \{ \varphi \lor \psi : \varphi \in \Phi \}$ and $\bigvee \{ \varphi _1,\ldots, \varphi _m \} \,{:=}\, \varphi _1 \lor (\varphi _2 \lor \ldots (\ldots \lor \varphi _n)\ldots )$ .

Definition 67. Let $\textsf{R}$ be a calculus. We define $\textsf{R}^{\lor }$ as the calculus

\begin{equation*} \left \{\frac {p\lor p}{p},\frac {p}{p \lor q}, \frac {p \lor q}{q \lor p}, \frac {p \lor (q \lor r)}{(p \lor q) \lor r}\right \} \cup \left \{\textsf {r}^\lor : \textsf {r} \in \textsf {R}\right \},\textit{ where, for each given rule $\textsf {r}=\frac {\Phi }{\Psi }$ in $\textsf {R}$,}\end{equation*}

the rule $\textsf{r}^\lor$ is set as: $\begin{array}{l@{\quad}l}\textsf{r} & in\;case\; \Phi\; is\;empty\;and\; \Psi\; is\; a\; singleton\\ \frac{\Phi \lor s}{s}, & in\;case\;\Psi\;is\;empty \\ \frac{\Phi \lor s}{(\bigvee \Psi ) \lor s}, & otherwise\\ \end{array}$

In all cases, $s$ is chosen to be a propositional variable not occurring in the rules that belong to $\textsf{R}$ .

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

Lemma 68 (Shoesmith and Smiley 1978, Thm. 5.37). Let $\textsf{R}$ be a calculus over a signature containing a binary connective $\lor$ . If $\vdash _{\textsf{R}}$ has a disjunction, then $\vdash _{\textsf{R}^\lor } \;=\; \vdash _{\textsf{R}}$ .

From this it immediately follows that:

Theorem 69. $\vdash _{\textsf{R}_{\leq }^\lor } ={\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }}$ .

7. Algebraic Study of $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ and $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$

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

We begin by recalling that, as observed earlier, the algebra $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ is a symmetric Heyting algebra in Monteiro’s sense.

Definition 70 (Monteiro 1980, Def. 1.2, p. 61). A symmetric Heyting algebra (SHA) is a $\Sigma ^{\textsf{DM}}_{\Rightarrow }$ -algebra $\langle A; \land, \lor, \Rightarrow, {\sim }, \bot, \top \rangle$ such that:

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

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

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

\begin{equation*} \frac {}{p \Rightarrow (q \Rightarrow p)}\,\textsf {r}^{\textsf M}_{1} \quad \frac {}{(p \Rightarrow (q \Rightarrow r)) \Rightarrow ((p \Rightarrow q) \Rightarrow (p \Rightarrow r))}\, \textsf {r}^{\textsf M}_{2} \end{equation*}

\begin{equation*} \frac {}{(p \land q) \Rightarrow p}\, \textsf {r}^{\textsf M}_{3} \quad \frac {}{(p \land q) \Rightarrow q}\, \textsf {r}^{\textsf M}_{4} \quad \frac {}{(p \Rightarrow q) \Rightarrow ((p \Rightarrow r) \Rightarrow (p \Rightarrow (q \land r)))}\, \textsf {r}^{\textsf M}_{5} \end{equation*}

\begin{equation*} \frac {}{p \Rightarrow (p \lor q)}\, \textsf {r}^{\textsf M}_{6} \quad \frac {}{q \Rightarrow (p \lor q)}\, \textsf {r}^{\textsf M}_{7} \quad \frac {}{(p \Rightarrow r) \Rightarrow ((q \Rightarrow r) \Rightarrow ((p \lor q) \Rightarrow r))}\, \textsf {r}^{\textsf M}_{8} \end{equation*}

\begin{equation*} \frac {}{p \Rightarrow \sim \sim p}\, \textsf {r}^{\textsf M}_{9} \quad \frac {}{\sim \sim p \Rightarrow p}\, \textsf {r}^{\textsf M}_{10} \end{equation*}

\begin{equation*} \frac {p, p\Rightarrow q}{q}\,\textsf {r}^{\textsf M}_{11} \quad \frac {p \Rightarrow q}{\sim q \Rightarrow \sim p}\, \textsf {r}^{\textsf M}_{12} \end{equation*}

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

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

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

\begin{equation*} \frac {}{\neg p \Rightarrow \sim \neg \neg p}\, \textsf {r}^{\top }_{1} \qquad \frac {}{\sim \neg \neg p \Rightarrow \neg p}\, \textsf {r}^{\top }_{2} \end{equation*}

\begin{equation*} \frac {}{({\circ (p_1 \Rightarrow p_2) \land \circ (p_2\Rightarrow p_3) }) \Rightarrow ({\circ p_1 \lor \circ p_4 \lor \circ (p_4\Rightarrow p_3)} \lor \circ (p_3\Rightarrow p_2) \lor \circ (p_2\Rightarrow p_1))}\, \textsf {r}^{\top }_{3} \end{equation*}

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

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

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

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

Example 7 (Sankappanavar 1987, p. 568). Let $\mathbf{A}[D]$ be a finite De Morgan algebra and let $\mathbf{A}[C]^+_n$ and $\mathbf{A}[C]^-_n$ be two $n$ -element chains, which we view as lattices. Denoting $C^+_n \,{:=}\, \{ c_1, \ldots, c_n \}$ , with $c_1 \lt \ldots \lt c_n$ , let $C^-_n \,{:=}\, \{{\sim } c_1, \ldots, {\sim } c_n \}$ , with ${\sim } c_n \lt \ldots \lt{\sim } c_1$ . Consider the ordinal sum of these lattices, $\mathbf{A}[D]^{\mathbf{A}[C]} : = \mathbf{A}[C]^-_n \oplus \mathbf{A}[D] \oplus \mathbf{A}[C]^+_n$ , in which the order and the De Morgan negation are defined as follows: for all $d \in D$ and $c_i \in C^+_n$ , we let ${\sim } c_i\lt d\lt c_i$ and ${\sim }^{\mathbf{A}[D]^{\mathbf{A}[C]}} d ={\sim }^{\mathbf{A}[D]} d$ . Then, $\mathbf{A}[D]^{\mathbf{A}[C]}$ is a finite De Morgan algebra, and can therefore be endowed with the Heyting implication determined by the order, turning it into a symmetric Heyting algebra.

We now proceed to the axiomatization of $\mathbb{V}(\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}})$ . First, we define an equational class we shall call $\mathbb{PP}^{\Rightarrow _{\textsf{H}}}$ , then we show that it coincides with $\mathbb{V}(\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}})$ .

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

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

2. (2) $\mathbf{A}$ satisfies the following equation:

   \begin{equation*} {{\circ }(x_1 \Rightarrow x_2) \land {\circ }(x_2\Rightarrow x_3) } \leq {{\circ } x_1 \lor {\circ } x_4 \lor {\circ }(x_4\Rightarrow x_3)} \lor {\circ }(x_3\Rightarrow x_2) \lor {\circ }(x_2\Rightarrow x_1). \end{equation*}

Our next aim is to check the following results: $\mathbb{PP}^{\Rightarrow _{\textsf{H}}}$ is the variety (and the quasi-variety) generated by $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ (Theorem 77), and $\mathbb{PP}^{\Rightarrow _{\textsf{H}}}$ is the equivalent algebraic semantics of the algebraizable logic $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ (Theorem 78).

We shall prove the above by relying on a few lemmas that also have an independent interest, in that they shed some light on the structures of symmetric Heyting algebras in general and of algebras in $\mathbb{V}(\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}})$ in particular.

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

\begin{equation*} \neg ^{\mathbf {PP_6^{\Rightarrow _{\textsf {H}}}}}(a) = \begin {cases} {\hat {\mathbf {t}}} & \text {if } a = {\hat {\mathbf {f}}},\\ {\hat {\mathbf {f}}} & \text {otherwise.} \end {cases} \quad \text {and} \quad \Delta ^{\mathbf {PP_6^{\Rightarrow _{\textsf {H}}}}}(a) = \begin {cases} {\hat {\mathbf {t}}} & \text { if } a = {\hat {\mathbf {t}}},\\ {\hat {\mathbf {f}}} & \text { otherwise.} \end {cases} \end{equation*}

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

Lemma 73 (Sankappanavar 1987, Thm. 3.3). The lattice of congruences of each SHA $\mathbf{A}$ is isomorphic to the lattice of regular filters on $\mathbf{A}$ .

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

\begin{equation*} \Delta \Delta x \approx \Delta x\qquad \qquad ({\Delta\text{-idemp}}) \end{equation*}

Lemma 74 (Monteiro, 1980, Thm. 4.17, p. 82). Let $\mathbf{A}$ be a SHA that satisfies $({\Delta\text{-idemp}})$ and let $B \subseteq A$ . The regular filter $F(B)$ generated by $B$ is given by:

\begin{equation*} F(B) \,{:=}\, \{ a \in A : \Delta (a_1 \land \ldots \land a_n) \leq a \text { for some } a_1, \ldots, a_n \in B \}. \end{equation*}

Lemma 75 (Sankappanavar, 1987, Cor. 4.8). Let $\mathbf{A}$ be a SHA that satisfies $({\Delta\text{-idemp}})$ . The following are equivalent:

1. (1) $\mathbf{A}$ is directly indecomposable.

2. (2) $\mathbf{A}$ is subdirectly irreducible.

3. (3) $\mathbf{A}$ is simple.

The subvariety of SHAs defined by the equation $({\Delta\text{-idemp}})$ is dubbed $\mathbb{SDH}_1$ by Sankappanavar (1987), who observes that it is a discriminator³ variety (see Burris and Sankappanavar 2011, Def. IV.9.3). This entails that $\mathbb{PP}^{\Rightarrow _{\textsf{H}}}$ is also a discriminator variety. The discriminator term for $\mathbb{PP}^{\Rightarrow _{\textsf{H}}}$ is the following:

\begin{equation*} t(x,y,z):=( \Delta (x \Leftrightarrow y) \land z )\lor ({\sim } \Delta (x \Leftrightarrow y) \land x ) \end{equation*}

where $x \Leftrightarrow y \,{:=}\, (x \Rightarrow y) \land (y \Rightarrow x)$ . To see this, consider Theorem 77 and note that on $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ we have, for all $c,d \in \mathcal{V}_6$ ,

\begin{equation*} \Delta ^{\mathbf {PP_6^{\Rightarrow _{\textsf {H}}}}} (c \Leftrightarrow d) = \begin {cases} {\hat {\mathbf {t}}} & \text { if } c = d,\\ {\hat {\mathbf {f}}} & \text { otherwise.} \end {cases} \end{equation*}

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

Lemma 76. Every simple algebra $\mathbf{A} \in \mathbb{PP}^{\Rightarrow _{\textsf{H}}}$ is (isomorphic to) a subalgebra of $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ .

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

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

Now assume, by way of contradiction, that there are elements $a_1, a_2, a_3, a_4 \in D$ such that $a_1 \lt a_2 \lt a_3 \lt a_4$ , forming a four-element chain. Then the inequality in the second item of Definition 72 would fail, for we would have:

\begin{align*} {{\circ }(a_1 \Rightarrow a_2) \land {\circ }(a_2\Rightarrow a_3) } &= {\circ } \top \land {\circ } \top\\ &= \top\\ &\not \leq \bot\\ &= {\circ } a_1 \lor {\circ } a_4 \lor {\circ }(a_4 \Rightarrow a_3) \lor {\circ }( a_3\Rightarrow a_2) \lor {\circ }( a_2\Rightarrow a_1). \end{align*}

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

Theorem 77 below, the first of the announced goals, is then essentially an immediate corollary of Lemma 76:

Theorem 77. $\mathbb{PP}^{\Rightarrow _{\textsf{H}}}$ is the variety (and the quasi-variety) generated by $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ .

Proof. From Lemma 76 and, for the quasi-variety result, see for example Clark and Davey (1998, Thm. 1.3.6.ii).

We are also ready to prove the second of the goals:

Theorem 78. $\mathbb{PP}^{\Rightarrow _{\textsf{H}}}$ is the equivalent algebraic semantics of the algebraizable logic $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ .

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

Another consequence of Lemma 76 that has a logical impact is the following. Recall that the universes of subalgebras of $\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}$ are the same as those of $\mathbf{PP_6}$ , minus the five-element chain. Let us denote the corresponding algebras by $ \mathbf{PP_4^{\Rightarrow _{\textsf{H}}}}, \mathbf{PP_3^{\Rightarrow _{\textsf{H}}}}$ and $\mathbf{PP_2^{\Rightarrow _{\textsf{H}}}}$ .

Corollary 79. The (proper, non-trivial) subvarieties of $\mathbb{PP}^{\Rightarrow _{\textsf{H}}}$ are precisely the following (the axiomatizations are obtained by adding the mentioned equations to the axiomatization of $\mathbb{PP}^{\Rightarrow _{\textsf{H}}}$ ):

1. (1) $\mathbb{V} (\mathbf{PP_4^{\Rightarrow _{\textsf{H}}}})$ , axiomatized by the equation $ x \land{\sim } x \leq y \lor{\sim } y$ .

2. (2) $\mathbb{V} (\mathbf{PP_3^{\Rightarrow _{\textsf{H}}}})$ , axiomatized by $ x \lor (x \Rightarrow (y \lor \neg y ) ) \approx \top$ .

3. (3) $\mathbb{V} (\mathbf{PP_2^{\Rightarrow _{\textsf{H}}}})$ , axiomatized by $x \lor{\sim } x \approx \top$ .

Note that $\mathbb{V} (\mathbf{PP_4^{\Rightarrow _{\textsf{H}}}})$ and $\mathbb{V} (\mathbf{PP_3^{\Rightarrow _{\textsf{H}}}})$ are incomparable, while $\mathbb{V} (\mathbf{PP_2^{\Rightarrow _{\textsf{H}}}})$ , which is (up a choice of language) just the variety of Boolean algebras, is included in both of them.

Proof. All claims are established by easy computations. The main observation we need is that, by Jónsson’s Lemma (see Burris and Sankappanavar 2011, Cor. IV.6.10), for $\mathbf{A} \in \{ \mathbf{PP_4^{\Rightarrow _{\textsf{H}}}}, \mathbf{PP_3^{\Rightarrow _{\textsf{H}}}}, \mathbf{PP_2^{\Rightarrow _{\textsf{H}}}}\}$ , the subdirectly irreducible (here meaning simple) algebras in each $\mathbb{V} (\mathbf{A})$ are in $ \mathbb{H} \mathbb{S} (\mathbf{A})$ , and $\mathbb{H}\mathbb{S} (\mathbf{A}) = \mathbb{S} (\mathbf{A})$ .

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

Proposition 80. $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ is determined by $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}, \{{\hat{\mathbf{t}}} \} \rangle$ .

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

\begin{equation*} \Phi \vdash _{\mathcal {PP}^{\Rightarrow _{\textsf {H}}}_\top } \varphi \quad \text { if, and only if, } \quad \Delta \Phi \vdash _{\mathcal {PP}^{\Rightarrow _{\textsf {H}}}_{\!\leq }} \varphi \end{equation*}

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

\begin{equation*} \Phi, \varphi \vdash _{\mathcal {PP}^{\Rightarrow _{\textsf {H}}}_\top } \psi \quad \text { iff } \quad \Phi \vdash _{\mathcal {PP}^{\Rightarrow _{\textsf {H}}}_\top } \Delta \varphi \Rightarrow \psi . \end{equation*}

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

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

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

\begin{equation*} \Delta (a \Rightarrow b), \Delta (b \Rightarrow a) \in D. \end{equation*}

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

\begin{equation*} F(\{ a \Rightarrow b \}) = \{ c \in A : \Delta (a \Rightarrow b) \leq c \}. \end{equation*}

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

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

8. On Interpolation for $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ and $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ , and Amalgamation for $\mathbb{PP}^{\Rightarrow _{\textsf{H}}}$

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

Definition 82. A $\Sigma$ -logic $\vdash$ has the

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

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

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

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

Let us see now which of these interpolation properties the logic $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ satisfies.

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

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

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

Let us now take a look at the situation for $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ . Recall that, in the previous section, we presented the DDT for this logic, which demands a (derived) connective different from $\Rightarrow$ to play the role of implication. In the same way as in the proof of the above theorem, this DDT guarantees that the (EIP) holds for this logic. We show however that (CIP) and (MIP) also hold. In what follows, recall from Proposition 80 that $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ is determined by the single matrix $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}, \{{\hat{\mathbf{t}}} \} \rangle$ .

Theorem 84. The logic $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ has the (EIP), the (CIP), and the (MIP).

Proof. It is enough to show it has the (MIP). Since $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ is finitary, it suffices to consider finite sets. Given $\Phi, \Psi \vdash _{\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top } \varphi$ , let $\textsf{props}(\Phi )\cap \textsf{props}(\Psi \cup \{\varphi \})=\{p_1,\ldots, p_k\}\neq \varnothing$ . Consider $\mathcal{U} \,{:=}\, \{v\in \textsf{Hom} (L_{\Sigma }(\{p_1,\ldots, p_k\}), \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}}) : v(\Phi )={\hat{\mathbf{t}}}\}$ . For each $v\in \mathcal{U}$ and $1\leq i\leq k$ , let

\begin{align*} \varphi ^v_i(p)& \,{:=}\, \begin{cases} p\land{\circ } p & \mbox{ if }v(p_i)={\hat{\mathbf{t}}}\\{\sim }{\downarrow } p & \mbox{ if }v(p_i)={\mathbf{t}}\\{\uparrow } p\land{\downarrow } p \land{\sim }{\circ } p & \mbox{ if }v(p_i)\in \{{\mathbf{b}},{\mathbf{n}}\}\\{\sim }{\uparrow } p & \mbox{ if }v(p_i)={\mathbf{f}}\\{\sim } p\land{\circ } p & \mbox{ if }v(p_i)={\hat{\mathbf{f}}} \end{cases}\\ I^v_{\mathbf{b}}& \,{:=}\, \{i:v(p_i)={\mathbf{b}}\}\\ J^v_{\mathbf{n}}& \,{:=}\, \{j:v(p_j)={\mathbf{n}}\} \end{align*}

and

\begin{align*} \psi _v&\,{:=}\,\bigwedge _{1\leq i\leq k}\varphi ^v_i(p_i)\land \bigwedge _{i\in I_{\mathbf{b}}^v,j\in J_{\mathbf{n}}^v}{\sim }{\circ }(p_i\Rightarrow p_j)\\ \xi &\,{:=}\,\bigvee _{v\in \mathcal{U}}\psi _v \end{align*}

If we set $\equiv \; \subseteq \mathcal{V}_6\times \mathcal{V}_6$ such that $a \equiv b$ iff $a=b$ or $\{a,b\}=\{{\mathbf{b}},{\mathbf{n}}\}$ we obtain that, for all $v'\in \textsf{Hom} (\mathbf{L}_{\Sigma }(P), \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}})$ ,

\begin{equation*}v'(\varphi ^v_i(p))= \begin {cases} {\hat {\mathbf {t}}} & \text {if } v'(p)\equiv v(p_i) \\ {\hat {\mathbf {f}}} & \text {otherwise.}\\ \end {cases} \end{equation*}

Thus, if $v'(\psi _v)={\hat{\mathbf{t}}}$ then $v(p_i)\equiv v'(p_i)$ for every $1\leq i\leq k$ .

Let us show that $\xi \vdash _{\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top } \varphi$ . For every $v'\in \textsf{Hom} (\mathbf{L}_{\Sigma }(P), \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}})$ such that $v'(\xi )={\hat{\mathbf{t}}}$ , there is $v\in \mathcal{U}$ such that $v(p_i)\equiv v'(p_i)$ for every $1\leq i\leq k$ . Also, $\{{\mathbf{b}},{\mathbf{n}}\}=\{v(p_i),v(p_j)\}$ if, and only if, $\{{\mathbf{b}},{\mathbf{n}}\}=\{v'(p_i),v'(p_j)\}$ , and therefore $v(\psi )=v'(\psi )$ for every $\psi$ such that $\textsf{props}(\psi )\subseteq \{p_1,\ldots, p_k\}$ . Thus, without loss of generality, we proceed considering that $v(p_i)=v'(p_i)$ for $1\leq i\leq k$ .

Considering $v''\in \textsf{Hom} (\mathbf{L}_{\Sigma }(P), \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}})$ such that

\begin{equation*}v''(p)\,{:=}\, \begin {cases} v(p) & p\in P{\setminus }\textsf {props}(\Phi )\\ v'(p) &p\in \textsf {props}(\Phi ){\setminus }\{p_1,\ldots, p_k\} \end {cases}\end{equation*}

we have that $v''(\Phi )=v''(\Psi )={\hat{\mathbf{t}}}$ , thus from $\Phi, \Psi \vdash _{\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top } \varphi$ we conclude that $v''(\varphi )=v'(\psi )={\hat{\mathbf{t}}}$ and therefore $\xi \vdash _{\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top } \varphi$ . Finally, to see that $\Phi \vdash _{\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top } \xi$ , note that if $v(\Phi )=\{{\hat{\mathbf{t}}}\}$ then, by definition, $v\in \mathcal{U}$ and therefore $v(\psi _v)=v(\xi )={\hat{\mathbf{t}}}$ .

When a logic satisfies some of the above interpolation properties and we know it is algebraizable, the class of algebras corresponding to the equivalent algebraic semantics satisfies so-called “amalgamation properties,” which we formulate below based on Czelakowski and Pigozzi (1998).

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

Definition 85 (Czelakowski and Pigozzi 1998, Def. 5.2). A class of algebras $\textsf{K}$ has the

1. (1) ordinary amalgamation property (OAP) when for all $\mathbf{A},\mathbf{B},\mathbf{C} \in \textsf{K}$ , and all homomorphisms $f : \mathbf{C} \rightarrowtail \mathbf{A}$ and $g : \mathbf{C} \rightarrowtail \mathbf{B}$ , there exists $\mathbf{D} \in \textsf{K}$ and homomorphisms $h : \mathbf{A} \rightarrowtail \mathbf{D}$ and $k : \mathbf{B} \rightarrowtail \mathbf{D}$ such that $hf = kg$ .

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

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

The reader is referred to Czelakowski and Pigozzi (1998, Thm. 5.3) for the relationships between the above notions of amalgamation. In particular, we have that (MAP) implies both (FAP) and (OAP).

Theorem 86. $\mathbb{PP}^{\Rightarrow _{\textsf{H}}}$ has the (OAP), the (FAP), and the (MAP).

Proof. Clearly, it suffices to show that $\mathbb{PP}^{\Rightarrow _{\textsf{H}}}$ has the (MAP). By Theorem 78, we know that $\mathbb{PP}^{\Rightarrow _{\textsf{H}}}$ is the equivalent algebraic semantics of $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ . We just saw that this logic satisfies (MIP); hence, by Czelakowski and Pigozzi (1998, Cor. 5.27), $\mathbb{PP}^{\Rightarrow _{\textsf{H}}}$ satisfies (MAP).

9. Conclusions and Future Work

The present paper has initiated the study of implicative expansions of logics of perfect paradefinite algebras by considering classic-like and Heyting implications, both in the and in the framework. We investigated semantical characterizations (via classes of algebras and logical matrices) as well as proof-theoretical ones (via and Hilbert-style calculi) of these expansions. For the expansions with a Heyting implication, the new connective introduced a further challenge, for the resulting logic ( $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ ) cannot be characterized by a single logical matrix; however, we have proved that it can be characterized by a single finite PNmatrix. Over such expansions, we also studied properties of interpolation and amalgamation for the corresponding algebraic models. We indicate below a few directions that we believe could prove worthwhile pursuing in future research.

Alternative expansions of the logics of PP-algebras

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

Extensions of $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$

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

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

  1. (1) the logic of $\mathbb{V} (\mathbf{PP_4^{\Rightarrow _{\textsf{H}}}})$ is axiomatized by $(p \land{\sim } p) \Rightarrow (q \lor{\sim } q)$ ;

  2. (2) the logic of $\mathbb{V} (\mathbf{PP_3^{\Rightarrow _{\textsf{H}}}})$ by $ p \lor (p \Rightarrow (q \lor \neg q ) )$ ; and

  3. (3) the logic of $\mathbb{V} (\mathbf{PP_2^{\Rightarrow _{\textsf{H}}}})$ , which is (up to the choice of language) just classical logic, by $p \lor{\sim } p$ .

• • The number of axiomatic extensions of $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ (all logics which are obviously finitary) is larger but also finite, for each axiomatic extension may be characterized by the submatrices of the original matrices that satisfy the axioms.⁴

• • As we have seen (cf. Proposition 80), the assertional logic $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ is itself a (non-axiomatic, non-self-extensional) extension of $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ . Algebraizability of $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ (Theorem 78) entails that its axiomatic extensions are in one-to-one correspondence with the subvarieties of $\mathbb{V}(\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}})$ , so again we can conclude that there are only three of them.

• • In contrast to the preceding results, we conjecture that it may be possible to construct countably many distinct (non-axiomatic) finitary extensions of $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ . The theory of algebraizability would then tell us that the variety $\mathbb{PP}^{\Rightarrow _{\textsf{H}}}$ has at least countably many subquasivarieties.

Now considering the extensions of $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\textsf{up}}$ , we can say the following:

• • Similarly to the setting, all axiomatic extensions of $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\textsf{up}}$ are characterized by the sets of (sub)matrices in $ \{ \langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}},{\uparrow } a \rangle : a \in \mathcal{V} \}$ that satisfy the corresponding axioms, hence their cardinality is also finite. Their companions are obtained by adding the same axioms to $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ .

• • In consequence, there are at least three self-extensional extensions of $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\textsf{up}}$ , namely, the ones determined by the matrices which satisfy the corresponding axioms. (There may be more, but each of them will have as companion one of the three self-extensional extensions of $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ mentioned earlier.)

• • The methods used in the previous sections may be used to obtain analytic axiomatizations for all the logics determined by sets of (sub)matrices in $ \{ \langle \mathbf{PP}_6^{\Rightarrow _{\textsf{H}}},{\uparrow } a \rangle : a \in \mathcal{V} \}$ .

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

Problem 1. Describe the lattice of all ( ) extensions of $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$ and the lattice of all ( ) extensions of $\mathcal{PP}^{\rhd, \Rightarrow _{\textsf{H}}}_{\textsf{up}}$ .

Problem 2. Look at the same problem again, but now restricting one’s attention, on the one hand, to the sublattice consisting of all the extensions of $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ , and on the other hand, to the sublattice consisting of all the extensions of the logic determined by the matrix $\langle \mathbf{PP_6^{\Rightarrow _{\textsf{H}}}},{{\uparrow }{\hat{\mathbf{t}}}} \rangle$ . Due to the algebraizability of $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_\top$ , for finitary logics the problem may be rephrased as: describe the lattice of all subquasivarieties of $\mathbb{V}(\mathbf{PP_6^{\Rightarrow _{\textsf{H}}}})$ .

Fragments of the language of $\mathcal{PP}^{\Rightarrow _{\textsf{H}}}_{\!\leq }$

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