2 Preliminaries

We adopt the standard terminology and notation employed in Abstract Algebraic Logic (AAL), and refer the reader to [Reference Font32] for a recent and thorough treatment on the subject. We will here only briefly introduce the AAL notions needed in the sequel. These often rely on ground concepts from Universal Algebra and the theory of sentential logics. Classical references on these subjects are [Reference Burris and Sankappanavar10, Reference Wójcicki56].

We trust the reader is acquainted with the notions of algebra, homomorphism, congruence, variety, and quasivariety. We ought however to fix some notation. Given two algebras ${\boldsymbol {A}},{\boldsymbol {B}}$ , we denote a homomorphism h from ${\boldsymbol {A}}$ to ${\boldsymbol {B}}$ simply by $h: {\boldsymbol {A}} \to {\boldsymbol {B}}$ , and the least congruence on ${\boldsymbol {A}}$ containing a subset $X \subseteq A \times A$ by $\Theta ^{\boldsymbol {A}}(X)$ . The set of all congruences on ${\boldsymbol {A}}$ will be denoted by $\mathrm {Co}\, {\boldsymbol {A}}$ ; and given a class of algebras ${\mathsf {K}}$ , the set of all congruences $\theta \in \mathrm {Co}\, {\boldsymbol {A}}$ such that ${\boldsymbol {A}}/\theta \in {\mathsf {K}}$ will be denoted by $\mathrm {Co}_{\mathsf {K}}{\boldsymbol {A}}$ , and will be referred to as the set of congruences of ${\boldsymbol {A}}$ relative to ${\mathsf {K}}$ , or simply the set ${\mathsf {K}}$ -relative congruences of ${\boldsymbol {A}}$ .

Let ${\boldsymbol {A}}$ be an algebra. A subset $B \subseteq A$ is a subuniverse of ${\boldsymbol {A}}$ , if it is closed under the operations of ${\boldsymbol {A}}$ . That is, if for every n-ary operation symbol $f \in {\mathcal {L}}$ and for every $b_1 , \ldots , b_n \in B$ , it holds that $f^{\boldsymbol {A}}(b_1 , \ldots , b_n) \in B$ . An algebra ${\boldsymbol {B}}$ of the same similarity type as ${\boldsymbol {A}}$ is a subalgebra of ${\boldsymbol {A}}$ , fact which we shall denote by ${\boldsymbol {B}} \leq {\boldsymbol {A}}$ , if $B \subseteq A$ and for every operation symbol $f \in {\mathcal {L}}$ , it holds that $f^{\boldsymbol {B}} = f^{\boldsymbol {A}} \!\! \upharpoonright _{B}$ . Clearly, if ${\boldsymbol {B}}$ is a subalgebra of ${\boldsymbol {A}}$ , then B is a subuniverse of ${\boldsymbol {A}}$ . Given an algebra ${\boldsymbol {A}}$ and a subset $X \subseteq A$ , the subuniverse generated by X, which we shall denote by $\mathrm {Sg}_{\mathcal {L}}^{\boldsymbol {A}}(X)$ , is the least subuniverse of ${\boldsymbol {A}}$ containing X.

Let ${\boldsymbol {A}}$ be an algebra. A congruence $\theta \in \mathrm {Co}\, {\boldsymbol {A}}$ is compatible with a subset $F \subseteq A$ , if whenever $\langle a,b \rangle \in \theta $ and $a \in F$ , then $b \in F$ ; in other words, $\theta $ does not identify elements inside F with elements outside F. The least congruence on ${\boldsymbol {A}}$ compatible with a given $F \subseteq A$ is the identity congruence on ${\boldsymbol {A}}$ , hereby denoted by $id_{\boldsymbol {A}}$ , while the largest congruence on ${\boldsymbol {A}}$ compatible with F, which always exists, is known as the Leibniz congruence of F, and is denoted by ${\boldsymbol {\varOmega }}^{\boldsymbol {A}}(F)$ . The Leibniz congruence can be lifted to the powerset. Given ${\mathscr {C}} \subseteq \mathscr {P}(A)$ , the Tarski congruence of ${\mathscr {C}}$ is the largest congruence on ${\boldsymbol {A}}$ compatible with every $F \in {\mathscr {C}}$ ; that is, .

Given a class of algebras ${\mathsf {K}}$ , we denote by $\mathbb {Q}{\mathsf {K}}$ and $\mathbb {V}{\mathsf {K}}$ the least quasivariety containing ${\mathsf {K}}$ and the least variety containing ${\mathsf {K}}$ , respectively, and we denote by $\mathbb {I}$ , $\mathbb {P}$ , $\mathbb {P}_{\scriptscriptstyle \!\mathrm {S}}$ , $\mathbb {S}$ , and $\mathbb {H}$ the isomorphism, direct product, subdirect product, subalgebra, and homomorphic image operators, respectively. Recall that a trivial algebra is one with a single element universe, and observe that every quasivariety (and hence every variety as well) contains all trivial algebras. We assume the reader is familiar with the notion of subdirectly irreducible algebra, as well as Birkhoff’s famous result characterizing varieties in terms of their subdirectly irreducible elements [Reference Birkhoff5, Theorem 2]. Namely, if ${\mathsf {K}}$ is a variety, then ${\mathsf {K}} = \mathbb {IP}_{\mathrm {S}}({\mathsf {K}}_{\mathrm {s.i.}})$ , where ${\mathsf {K}}_{\mathrm {s.i.}}$ denotes the set of subdirectly irreducible elements of ${\mathsf {K}}$ —see for instance [Reference Burris and Sankappanavar10, Corollary 9.7] or [Reference Bergman4, Theorem 3.44].

A generalization of Birkhoff’s result for quasivarieties will be needed in Section 9.2. Given a class of algebras ${\mathsf {K}}$ , an algebra ${\boldsymbol {A}}$ is subdirectly irreducible relative to ${\mathsf {K}}$ , or is subdirectly ${\mathsf {K}}$ -irreducible, if for every subdirect embedding $\alpha : {\boldsymbol {A}} \rightarrow \prod _{i \in I} {\boldsymbol {A}}_i$ , with $\{ {\boldsymbol {A}}_i : i \in I \} \subseteq {\mathsf {K}}$ , there exists $i \in I$ such that $\pi _i \circ \alpha : {\boldsymbol {A}} \rightarrow {\boldsymbol {A}}_i$ is an isomorphism. Quasivarieties can also be characterized in terms of their relative subdirectly irreducible elements—this fact is not so well-known as its particular case for varieties, but a proof can be found in [Reference Caicedo11, Corollary 6] or [Reference Gorbunov35, Theorem 3.1.1]; in the latter reference the original result is credited to Mal’cev [Reference Mal’cev41]. Consequently, if ${\mathsf {K}}$ is a quasivariety, then ${\mathsf {K}} = \mathbb {IP}_s({\mathsf {K}}_{\mathrm {r.s.i.}})$ , where ${\mathsf {K}}_{\mathrm {r.s.i.}}$ denotes a set of subdirectly ${\mathsf {K}}$ -irreducible elements of ${\mathsf {K}}$ .

By a (sentential) logic we understand a structural consequence relation on $\mathrm {Fm}_{\mathcal {L}}$ , where $\mathrm {Fm}_{\mathcal {L}}$ denotes the universe of the free algebra of terms ${\boldsymbol {Fm}}$ generated by a denumerable set of variables $\mathrm {Var}$ over an algebraic language ${\mathcal {L}}$ . It is common practice to denote by ${\mathcal {S}}$ an arbitrary logic, i.e., the set of all rules of ${\mathcal {S}}$ , and by $\Gamma \vdash _{\mathcal {S}} \varphi $ or $\langle \Gamma ,\varphi \rangle \in \; \vdash _{\mathcal {S}}$ , with $\Gamma \cup \{\varphi \} \subseteq \mathrm {Fm}_{\mathcal {L}}$ , one such particular rule. We abbreviate $\varnothing \vdash \varphi $ simply by $\vdash \varphi $ , and the facts $\varphi \vdash _{\mathcal {S}} \psi $ and $\psi \vdash _{\mathcal {S}} \varphi $ by $\varphi \dashv \vdash _{\mathcal {S}} \psi $ . The relation identifying such pairs of formulas is called the interderivability relation.

Let ${\mathcal {S}}$ be a logic. A logic ${\mathcal {S}}'$ (in the same language of ${\mathcal {S}}$ ) is an extension of ${\mathcal {S}}$ , if $\vdash _{\mathcal {S}} \; \subseteq \; \vdash _{{\mathcal {S}}'}$ , a fact which we will denote simply by ${\mathcal {S}} \leq {\mathcal {S}}'$ . Now, let ${\mathcal {L}}'$ be a language such that ${\mathcal {L}} \subseteq {\mathcal {L}}'$ . A logic ${\mathcal {S}}'$ in the language ${\mathcal {L}}'$ is an expansion of ${\mathcal {S}}$ , if for every set of ${\mathcal {L}}$ -formulas $\Gamma \cup \{\varphi \} \subseteq \mathrm {Fm}_{\mathcal {L}}$ , $\Gamma \vdash _{\mathcal {S}} \varphi \; \Rightarrow \; \Gamma \vdash _{{\mathcal {S}}'} \varphi $ ; in case the converse implication also holds, that is for every set of ${\mathcal {L}}$ -formulas $\Gamma \cup \{\varphi \} \subseteq \mathrm {Fm}_{\mathcal {L}}$ we have $\Gamma \vdash _{\mathcal {S}} \varphi \; \Leftrightarrow \; \Gamma \vdash _{{\mathcal {S}}'} \varphi $ , the logic ${\mathcal {S}}'$ is called a conservative expansion of ${\mathcal {S}}$ , and the logic ${\mathcal {S}}$ is called the ${\mathcal {L}}$ -fragment of ${\mathcal {S}}'$ .

The sets of formulas which are $\vdash _{\mathcal {S}}$ -closed are called ${\mathcal {S}}$ -theories. The set of all ${\mathcal {S}}$ -theories is denoted by $\mathcal {T}\!h({\mathcal {S}})$ and the least ${\mathcal {S}}$ -theory, whose elements are called ${\mathcal {S}}$ -theorems, is denoted by ${\mathrm{Thm}}_{{\mathcal {S}}}$ . A logic ${\mathcal {S}}$ is called inconsistent if ${\mathrm{Thm}}_{\mathcal {S}} = \mathrm {Fm}_{\mathcal {L}}$ . The notion of ${\mathcal {S}}$ -theory turns out to be an instance of a more general notion, applicable to arbitrary algebras. Given an algebra ${\boldsymbol {A}}$ , an ${\mathcal {S}}$ -filter of ${\boldsymbol {A}}$ is a subset $F \subseteq A$ such that, for every homomorphism $h \colon {\boldsymbol {Fm}} \to {\boldsymbol {A}}$ and every $\Gamma \cup \{ \varphi \} \subseteq \mathrm {Fm}_{\mathcal {L}}$ , if $\Gamma \vdash _{\mathcal {S}} \varphi $ and $h(\Gamma ) \subseteq F$ , then $h(\varphi ) \in F$ . We denote the set of all ${\mathcal {S}}$ -filters of ${\boldsymbol {A}}$ by . As claimed, . The least ${\mathcal {S}}$ -filter of ${\boldsymbol {A}}$ containing $X \subseteq A$ is denoted by , and the least ${\mathcal {S}}$ -theory containing $\Gamma \subseteq \mathrm {Fm}_{\mathcal {L}}$ is denoted by .

Although the Leibniz and Tarski congruences were defined for arbitrary sets and families of sets, respectively, we shall usually consider them over ${\mathcal {S}}$ -filters and families of ${\mathcal {S}}$ -filters, respectively. The next auxiliary lemma relates the notions of logical filter, Leibniz congruence, and subalgebra.

An ${\mathcal {L}}$ -equation is a pair of formulas $\langle \varphi ,\psi \rangle \in \mathrm {Fm}_{\mathcal {L}} \times \mathrm {Fm}_{\mathcal {L}}$ , usually abbreviated as $\varphi \approx \psi $ . We denote the set of all ${\mathcal {L}}$ -equations by $\mathrm {Eq}_{\mathcal {L}}$ . Given a class of algebras ${\mathsf {K}}$ , the equational consequence relation relative to ${\mathsf {K}}$ is the relation $\vDash _{\mathsf {K}} \; \subseteq \mathscr {P}(\mathrm {Eq}_{\mathcal {L}}) \times \mathrm {Eq}_{\mathcal {L}}$ defined by

$$ \begin{align*} \Pi \vDash_{\mathsf{K}} \varphi \approx \psi\quad \text{iff}\quad & \forall {\boldsymbol{A}} \in {\mathsf{K}} \; \forall h : {\boldsymbol{Fm}} \to {\boldsymbol{A}} \\ & \forall \delta \approx \epsilon \in \Pi \quad h(\delta) = h(\epsilon) \; \Rightarrow \; h(\varphi) = h(\psi). \end{align*} $$

It is common practice to abbreviate $\vDash _{\{{\boldsymbol {A}}\}}$ simply by $\vDash _{\boldsymbol {A}}$ .

A matrix model of ${\mathcal {S}}$ is a pair $\langle {\boldsymbol {A}} , F \rangle $ such that . We denote the class of all matrix models of a logic ${\mathcal {S}}$ by ${\mathsf {Mod}}({\mathcal {S}})$ . A matrix model $\langle {\boldsymbol {A}} , F \rangle \in {\mathsf {Mod}}({\mathcal {S}})$ is called reduced if ${\boldsymbol {\varOmega }}^{\boldsymbol {A}}(F) = id_{\boldsymbol {A}}$ . We denote the class of all reduced matrix models by ${\mathsf {Mod}}^*({\mathcal {S}})$ .

Two classes of algebras are usually considered in AAL as naturally, and intrinsically, associated with a logic. These are obtained as follows:

(1)

It turns out that ${\mathsf {Alg}}({\mathcal {S}}) = \mathbb {P}_{\scriptscriptstyle \!\mathrm {S}}\,{\mathsf {Alg}}^*({\mathcal {S}})$ [Reference Font and Jansana33, Theorem 2.23]. When one wishes to associate with a logic ${\mathcal {S}}$ an “algebraic counterpart” which is necessarily a variety, a third class of algebras is often considered, defined by

It can be proved that $\mathbb {V}({\mathcal {S}})$ is in fact the least variety containing ${\mathsf {Alg}}^*({\mathcal {S}})$ , i.e., $\mathbb {V}({\mathcal {S}}) = \mathbb {V}\,{\mathsf {Alg}}^*({\mathcal {S}})$ , and it is called the intrinsic variety of ${\mathcal {S}}$ .

2.1 The Leibniz and Frege hierarchies

The main classification of sentential logics in AAL is the so-called Leibniz hierarchy, characterizing logics by means of algebraic properties of the Leibniz operator.Footnote ⁴ For instance, the Leibniz operator (over the ${\mathcal {S}}$ -filters of an arbitrary algebra ${\boldsymbol {A}}$ ) of an algebraizable logic ${\mathcal {S}}$ is an isomorphism between the lattice of ${\mathcal {S}}$ -filters of ${\boldsymbol {A}}$ and the lattice of ${\mathsf {Alg}}^*({\mathcal {S}})$ -relative congruences of ${\boldsymbol {A}}$ , which furthermore commutes with inverse images of homomorphisms. In [Reference Lewin, Mikenberg and Schwarze39], the non-algebraizability of ${\mathscr {C}}_1$ was established by exhibiting an algebra ${\boldsymbol {A}}$ where the Leibniz operator over the ${\mathscr {C}}_1$ -filters of ${\boldsymbol {A}}$ was not injective.

We next introduce the main classes of logics belonging to the Leibniz hierarchy. However, since their characterizations in terms of the algebraic properties of Leibniz operator will not be used in the sequel, we have chosen to define them here in a manner that will suit our purposes better.

Definition 2.2. A logic ${\mathcal {S}}$ is:

1. (i) protoalgebraic if there exists a set of formulas ${\boldsymbol {\rho }}(x,y) \subseteq \mathrm {Fm}_{\mathcal {L}}$ satisfying

   (R) $$ \begin{align} \varnothing \vdash_{\mathcal{S}} {\boldsymbol{\rho}}(x,x), \end{align} $$
   (MP) $$ \begin{align} x , {\boldsymbol{\rho}}(x,y) \vdash_{\mathcal{S}} y , \end{align} $$

2. (ii) equivalential if there exists a set of formulas ${\boldsymbol {\rho }}(x,y) \subseteq \mathrm {Fm}_{\mathcal {L}}$ satisfying (R), (MP) and for every n-ary function symbol $f \in \mathcal {L}$ ,

   (RP) $$ \begin{align} {\boldsymbol{\rho}}(x_1 ,y_1) \cup \cdots \cup {\boldsymbol{\rho}}(x_n ,y_n) \vdash_{\mathcal{S}} {\boldsymbol{\rho}}\big(f(x_1 \ldots x_n) , f(y_1 \ldots y_n)\big) , \end{align} $$

3. (iii) truth-equational if there exists a set of equations ${\boldsymbol {\tau }}(x) \subseteq \mathrm {Eq}_{\mathcal {L}}$ such that

   $$ \begin{align*} \forall \langle {\boldsymbol{A}} , F \rangle \in {\mathsf{Mod}}^*({\mathcal{S}}) \; \forall a \in A \quad a \in F \;\Leftrightarrow\; \forall \delta &\approx \epsilon \in {\boldsymbol{\tau}}(x) \; \delta^{\boldsymbol{A}}(a)\\ &= \epsilon^{\boldsymbol{A}}(a), \end{align*} $$

4. (iv) weakly algebraizable if it is protoalgebraic and truth-equational,

5. (v) algebraizable if it is equivalential and truth-equational.

In case the set of congruence formulas in item (ii) is finite, the underlying logic is called finitely equivalential, and if the logic is furthermore truth-equational, it is called finitely algebraizable.

We shall make use of an equivalent formulation of truth-equationality also established by Raftery in [Reference Raftery51, Proposition 22]. A logic ${\mathcal {S}}$ is truth-equational if and only if there exists a set of equations ${\boldsymbol {\tau }}(x) \subseteq \mathrm {Eq}_{\mathcal {L}}$ such that

$$\begin{align*}\forall \langle {\boldsymbol{A}} , F \rangle \in {\mathsf{Mod}}({\mathcal{S}}) \quad F = \{ a \in A : {\boldsymbol{\tau}}^{\boldsymbol{A}}(a) \subseteq {\boldsymbol{\varOmega}}^{\boldsymbol{A}}(F) \} , \end{align*}$$

where ${\boldsymbol {\tau }}^{\boldsymbol {A}}(a) = \{ \delta ^{\boldsymbol {A}}(a) \approx \epsilon ^{\boldsymbol {A}}(a) : \delta \approx \epsilon \in {\boldsymbol {\tau }}(x) \}$ . Notice that condition (iii) is the particular case of the condition above for reduced ${\mathcal {S}}$ -models.

Parallel to the Leibniz hierarchy, the Frege hierarchy classifies sentential logics according to some replacement properties, which can also be expressed by the congruentiality of the Frege relation (either over the ${\mathcal {S}}$ -theories of the underlying logic or over the ${\mathcal {S}}$ -filters of arbitrary algebras). The Frege relation of $F\subseteq A$ on ${\boldsymbol {A}}$ (relative to ${\mathcal {S}}$ ) is defined by

Notice that unlike the Leibniz congruence ${\boldsymbol {\varOmega }}^{\boldsymbol {A}}(F)$ , the equivalence relation

is not necessarily a congruence on ${\boldsymbol {A}}$ . The relation

is called the interderivability relation on ${\boldsymbol {A}}$ , and traditionally

is abbreviated by $\varphi \dashv \vdash _{\mathcal {S}} \psi $ , as we have seen already on page 482.

The Frege hierarchy comprises four classes of logics, which we next introduce.

Definition 2.3. A logic ${\mathcal {S}}$ is:

1. (i) self-extensional, if ,

2. (ii) Fregean, if for every $T \in \mathcal {T}\!h({\mathcal {S}})$ , ,

3. (iii) fully self-extensional, if for every ${\boldsymbol {A}}$ , ,

4. (iv) fully Fregean, if for every ${\boldsymbol {A}}$ and every , .

2.2 Parameterized sets of congruence formulas

The notion of (parameterized) sets of congruence formulas is a cornerstone of the theory of protoalgebraic logics and will play a prominent role in the present work. In particular, the subtle difference between having parameters or not will be crucial in our study of axiomatic extensions of ${\mathscr {C}}_1$ . We next compile some auxiliary facts concerning (parameterized) sets of congruence formulas which we will be used in the sequel.

Throughout the rest of the section, let $x,y \in \mathrm {Var}$ be two fixed distinct variables, and $\overline {z}$ an arbitrary possibly infinite sequence of variables (distinct from x and y). In particular, $\Delta (x,y,\overline {z}) \subseteq \mathrm {Fm}_{\mathcal {L}}$ denotes a set of formulas in the variables $x,y$ and possibly variables $\overline {z}$ . For ease of notation, we will use $c_1,c_2,c_3,\ldots $ to denote the elements of $\overline {c}$ , and simply write $\overline {c} \in A$ if all the elements are in A.

Definition 2.4. Let ${\mathcal {S}}$ be a logic, ${\boldsymbol {A}}$ an algebra, and . A set of formulas $\Delta (x,y,\overline {z}) \subseteq \mathrm {Fm}_{\mathcal {L}}$ is a set of parameterized congruence formulas for ${\mathcal {S}}$ , if for every ${\boldsymbol {A}}$ , every , and every $a,b \in A$ ,

$$\begin{align*}\langle a,b \rangle \in {\boldsymbol{\varOmega}}^{\boldsymbol{A}}(F) \quad\Leftrightarrow\quad \forall \overline{c} \in A \quad \Delta^{\boldsymbol{A}}(a,b,\overline{c}) \subseteq F {\kern0.3pt}. \end{align*}$$

In case $\Delta (x,y) \subseteq \mathrm {Fm}_{\mathcal {L}}$ has no parameters, it is called a set of congruence formulas for ${\mathcal {S}}$ .

The parameters are the variables $\overline {z}$ , which by no means need be in finite number. But if we pick a formula $\delta \in \Delta (x,y,\overline {z})$ , then we can write $\delta (x,y,z_1 , \ldots , z_n)$ , with $z_1 , \ldots , z_n$ occurring in $\overline {z}$ . For the sake of notation easiness, when the context is understood we sometimes write simply $\Delta $ instead of $\Delta (x,y,\overline {z})$ , or $\Delta (x,y)$ .

We shall need yet another important notation. Given a set of formulas $\Delta (x,y,\overline {z}) \subseteq \mathrm {Fm}_{\mathcal {L}}$ , let

The main characterization of a set of parameterized congruence formulas (in fact the original definition for the case without parameters [Reference Czelakowski28, Definition I.10]; for the case with parameters, see [Reference Font32, Exercise 6.28]) is the following:

Theorem 2.5. A set of formulas $\Delta (x,y,\overline {z}) \subseteq \mathrm {Fm}_{\mathcal {L}}$ is a set of parameterized congruence formulas for ${\mathcal {S}}$ if and only if the following conditions hold:

(p-R) $$ \begin{align} \varnothing \vdash_{\mathcal{S}} \Delta \langle x,x \rangle,\end{align} $$

(p-Sym) $$ \begin{align}\Delta \langle x,y \rangle \vdash_{\mathcal{S}} \Delta \langle y,x \rangle,\end{align} $$

(p-Trans) $$ \begin{align}\Delta \langle x,y \rangle \cup \Delta \langle y,z \rangle \vdash_{\mathcal{S}} \Delta \langle x,z \rangle,\end{align} $$

(p-MP) $$ \begin{align}x , \Delta \langle x,y \rangle \vdash_{\mathcal{S}} y,\end{align} $$

(p-Re) $$ \begin{align}\Delta \langle x_1,y_1 \rangle \cup \cdots \cup \Delta \langle x_n,y_n \rangle \vdash_{\mathcal{S}} \Delta \big\langle f(x_1,\ldots,x_n) , f(y_1,\ldots,y_n) \big\rangle \end{align} $$

for every n-ary function symbol $f \in {\mathcal {L}}$ .

Conditions (p-Sym) and (p-Trans) actually follow from the three remaining conditions (see [Reference Font32, Corollary 6.61]), but their presence helps us understand the intuition behind the terminology “congruence formulas.”

As it turns out, Definition 2.4 captures two classes of logics within the Leibniz hierarchy. Indeed, the existence of a set of parameterized congruence formulas characterizes protoalgebraic logics, while the existence of a set of congruence formulas without parameters characterizes equivalential logics (see [Reference Font32, Theorem 6.57 and Definition 6.63]).

The next technical result will be used in Section 10 to prove that the logic ${\mathcal {C}ilow}$ is not equivalential. The auxiliary lemma is taken from Jansana’s AAL lecture notes [Reference Jansana37, Exercise 4.36, p. 89].

Lemma 2.6. If $\Delta (x,y,\overline {z})$ and $\Delta '(x,y,\overline {z'})$ are two sets of parameterized congruence formulas for ${\mathcal {S}}$ , then $\Delta \langle x,y \rangle \dashv \vdash _{\mathcal {S}} \Delta '\langle x,y \rangle $ .

Proposition 2.7. Let ${\mathcal {S}}$ be an equivalential logic. If $\Delta \subseteq \mathrm {Fm}_{\mathcal {L}}$ is a set of parameterized congruence formulas for ${\mathcal {S}}$ , then for every substitution $\sigma : {\boldsymbol {Fm}} \to {\boldsymbol {Fm}}(x,y)$ leaving $x,y$ unchanged and replacing any other variable z with $\sigma \,z \in \{x,y\}$ , $\sigma \,\Delta \subseteq \mathrm {Fm}_{\mathcal {L}}(x,y)$ is a set of congruence formulas for ${\mathcal {S}}$ .

Proof Let $\Delta (x,y,\overline {z}) \subseteq \mathrm {Fm}_{\mathcal {L}}$ be a set of parameterized congruence formulas for ${\mathcal {S}}$ and $\Delta '(x,y)$ be a set of congruence formulas (without parameters) for ${\mathcal {S}}$ . Notice that $\Delta '$ must exist by hypothesis. It follows by Lemma 2.6 that $\Delta \langle x,y \rangle \dashv \vdash _{\mathcal {S}} \Delta '(x,y)$ . It follows by structurality that $\sigma \Delta \langle x,y \rangle \dashv \vdash _{\mathcal {S}} \Delta '(x,y)$ , bearing in mind that $\sigma $ leaves $x,y$ unchanged and replaces any other variable z with $\sigma \,z \in \{x,y\}$ . Thus $\sigma \Delta \langle x,y \rangle \subseteq \mathrm {Fm}_{\mathcal {L}}(x,y)$ is also a set of congruence formulas (without parameters) for ${\mathcal {S}}$ .

2.3 Algebraic semantics

The notion of algebraic semantics was originally introduced in [Reference Blok and Pigozzi6] (assuming ${\mathcal {S}}$ is finitary, ${\mathsf {K}}$ a quasivariety, and ${\boldsymbol {\tau }}(x)$ finite), and was further investigated per se in [Reference Blok and Rebagliato8]. We choose here to make explicit its dependence on the set of equations ${\boldsymbol {\tau }}$ , following the more works [Reference Blok and Raftery7, Reference Raftery51]. More recent developments on algebraic semantics can be found in [Reference Moraschini43].

Definition 2.8. Let ${\mathcal {S}}$ be a logic and ${\boldsymbol {\tau }}(x) \subseteq \mathrm {Eq}_{\mathcal {L}}$ . A class of algebras ${\mathsf {K}}$ is a ${\boldsymbol {\tau }}$ -algebraic semantics for ${\mathcal {S}}$ if for every $\Gamma \cup \{\varphi \} \subseteq \mathrm {Fm}_{\mathcal {L}}$ ,

(ALG1) $$ \begin{align} \Gamma \vdash_{\mathcal{S}} \varphi \quad \Leftrightarrow \quad {\boldsymbol{\tau}}(\Gamma) \vDash_{\mathsf{K}} {\boldsymbol{\tau}}(\varphi) . \end{align} $$

Despite the fact that no characterization of Definition 2.8 in terms of the Leibniz operator is known, there is a close relation between the notion of algebraic semantics and the Leibniz hierarchy. Indeed, algebraizable logics were originally defined (apart from finitariness issues) as those logics ${\mathcal {S}}$ for which there exist a class of algebras ${\mathsf {K}}$ , a set of equations in at most one variable ${\boldsymbol {\tau }}(x) \subseteq \mathrm {Eq}_{\mathcal {L}}$ , and a set of formulas in at most two variables ${\boldsymbol {\rho }}(x,y) \subseteq \mathrm {Fm}_{\mathcal {L}}$ , such that

(ALG1) $$ \begin{align} \Gamma \vdash_{\mathcal{S}} \varphi &\Leftrightarrow {\boldsymbol{\tau}}(\Gamma) \vDash_{\mathsf{K}} {\boldsymbol{\tau}}(\varphi), \end{align} $$

(ALG2)

for every $\Gamma \cup \{\varphi \} \subseteq \mathrm {Fm}_{\mathcal {L}}$ . It is thus clear by the definitions involved that every algebraizable logic has an algebraic semantics, which in this case is called an equivalent algebraic semantics.

The next result, whose proof can be found in [Reference Raftery51, Corollary 6], will be used for establishing that ${\mathscr {C}}_1$ admits no algebraic semantics (Theorem 5.6). We state it here for the particular case of protoalgebraic logics.

Proposition 2.9. If a protoalgebraic logic ${\mathcal {S}}$ has a ${\boldsymbol {\tau }}$ -algebraic semantics, then ${\boldsymbol {\tau }}(T) \subseteq {\boldsymbol {\varOmega }}^{\boldsymbol {Fm}}(T)$ for every $T \in \mathcal {T}\!h({\mathcal {S}})$ .

Part I. Da Costa’s logic $\mathbf {\mathscr {C}}_1$ .

In the first part of our work we deal exclusively with the logic ${\mathscr {C}}_1$ and the related family of logics ${\mathscr {C}}_n$ , with $n \geq 1$ . Our main goals are to classify ${\mathscr {C}}_1$ within the Leibniz and Frege hierarchies, collect some algebraic consequences of the fact that ${\mathscr {C}}_1$ admits a Deduction-Detachment Theorem (Theorem 3.10), present a set of parameterized congruence formulas for ${\mathscr {C}}_1$ (Theorem 4.3), and prove that ${\mathscr {C}}_1$ does not admit any algebraic semantics whatsoever in the sense of Blok and Pigozzi (Theorem 5.6).

3 The logic ${\mathscr {C}}_1$

In this section we introduce the logic ${\mathscr {C}}_1$ alongside with the family of logics ${\mathscr {C}}_n$ , with $n \geq 1$ . We then proceed to classify ${\mathscr {C}}_1$ within the Leibniz and Frege hierarchies and state some algebraic consequences of the Deduction-Detachment Theorem for ${\mathscr {C}}_1$ .

Throughout the present work we assume fixed the language

$$\begin{align*}{\mathcal{L}} = \langle \wedge , \vee , \to , \neg \rangle , \end{align*}$$

where $\wedge ,\vee ,\to $ are binary operation symbols and $\neg $ is a unary operation symbol. We shall also consider two unary non-primitive connectives and , and one binary non-primitive connective , with $\varphi ,\psi \in \mathrm {Fm}_{\mathcal {L}}$ . The traditional Hilbert-style axiomatics for ${\mathscr {C}}_1$ is presented in the next definition, as given in [Reference da Costa21, pp. 498–499].

Definition 3.1. The logic ${\mathscr {C}}_1$ is induced by the following Hilbert-style axioms and inference rule:

(Ax1) $$ \begin{align} &\vdash \varphi \to (\psi \to \varphi),\end{align} $$

(Ax2) $$ \begin{align}&\vdash (\varphi \to \psi) \to \Big( \big( \varphi \to (\psi \to \xi) \big) \to (\varphi \to \xi) \Big),\end{align} $$

(Ax3) $$ \begin{align}&\vdash (\varphi \wedge \psi) \to \varphi,\end{align} $$

(Ax4) $$ \begin{align}&\vdash (\varphi \wedge \psi) \to \psi,\end{align} $$

(Ax5) $$ \begin{align}&\vdash \varphi \to \big(\psi \to (\varphi \wedge \psi)\big),\end{align} $$

(Ax6) $$ \begin{align}&\vdash \varphi \to (\varphi \vee \psi),\end{align} $$

(Ax7) $$ \begin{align}&\vdash \psi \to (\varphi \vee \psi),\end{align} $$

(Ax8) $$ \begin{align}&\vdash (\varphi \to \xi) \to \Big((\psi \to \xi) \to \big((\varphi \vee \psi) \to \xi\big) \Big),\end{align} $$

(Ax9) $$ \begin{align}&\vdash \varphi \vee \neg \varphi,\end{align} $$

(Ax10) $$ \begin{align}&\vdash \neg \neg \varphi \to \varphi,\end{align} $$

(Ax11) $$ \begin{align}&\vdash \psi^{\circ} \to \Big( (\varphi \to \psi) \to \big( (\varphi \to \neg \psi) \to \neg \varphi \big) \Big),\end{align} $$

(Ax12) $$ \begin{align}&\vdash (\varphi^{\circ} \wedge \psi^{\circ}) \to (\varphi \wedge \psi)^{\circ},\end{align} $$

(Ax13) $$ \begin{align}&\vdash (\varphi^{\circ} \wedge \psi^{\circ}) \to (\varphi \vee \psi)^{\circ},\end{align} $$

(Ax14) $$ \begin{align}&\vdash (\varphi^{\circ} \wedge \psi^{\circ}) \to (\varphi \to \psi)^{\circ},\end{align} $$

(MP) $$ \begin{align}&\varphi , \varphi \to \psi \vdash \psi. \end{align} $$

By definition, ${\mathscr {C}}_1$ is obviously a finitary logic, also called a deductive system in the literature. The schemata (Ax1)–(Ax8) axiomatize positive intuitionistic propositional logic ( $\mathcal {IL}^+$ ), and hence ${\mathscr {C}}_1$ is an (axiomatic) extension of $\mathcal {IL}^+$ . Also, classical propositional logic ( $\mathcal {CL}$ ) is an extension of ${\mathscr {C}}_1$ , axiomatized relatively to it by the principle of contradiction $\neg (\varphi \wedge \neg \varphi )$ .

The logic ${\mathscr {C}}_{\omega }$ is axiomatized by the schemata (Ax1)–(Ax10) and inference rule (MP). It is the weakest among all of da Costa’s ${\mathscr {C}}$ -systems. LetFootnote ⁵

The logic ${\mathscr {C}}_n$ , with $n \geq 1$ , is the least extension of ${\mathscr {C}}_{\omega }$ closed under the following additional axiom schemata:

(Ax11n) $$ \begin{align} &\vdash \psi^{\scriptscriptstyle {(n)}} \to \Big( (\varphi \to \psi) \to \big( (\varphi \to \neg \psi) \to \neg \varphi \big) \Big), \end{align} $$

(Ax12n) $$ \begin{align} &\hspace{-120pt}\vdash (\varphi^{\scriptscriptstyle {(n)}} \wedge \psi^{\scriptscriptstyle {(n)}}) \to (\varphi \wedge \psi)^{\scriptscriptstyle {(n)}}, \end{align} $$

(Ax13n) $$ \begin{align} &\hspace{-120pt}\vdash (\varphi^{\scriptscriptstyle {(n)}} \wedge \psi^{\scriptscriptstyle {(n)}}) \to (\varphi \vee \psi)^{\scriptscriptstyle {(n)}}, \end{align} $$

(Ax14n) $$ \begin{align} &\hspace{-120pt}\vdash (\varphi^{\scriptscriptstyle {(n)}} \wedge \psi^{\scriptscriptstyle {(n)}}) \to (\varphi \to \psi)^{\scriptscriptstyle {(n)}}. \end{align} $$

For $n = 1$ , the logic just defined coincides with the logic ${\mathscr {C}}_1$ in Definition 3.1. Da Costa proved in [Reference da Costa18, Théorème 7] (the proof is credited to A. I. Arruda) that his ${\mathscr {C}}$ -systems form a hierarchy of proper extensions, i.e.,

$$\begin{align*}{\mathscr{C}}_{\omega} < \cdots < {\mathscr{C}}_{n+1} < {\mathscr{C}}_n < \cdots < {\mathscr{C}}_1 \;. \end{align*}$$

The logic ${\mathscr {C}}_{\omega }$ is not the infimum of the family of logics $\{ {\mathscr {C}}_n : n \geq 1 \}$ , although the notation may suggest it. For more details on this issue, see [Reference Carnielli and Marcos15].

The following auxiliary facts about ${\mathscr {C}}_1$ will be used exhaustively in the sequel. See [Reference da Costa, Krause and Bueno26, Theorems 2.1.6, 2.1.8, 2.1.13, and 2.1.14].

Several semantics have been put forward in the literature for the logic ${\mathscr {C}}_1$ , namely, behavioral semantics [Reference Caleiro and Gonçalves12, Reference Caleiro, Gonçalves and Martins13], possible-translations semantics [Reference Bueno-Soler and Carnielli9], and the so-called da Costa algebras investigated in [Reference Carnielli and de Alcantara14, Reference Seoane and de Alcantara52] and generalizing the ${\mathscr {C}}_1$ -algebras introduced by da Costa himself in [Reference da Costa19]. Da Costa’s proposal has the drawback (from an AAL point of view) of changing the underlying language of the class of algebras associated with ${\mathscr {C}}_1$ . One further semantics for ${\mathscr {C}}_1$ can be found in the literature, developed by da Costa and Alves in [Reference da Costa and Alves23], and which will be very useful in the sequel. We next introduce da Costa and Alves’s two-valued semantics for the logic ${\mathscr {C}}_1$ and state the completeness result w.r.t. this non-truth-functional semantics.

Given a bivaluation v of ${\mathscr {C}}_1$ , we have [Reference da Costa and Alves23, Theorem 2]:

$$\begin{align*}v(\sim\! \varphi) = 1 \;\Leftrightarrow\; v(\varphi) = 0. \end{align*}$$

In fact, the connective $\sim \!$ behaves like classical negation.

3.1 Classification of ${\mathscr {C}}_1$ within the Leibniz and Frege hierarchies

The classification of ${\mathscr {C}}_1$ (or more generally, of da Costa’s ${\mathscr {C}}$ -systems ${\mathscr {C}}_n$ ) within the Leibniz and Frege hierarchies is scattered along the literature, sometimes appearing as mere observations, and most often without explicit proofs. The notorious exception is the non-algebraizability of ${\mathscr {C}}_1$ established in [Reference Lewin, Mikenberg and Schwarze39]. We next compile these scattered results and fully classify the logic ${\mathscr {C}}_1$ within the Leibniz hierarchy, which since the non-algebraizability result of Lewin, Mikenberg, and Schwarze in 1991, has been enlarged with two further classes of logics (namely, the classes of weakly algebraizable [Reference Czelakowski and Jansana29] and truth-equational logics [Reference Raftery51]).

The protoalgebraicity of ${\mathscr {C}}_1$ was left as an open question in [Reference Carnielli and Marcos16, p. 81] (perhaps because the condition said to characterize protoalgebraicity in [Reference Carnielli and Marcos16, p. 81] is in fact equivalent to weak algebraizability), but was later observed to hold in [Reference Bueno-Soler and Carnielli9, p. 2]. Indeed, it follows by manipulation of axioms (Ax1), (Ax2), and rule (MP) in Definition 3.1, or at once by Lemma 3.2.11, that ${\boldsymbol {\rho }}(x,y) = \{ x \to y \}$ complies with Definition 2.2 (i).

Proposition 3.5. ${\mathscr {C}}_1$ is protoalgebraic.

Proposition 3.5 immediately prompts the question of whether ${\mathscr {C}}_1$ is furthermore equivalential. The answer this time is negative, as first observed in [Reference Herrmann36, pp. 425–426], and also mentioned in [Reference Font32, Example 6.77]. The proof uses as a counterexample the five-element algebra of [Reference Lewin, Mikenberg and Schwarze39] depicted in Figure 2 (Table 1).

Proposition 3.6. ${\mathscr {C}}_1$ is not equivalential.

Proof Consider the algebra ${\boldsymbol {A}} = \langle A , \wedge ^{\boldsymbol {A}} , \vee ^{\boldsymbol {A}} , \to ^{\boldsymbol {A}} , \neg ^{\boldsymbol {A}} , 0^{\boldsymbol {A}} ,1^{\boldsymbol {A}} \rangle $ with universe $A = \{ 0,a,b,1,u\}$ , whose lattice operations are given by Figure 2 and with the truth-tables of $\neg ^{\boldsymbol {A}}$ and $\to ^{\boldsymbol {A}}$ given by Table 2, respectively. Consider moreover the subalgebra ${\boldsymbol {B}}$ with universe $B = \{ 0,a,b,1\}$ . It is clear that ${\boldsymbol {A}} \in {\mathsf {Alg}}^*({\mathscr {C}}_1)$ , since for instance witnesses $\langle {\boldsymbol {A}} , F \rangle \in {\mathsf {Mod}}^*({\mathscr {C}}_1)$ . Now, fix . It is not difficult to check that $\langle a,1 \rangle \in {\boldsymbol {\varOmega }}^{\boldsymbol {B}}(G)$ . Then ${\boldsymbol {\varOmega }}^{\boldsymbol {B}}(G) \neq id_{\boldsymbol {B}}$ , and therefore $\langle {\boldsymbol {B}} , G \rangle \notin {\mathsf {Mod}}^*({\mathscr {C}}_1)$ . We conclude that the class ${\mathsf {Mod}}^*({\mathscr {C}}_1)$ is not closed under submatrices, and hence ${\mathscr {C}}_1$ cannot be equivalential (see for instance [Reference Font32, Theorem 6.73]).

Figure 2 The algebra ${\boldsymbol {A}}$ of [Reference Lewin, Mikenberg and Schwarze39] and its ${\mathscr {C}}_1$ -filters.

Table 1 The algebra ${\boldsymbol {A}}$ of [Reference Lewin, Mikenberg and Schwarze39] and the Leibniz congruences of its ${\mathscr {C}}_1$ -filters.

Table 2 Truth-tables of the connectives $\neg ^{\boldsymbol {A}}$ and $\to ^{\boldsymbol {A}}$ .

We are left to see whether ${\mathscr {C}}_1$ is truth-equational. But, in fact, this was implicitly established in [Reference Lewin, Mikenberg and Schwarze39]—implicitly, simply because truth-equational logics had not yet been defined in 1991. Indeed, the five-element algebra ${\boldsymbol {A}}$ exhibited in [Reference Lewin, Mikenberg and Schwarze39] (and reproduced in Figure 2) is such that the Leibniz operator on ${\boldsymbol {A}}$ over the ${\mathscr {C}}_1$ -filters is not injective. Recall that Raftery proved that the Leibniz operator is completely order-reflecting (and hence, injective) on arbitrary algebras for truth-equational logics [Reference Raftery51]. It follows at once that:

Proposition 3.7. ${\mathscr {C}}_1$ is not truth-equational.

Having in mind Definition 2.2(iv), it follows at once that ${\mathscr {C}}_1$ is not weakly algebraic. Indeed, Font’s [Reference Font32, Example 6.122.9] generalizes that “neither of the logic ${\mathscr {C}}_n$ is weakly algebraizable.”

As a matter of fact, by direct inspection of Table 2, one sees that truth is not even implicitly definable Footnote ⁶ in the class ${\mathsf {Mod}}^*({\mathscr {C}}_1)$ , which is a weaker condition than equational definability of truth in the class ${\mathsf {Mod}}^*({\mathscr {C}}_1)$ .

Propositions 3.5–3.7 settle the classification of the logic ${\mathscr {C}}_1$ within the Leibniz hierarchy. As to the Frege hierarchy, the logic ${\mathscr {C}}_1$ falls outside its scope, as first shown by da Costa and Guillaume as early as in [Reference da Costa and Guillaume25].

Proposition 3.8. ${\mathscr {C}}_1$ is not self-extensional.

Proof For instance, $\varphi \to \varphi \dashv \vdash _{{\mathscr {C}}_1} \psi \to \psi $ , but the matrix model $\langle {\boldsymbol {A}} , \{1,u\} \rangle \in {\mathsf {Mod}}({\mathscr {C}}_1)$ , with ${\boldsymbol {A}}$ given as in Figure 2, and any homomorphism $h : {\boldsymbol {Fm}} \to {\boldsymbol {A}}$ such that $h(\varphi ) = u$ and $h(\psi ) = 1$ witness $\neg (\varphi \to \varphi ) \not \vdash _{{\mathscr {C}}_1} \neg (\psi \to \psi )$ .

It is worth mentioning that it was precisely the non-self-extensionality of ${\mathscr {C}}_1$ that motivated the first algebraic studies about this paraconsistent logic.

So far we have only seen one positive result about ${\mathscr {C}}_1$ , namely that it is protoalgebraic. This fact will be the ground upon which Sections 3.2 and 4 will be built on.

3.2 The Deduction-Detachment Theorem for ${\mathscr {C}}_1$

Protoalgebraic logics are characterized by possessing a weak form of the Deduction-Detachment Theorem (DDT), the so-called Parameterized Local Deduction-Detachment Theorem (PLDDT). Some famous bridge theorems in AAL establish correspondences between stronger versions of the PLDDT and purely algebraic properties. For instance, for finitary logics, the LDDT (a non-parameterized version of the PLDDT) corresponds to the Filter Extension Property (FEP) of the class of matrix models of the underlying logic, while, again for finitary logics, the DDT (a non-local and non-parameterized version of the PLDDT) corresponds to the property of the lattice of finitely generated filters being dually Brouwerian.

It is easy to check that logic ${\mathscr {C}}_1$ admits a “classical” DDT witnessed by one single formula with no parameters. In fact, any finitary logic in the language ${\mathcal {L}}$ having (Ax1) and (Ax2) among its axioms and (MP) as its only inference rules satisfies the classical DDT (see [Reference Font32, Theorem 3.72]).

Proposition 3.9. For every $\Gamma \cup \{\varphi ,\psi \} \in \mathrm {Fm}_{\mathcal {L}}$ ,

(DDT) $$ \begin{align} \Gamma,\varphi \vdash_{{\mathscr{C}}_1} \psi \quad\Leftrightarrow\quad \Gamma \vdash_{{\mathscr{C}}_1} \varphi \to \psi . \end{align} $$

That is, $\{ p \to q\}$ is a DD set for the logic ${\mathscr {C}}_1$ .

As a consequence of Proposition 3.9, the class ${\mathsf {Mod}}({\mathscr {C}}_1)$ has the FEP.Footnote ⁷ We compile this and other algebraic properties of the logic ${\mathscr {C}}_1$ in the next result, all of which are consequences of more general AAL results for finitary protoalgebraic logics having a DD set—see [Reference Font32, Theorems 6.24 and 6.28 and Corollary 6.30].

Theorem 3.10.

1. 1. For every ${\boldsymbol {A}}$ , the join-semilattice of the finitely generated ${\mathscr {C}}_1$ -filters of ${\boldsymbol {A}}$ is dually Brouwerian.

2. 2. The logic ${\mathscr {C}}_1$ is filter-distributive.

3. 3. The class ${\mathsf {Mod}}({\mathscr {C}}_1)$ has the FEP.

An observation which will be used in the sequel is that every axiomatic extension of ${\mathscr {C}}_1$ enjoys the FEP.

The DDT lifts to arbitrary algebras given an underlying protoalgebraic logic—see [Reference Font32, Theorem 3.81]. Once applied to the logic ${\mathscr {C}}_1$ , we obtain that for every ${\boldsymbol {A}}$ and every $X \cup \{a,b\} \subseteq A$ ,

A consequence of this fact is a characterization of the Frege relation for the logic ${\mathscr {C}}_1$ . We omit the easy proof.

Proposition 3.11. For every ${\boldsymbol {A}}$ ,

, and $a,b \in A$ ,

Proposition 3.11 shows us that the classical characterization of the Leibniz congruence of a $\mathcal {CL}$ -filter defines the Frege relation of a ${\mathscr {C}}_1$ -filter. This relation is not necessarily a congruence, for ${\mathscr {C}}_1$ is not (fully) self-extensional.

4 Parameterized congruence formulas for ${\mathscr {C}}_1$

Our goal in this section is to provide a set of parameterized congruence formulas for the logic ${\mathscr {C}}_1$ . In fact, we shall provide two such sets, namely in Proposition 4.1 and Theorem 4.3. While the former is a rather trivial one, the latter is fairly complex and will be needed in the sequel.

Since ${\mathscr {C}}_1$ is protoalgebraic, but not equivalential (recall Propositions 3.5 and 3.6), we know a priori that ${\mathscr {C}}_1$ admits a set of parameterized congruence formulas, but no set of congruence formulas without parameters. The first set of parameterized congruence formulas we provide for ${\mathscr {C}}_1$ is rather trivial, but will be useful in our analysis.

Proposition 4.1. The set

is a set of parameterized congruence formulas for the logic ${\mathscr {C}}_1$ .

The second set of parameterized congruence formulas for ${\mathscr {C}}_1$ we consider, on the opposite, is quite complex. In order to establish it we need an auxiliary lemma.

Compare Lemma 3.2.8 with Lemma 4.2.2. The latter provides a weaker condition in order to establish $\neg \varphi \leftrightarrow \neg \psi $ , and it will be used exhaustively throughout the rest of the work.

We still need a couple of auxiliary definitions before stating the main result of this section. For every $m \in \omega $ and every $\varphi \in \mathrm {Fm}_{\mathcal {L}}$ , letFootnote ⁸

In particular, $\neg ^0 \varphi = \varphi $ and $\neg ^1 \varphi = \neg \varphi $ . Let us also define

$$ \begin{align*} \Phi_0(x,y) = \big\{ &x \leftrightarrow y \big\} , \\[0.5ex] \Phi_1(x,y,z_1) = \big\{ &\neg^{m_1} (x *_1 z_1) \leftrightarrow \neg^{m_1} (y *_1 z_1) : \\ &*_1 \in \{\wedge,\vee,\to\} , m_1 \in \omega \big\} , \\ \Phi_2(x,y,z_1,z_2) = \big\{ &\neg^{m_2} \big( \neg^{m_1} (x *_1 z_1) *_2 z_2 \big) \leftrightarrow \\ &\neg^{m_2} \big( \neg^{m_1} (y *_1 z_1) *_2 z_2 \big) : \\ &*_1,*_2 \in \{\wedge,\vee,\to\} , m_1,m_2 \in \omega \big\} , \\ \quad\vdots\qquad\qquad&\\ \Phi_n(x,y,z_1,z_2,\ldots,z_n) = \big\{ & \neg^{m_n} \big( \cdots \neg^{m_2} (\neg^{m_1} (x *_1 z_1) *_2 z_2) \cdots *_n z_n \big) \leftrightarrow \\ &\neg^{m_n} \big( \cdots \neg^{m_2} ( \neg^{m_1} (y *_1 z_1) *_2 z_2) \cdots *_n z_n \big) : \\ &*_1,\ldots,*_n \in \{\wedge,\vee,\to\} , m_1,\ldots,m_n \in \omega \big\} , \end{align*} $$

and

$$ \begin{align*} \Psi_0(x,y) = \big\{ &x \leftrightarrow y \big\} , \\[0.5ex] \Psi_1(x,y,z_1) = \big\{ &\neg^{m_1} (z_1 *_1 x) \leftrightarrow \neg^{m_1} (z_1 *_1 y) : \\ &*_1 \in \{\wedge,\vee,\to\} , m_1 \in \omega \big\} , \\ \Psi_2(x,y,z_1,z_2) = \big\{ &\neg^{m_2} \big( \neg^{m_1} (z_1 * x) *_2 z_2 \big) \leftrightarrow \\ &\neg^{m_2} \big( \neg^{m_1} (z_1 * y) *_2 z_2 \big) : \\ &*_1,*_2 \in \{\wedge,\vee,\to\} , m_1,m_2 \in \omega \big\} , \\ \quad\vdots\qquad\qquad&\\ \Psi_n(x,y,z_1,z_2,\ldots,z_n) = \big\{ &\neg^{m_n} \big(\cdots \neg^{m_2} (\neg^{m_1} (z_1 *_1 x) *_2 z_2) \cdots *_n z_n \big) \leftrightarrow \\ &\neg^{m_n} \big( \cdots \neg^{m_2} (\neg^{m_1} (z_1 *_1 y) *_2 z_2) \cdots *_n z_n \big) : \\ &*_1,\ldots,*_n \in \{\wedge,\vee,\to\} , m_1,\ldots,m_n \in \omega \big\}. \end{align*} $$

We are now ready to state the main result of this section.

Theorem 4.3. For every ${\boldsymbol {A}}$ , , and $a,b \in A$ ,

$$ \begin{align*} \langle a,b \rangle \in {\boldsymbol{\varOmega}}^{\boldsymbol{A}}(F) &\Leftrightarrow \forall n \in \omega \; \forall m \in \omega \; \forall c_1,\ldots,c_n \in A, \\ &\quad \Phi_n^{\boldsymbol{A}}(\neg^m a, \neg^m b, c_1,\ldots,c_n) \subseteq F , \\ &\quad \Psi_n^{\boldsymbol{A}}(\neg^m a, \neg^m b, c_1,\ldots,c_n) \subseteq F. \end{align*} $$

Proof For the sake of simplicity, define the relation $R \subseteq A \times A$ by

$$ \begin{align*} \langle a,b \rangle \in R &\Leftrightarrow \forall n \in \omega \; \forall m \in \omega \; \forall c_1,\ldots,c_n \in A, \\ &\quad \Phi_n^{\boldsymbol{A}}(\neg^m a, \neg^m b, c_1,\ldots,c_n) \subseteq F , \\ &\quad \Psi_n^{\boldsymbol{A}}(\neg^m a, \neg^m b, c_1,\ldots,c_n) \subseteq F. \end{align*} $$

Suppose that $\langle a,b \rangle \in {\boldsymbol {\varOmega }}^{\boldsymbol {A}}(F)$ . It follows by Proposition 4.1 that $a\,Rb$ . Conversely, we claim that R is a congruence relation on ${\boldsymbol {A}}$ compatible with F. It should be clear that R is an equivalence relation on A, given Lemma 3.2.1–3. Notice next that the relation R is compatible with the connective $\neg $ , since by construction of R we are ranging $\neg ^m a$ and $\neg ^m b$ over $m \in \omega $ . We are left to prove that R is also compatible with the binary language operations of ${\mathscr {C}}_1$ . Let $\langle a_1,b_1 \rangle \in R$ and $\langle a_2,b_2 \rangle \in R$ . We claim that for every $c_1,\ldots ,c_n \in A$ ,

$$ \begin{align*} &\bigcup_{n \in \omega} \bigcup_{m \in \omega} \Phi_n^{\boldsymbol{A}}(\neg^m (a_1*a_2), \neg^m (b_1*b_2), c_1,\ldots,c_n) \subseteq F , \end{align*} $$

with $* \in \{\wedge ,\vee ,\to \}$ . Let $n \in \omega $ , $c_1,\ldots ,c_n \in A$ , $*,*_1,\ldots ,*_n \in \{\wedge ,\vee ,\to \}$ and $m,m_1,\ldots ,m_n \in \omega $ . Consider $\Phi _{n+1}(a_1,b_1,a_2,c_1,\ldots ,c_n)$ with $m'=0$ , $m_1'=m,m_2'=m_1,\ldots ,m_{n+1}'=m_n$ . Since $\Phi _{n+1}(a_1,b_1,a_2,c_1,\ldots ,c_n) \subseteq F$ by the assumption $\langle a_1,b_1 \rangle \in R$ , we have

$$ \begin{align*} &\neg^{m_n} (\cdots \neg^{m_1} (\neg^m (a_1 * a_2) *_1 c_1) \cdots *_n c_n) \leftrightarrow \\ &\neg^{m_n} ( \cdots \neg^{m_1} ( \neg^m (b_1 * a_2) *_1 c_1) \cdots *_n c_n) \in F. \end{align*} $$

Next, consider $\Psi _{n+1}(a_2,b_2,b_1,c_1,\ldots ,c_n)$ with $m'=0$ , $m_1'=m,m_2'=m_1,\ldots, m_{n+1}'=m_n$ . Since $\Psi _{n+1}(a_2,b_2,b_1,c_1,\ldots ,c_n) \subseteq F$ by the assumption $\langle a_2,b_2 \rangle \in R$ , we have

$$ \begin{align*} &\neg^{m_n} (\cdots \neg^{m_1} (\neg^m (b_1 * a_2) *_1 c_1) \cdots *_n c_n) \leftrightarrow \\ &\neg^{m_n} ( \cdots \neg^{m_1} ( \neg^m (b_1 * b_2) *_1 c_1) \cdots *_n c_n) \in F. \end{align*} $$

It then follows by transitivity (Lemma 3.2.3) that

$$ \begin{align*} &\neg^{m_n} (\cdots \neg^{m_1} (\neg^m (a_1 * a_2) *_1 c_1) \cdots *_n c_n) \leftrightarrow \\ &\neg^{m_n} ( \cdots \neg^{m_1} ( \neg^m (b_1 * b_2) *_1 c_1) \cdots *_n c_n) \in F. \end{align*} $$

Thus, $\Phi _n\big (\neg ^m (a_1 * a_2), \neg ^m (b_1 * b_2), c_1,\ldots ,c_n\big ) \subseteq F$ .

Similarly, one proves that for every $c_1,\ldots ,c_n \in A$ ,

$$ \begin{align*} &\bigcup_{n \in \omega} \bigcup_{m \in \omega} \Psi_n^{\boldsymbol{A}}(\neg^m (a_1*a_2), \neg^m (b_1*b_2), c_1,\ldots,c_n) \subseteq F , \end{align*} $$

with $* \in \{\wedge ,\vee ,\to \}$ . Finally, in order to see that R is compatible with F, let $\langle a,b \rangle \in R$ and assume $a \in F$ . Since by assumption $\Phi _0(a,b) \subseteq F$ , it follows that $a \to b \in F$ , and hence by (MP) that $b \in F$ . Thus, $R \subseteq {\boldsymbol {\varOmega }}^{\boldsymbol {A}}(F)$ .

In other words, Theorem 4.3 tells us that the set

$$ \begin{align*} \Delta(x,y,\overline{z}) =& \bigcup_{n \in \omega} \bigcup_{m \in \omega} \Phi_n(\neg^m x, \neg^m y, z_1,\ldots,z_n) \; \cup \\ &\bigcup_{n \in \omega} \bigcup_{m \in \omega} \Psi_n(\neg^m x, \neg^m y, z_1,\ldots,z_n) \end{align*} $$

is a set of parameterized congruence formulas for the logic ${\mathscr {C}}_1$ . Although the set $\Delta (x,y,\overline {z})$ above may seem of little more practical usage than the one given in Proposition 4.1, it will be the key to proving Theorem 9.1 later on.

5 Algebraic semantics for ${\mathscr {C}}_1$

As we have mentioned in the Introduction, several semantical approaches to the logic ${\mathscr {C}}_1$ have been put forward in the literature, namely, behavioral semantics [Reference Caleiro and Gonçalves12, Reference Caleiro, Gonçalves and Martins13], possible-translations semantics [Reference Bueno-Soler and Carnielli9], da Costa algebras [Reference Carnielli and de Alcantara14, Reference Seoane and de Alcantara52], ${\mathscr {C}}_1$ -algebras [Reference da Costa19], and a two-valued semantics [Reference da Costa and Alves22, Reference da Costa and Alves23], this latter already introduced in Definition 3.3. From an AAL perspective, however, there are still two natural candidates for a semantical approach left unstudied—the class ${\mathsf {Alg}}^*({\mathscr {C}}_1)$ and Blok and Pigozzi’s notion of algebraic semantics. In this section we will investigate both these approaches, and conclude that neither provides a meaningful algebraic counterpart to the logic ${\mathscr {C}}_1$ .

5.1 The class ${\mathsf {Alg}}^*({\mathscr {C}}_1)$

The first (negative) result on the algebraization of ${\mathscr {C}}_1$ was established by Mortensen in [Reference Mortensen44], by proving that the only congruence on the formula algebra compatible with the set of ${\mathscr {C}}_1$ -theorems is the identity relation. This fact can be re-written as:

Proposition 5.1 Mortensen

${\boldsymbol {\varOmega }}^{\boldsymbol {Fm}}({\mathrm{Thm}}_{{\mathscr {C}}_1}) = id_{\boldsymbol {Fm}}$ .

In light of Proposition 5.1, it follows by Theorem 4.3 that for every $\varphi ,\psi \in \mathrm {Fm}_{\mathcal {L}}$ ,

Having in mind (1) on page 483, Mortensen’s result can be re-stated as follows:

Proposition 5.2. ${\boldsymbol {Fm}} \in {\mathsf {Alg}}^*({\mathscr {C}}_1)$ .

Proposition 5.2 has a most crucial consequence upon the intrinsic variety of the logic ${\mathscr {C}}_1$ .

Corollary 5.3. The intrinsic variety of ${\mathscr {C}}_1$ is the class of all ${\mathcal {L}}$ -algebras. That is, $\mathbb {V}({\mathscr {C}}_1) = \{ {\boldsymbol {A}} : {\boldsymbol {A}} \text { is an } {\mathcal {L}}\text {-algebra} \}$ .

Proof Since ${\boldsymbol {Fm}}$ is the absolutely free ${\mathcal {L}}$ -algebra over the (denumerable) set of variables $\mathrm {Var}$ , it is well-known that $\mathbb {V}({\boldsymbol {Fm}})$ is the class of all ${\mathcal {L}}$ -algebras. Moreover , bearing in mind that by protoalgebraicity of ${\mathscr {C}}_1$ and Proposition 5.1, respectively.

Corollary 5.3 sets aside the possibility of associating with ${\mathscr {C}}_1$ its intrinsic variety as the class of algebras one could canonically associate with it.

Notice that since ${\mathscr {C}}_1$ is an extension of ${\mathscr {C}}_n$ , we also have ${\boldsymbol {Fm}} \in {\mathsf {Alg}}^*({\mathscr {C}}_1) \subseteq {\mathsf {Alg}}^*({\mathscr {C}}_n)$ , for every $n \geq 1$ . As such, Corollary 5.3 also holds for the logics ${\mathscr {C}}_n$ , with $n \geq 1$ . Consequently, the intrinsic varieties of all da Costa’s ${\mathscr {C}}$ -systems coincide. It is an open problem whether the quasivarieties $\mathbb {Q}\,{\mathsf {Alg}}^*({\mathscr {C}}_n)$ , with $n \geq 1$ , also coincide, or even if the classes ${\mathsf {Alg}}^*({\mathscr {C}}_n)$ , with $n \geq 1$ , happen to coincide.

Given the fact that the intrinsic variety of a logic is generated by its algebraic counterpart (see page 483), it follows by Corollary 5.3 that ${\mathsf {Alg}}^*({\mathscr {C}}_1)$ generates the variety of all ${\mathcal {L}}$ -algebras.

We now proceed to prove that ${\mathsf {Alg}}^*({\mathscr {C}}_1)$ is not a quasivariety. In order to see that, we borrow the next example from [Reference Urbas54, p. 590], and prove that ${\mathsf {Alg}}^*({\mathscr {C}}_1)$ is not closed under subalgebras. Notice that the proof of Theorem 3.6 provides a counterexample for the fact that ${\mathsf {Mod}}^*({\mathscr {C}}_1)$ is not closed under submatrices, but the subalgebra ${\boldsymbol {B}}$ there presented still belongs to ${\mathsf {Alg}}^*({\mathscr {C}}_1)$ , because ${\boldsymbol {\varOmega }}^{\boldsymbol {B}}(\{1\}) = id_{\boldsymbol {B}}$ and .

Proposition 5.4. ${\mathsf {Alg}}^*({\mathscr {C}}_1)$ is not a quasivariety.

Proof We prove that ${\mathsf {Alg}}^*({\mathscr {C}}_1)$ is not closed under subalgebras. Consider the algebra ${\boldsymbol {A}}$ defined by the truth-tables given in Table 3 and fix . First, one must check that and furthermore that ${\boldsymbol {\varOmega }}^{\boldsymbol {A}}(F) = id_{\boldsymbol {A}}$ (we leave the details to the reader). Thus, ${\boldsymbol {A}} \in {\mathsf {Alg}}^*({\mathscr {C}}_1)$ . Now, consider the subalgebra ${\boldsymbol {B}} \leq {\boldsymbol {A}}$ with universe $B = \{0,4,5\}$ . We have $\mathrm {Sg}_{\mathcal {L}}^{\boldsymbol {A}}(B) = B$ and . In fact , because the singletons $\{0\}, \{4\}, \{5\}$ are not ${\mathscr {C}}_1$ -filters, and neither are the subsets $\{0,5\}$ and $\{4,5\}$ . We now claim that $\langle 0,4 \rangle \in {\boldsymbol {\varOmega }}^{\boldsymbol {B}}(F \cap B)$ . We shall make use of Theorem 4.3. Notice that $0 \leftrightarrow 4 = 0 \in F \cap B$ , and since $\neg 0 = \neg 4$ , it follows that $\neg ^m 0 = \neg ^m 4$ , for every $m \in \omega $ , and therefore $\neg ^m 0 \leftrightarrow \neg ^m 4 = 0 \in F \cap B$ . Furthermore, by looking at the truth tables of ${\boldsymbol {A}}$ restricted to the subuniverse B, one sees that for every $*_1,\ldots ,*_n \in \{\wedge ,\vee ,\to \}$ , every $m_1,\ldots ,m_n \in \omega $ , and every $c_1,\ldots ,c_n \in A$ ,

$$ \begin{align*} &\neg^{m_n} (\cdots (\neg^{m_2} (\neg^{m_1} (0 *_1 c_1) *_2 c_2) \cdots) *_n c_n) = \\ &\neg^{m_n} ( \cdots ( \neg^{m_2} ( \neg^{m_1} (4 *_1 c_1) *_2 c_2) \cdots) *_n c_n), \end{align*} $$

and

$$ \begin{align*} &\neg^{m_n} (\cdots (\neg^{m_2} (\neg^{m_1} (c_1 *_1 0) *_2 c_2) \cdots) *_n c_n) = \\ &\neg^{m_n} ( \cdots ( \neg^{m_2} ( \neg^{m_1} (c_1 *_1 4) *_2 c_2) \cdots) *_n c_n). \end{align*} $$

Therefore,

$$ \begin{align*} &\neg^{m_n} (\cdots (\neg^{m_2} (\neg^{m_1} (0 *_1 c_1) *_2 c_2) \cdots) *_n c_n) \leftrightarrow \\ &\neg^{m_n} ( \cdots ( \neg^{m_2} ( \neg^{m_1} (4 *_1 c_1) *_2 c_2) \cdots) *_n c_n) = 0 \in F \cap B, \end{align*} $$

and

$$ \begin{align*} &\neg^{m_n} (\cdots (\neg^{m_2} (\neg^{m_1} (c_1 *_1 0) *_2 c_2) \cdots) *_n c_n) \leftrightarrow \\ &\neg^{m_n} ( \cdots ( \neg^{m_2} ( \neg^{m_1} (c_1 *_1 4) *_2 c_2) \cdots) *_n c_n) = 0 \in F \cap B. \end{align*} $$

It follows by Theorem 4.3 that $\langle 0,4 \rangle \in {\boldsymbol {\varOmega }}^{\boldsymbol {B}}(F \cap B)$ . Thus, ${\boldsymbol {\varOmega }}^{\boldsymbol {B}}(F \cap B) \neq id_{{\boldsymbol {B}}}$ . We conclude that ${\boldsymbol {B}} \notin {\mathsf {Alg}}^*({\mathscr {C}}_1)$ and hence ${\mathsf {Alg}}^*({\mathscr {C}}_1)$ is not closed under subalgebras.

Table 3 Truth-tables of the algebra ${\boldsymbol {A}}$ of [Reference Urbas54, p. 590].

Corollary 5.5. ${\mathsf {Alg}}^*({\mathscr {C}}_1) \subsetneq \mathbb {V}({\mathscr {C}}_1)$ .

Proof Since ${\mathsf {Alg}}^*({\mathscr {C}}_1)$ is not a quasivariety by Proposition 5.4, it follows at once that ${\mathsf {Alg}}^*({\mathscr {C}}_1) \subsetneq \mathbb {Q}{\mathsf {Alg}}^*({\mathscr {C}}_1) \subseteq \mathbb {V}({\mathscr {C}}_1)$ .

In summary, the class ${\mathsf {Alg}}^*({\mathscr {C}}_1)$ seems to be of little interest from an algebraic point of view. Indeed, it is not a quasivariety (Proposition 5.4), the formula algebra ${\boldsymbol {Fm}}$ belongs to ${\mathsf {Alg}}^*({\mathscr {C}}_1)$ (Proposition 5.2), and the variety generated by ${\mathsf {Alg}}^*({\mathscr {C}}_1)$ is the class of all ${\mathcal {L}}$ -algebras (Corollary 5.3).

6 The subalgebra ${\boldsymbol {A}}^{\circ }$

In this section we study a special subalgebra whose ${\mathscr {C}}_1$ -filters satisfy “classical” properties. Most notably, the quotient of such subalgebra over the Leibniz congruence of any of its ${\mathscr {C}}_1$ -filters is a Boolean Algebra (Theorem 6.6). The results of this section lay the groundwork for Sections 7 and 8.

Throughout the present section let ${\mathcal {S}}$ be an extension of ${\mathscr {C}}_1$ , extended itself by $\mathcal {CL}$ , that is, ${\mathscr {C}}_1 \leq {\mathcal {S}} \leq \mathcal {CL}$ . Let also ${\boldsymbol {A}}$ be an arbitrary fixed algebra. Consider the subset and let ${\boldsymbol {A}}^{\circ }$ be the subalgebra of ${\boldsymbol {A}}$ generated by the subuniverse $\mathrm {Sg}_{\mathcal {L}}^{\boldsymbol {A}}(A^{\circ })$ .

Let us start by observing that the subset $A^{\circ }$ is in fact a subuniverse of A.

In light of Lemma 6.1, from here on, we shall denote the subuniverse $\mathrm {Sg}_{\mathcal {L}}^{\boldsymbol {A}}(A^{\circ })$ simply by $A^{\circ }$ . Another useful observation is that $a^{\circ } \in A^{\circ }$ , for every $a \in A$ . We register this fact for future reference.

Our first goal is to show that, by restricting ourselves to the subuniverse $A^{\circ }$ , the Leibniz congruence on ${\boldsymbol {A}}^{\circ }$ of ${\mathcal {S}}$ -filters of ${\boldsymbol {A}}^{\circ }$ can be “classically” characterized. For ease of notation we shall drop the superscript $^{\boldsymbol {A}}$ on ${a^{\circ }}^{\boldsymbol {A}}$ .

Proposition 6.3. For every ${\boldsymbol {A}}$ , and $a,b \in A^{\circ }$ ,

$$\begin{align*}\langle a,b \rangle \in {\boldsymbol{\varOmega}}^{{\boldsymbol{A}}^{\circ}}(F) \quad\Leftrightarrow\quad a \leftrightarrow^{{\boldsymbol{A}}^{\circ}} b \in F. \end{align*}$$

Corollary 6.4. For every ${\boldsymbol {A}}$ and

,

Corollary 6.4 reinforces the “classical” flavour of the subalgebra ${\boldsymbol {A}}^{\circ }$ . Recall that the Leibniz congruence and Frege relation coincide on classical filters, for arbitrary algebras.

As it turns out, not only is the Leibniz congruence on ${\boldsymbol {A}}^{\circ }$ of an ${\mathcal {S}}$ -filter classically defined (Proposition 6.3), but it is actually a congruence relative to $\mathsf {BA}$ .Footnote ⁹ (Theorem 6.6) In order to prove it, we compile some auxiliary facts, whose proofs we leave for the reader—item 3 below is proved in [Reference Carnielli and Marcos15, Proposition 4.2].

Proof Let ${\boldsymbol {A}}$ arbitrary and . Fix . We must prove that $\langle {\boldsymbol {B}} , \wedge ^{\boldsymbol {B}} , \vee ^{\boldsymbol {B}} , \to ^{\boldsymbol {B}} , \neg ^{\boldsymbol {B}} \rangle $ is a distributive, bounded, and complemented lattice. Let $\pi : {\boldsymbol {A}}^{\circ } \to {\boldsymbol {B}}$ be the natural map. For every $a,b \in A^{\circ }$ , define the relation $\leq ^{\boldsymbol {B}} \subseteq B \times B$ by

$$\begin{align*}\pi(a) \leq^{\boldsymbol{B}} \pi(b) \quad\Leftrightarrow\quad a \to^{{\boldsymbol{A}}^{\circ}} b \in F. \end{align*}$$

It is easy to see that $\leq ^{\boldsymbol {B}}$ is reflexive and transitive, by Lemma 3.2.11 and 12. Furthermore, if $\pi (a) \leq ^{\boldsymbol {B}} \pi (b)$ and $\pi (b) \leq ^{\boldsymbol {B}} \pi (a)$ , that is, $a \leftrightarrow ^{{\boldsymbol {A}}^{\circ }} b \in F$ , it follows by Proposition 6.3 that $\langle a,b \rangle \in {\boldsymbol {\varOmega }}^{{\boldsymbol {A}}^{\circ }}(F)$ , and hence $\pi (a) = \pi (b)$ . So, $\leq ^{\boldsymbol {B}}$ is a partial order on ${\boldsymbol {B}}$ .

It follows by (Ax3), (Ax4), and (Ax5) that $\wedge ^{\boldsymbol {B}}$ is the infimum induced by the order $\leq ^{\boldsymbol {B}}$ , and by (Ax6), (Ax7), and (Ax8) that $\vee ^{\boldsymbol {B}}$ is the supremum induced by the order $\leq ^{\boldsymbol {B}}$ . So, $\langle {\boldsymbol {B}} , \wedge ^{\boldsymbol {B}} , \vee ^{\boldsymbol {B}} \rangle $ is indeed a lattice. Moreover, it follows by Lemma 6.5.1 and 2 that it is a distributive lattice.

We next prove that ${\boldsymbol {B}}$ is limited. Let $a \in F \subseteq A^{\circ }$ and $b \in A^{\circ }$ . It follows by (Ax1) and (MP) that $b \to ^{{\boldsymbol {A}}^{\circ }} a \in F$ , that is, $\pi (b) \leq ^{\boldsymbol {B}} \pi (a)$ . So, $\pi (a)$ is the top element of B w.r.t. the order $\leq ^{\boldsymbol {B}}$ . In particular, $\pi (\neg ^{{\boldsymbol {A}}^{\circ }} b) \leq ^{\boldsymbol {B}} \pi (a)$ , i.e., $\neg ^{{\boldsymbol {A}}^{\circ }} b \to ^{{\boldsymbol {A}}^{\circ }} a \in F$ . Since $a \in A^{\circ }$ , we have . It follows by Lemma 3.2.7 that $\neg ^{{\boldsymbol {A}}^{\circ }} a \to ^{{\boldsymbol {A}}^{\circ }} \neg ^{{\boldsymbol {A}}^{\circ }} \neg ^{{\boldsymbol {A}}^{\circ }} b \in F$ . But $\neg ^{{\boldsymbol {A}}^{\circ }} \neg ^{{\boldsymbol {A}}^{\circ }} b \to ^{{\boldsymbol {A}}^{\circ }} b \in F$ by (Ax10), so by transitivity $\neg ^{{\boldsymbol {A}}^{\circ }} a \to ^{{\boldsymbol {A}}^{\circ }} b \in F$ , that is, $\pi (\neg ^{{\boldsymbol {A}}^{\circ }} a) \leq ^{\boldsymbol {B}} \pi (b)$ . Therefore, $\neg ^{\boldsymbol {B}} \pi (a)$ is the bottom element of B w.r.t. the order $\leq ^{\boldsymbol {B}}$ .

We are left to prove that ${\boldsymbol {B}}$ is complemented. Let $a \in F \subseteq A^{\circ }$ and $b \in A^{\circ }$ . It follows by Lemma 6.5.3 that $a \leftrightarrow ^{{\boldsymbol {A}}^{\circ }} (b \vee ^{{\boldsymbol {A}}^{\circ }} \neg ^{{\boldsymbol {A}}^{\circ }} b) \in F$ , and hence

$$\begin{align*}\pi(a) = \pi(b \vee^{{\boldsymbol{A}}^{\circ}} \neg^{{\boldsymbol{A}}^{\circ}} b) = \pi(b) \vee^{\boldsymbol{B}} \neg^{\boldsymbol{B}} \pi(b). \end{align*}$$

Moreover, since and $a \in F$ , it follows by Lemma 6.5.5 that $(b \wedge ^{{\boldsymbol {A}}^{\circ }} \neg ^{{\boldsymbol {A}}^{\circ }} b) \leftrightarrow ^{{\boldsymbol {A}}^{\circ }} \neg ^{{\boldsymbol {A}}^{\circ }} a \in F$ , and hence

$$\begin{align*}\pi(b) \wedge^{\boldsymbol{B}} \neg^{\boldsymbol{B}} \pi(b) = \pi(b \wedge^{{\boldsymbol{A}}^{\circ}} \neg^{{\boldsymbol{A}}^{\circ}} b) = \pi(\neg^{{\boldsymbol{A}}^{\circ}} a) = \neg^{\boldsymbol{B}} \pi(a). \end{align*}$$

Since we have seen already $\pi (a)$ and $\neg ^{\boldsymbol {B}} \pi (a)$ to be the top and bottom elements of B, respectively, it follows that ${\boldsymbol {B}}$ is complemented.

7 A sufficient condition for ${\boldsymbol {A}}^{\circ } \in \mathsf {BA}$

Our goal in this section is to isolate a general condition which will allow us to prove stronger algebraic results than those seen so far for the logic ${\mathscr {C}}_1$ .

Throughout the present section, let ${\mathcal {S}}$ be such that ${\mathscr {C}}_1 \leq {\mathcal {S}} \leq \mathcal {CL}$ and satisfying the following condition: For every ${\boldsymbol {A}}$ , and $a,b \in A^{\circ }$ ,

(⋆) $$ \begin{align} \langle a,b \rangle \in {\boldsymbol{\varOmega}}^{\boldsymbol{A}}(F) \quad\Leftrightarrow\quad a \leftrightarrow^{\boldsymbol{A}} b \in F . \end{align} $$

To put it in words, by restricting ourselves to the subuniverse $A^{\circ }$ , the Leibniz congruence on ${\boldsymbol {A}}$ of ${\mathcal {S}}$ -filters of ${\boldsymbol {A}}$ can be “classically” characterized. Comparing condition (⋆) with Proposition 6.3, we see that the former is applicable to ${\mathcal {S}}$ -filters of ${\boldsymbol {A}}$ while the latter is applicable to ${\mathcal {S}}$ -filters of the subalgebra ${\boldsymbol {A}}^{\circ }$ .

Notice that for every $a,b \in A^{\circ }$ and every , we have , and hence $a^{\circ } \leftrightarrow b^{\circ } \in F$ . Therefore, condition (⋆) is equivalent to the following condition: For every ${\boldsymbol {A}}$ , and $a,b \in A^{\circ }$ ,

$$ \begin{align*} \langle a,b \rangle \in {\boldsymbol{\varOmega}}^{\boldsymbol{A}}(F) \quad\Leftrightarrow\quad a \leftrightarrow^{\boldsymbol{A}} b \in F \text{ and } a^{\circ} \leftrightarrow^{\boldsymbol{A}} b^{\circ} \in F , \end{align*} $$

and having in mind Lemma 4.2.2, it is also equivalent to the following condition: For every ${\boldsymbol {A}}$ , and $a,b \in A^{\circ }$ ,

(⋆⋆) $$ \begin{align} \langle a,b \rangle \in {\boldsymbol{\varOmega}}^{\boldsymbol{A}}(F) \quad\Leftrightarrow\quad a \leftrightarrow^{\boldsymbol{A}} b \in F \text{ and } \neg a \leftrightarrow^{\boldsymbol{A}} \neg b \in F . \end{align} $$

Observe that, as claimed, condition (⋆) does not hold for ${\mathscr {C}}_1$ . Indeed, consider the algebra ${\boldsymbol {A}}$ depicted in Figure 2 and fix . On the one hand, $a^{\circ } = 1^{\circ } = 1 \in F_0$ and $a \leftrightarrow 1 \in F_0$ . On the other hand, $\langle a,1 \rangle \notin {\boldsymbol {\varOmega }}^{\boldsymbol {A}}(F_0) = id_{\boldsymbol {A}}$ .

In light of Lemma 6.2, a particular case of condition (⋆) arises when dealing with $a^{\circ },b^{\circ } \in A$ .

Corollary 7.1. For every ${\boldsymbol {A}}$ , and $a,b \in A$ ,

$$\begin{align*}\langle a^{\circ},b^{\circ} \rangle \in {\boldsymbol{\varOmega}}^{\boldsymbol{A}}(F) \quad\Leftrightarrow\quad a^{\circ} \leftrightarrow b^{\circ} \in F. \end{align*}$$

The next result is a very important consequence of condition (⋆)—in fact, it is equivalent to it.

Theorem 7.2. For every ${\boldsymbol {A}}$ and ,

$$\begin{align*}{\boldsymbol{\varOmega}}^{\boldsymbol{A}}(F) \!\!\downharpoonright_{{\boldsymbol{A}}^{\circ}} = {\boldsymbol{\varOmega}}^{{\boldsymbol{A}}^{\circ}}(F \cap A^{\circ}). \end{align*}$$

Notice that Theorem 7.2 holds for every equivalential extension of ${\mathscr {C}}_1$ . Indeed, it is known (see [Reference Font32, Lemma 6.72]) that given an equivalential logic ${\mathcal {S}}$ , we have ${\boldsymbol {\varOmega }}^{\boldsymbol {A}}(F) \!\!\downharpoonright _{{\boldsymbol {B}}} = {\boldsymbol {\varOmega }}^{{\boldsymbol {B}}}(F \cap B)$ , for every algebra ${\boldsymbol {A}}$ , , and every subalgebra ${\boldsymbol {B}} \leq {\boldsymbol {A}}$ . Theorem 7.2 is simply the particular case for the subalgebra ${\boldsymbol {A}}^{\circ }$ .

Theorems 6.6 and 7.2 taken together have one major consequence. As it turns out, the subalgebra ${\boldsymbol {A}}^{\circ }$ of an algebra ${\boldsymbol {A}} \in {\mathsf {Alg}}^*({\mathcal {S}})$ is a Boolean algebra.

Corollary 7.3 does not hold for the logic ${\mathscr {C}}_1$ . Indeed, consider the algebra ${\boldsymbol {A}}$ whose truth-tables are given as in Table 3. We have $A^{\circ } = \{ 0,4,5 \}$ . Since $|A^{\circ }| = 3$ , necessarily ${\boldsymbol {A}}^{\circ } \notin \mathsf {BA}$ .

The next two consequences of Corollary 7.3 concern the ${\mathcal {S}}$ -filters of the subalgebra ${\boldsymbol {A}}^{\circ }$ , and in particular its least element. Given a lattice $\langle {\boldsymbol {A}} , \wedge , \vee \rangle $ , let $\mathrm {Filt}{\boldsymbol {A}}$ denote the set of lattice filters of ${\boldsymbol {A}}$ w.r.t. the order $a \leq ^{\boldsymbol {A}} b$ iff $a \wedge ^{\boldsymbol {A}} b = a$ iff $a \vee ^{\boldsymbol {A}} b = b$ , for every $a,b \in A$ . Recall that, given ${\boldsymbol {A}} \in \mathsf {BA}$ , we have .

Corollary 7.5. If ${\boldsymbol {A}} \in {\mathsf {Alg}}^*({\mathcal {S}})$ , then

where $1$ is the top element of ${\boldsymbol {A}}^{\circ }$ .

8 Subdirectly irreducible algebras relative to ${\mathsf {Alg}}^*({\mathcal {S}})$

We are now ready to investigate the subdirectly irreducible algebras in ${\mathsf {Alg}}^*({\mathcal {S}})$ relative to ${\mathsf {Alg}}^*({\mathcal {S}})$ , and to prove the two main results of Part II (Theorems 8.3 and 8.7), namely:

1. 1. Let ${\mathscr {C}}_1 \leq {\mathcal {S}} \leq \mathcal {CL}$ satisfy condition (⋆). If ${\boldsymbol {A}} \in {\mathsf {Alg}}^*({\mathcal {S}})$ is a non-trivial algebra subdirectly irreducible relative to ${\mathsf {Alg}}^*({\mathcal {S}})$ , then .

2. 2. Let ${\mathscr {C}}_1 \leq {\mathcal {S}} \leq \mathcal {CL}$ be finitely equivalential with set of congruence formulas ${\boldsymbol {\rho }}(x,y) = \{ x \leftrightarrow y , \neg x \leftrightarrow \neg y \}$ . If ${\boldsymbol {A}} \in {\mathsf {Alg}}^*({\mathcal {S}})$ is a non-trivial algebra subdirectly irreducible relative to ${\mathsf {Alg}}^*({\mathcal {S}})$ , then $|A| \leq 3$ .

We start by discarding the case of a trivial (Boolean) algebra in Corollary 7.3. Unless otherwise stated, we continue to assume that the underlying logic ${\mathcal {S}}$ satisfies condition (⋆).

We are now able to identify, up to isomorphism, the (Boolean) subalgebra ${\boldsymbol {A}}^{\circ }$ of any non-trivial algebra ${\boldsymbol {A}} \in {\mathsf {Alg}}^*({\mathcal {S}})$ subdirectly irreducible relative to ${\mathsf {Alg}}^*({\mathcal {S}})$ .

Having determined the cardinality of the subuniverse $A^{\circ }$ , given ${\boldsymbol {A}} \in {\mathsf {Alg}}^*({\mathcal {S}})$ non-trivial subdirectly irreducible relative to ${\mathsf {Alg}}^*({\mathcal {S}})$ , we now wish to determine the cardinality of the universe A itself. In fact, we want to prove that $|A| \leq 3$ . For this purpose we will need to strengthen our assumption over ${\mathcal {S}}$ . The next auxiliary results however still holds under our current assumption, that is, ${\mathcal {S}}$ satisfying (⋆). In light of Corollary 7.3, let $1$ denote the top element of ${\boldsymbol {A}}^{\circ }$ and let $0 = \neg 1$ .

For the last result of the section let ${\mathcal {S}}$ be a finitary and finitely equivalential extension of ${\mathscr {C}}_1$ , extended itself by $\mathcal {CL}$ , with (finite) set of congruence formulas ${\boldsymbol {\rho }}(x,y) = \{ x \leftrightarrow y , \neg x \leftrightarrow \neg y \}$ . Let us first see that our new assumption is stronger than condition (⋆).

Proof Our hypothesis tells us that for every algebra ${\boldsymbol {A}}$ , and $a,b \in A$ ,

$$\begin{align*}\langle a,b \rangle \in {\boldsymbol{\varOmega}}^{\boldsymbol{A}}(F) \quad\Leftrightarrow\quad a \leftrightarrow^{\boldsymbol{A}} b \in F \text{ and } \neg a \leftrightarrow^{\boldsymbol{A}} \neg b \in F. \end{align*}$$

But this clearly implies (⋆⋆)—which is the particular case where $a,b \in A^{\circ }$ —and we have seen it already to be equivalent to (⋆).

A careful look at the proof of Theorem 8.7 show us why condition (⋆) does not suffice. We need to extend (⋆) to elements $a,b \in A - A^{\circ }$ . That is: for every ${\boldsymbol {A}}$ , and $a,b \in A - A^{\circ }$ ,

$$ \begin{align*} \langle a,b \rangle \in {\boldsymbol{\varOmega}}^{\boldsymbol{A}}(F) \quad\Leftrightarrow\quad a \leftrightarrow^{\boldsymbol{A}} b \in F \text{ and } \neg a \leftrightarrow^{\boldsymbol{A}} \neg b \in F. \end{align*} $$

An important consequence of our stronger assumption on ${\mathcal {S}}$ (that is, ${\mathcal {S}}$ is finitary and finitely equivalential) is that the class of algebraic reducts of ${\mathcal {S}}$ is a quasivariety—see [Reference Font32, Corollary 6.80]. Quasivarieties are fully determined by their relative subdirectly irreducible algebras. In Part III, we will characterize the quasivariety ${\mathsf {Alg}}^*({\mathcal {S}})$ in terms of the subdirectly irreducible algebras in ${\mathsf {Alg}}^*({\mathcal {S}})$ relative to ${\mathsf {Alg}}^*({\mathcal {S}})$ , for the equivalential extensions of ${\mathscr {C}}_1$ considered in the literature . In light of Theorem 8.7, we will do this by determining the truth-tables of the three-element algebras in ${\mathsf {Alg}}^*({\mathcal {S}})$ subdirectly irreducible relative to ${\mathsf {Alg}}^*({\mathcal {S}})$ .

Part III. Axiomatic extensions of $\mathbf {\mathscr {C}}_{\mathbf {1}}$ .

In this last part we extend our AAL study of ${\mathscr {C}}_1$ to some of its paraconsistent extensions considered in the literature. To settle the scope of the logics under study, we shall focus ourselves on the so-called $d{\mathscr {C}}$ -systems, according to the terminology of [Reference Carnielli and Marcos16, Section 3.8] or [Reference Carnielli, Coniglio and Marcos17, Section 5.1]. In particular, we shall be mainly interested in the logics ${\mathcal {C}ilo}$ , ${\mathcal {C}ilow}$ , ${\mathcal {C}ibv}$ , , , and —recall Figure 1 for the inclusion relations among these logics.

In the sequel we will only classify sentential logics within the Leibniz hierarchy, leaving aside the Frege hierarchy. The reason for this omission is that every extension of ${\mathscr {C}}_1$ (weaker than $\mathcal {CL}$ ) is not self-extensional—see [Reference Carnielli and Marcos16, Corollary 3.65]—and therefore falls outside the Frege hierarchy.

9 The logic ${\mathcal {C}ilo}$

The goals of this section are to introduce the logic ${\mathcal {C}ilo}$ , prove that it satisfies condition (⋆) (Corollary 9.2), and classify it within the Leibniz hierarchy (Propositions 9.6 and 9.9). We finish with a brief discussion about the class ${\mathsf {Alg}}^*({\mathcal {C}ilo})$ in order to clarify a couple of incorrect claims in the literature.

We first consider an extension of ${\mathscr {C}}_1$ introduced by da Costa, Béziau, and Bueno in [Reference da Costa, Béziau and Bueno24]. We follow the presentation of [Reference Carnielli and Marcos16], as well as the notation adopted there—the reason for choosing the notation ${\mathcal {C}ilo}$ of [Reference Carnielli and Marcos16] instead of the original notation ${\mathscr {C}}_1^+$ of [Reference da Costa, Béziau and Bueno24] is so that it does not collide with the notation of the strong version of ${\mathscr {C}}_1$ [Reference Albuquerque, Font and Jansana1]. Let us define the logic ${\mathcal {C}ilo}$ as the logic axiomatized by (Ax1)–(Ax11) plus (MP), together with the following axioms:

(Ax12a) $$ \begin{align} &\vdash (\varphi^{\circ} \vee \psi^{\circ}) \to (\varphi \wedge \psi)^{\circ}. \end{align} $$

(Ax13a) $$ \begin{align} &\vdash (\varphi^{\circ} \vee \psi^{\circ}) \to (\varphi \vee \psi)^{\circ}. \end{align} $$

(Ax14a) $$ \begin{align} &\vdash (\varphi^{\circ} \vee \psi^{\circ}) \to (\varphi \to \psi)^{\circ}. \end{align} $$

Clearly the logic ${\mathcal {C}ilo}$ is an extension of ${\mathscr {C}}_1$ , that is ${\mathscr {C}}_1 \leq {\mathcal {C}ilo}$ , and therefore Lemma 3.2 still holds for the consequence relation $\vdash _{{\mathcal {C}ilo}}$ . In particular,

$$\begin{align*}\varphi^{\circ} \vdash_{{\mathcal{C}ilo}} (\neg \varphi)^{\circ}. \end{align*}$$

Although the axiomatization of ${\mathcal {C}ilo}$ resembles that of ${\mathscr {C}}_1$ , the logic ${\mathcal {C}ilo}$ is stronger enough to obtain better results than those seen for ${\mathscr {C}}_1$ , at least from an AAL point of view. By “stronger enough,” we mean ${\mathcal {C}ilo}$ satisfies (⋆).

To begin with, let us stress that , for an arbitrary algebra ${\boldsymbol {A}}$ , and therefore the results seen so far for ${\mathscr {C}}_1$ -filters are also applicable to ${\mathcal {C}ilo}$ -filters. In particular, and having in mind that sets of parameterized congruence formulas are preserved by extensions, for every algebra ${\boldsymbol {A}}$ , , and $a,b \in A$ ,

$$ \begin{align*} \langle a,b \rangle \in {\boldsymbol{\varOmega}}^{\boldsymbol{A}}(F) \quad\Leftrightarrow\quad &\forall n \in \omega \; \forall m \in \omega \; \forall c_1,\ldots,c_n \in A, \\ &\Phi_n^{\boldsymbol{A}}(\neg^m a, \neg^m b, c_1,\ldots,c_n) \subseteq F , \\ &\Psi_n^{\boldsymbol{A}}(\neg^m a, \neg^m b, c_1,\ldots,c_n) \subseteq F. \end{align*} $$

We now prove that ${\mathcal {C}ilo}$ satisfies (⋆). The proof makes use of the (rather complex) set of parameterized congruence formulas given in Theorem 4.3. It is interesting to observe where the axioms (Ax12a)–(Ax14a) play its role, and why the axioms (Ax12)–(Ax14) do not suffice for our purposes.

Theorem 9.1. Let ${\boldsymbol {A}}$ be arbitrary, , and $a,b \in A$ . If $a^{\circ },b^{\circ } \in F$ , then

$$\begin{align*}\langle a,b \rangle \in {\boldsymbol{\varOmega}}^{\boldsymbol{A}}(F) \quad\Leftrightarrow\quad a \leftrightarrow b \in F. \end{align*}$$

Proof If $\langle a,b \rangle \in {\boldsymbol {\varOmega }}^{\boldsymbol {A}}(F)$ , then $a \leftrightarrow b \in F$ by Proposition 4.1. Conversely, assume $a \leftrightarrow b \in F$ . We claim that for every $c_1,\ldots ,c_n \in A$ ,

$$\begin{align*}\bigcup_{n \in \omega} \bigcup_{m \in \omega} \Phi_n^{\boldsymbol{A}}(\neg^m a, \neg^m b, c_1,\ldots,c_n) \subseteq F. \end{align*}$$

The proof goes by induction on $n \in \omega $ .

Basis: We must prove that for every $m \in \omega $ , $\neg ^m a \leftrightarrow \neg ^m b \in F$ . The proof goes by induction on $m \in \omega $ . Assume first $m=0$ . It follows by assumption that $a \leftrightarrow b \in F$ . Assume now that $m> 0$ . On the one hand, we have $\neg ^m a \leftrightarrow \neg ^m b \in F$ , by inductive hypothesis. On the other hand, since $a^{\circ },b^{\circ } \in F$ , it follows by m applications of Lemma 3.2.19 that $(\neg ^m a)^{\circ },(\neg ^m b)^{\circ } \in F$ . So it follows by Lemma 3.2.8 that $\neg ^{m+1} a \leftrightarrow \neg ^{m+1} b \in F$ . Thus, $\bigcup _{m \in \omega } \Phi _0(\neg ^m a, \neg ^m b) \subseteq F$ .

Step: Let $m,m_1,\ldots ,m_{n+1} \in \omega $ , $c_1,\ldots ,c_{n+1} \in A$ , and $*_1,\ldots ,*_{n+1} \in \{ \wedge , \vee , \to \}$ .

• • $\Phi _{n+1}(\neg ^m a, \neg ^m b, c_1, c_2,\ldots ,c_{n+1})$ with $m_{n+1} = 0$ : It follows by inductive hypothesis that $\Phi _n(\neg ^m a, \neg ^m b, c_1,\ldots ,c_n) \subseteq F$ . Therefore,

  $$ \begin{align*} &\neg^{m_n} (\cdots \neg^{m_2} (\neg^{m_1} (\neg^m a *_1 c_1) *_2 c_2) \cdots *_n c_n) \leftrightarrow \\ &\neg^{m_n} ( \cdots \neg^{m_2} ( \neg^{m_1} (\neg^m b *_1 c_1) *_2 c_2) \cdots *_n c_n) \in F. \end{align*} $$
  Since moreover $c_{n+1} \leftrightarrow c_{n+1} \in F$ by Lemma 3.2.1, it follows by Lemma 3.2.4–6 that
  $$ \begin{align*} &\neg^{m_n} (\cdots \neg^{m_2} (\neg^{m_1} (\neg^m a *_1 c_1) *_2 c_2) \cdots *_n c_n) *_{n+1} c_{n+1} \leftrightarrow \\ &\neg^{m_n} ( \cdots \neg^{m_2} ( \neg^{m_1} (\neg^m b *_1 c_1) *_2 c_2) \cdots *_n c_n) *_{n+1} c_{n+1} \in F. \end{align*} $$
  Thus, $\Phi _{n+1}(\neg ^m a, \neg ^m b, c_1, c_2,\ldots ,c_{n+1}) \subseteq F$ .

• • $\Phi _{n+1}(\neg ^m a, \neg ^m b, c_1, c_2,\ldots ,c_{n+1})$ with $m_{n+1}> 0$ : Since $a^{\circ } \in F$ by hypothesis, it follows by m applications of Lemma 3.2.19 that $(\neg ^m a)^{\circ } \in F$ . It then follows by (Ax12a)–(Ax14a) that $(\neg ^m a *_1 c_1)^{\circ } \in F$ ; then by $m_1$ applications of Lemma 3.2.19 that $\big ( \neg ^{m_1} (\neg ^m a *_1 c_1) \big )^{\circ } \in F$ ; and again by (Ax12a)–(Ax14a) that $\big ( \neg ^{m_1} (\neg ^m a *_1 c_1) *_2 c_2\big )^{\circ } \in F$ ; and so on, until we obtain

  (2) $$ \begin{align} \big( \neg^{m_n} \big( \cdots \neg^{m_2} \big( \neg^{m_1} (\neg^m a *_1 c_1) *_2 c_2\big) \cdots *_n c_n \big) *_{n+1} c_{n+1} \big)^{\circ} \in F. \end{align} $$
  Similarly,
  (3) $$ \begin{align} \big( \neg^{m_n} \big( \cdots \neg^{m_2} \big( \neg^{m_1} (\neg^m b *_1 c_1) *_2 c_2\big) \cdots *_n c_n \big) *_{n+1} c_{n+1} \big)^{\circ} \in F. \end{align} $$
  Moreover, it follows by inductive hypothesis that
  $$ \begin{align*} &\neg^{m_n} \big( \cdots \neg^{m_2} \big( \neg^{m_1} (\neg^m a *_1 c_1) *_2 c_2\big) \cdots *_n c_n \big) \leftrightarrow \\ &\neg^{m_n} \big( \cdots \neg^{m_2} \big( \neg^{m_1} (\neg^m b *_1 c_1) *_2 c_2\big) \cdots *_n c_n \big) \in F. \end{align*} $$
  So by Lemma 3.2.4–6,
  (4) $$ \begin{align} &\neg^{m_n} \big( \cdots \neg^{m_2} \big( \neg^{m_1} (\neg^m a *_1 c_1) *_2 c_2\big) \cdots *_n c_n \big) *_{n+1} c_{n+1} \leftrightarrow \notag \\ &\neg^{m_n} \big( \cdots \neg^{m_2} \big( \neg^{m_1} (\neg^m b *_1 c_1) *_2 c_2\big) \cdots *_n c_n \big) *_{n+1} c_{n+1} \in F. \end{align} $$
  It finally follows by (2), (3), (4) and Lemma 3.2.8 that
  (5) $$ \begin{align} &\neg \big( \neg^{m_n} \big( \cdots \neg^{m_2} \big( \neg^{m_1} (\neg^m a *_1 c_1) *_2 c_2\big) \cdots *_n c_n \big) *_{n+1} c_{n+1} \big) \leftrightarrow \notag \\ &\neg \big( \neg^{m_n} \big( \cdots \neg^{m_2} \big( \neg^{m_1} (\neg^m b *_1 c_1) *_2 c_2\big) \cdots *_n c_n \big) *_{n+1} c_{n+1} \big) \in F. \end{align} $$
  Having arrived here, by (2) and Lemma 3.2.19 we have
  (6) $$ \begin{align} \Big( \neg \big( \neg^{m_n} \big( \cdots \neg^{m_2} \big( \neg^{m_1} (\neg^m a *_1 c_1) *_2 c_2\big) \cdots *_n c_n \big) *_{n+1} c_{n+1} \big) \Big)^{\circ} \in F. \end{align} $$
  Similarly, by (3) and Lemma 3.2.19 we have
  (7) $$ \begin{align} \Big( \neg \big( \neg^{m_n} \big( \cdots \neg^{m_2} \big( \neg^{m_1} (\neg^m b *_1 c_1) *_2 c_2\big) \cdots *_n c_n \big) *_{n+1} c_{n+1} \big) \Big)^{\circ} \in F. \end{align} $$
  This time it follows by (5)–(7) and Lemma 3.2.8 that
  $$ \begin{align*} &\neg^2 \big( \neg^{m_n} \big( \cdots \big( \neg^{m_2} \big( \neg^{m_1} (\neg^m a *_1 c_1) *_2 c_2\big) \cdots \big) *_n c_n \big) *_{n+1} c_{n+1} \big) \leftrightarrow \\ &\neg^2 \big( \neg^{m_n} \big( \cdots \big( \neg^{m_2} \big( \neg^{m_1} (\neg^m b *_1 c_1) *_2 c_2\big) \cdots \big) *_n c_n \big) *_{n+1} c_{n+1} \big) \in F. \end{align*} $$
  By repeating this process $m_{n+1}$ times, we eventually obtain
  $$ \begin{align*} &\neg^{m_{n+1}} \big( \neg^{m_n} \big( \cdots \neg^{m_2} \big( \neg^{m_1} (\neg^m a *_1 c_1) *_2 c_2\big) \cdots *_n c_n \big) *_{n+1} c_{n+1} \big) \leftrightarrow \\ &\neg^{m_{n+1}} \big( \neg^{m_n} \big( \cdots \neg^{m_2} \big( \neg^{m_1} (\neg^m b *_1 c_1) *_2 c_2\big) \cdots *_n c_n \big) *_{n+1} c_{n+1} \big) \in F. \end{align*} $$
  Thus, $\Phi _{n+1}(\neg ^m a, \neg ^m b, c_1, c_2,\ldots ,c_{n+1}) \subseteq F$ .

We conclude that for every $c_1,\ldots ,c_n \in A$ ,

$$\begin{align*}\bigcup_{n \in \omega} \bigcup_{m \in \omega} \Phi_n^{\boldsymbol{A}}(\neg^m a, \neg^m b, c_1,\ldots,c_n) \subseteq F. \end{align*}$$

Similarly, one proves that for every $c_1,\ldots ,c_n \in A$ ,

$$\begin{align*}\bigcup_{n \in \omega} \bigcup_{m \in \omega} \Psi_n^{\boldsymbol{A}}(\neg^m a, \neg^m b, c_1,\ldots,c_n) \subseteq F. \end{align*}$$

Since , it follows by Theorem 4.3 that $\langle a,b \rangle \in {\boldsymbol {\varOmega }}^{\boldsymbol {A}}(F)$ .