Maximality in finite-valued Lukasiewicz logics defined by order filters
Marcelo E. Coniglio Francesc Esteva Joan Gispert Lluis Godo






Maximality

in finite-valued Łukasiewicz logics defined by order filters

    Marcelo E. Coniglio^1, Francesc Esteva^2, Joan Gispert^3 and Lluis Godo^2 
 

^1 Dept. of Philosophy - IFCH and  
 Centre for Logic, Epistemology and the History of Science, 
 University of Campinas, Brazil 

coniglio@cle.unicamp.br 

^2 Artificial Intelligence Research Institute (IIIA) - CSIC, Barcelona, Spain 

{esteva,godo}@iiia.csic.es 

^3 Dept. of Mathematics and Computer Science, University of Barcelona, Spain 

jgispertb@ub.edu

    
============================================================================================================================================================================================================================================================================================================================================================================================================================================================





 In this paper we consider the logics 𝖫_n^i obtained from the (n+1)-valued  Łukasiewicz logics Ł_n+1 by taking the order filter generated by i/n as the set of designated elements. In particular, the conditions of maximality and strong maximality among them are analyzed. We present a very general theorem which provides sufficient conditions for maximality between logics. As a consequence of this theorem it is shown that 𝖫_n^i is maximal w.r.t. CPL whenever n is prime. Concerning strong maximality between the logics 𝖫_n^i (that is, maximality w.r.t. rules instead of axioms), we provide algebraic arguments in order to show that the logics 𝖫_n^i are not strongly maximal w.r.t. CPL, even for n prime. Indeed, in such case, we show there is just one extension between 𝖫_n^i and CPL obtained by adding to 𝖫_n^i  a kind of graded explosion rule.  Finally, using these results, we show that the logics  𝖫_n^i with n prime and i/n < 1/2 are ideal paraconsistent logics.





§ INTRODUCTION


In this paper we study the notion of  maximality and strong maximality among finite-valued propositional logics. Recall the usual notion of maximality found in the literature:  a propositional logic L_1,  that is a sublogic of another logic L_2  (in the sense of inclusionship of their consequence relations over the same signature), is called maximal
with respect to L_2  if, roughly speaking, L_1 extended with any theorem of L_2 which is not a theorem of L_1, coincides with L_2. Similarly, recall the stronger notion of strong maximality following <cit.>:  L_1 is called strongly maximal  with respect to L_2  if, roughly speaking again, L_1 extended with  a rule of inference valid in L_2 but not a valid in L_1, coincides with L_2.

The problem of finding and characterizing maximal sublogics (in both senses) of a given logic has already been addressed in the literature, specially in the context of paraconsistent logics, where being maximal with respect to classical logic is felt as a desirable or ideal feature, c.f. <cit.>. Indeed,  being maximal means that, while still allowing non-trivial inconsistent theories, it retains as much as possible of classical logic.

In the present paper we approach the general problem of characterizing maximality (not necessarily for paraconsistent logics) in two different scenarios. The first one considers a very general class of finite-valued logics, those defined by almost arbitrary finite logical matrices. In such a context, we provide a sufficient condition for a logic to be maximal w.r.t. another one with less truth-values under very general conditions. This result, inspired on the notion of recovery operators from paraconsistent logics, turns out to be very powerful and encompasses many maximality results scattered in the literature.

The second scenario considers a particular class of finite-valued logics, the class of n-valued Łukasiewicz logics Ł_n and their related logics defined by order filters. We show that these logics, for n being prime, are maximal but not strongly maximal with respect to classical logic. Actually, we show that each of these logics can always be uniquely extended with a sort of explosion inference rule such that the obtained logic is the unique one below classical logic, and hence strongly maximal.

The paper is structured as follows. After this introduction, we provide in Section <ref> a very general condition for a finite matrix logic to be maximal w.r.t. another one with less truth-values, and we analyze in particular the case of 3-valued logics. In the rest of the paper we focus our attention on the class of finite-valued Łukasiewicz logics 𝖫_n^i defined by order filters. In Section <ref>  we identify which of these logics are maximal with respect to classical logic, while in Section <ref> we study their status regarding the property of strong maximality.  It is in Section <ref> where we fully characterize, by algebraic techniques, conditions of strong maximality.  Finally, in Section <ref> the question of ideal paraconsistent logics (as introduced in <cit.>) will be analized in the present framework. Specifically, it will be shown that the logics  𝖫_n^i with n prime and i/n < 1/2 are ideal paraconsistent logics. In addition, the case 𝖫_3^1 will be discussed with more detail, and it will be argued that this logic constitutes the 4-valued version of the well-known 3-valued paraconsistent logic   𝖩_3 (see <cit.>).
We finish in Section <ref> with some conclusions and prospects of future research.




§ MAXIMALITY AND RECOVERY OPERATORS
 

Let us recall the usual notion of maximality of a  (standard) logic with respect to another:


Let L_1  and L_2 two standard propositional logics defined over the same signature Θ such that L_1  is a proper sublogic of  L_2, i.e.  such that ⊢_L_1⊊⊢_L_2, where ⊢_L_i denotes the consequence relation of  L_i (for i=1,2). Then, L_1 is said to be maximal w.r.t. L_2 if, for every formula φ over Θ, if ⊢_L_2φ but ⊬_L_1φ, then the logic L_1^+  obtained from  L_1   by adding φ as a theorem, coincides with L_2.


By L_1^+  above we mean the logic whose consequence relation is obtained from the one of  L_1 as follows: for every set of formulas Γ∪{ψ} over Θ,
 
    Γ⊢_L_1^+ψ  Γ, {σ(φ)  :  σ }⊢_L_1ψ.



 
It should be noticed that, according to the above definition, if L_1 is a proper sublogic of L_2 such that they validate the same formulas (that is: ⊢_L_1φ   iff   ⊢_L_2φ, for every  formula φ) then L_1 is maximal w.r.t. L_2.



In this section, for the class of  propositional logics induced by finite logical matrices, we will provide a very general sufficient condition for a logic to be maximal w.r.t. another one (see Theorem <ref> below), its proof being inspired in the role played by the so-called recovery operators in paraconsistent and adaptive logics. Recall from <cit.> (see also <cit.>)  the definition of the class of paraconsistent logics called Logics of Formal Inconsistency (LFIs):  a given logic, say L, is an LFI if it is paraconsistent w.r.t. some negation, say  (that is, there exist formulas α and β such that β does not follows from {α,α} in L). In addition, there is a  (primitive of definable) unary connective ∘ in L (called a consistency operator) such that every formula β follows in L from a set of the form{α,α, ∘α}.[This is a slightly simplified presentation of the original definition of LFIs.]  If L is an  LFI which is sublogic of  classical propositional logic (CPL), presented in the same signature of L,[In this case, the formulas ∘α take the value 1 for every evaluation in  CPL.]  then the consistency operator ∘ allows to recover CPL inside  L by adding additional hypothesis concerning the consistency (or `classicality', or `well-behavior') of some formulas. Namely, for every (finite) set Γ∪{ψ} of formulas,

    Γ⊢_ CPLψ  (∃Λ)[Γ, {∘α :  α∈Λ}⊢_L ψ],

where Λ is a set of formulas. This is what is called  a Derivability Adjustment Theorem (DAT).
The idea of DATs was proposed by Battens in the context of Adaptive logics, but this technique (as well as the notion of consistency operator) was already used by da Costa for his well-known hierarchy of paraconsistent systems C_n (see <cit.>).

A more interesting DAT (as, for instance, the ones obtained by da Costa) requires that the consistency (or well-behavior) operator ∘ can just be applied to the propositional variables occurring in  Γ∪{ψ}. This suggests that, given two standard propositional logics L_1  and L_2 defined over the same signature Θ such that ⊢_L_1⊆⊢_L_2, a DAT between both logics can be defined in terms of a recovery operator ∘ (generalizing the idea of LFIs):
 for every (finite) Γ∪{ψ},

    Γ⊢_L_2ψ  Γ, {∘ p_1, …,∘ p_m}⊢_L_1ψ,

where {p_1, …, p_m} is the set of propositional variables occurring in Γ∪{ψ}.

The idea then is that if one of such recovery operators ∘_φ can be defined as  a family of instances of a theorem φ of L_2 which is not derivable in L_1, and if this process can be reproduced for any of such formulas φ, then it will follow that L_2 is maximal w.r.t. L_1. To be more general, a finite recovery set ◯(p) of formulas depending only on one variable p will be considered instead of a single formula ∘(p), following the original definition of LFIs. Actually, in Theorem <ref> below some sufficient conditions are given in order to define such recovery sets, which will allow us to determine if one logic is maximal w.r.t. another.


In what follows, ℒ(Θ) will denote the term algebra generated by a propositional signature Θ from a fixed set P={p_n   :  n ≥ 1} of propositional variables. If A is an algebra over Θ then the set of homomorphisms from ℒ(Θ) to A will be denoted by Hom(ℒ(Θ), A).

Given an algebra A over Θ and a non-empty subset F ⊆ A, the pair ⟨ A, F⟩ is called a logical matrix <cit.>. The logic L defined by the matrix ⟨ A, F⟩ over ℒ(Θ) is given by the following consequence relation: for every set of formulas Γ∪{φ}⊆ℒ(Θ),

    Γ⊢_L φ e∈ Hom(ℒ(Θ), A), e(ψ) ∈ F ψ∈Γ e(φ) ∈ F .

From now on, with no danger of confusion,  given a logical matrix ⟨ A, F⟩  we will write L = ⟨ A, F⟩ to refer to the corresponding induced logic defined as above. We will also use the term matrix logic to refer a logic defined by a logical matrix.



 
Let L_1=⟨ A_1, F_1⟩  and L_2=⟨ A_2, F_2⟩ be two matrix logics defined over a signature Θ such that
A_2 is a subalgebra of A_1 and F_2 = F_1 ∩ A_2. Then ⊢_L_1⊆⊢_L_2, that is: for every Γ∪{ψ}, if Γ⊢_L_1ψ then Γ⊢_L_2ψ.


Assume that Γ⊢_L_1ψ. Let e ∈ Hom(ℒ(Θ), A_2) be an evaluation for L_2 such that e[Γ] ⊆ F_2. Let e̅:ℒ(Θ)→ A_1 such that e̅(φ)=e(φ) for every φ∈ℒ(Θ). Then e̅∈ Hom(ℒ(Θ), A_1), so e̅ is an evaluation for L_1 such that e̅[Γ] ⊆ F_1. By hypothesis, e̅(ψ) ∈ F_1 and so e(ψ) ∈ F_1 ∩ A_2=F_2. This shows that   Γ⊢_L_2ψ.


After this previous lemma, we can state the main result on this section.

 
Let L_1=⟨ A_1, F_1⟩  and L_2=⟨ A_2, F_2⟩ be two distinct finite matrix logics over a same signature Θ such that A_2 is a subalgebra of A_1 and F_2 = F_1 ∩ A_2.
 Assume the following:


  * A_1={0,1,a_1,…,a_k,a_k+1,…,a_n}   and  A_2={0,1,a_1,…,a_k} are finite such that 0 ∉F_1, 1 ∈ F_2 and {0,1} is a subalgebra of A_2.

  * There are formulas ⊤(p) and (p) in ℒ(Θ) depending at most on one variable p such that e(⊤(p))=1 and e((p))=0, for every evaluation e for L_1.

  * For every k+1 ≤ i ≤ n and 1 ≤ j ≤ n (with i ≠ j) there exists a formula α^i_j(p) in ℒ(Θ) depending  at most on one variable p such that, for every evaluation e, e(α^i_j(p))=a_j if e(p)=a_i. 
Then,  L_1 is maximal w.r.t.  L_2.


Let us begin by  observing that the family of evaluations for L_1 which take values in A_2 for every propositional variable can be identified with the family of evaluations for L_2.[This fact was used in the proof of Lemma <ref>.]

Notice that, by  Lemma <ref>, ⊢_L_1⊆⊢_L_2. Suppose that there is some formula φ(p_1,…,p_m)  such that ⊢_L_2φ but ⊬_L_1φ (otherwise the proof is done, by Remark <ref>). Then, e(φ) ∈ F_2 for every evaluation e ∈ Hom(ℒ(Θ), A_2), but there is an homomorphism e_0 ∈ Hom(ℒ(Θ), A_1) such that e_0(φ) ∉F_1. By the observation at the beginning of the proof (and by considering that F_2 ⊆ F_1), there exists a propositional variable p_i (for 1 ≤ i ≤ m) such that e_0(p_i) ∉A_2. Consider now a substitution σ_0 such that


    σ_0(p)= {⊤(p_1)    if e_0(p)=1,
    (p_1)    if e_0(p)=0,
    p_j    if e_0(p)=a_j (for 1 ≤ j ≤ n)
    .



and let γ(p_1,…,p_n)=σ_0(φ). Observe that some of the variables p_j may not appear in γ, but at least one variable p_j (with k+1 ≤ j ≤ n) must occur in γ, by the hypothesis over e_0. Now we can state two immediate facts:


  Fact 1: Given an evaluation e for L_1, if e(p_j)∈ A_2 for every 1 ≤ j ≤ n then
e(γ) ∈ F_2.

Proof:  follows from the observation at the beginning  of the proof, and by noting that  γ is an instance of a tautology of L_2.


  Fact 2:  Given an evaluation e for L_1, if e(p_j)=a_j for 1 ≤ j ≤ n then  e(γ) = e_0(φ) ∉F_1.

Proof: Observe that, from the hypothesis, it follows that e(σ_0(p_i))=e_0(p_i) for every 1 ≤ i ≤ m. 


Now, for any propositional variable p, let  α^j_j(p)=p for every 1 ≤ j ≤ n, and let ◯(p) be the finite set of formulas

    ◯(p) = {γ(α^i_1(p),…,α^i_n(p))  :   k+1 ≤ i ≤ n}.

Let e be an evaluation in L_1. Observe the following:

(i) If e(p)∈ A_2 then e(α^i_j(p)) ∈ A_2 (since A_2 is a subalgebra). For each k+1 ≤ i ≤ n let e_i be an evaluation for L_1 such that e_i(p_j)= e(α^i_j(p)), for every 1 ≤ j ≤ n. Then e_i(γ) ∈ F_2 , by Fact 1. But e_i(γ) = e(γ(α^i_1(p),…,α^i_n(p)))  and so
e(γ(α^i_1(p),…,α^i_n(p))) ∈ F_2
for every k+1 ≤ i ≤ n. This means that e[◯(p)] ⊆ F_1 if e(p)∈ A_2. 

(ii) If e(p)∉ A_2 then e(p)=a_i for some k+1 ≤ i ≤ n. From this, e(α^i_j(p))=a_j for all 1 ≤ j ≤ n. Let e' be an evaluation for L_1 such that e'(p_j)=a_j, for every 1 ≤ j ≤ n. Then e'(γ) = e(γ(α^i_1(p),…,α^i_n(p))). But, by Fact 2, e'(γ) =e_0(φ) ∉ F_1 and so e(γ(α^i_1(p),…,α^i_n(p))) ∉ F_1. Thus, e[◯(p)] ⊈F_1 if e(p) ∉ A_2. Equivalently, e(p) ∈ A_2 if e[◯(p)] ⊆ F_1. 

From the observations (i) and (ii) it follows that


 (*) e[◯(p)] ⊆ F_1   e(p) ∈ A_2.

Finally, let L_1^+ be the logic obtained from L_1 by adding φ (and all of its instances) as a theorem.
As observed above,

    Γ⊢_L_1^+ψ  Γ, {σ(φ)  :  σ }⊢_L_1ψ.




  Fact 3:

Let Γ∪{ψ} be  a finite a set of formulas in ℒ(Θ) depending on the variables p_1,…,p_t. Then 

(**) Γ⊢_L_2ψ  Γ, ◯(p_1), …, ◯(p_t) ⊢_L_1ψ. 

Proof: Assume that Γ⊢_L_2ψ and let  e ∈ Hom(ℒ(Θ), A_1) such that e[Γ∪⋃_i=1^t ◯(p_i)] ⊆ F_1. By (*), e(p_i) ∈ A_2 for every 1 ≤ i ≤ t. Consider now an evaluation e̅∈ Hom(ℒ(Θ), A_2) such that e̅(p)=e(p) if p ∈{p_1,…,p_t}, and e̅(p)=0 otherwise. Then e̅(β)=e(β) for every β in ℒ(Θ) depending on the variables p_1,…,p_t. Thus, e̅[Γ] ⊆ F_1 ∩ A_2 = F_2 whence e̅(ψ) ∈ F_2, by hypothesis. That is, e(ψ) ∈ F_1 and so  Γ, ◯(p_1), …, ◯(p_t) ⊢_L_1ψ.

Conversely, assume that Γ, ◯(p_1), …, ◯(p_t) ⊢_L_1ψ and consider an evaluation e̅∈ Hom(ℒ(Θ), A_2) such that e̅[Γ] ⊆ F_2. Define an evaluation e ∈ Hom(ℒ(Θ), A_1) such that e(p)=e̅(p) for every variable p. Then e(β)=e̅(β) for every β in ℒ(Θ) and so e[Γ] ⊆ F_1 and also e[◯(p_i)] ⊆ F_1 for every 1 ≤ i ≤ t, by (*). By hypothesis, e(ψ) ∈ F_1 and then e̅(ψ) ∈ F_1 ∩ A_2, that is, e̅(ψ) ∈ F_2. This shows that  Γ⊢_L_2ψ, proving Fact 3.


Consider now a finite a set of formulas   Γ∪{ψ} in ℒ(Θ) depending on the variables p_1,…,p_t. Suppose that Γ⊢_L_2ψ. Then Γ, ◯(p_1), …, ◯(p_t) ⊢_L_1ψ, by Fact 3. But the latter implies that Γ, {σ(φ)  :  σ }⊢_L_1ψ, because each ◯(p_i) is a set of instances of φ. From this, it follows that Γ⊢_L_1^+ψ, by definition of L_1^+.

On the other hand,  suppose that Γ⊢_L_1^+ψ. Given that ⊢_L_1⊆⊢_L_2 (by  Lemma <ref>)  and that ⊢_L_2φ (by hypothesis) then Γ⊢_L_2ψ, by definition of L_1^+. This shows that L_1^+ coincides with L_2 and so L_1 is maximal w.r.t. L_2.



In the next example we show an application of Theorem <ref> in order to prove some maximality conditions for two logics related to the well-known 4-valued logic ℱ𝒪𝒰ℛ introduced by Belnap and Dunn <cit.>. 








Consider Belnap-Dunn's matrix logic  ℬ𝒟=⟨𝔐_4,{1,B}⟩, where  𝔐_4=⟨ M_4, , , ⟩ is the algebra associated to the logical lattice M_4 (see Fig. 1) expanded with the De Morgan negation  defined as:




       

 1       0    
 B        B    
 N        N    
 0       1    
 



Much later, De and Omori considered in <cit.> the expansion ℬ𝒟^∼ of ℬ𝒟 by adding the strong negation ∼, given by the following table:




         x     ∼x 
 0           1          

N           B          

B           N          

1           0          
 




On the other hand, before Belnap and Dunn's investigations,  L. Monteiro  already considered in 1963  (see <cit.>) the 4-valued algebra  𝔐_4m obtained from  𝔐_4  by adding a modal operator □  defined as follows:




      □ 

 1       1    
 B       0    
 N       0    
 0       0    
 



This led to  A. Monteiro to consider the variety 𝐓𝐌𝐀 of tetravalent modal algebras, which is the one generated by  𝔐_4m (cf. <cit.>).  As  proven by Font and Rius in <cit.>, the (degree-preserving) logic of 𝐓𝐌𝐀 is characterized by the matrix logic M_B =⟨𝔐_4m,{B, 1}⟩.
Previous to <cit.> and with a different motivation, Coniglio and Figallo define in <cit.> the logic M_B^∼ =⟨𝔐_4m^∼,{B, 1}⟩, the expansion of M_B with the strong negation ∼ described above,  characterizing the (degree-preserving) logic of the variety generated by 𝔐_4m^∼  (which was independently introduced by A. Monteiro in <cit.> and by G. Moisil in <cit.>.)


By using Theorem <ref>, it is easy to show that both  M_B^∼ and ℬ𝒟^∼ are maximal relative to CPL presented in the signature Θ={,,∼,□} and Θ'={,,∼} over the two-element Boolean algebra 𝔅_2, respectively (where □ p is equivalent to p and  p is equivalent to  ∼p). Indeed, observe that B_2 (expanded by ∼ and □) is a subalgebra of 𝔐_4m^∼, and ⊤(p)=p ∼ p and (p)=p ∼p are as required. Notice that, since there are in M_4 just two values besides the `classical' ones, namely a_1=N and a_2=B, the formulas α^1_2(p)=α^2_1(p)=∼p are such that e(α^1_2(p))=B if e(p)=N, e(α^2_1(p))=N if e(p)=B. Therefore, it follows from Theorem <ref> that M_B^∼  is maximal reative to CPL presented over the signature Θ. Similarly, it also follows that ℬ𝒟^∼ is maximal relative to CPL presented over the signature Θ' (the latter corresponding to <cit.>).  ▪


As an immediate consequence of Theorem <ref>, it follows that any 3-valued logic which extends CPL and it can express the top and the bottom formulas, is maximal w.r.t. CPL.


 
Let A_1 be an algebra defined over a signature Θ with domain A_1={0,1/2,1}, and consider the matrix logic  L_1=⟨ A_1, F_1⟩ where 0 ∉F_1 and 1 ∈ F_1. Further, let A_2 be a subalgebra of A_1, with A_2 = {0, 1}, and assume that the matrix logic L_2=⟨ A_2, {1}⟩ is a presentation of classical propositional logic CPL over signature Θ such that L_2 is distinct from L_1.
Suppose additionally there are formulas ⊤(p) and (p) in ℒ(Θ) on one variable p such that e(⊤(p))=1 and e((p))=0, for every evaluation e for L_1. Then,  L_1 is maximal w.r.t. CPL (presented as L_2).


Observe that L_1 and L_2  are  matrix logics as in Lemma <ref>, since {1}=F_1 ∩ A_2.
Given that A_1 contains just one element out of {0,1}, namely a_1=1/2, then Theorem <ref> can be applied (since requirement (3) is satisfied by vacuity). As a consequence of Theorem <ref>, L_1 is maximal w.r.t. CPL (presented as L_2).


In the next example some instances of Corollary <ref> are analyzed, showing the strength of this result: indeed, several well-known 3-valued logics which are known to be maximal w.r.t. CPL fall inside the scope of  Corollary <ref>. 

 
(1) Let us begin with Łukasiewicz 3-valued logic Ł_3=⟨_3,{1}⟩, where _3 is the usual 3-valued algebra for Ł_3 over Θ={,→} with domain {0,1/2,1}.
 Let 𝖫_1^1=⟨ B_2,F⟩ be a presentation of CPL, where  B_2 is  the two-element Boolean algebra over Θ with domain {0,1} and F={1}. It is easy to see that Ł_3 satisfies the requirements of Corollary <ref> by taking ⊤(p)=(p → p) and (p)= (p → p). This produces a new proof of the maximality of Ł_3 w.r.t. CPL. In order to illustrate this fact consider by  instance  φ(p_1)=p_1 ∨ p_1 := (p_1 →¬ p_1)→¬ p_1, a formula which is valid in CPL but it is not valid in  Ł_3. Indeed, any evaluation e_0 in Ł_3 where e_0(p_1)=1/2 is such that e_0(φ)=1/2, a non-designated truth-value. By following the construction described in the proof of Theorem <ref> (where α^1_1(p)=p), it follows that γ(p_1)=φ(p_1), and so ∘(p)=p ∨ p is a recovery operator for Ł_3 w.r.t. CPL defined in terms of  φ. Thus, Ł_3 plus φ coincides with CPL. Notice that the truth-table of the recovery operator ∘ is as follows:

    [       ∘;   1   1; 1/2 1/2;   0   1;     ]

(2) Consider now the logic 𝖫_2^1=⟨_3,{1, 1/2}⟩. As it is well known, the matrices of Ł_3 are functionally equivalent to that of the 3-valued paraconsistent logic J_3, introduced by da Costa and  D'Ottaviano, see <cit.>. This means that  𝖫_2^1 coincides with J_3 up to language. By item (1) and  Corollary <ref> it follows that  𝖫_2^1 is maximal w.r.t. CPL.  This constitutes a new proof of the maximality of J_3 (and all of its alternative presentations, such as LFI1 or MPT, see <cit.>) w.r.t. CPL. A generalization of J_3 to Ł_4, called J_4, will be proposed in Subsection <ref>. As an illustration  of how the technique of the proof works, let φ(p_1)=(( p_1 → p_1) ∧ (p_1 → p_1)). It is easy to see that    φ(p_1) is valid in CPL but it is not valid in    𝖫_2^1: any evaluation e_0 in 𝖫_2^1 with e_0(p_1)=1/2 is such that e_0(φ)=0. Then, by the proof of Theorem <ref> (where α^1_1(p)=p),  γ(p_1)=φ(p_1) and so ∘(p)= (( p → p) ∧ (p → p)) is a recovery operator  for   𝖫_2^1 w.r.t. CPL defined in terms of instances of φ. This means that  𝖫_2^1 plus φ coincides with CPL.  The truth-table of ∘ is as follows:

    [       ∘;   1   1; 1/2   0;   0   1;     ]

(3) In an unpublished draft, J. Marcos <cit.> (see also <cit.>) proposes a family of 8,192 logics which are 3-valued and paraconsistent, belonging to the hierarchy of LFIs. Among these logics, there is J_3  (whose truth-tables can define the matrices of all the other logics in the family) and Sette's logic 𝖯^1 (see <cit.>), whose truth-tables are definable by the matrices of any of the logics in the family. All these logics are maximal w.r.t. CPL presented in the signature {,,→,,∘} such that ∘φ is valid for every φ (that is, algebraically, ∘(x)=1 for all  x ∈{0,1}). The proof of maximality of all these logics w.r.t. CPL follows easily from Corollary <ref>  by taking ⊤(p)=p → p and (p)=p  p ∘ p.

(4) Let 𝖨^1 be the 3-valued paracomplete logic introduced by A.M. Sette and W.A. Carnielli in <cit.>. It is defined over Θ={→,} with domain {0,1/2,1} and designated value 1, and whose operations are given by the tables below.


    [   →   1 1/2   0;   1   1   0   0; 1/2   1   1   1;   0   1   1   1;     ][        ;   1   0; 1/2   0;   0   1;     ]


Once again, the maximality of 𝖨^1 w.r.t. CPL follows from Corollary <ref> by taking ⊤(p)=p → p and (p)=(p → p).

(5) Let G_n+1=⟨ G_n+1,{1}⟩ be the (n+1)-valued Gödel logic defined over the algebra G_n+1 for Θ={,,→,} with domain {0,1/n,…,n-1/n,1} such that x  y = min{x,y}; x  y = max{x,y}; x → y= 1 if x ≤ y and x → y= y otherwise; and x =1 if x=0 and x=0 otherwise. In particular, G_3 is defined over {0,1/2,1} with the following tables for → and :


    [   →   1 1/2   0;   1   1 1/2   0; 1/2   1   1   0;   0   1   1   1;     ][        ;   1   0; 1/2   0;   0   1;     ]


Clearly G_3 falls within the scope of Corollary <ref> (where  ⊤(p)=p → p and (p)=p  p) and so it is maximal w.r.t. CPL presented over Θ. Observe that  for n ≥ 3 the algebra G_n+1 does not have enough expressive power to define all the formulas α^i_j in order to apply Theorem <ref>. For instance, in G_4 there are no formulas α^1_2(p) and α^2_1(p) such that e(α^1_2(p))=2/3 if e(p)=1/3 and  e(α^2_1(p))=1/3 if e(p)=2/3. ▪


  In <cit.> the authors introduced the notion of ideal paraconsistent logics.  Together with this, they presented a family ℳ_n+2 of (n+2)-valued matrix logics (with n ≥ 2) which are ideal paraconsistent (and so, from the very definition, they are also maximal w.r.t. CPL, see Definition <ref> in Section <ref>). The fact that  all these logics are maximal w.r.t. CPL (as proved in  <cit.>) can also be proved by applying Theorem <ref>, as it will be shown in what follows.

Given n≥ 2 consider the algebras 𝐀_n+2 over the signature Θ={,♢,⊃} with domain A_n+2={0,1,a_1,…,a_n} such that the operations are defined as follows: 0=1, 1=0 and x=x otherwise; ♢ 0=1,  ♢ 1=0,  ♢ a_i=a_i+1 if i<n and  ♢ a_n=a_1; x ⊃ y = 1 if   x ∉ D={1,a_1} and x ⊃ y = y otherwise. The  logic ℳ_n+2 is defined by the logical matrix ⟨𝐀_n+2,D⟩ for every n≥ 2. Let us see that the conditions of Theorem <ref> are satisfied for every logic ℳ_n+2 w.r.t. CPL. It is easy to see that {0,1}  is a subalgebra of 𝐀_n+2 and so, by Lemma <ref>, ℳ_n+2 is a sublogic of CPL presented in the signature Θ in which ♢ coincides with negation and  1 is the designated value. In addition, it is easy to see that, given a propositional variable p, the formulas ⊤(p)=(p ⊃♢ p) ⊃ (p ⊃♢ p) and (p)=⊤(p) are such that e(⊤(p))=1 and e((p))=0, for every evaluation e. Consider now the formulas α^i_j(p)=♢^j-ip if i<j and    α^i_j(p)=♢^n-i+jp if i>j, where ♢^0p=p and ♢^i+1p=♢♢^i p, for every i. An easy computation shows that e(α^i_j(p))=a_j if e(p)=a_i, for every i≠ j. Therefore, the conditions of  Theorem <ref> are fullfilled and so each logic  ℳ_n+2 is maximal w.r.t. CPL.

The question of ideal paraconsistent logics in the present framework will be treated again in Section <ref>.▪



The examples given above show the value of  Theorem <ref> in order to state maximality of logics under certain hypothesis concerning the expressive power of the given logics. Indeed,  several proofs of maximality found in the literature can be easily obtained as a consequence of Theorem <ref>: for instance, the ones given for the 3-valued paraconsistent logic 𝖯^1 in <cit.>, for the 3-valued logic  𝖨^1  in <cit.> and for J_3 (formulated as the equivalent logic LFI1) in  <cit.>, respectively. It is worth noting that all the examples of maximality of a logic L_1 w.r.t. another logic L_2 given in this section, as well as the examples to be given in the rest of the paper, are non-vacuous in the sense of  Remark <ref>. Indeed, in all the examples of maximality presented here the set of theorems of L_1 is strictly contained in the set of theorems of L_2, thus the notion of maximality holds in a non-trivial way. For instance,   the formula p →∘ p is a theorem of CPL which does not hold in any of the logics presented in Example <ref>(3), while the formula p →♢ p is a theorem of CPL which does not hold in any of the systems ℳ_n+2 presented in Example <ref>.
 On the other hand, it should be observed that the set of designated values may not play a relevant role with respect to maximality, for instance, when analyzing maximality with respect to CPL (recall e.g. Corollary <ref> or see Proposition <ref> in next section).

As observed above,  Theorem <ref> cannot be applied to  logics which do not have enough expressive power, as seen in Examples <ref>(5) for Gödel's logics G_n (with n ≥ 4). This is not the case for finite-valued Łukasiewicz logics, as it will be shown in  the next section.




§ MAXIMALITY BETWEEN FINITE-VALUED ŁUKASIEWICZ LOGICS INDUCED BY ORDER FILTERS



In the rest of the paper we will deal with matrix logics based on the family of finite-valued Łukasiewicz logics Ł_n with n ≥ 2.
The (n+1)-valued Łukasiewicz logic can be semantically defined as the matrix logic

    Ł_n+1=⟨_n+1, {1}⟩,

where _n+1 = (_n+1, , →) with _n+1 = {0,1/n,…,n-1/n,1}, and the operations are defined as follows: for every x,y ∈_n+1,


   x =1-x (Łukasiewicz negation)

   x → y = min{1, 1-x+y} (Łukasiewicz implication)


The following operations can be defined in every algebra _n+1:



   x ⊗ y=(x → y)=max{0, x+y-1} (strong conjunction)

   x ⊕ y= x → y=min{1, x+y} (strong disjunction)

   x ∨ y=(x →  y) → y=max{x,y} (lattice disjunction)

   x ∧ y=(( x → y) → y)=min{x,y} (lattice conjunction)



Observe that Ł_2 is the usual presentation of  classical propositional logic CPL  as a matrix logic over the two-element Boolean algebra B_2 with domain {0,1} with signature {,→}.


The logics Ł_n can also be presented as Hilbert calculi that are axiomatic extensions of the infinite-valued Łukasiewicz logic Ł_∞.  Recall that Ł_∞ is algebraizable and the class MV of all MV-algebras is its equivalent quasivariety semantics <cit.>. Since algebraizability is preserved by finitary extensions then every finite valued Łukasiewicz logic Ł_n is also algebraizable, and we will denote by MV_n its corresponding subvariety of algebras.

In this section,  finite-valued Łukasiewicz logics with a set of designated values possibly different to { 1} will be studied from the point of view of maximality.  First, some notation will be introduced.

For every i≥ 1 and for every x ∈_n+1, i x will stand for x⊕…⊕ x (i-times), while x^i will stand for x⊗…⊗  x (i-times).

For 1 ≤ i ≤ n let

    F_i/n ={x ∈_n+1 :   x ≥ i/n}={i/n,…,n-1/n,1}

be the order filter generated by i/n, and let

    𝖫^i_n=⟨_n+1, F_i/n⟩

be the corresponding matrix logic.
From now on,  the consequence relation of 𝖫^i_n is denoted by _𝖫^i_n.
Observe that Ł_n+1= 𝖫^n_n for every n. In particular, CPL is 𝖫^1_1 (that is, Ł_2). If  1 ≤ i, m ≤ n, we can also consider the following matrix logic:

    𝖫^i/n_m=⟨_m+1, F_i/n∩_m+1⟩.

Since F_i/n∩_m+1 = F_j/m for some  1≤ j≤ m, 𝖫^i/n_m=𝖫^j_m for that j. It is interesting to notice that some of these logics are paraconsistent, and some are not. Indeed, it is easy to prove the following characterization.


  The logic 𝖫^i_n is paraconsistent w.r.t.  iff i/n ≤ 1/2.


𝖫^i_n is paraconsistent w.r.t.  iff there exists x ∈_n+1 such that x ≥ i/n and x ≥ i/n, iff i/n ≤ x ≤ (n-i)/n for some  x ∈_n+1, iff  i/n ≤  (n-i)/n, iff 2i ≤ n.


Thus, for instance, for n=5  it follows that 𝖫_5^1 and 𝖫_5^2 are paraconsistent, while 𝖫_5^3, 𝖫_5^4 and 𝖫_5^5=Ł_6 are  explosive. By its turn, if  n=3 then 𝖫_3^1  is paraconsistent, while 𝖫_3^2 and 𝖫_3^3=Ł_4 are  explosive. The paraconsistent logics of this form  which are maximal w.r.t. CPL  will be analyzed with more detail in Section <ref>.



Theorem <ref> can be  used in order to analyze the maximality of  the logic 𝖫^i_n w.r.t. 𝖫^i/n_m whenever m | n (taking into account that _m+1 is a subalgebra of _n+1 iff m|n). In particular, the maximality of  certain instances of 𝖫^i_n w.r.t. CPL can be obtained by using Theorem <ref>.


The following examples  deal with the algebras _n which, as observed above, can define a meet operator ∧ such that, for any order filter F, (a ∧ b) ∈ F iff a,b ∈ F. Because of this, a recovery operator ∘(p) will be considered instead of a recovery set ◯(p), consisting of the conjunction of all of its members.



 Let us first consider the case of _4.
For 1 ≤ i ≤ 3 let 𝖫^i_3=⟨_4,F_i/3⟩. Then F_1/3={1/3, 2/3,1}, F_2/3={2/3,1} and  F_3/3=F_1={1}.  As in the previous example, it can be proved that  each 𝖫^i_3 satisfies the requirements of Theorem <ref> w.r.t. CPL and so each 𝖫^i_3 is maximal w.r.t. CPL, presented as CPL=⟨ B_2,{1}⟩. Indeed, B_2 is a subalgebra of _4 and ⊤(p)=(p → p) and (p)= (p → p) are as required.   Finally, the formulas α^1_2(p)=α^2_1(p)= p are such that e(α^1_2(p))=2/3 if e(p)=1/3, e(α^2_1(p))=1/3 if e(p)=2/3.  (Observe that there are in _4 just two `non-classical' values: a_1=1/3 and a_2=2/3.)


Fix 1 ≤ i ≤ 3. Thus, given a theorem φ(p_1,…,p_m) of CPL which is not valid in 𝖫^i_3, consider the formula γ(p_1,p_2) as in the proof of Theorem <ref>. Then, the formula ∘(p)=γ(p, p) ∧γ( p,p) defines an operator (in terms of a conjunction of instances of φ) which allows to recover classical logic inside 𝖫^i_3. ▪




From Komori's characterization of axiomatic extensions of (infinite-valued) Łukasiewicz logic Ł_∞ <cit.>, it directly follows that the logic Ł_n+1 is maximal w.r.t. CPL iff n is a prime number. By adapting our previous arguments, we can obtain the following extension of  this classical result for logics matrix logics over _n+1 with (almost) arbitrary filters.



  Let  n≥ 2 and ∅≠ F ⊆_n+1. Then, the logic L=⟨_n+1,F⟩ is maximal w.r.t. CPL provided that 0 ∉ F and n is a prime number.


Observe that, as a direct consequence, all the logics 𝖫^i_q with q prime are maximal w.r.t. classical logic.

  Let  q be a prime number, and 1 ≤ i ≤ q. Then, the logic 𝖫^i_q is maximal w.r.t. CPL.



 
Note that, for a given prime q, if i < j the set of theorems of 𝖫^j_q is strictly included in the set of theorems of 𝖫^i_q. However this does not contradict the fact that both logics are maximal w.r.t. CPL, since their consequence relations are in fact incomparable.  For example, the set of theorems of 𝖫^2_3 is included in the set of theorems of 𝖫^1_3, but the inclusion is strict: _𝖫^1_3 (p ∨ p)⊗ (p ∨ p) while _𝖫^2_3 (p ∨ p)⊗ (p ∨ p). It suffices to consider an evaluation e such that e(p) = 1/3; then e((p ∨ p)⊗ (p ∨ p)) = 1/3 ≱2/3. On the other hand, 𝖫^2_3 is not a sublogic of 𝖫^1_3: p _𝖫^2_3 (p ⊗ p) ⊕ (p ⊗ p) but p _𝖫^1_3 (p ⊗ p) ⊕ (p ⊗ p). In order to see this, consider an evaluation e such that e(p) = 1/3; then e((p ⊗ p) ⊕ (p ⊗ p)) = 0.





Next examples exploit the fact that Ł_n+1  is a sublogic of Ł_m+1 iff m divides n, considering additional filters as designated values, and obtaining maximality in some cases.



 Now, the logics asociated to the algebra _5 will be analyzed.
For 1 ≤ i ≤ 4 let
𝖫_4^i=⟨_5,F_i/4⟩ such that F_1/4={1/4,1/2,3/4,1},  F_2/4=F_1/2={1/2,3/4,1}, F_3/4={3/4,1},  and F_4/4=F_1={1}. Since 2 divides 4 then _3 is a subalgebra of _5 and Ł_5 is a sublogic of Ł_3. We will prove that, indeed, any 𝖫_4^i (for 1 ≤ i ≤ 4) is maximal w.r.t. 𝖫_2^i/4=⟨_3,F_i/4∩_3⟩, by using Theorem <ref>.

By Lemma <ref>, each 𝖫_4^i is a sublogic of  𝖫_2^i/4. _3 is a subalgebra of  _5 and ⊤(p)=(p → p) and (p)= (p → p) are as required.  Let a_1=1/2, a_2=1/4 and a_3=3/4, and consider the formulas α^2_1(p)= p ⊕ p, α^2_3(p)=α^3_2(p)= p, and  α^3_1(p)=p ⊗ p.  Finally, let α^i_i(p)= p for i=2,3. Then, the formulas α^i_j defined above are such that e(α^i_j(p))=a_j if e(p)=a_i, for i=2,3 and j=1,2,3.

Fix 1 ≤ i ≤ 4. Thus, given a theorem φ_i(p_1,…,p_m_i) of 𝖫_2^i/4 which is not valid in 𝖫_4^i, consider the formula γ_i(p_1,p_2,p_3) as in the proof of Theorem <ref>. Then, the formula

    ∘_i(p)=γ_i(p⊕ p,p,  p) ∧γ_i(p⊗ p, p,p)

defines a recovery operator (in terms of a conjunction of instances of φ_i) which allows to recover 𝖫_2^i/4 inside 𝖫_4^i. This shows that the latter is maximal w.r.t. the former.   ▪





Consider  now the case of _7. Since 2 and 3 divide 6, it follows that _3 and _4 are subalgebras of _7 and so L=⟨_7,F⟩ is a sublogic of both ⟨_3,F∩_3 ⟩ and ⟨_4,F∩_4 ⟩ for any non-trivial filter F of _7. However, it is not possible to prove the maximality of L by applying Theorem <ref> since, for every formula α(p) and every evaluation e in _7, e(α(p))≠ 1/2 if e(p) ∈{1/3,2/3} (since _4 is a subalgebra), while  e(α(p))∉{1/3,2/3} if e(p)=  1/2 (since _3 is a subalgebra).   ▪


As another example of application of Theorem <ref>, we can obtain the following maximality condition of a logic 𝖫^i_n with respect to a logic L_m^i/n.

 Let 1 ≤ i,m ≤ n. Then 𝖫^i_n=⟨_n+1,F_i/n⟩ is maximal w.r.t.  𝖫_m^i/n=⟨_m+1, F_i/n∩_m+1⟩ if the following condition
 holds:  there is some prime number q and k ≥ 1 such that n=q^k, and  m=q^k-1.



We recall that  _n+1 is singly generated by any element 0<l/n<1 such that l and n are mutually prime <cit.>. Then,   since q is prime, _q^k+1∖_q^k-1+1={0<r/q^k<1   :  r  q } and therefore all conditions of Theorem <ref> are satisfied.





§ ON STRONG MAXIMALITY AND EXPLOSION RULES IN THE LOGICS 𝖫^I_Q
 

Along this section q will denote a prime number.


In the previous section we have seen that  all the logics of the form 𝖫^i_q=⟨_q+1, F_i/q⟩ are maximal w.r.t. CPL.
However, there are maximal logics that  are not maximal w.r.t. CPL in  an stronger sense, as firstly considered in <cit.> in the context of paraconsistent logics, or in <cit.> in a more general context of belief revision techniques for change of logics.




Let L_1  and L_2 two standard propositional logics defined over the same signature Θ such that L_1 is a proper sublogic of L_2, i.e.  such that ⊢_L_1⊊⊢_L_2. Then, L_1 is said to be strongly maximal w.r.t. L_2 if, for every finitary rule φ_1, … , φ_n/ ψ  over Θ, if φ_1, … , φ_n⊢_L_2ψ but φ_1, … , φ_n⊬_L_1ψ, then the logic L_1^*  obtained from  L_1   by adding φ_1, … , φ_n/ ψ as structural rule, coincides with L_2.



By L_1^*  above we mean the logic whose consequence relation ⊢_L_1^*  is the minimal extension of ⊢_L_1 such that
 σ(φ_1), … , σ(φ_n) ⊢_L_1^*σ(ψ) for any substitution σ over  Θ (see e.g. <cit.>).


For instance, as observed in <cit.>, the logic ℬ𝒟^∼ introduced in Section <ref>, that is maximal w.r.t. CPL, it is not strongly maximal relative to CPL.
Thus, a natural question is whether a given logic is strongly maximal w.r.t. another logic. In particular, in this section, we are interested in studying the status of the logics 𝖫^i_q=⟨_q+1, F_i/q⟩ with q prime in relation to the notion of strong maximality w.r.t. CPL. We will show that the answer is negative, as each of them admits a proper extension by a finitary rule related to the explosion law w.r.t. Łukasiewicz negation. In fact, in Section <ref>  it will be shown that such proper extensions are strongly maximal w.r.t. CPL.



 
By using the techniques presented in <cit.>, a sound and complete Hilbert calculus for each 𝖫^i_q (where i< q) can be defined from the one for Ł_q+1^≤ (the degree-preserving counterpart of Ł_q+1) by adding additional inference rules. The negative feature of such approach is that these Hilbert calculi have “global” inference rules, that is, inference rules such that one of its permises need to be a theorem of Ł_q+1.
By a general result by Blok and Pigozzi (see Theorem 4.3 in <cit.>) and from Theorem <ref> in Section <ref> below, a standard Hilbert calculus for 𝖫^i_q (for i< q) can be obtained from the usual one for 𝖫^q_q=Ł_q+1 by means of translations. That is, such calculi have no “global” inference rules. The negative side of this approach is that the resulting axiomatization is obtained by translating connectives from the other logic, and so the resulting calculus can appear as very artificial.
As an alternative, it seems that a direct method for defining a sound and complete “more natural” Hilbert calculus for each 𝖫^i_q over a suitable signature can also be  obtained by means of a `separation' technique for the truth-values, similar to the one used in Subection <ref> to define an alternative axiomatization for L^1_3. To verify this conjecture is left as an open problem.
Anyway, from now on it will be assumed the existence of a standard Hilbert calculus  H_q^i which is sound and complete for the logic 𝖫^i_q, where i< q.  Of course H_q^q will stand for the usual axiomatization of Ł_q+1.




According to the notation introduced at the beginning of Section <ref>, iα is an abbreviation for the formula α⊕…⊕α (i-times), and  the consequence relation of 𝖫^i_n is denoted by _𝖫^i_n. Recall the following basic property of _n+1.

 
For every 1 ≤ i ≤ n and  x ∈_n+1: ix <  i/n iff x=0. Thus, e(i α)< i/n iff e(α)=0 for every evaluation e in  _n+1 and every formula α.


From now on,  will denote any formula of the form (p → p), for a propositional variable p. Observe that e()=0 for every evaluation in _n+1, every n ≥ 1 and every propositional variable p. This is why the choice of p is inessential for  a concrete construction of .

Consider, for 1 ≤ i ≤ q, the i-explosion law

    (exp_i)  i(φφ)/ .

It is not hard to prove that this rule is not derivable in  any H_q^i, the sound and complete Hilbert calculus given for the  logic 𝖫^i_q (see Remark <ref>).


 
For every 1 ≤ i ≤ q, the rule (exp_i) is not derivable in H_q^i.


We first observe that  if  p, p' are two different  propositional variables, then i(p ∧ p) _𝖫^i_n p' for 1 ≤ i ≤ n. Indeed, let e be an evaluation in  _n+1 such that e(p)∉{0,1} and e(p')=0. Since  e(p ∧ p)≠ 0 then  e(i (p ∧ p))≥ i/n, by Lemma <ref>. Hence, i(p ∧ p) _𝖫^i_n p'. Finally, the corollary then follows  from soundness and completeness of H_q^i w.r.t. 𝖫^i_q.


However, the i-explosion rule is clearly admissible in H^i_q since it is a passive rule, that is: for no instance of the (exp_i) rule, the premisse can be a theorem of H^i_q. Indeed, for any classical evaluation over {0,1} it is the case that e(φ) ∈{0,1} for every formula φ and so e(i (φ∧φ)) < i/n, by Lemma <ref>. This leads us to consider the following definition.


 
 H^i_q is  the Hilbert calculus obtained from H^i_q by adding the i-explosion rule (exp_i).  We will denote by ⊢_ H^i_q and ⊢_ H^i_q the notions of proof associated to the Hilbert calculi H^i_q and  H^i_q, respectively.


The following is a characterization of ⊢_ H^i_q in terms of ⊢_ H^i_q.

 
Let Γ∪{φ} be a set of formulas. Then Γ⊢_ H^i_qφ iff either Γ⊢_ H^i_qφ, or  Γ⊢_ H^i_q i (ψ∧ψ) for some formula ψ.


`Only if' part: Suppose that Γ⊢_ H^i_qφ such that Γ⊬_ H^i_qφ. Then, any derivation in  H^i_q of φ from Γ must use the rule (exp_i). Let φ_1 …φ_n be a derivation  in  H^i_q of φ from Γ. Thus, there exists 1 ≤ m < n such that φ_m=i (ψ∧ψ)  for some formula ψ,  allowing so the first application of (exp_i) in the given derivation. This means that  Γ⊢_ H^i_q i (ψ∧ψ), since it was assumed that (exp_i) was not applied before φ_m in the given derivation.

`If' part: Suppose that   Γ⊢_ H^i_qφ. Then, clearly Γ⊢_ H^i_qφ.
Now, suppose that
Γ⊢_ H^i_q i (ψ∧ψ) for some formula ψ. Then Γ⊢_ H^i_q, by using (exp_i). But _𝖫^i_qφ and so ⊢_ H^i_qφ, by completeness of H^i_q w.r.t. 𝖫^i_q. This means that Γ⊢_ H^i_qφ.



The following question is how to characterize semantically the logic H^i_q with respect to  𝖫^i_q, the original sematics for  H^i_q. The answer  will be obtained in the next section by algebraic arguments (Theorem <ref> and Remark <ref>). Indeed, it will be shown there that H^i_q is sound and complete w.r.t. 𝖫̅^i_q where, for every i and n with 1 ≤ i ≤ n,

    𝖫̅^i_n=⟨_n+1×_2, F_i/n×{1}⟩

such that _2 is the  two-element Boolean algebra   B_2 with domain {0,1}.




§ TRANSLATIONS, EQUIVALENT LOGICS AND STRONG MAXIMALITY
 



 §.§ Preliminaries


Blok and Pigozzi introduce the notion of equivalent deductive systems in <cit.> (see also <cit.>). Two propositional deductive systems S_1 and S_2 in the same language ℒ are equivalent iff there are two translations τ_1, τ_2 (finite subsets of ℒ-propositional formulas in one variable) such that:
 
 
  * Γ⊢_S_1φ iff τ_1(Γ)⊢_S_2τ_1(φ),
 
  * Δ⊢_S_2ψ iff τ_2(Δ)⊢_S_1τ_2(ψ),
 
  * φ⊣⊢_S_1τ_2(τ_1(φ)),
 
  * ψ⊣⊢_S_2τ_1(τ_2(ψ)).

From very general  results stated in <cit.> it follows that two equivalent logic systems   are indistinguishable from the point of view of algebra, provided that one of them is algebraizable. Indeed, in such case if one of the systems is algebraizable  then the other will be also algebraizable w.r.t. the same quasivariety. By applying this fact to the systems of the form 𝖫^i_n studied in the previous sections, several results on relative maximality between these systems and classical logic will be obtained in the next Subsection <ref>. Actually, these results will be generalized in Subsection <ref> to obtain relative maximality results among the systems 𝖫^i_n.   However, for the sake of self containment, we prefer to leave the results of Subsection <ref> with their simpler proofs as well.

In the rest of this subsection, we provide the necessary preliminaries that will be needed in the subsequent subsections.

We recall that Ł_∞ is algebraizable and the class MV of all MV-algebras is its equivalent quasivariety semantics <cit.>. Since algebraizability is preserved by finitary extensions then every finite valued Łukasiewicz logic is also algebraizable.

Now we can prove that the deductive systems 𝖫^i_n and 𝖫^j_n are in fact equivalent in the above sense. First, observe that, by the McNaughton  functional representation theorem <cit.>, for every n≥2 and every 1≤ m≤ n there is an MV-term λ_m,n(p) such that for every a∈ [0,1],

    λ_m,n(a)={[              0,     if a≤m-1/n;;       na-(m-1), if m-1/n<a<m/n;;              1,      if m/n≤ a. ].


   The restrictions of the λ_i,m and λ_n,n functions on LV_n+1 are the characteristic functions of the order filters F_i/n and F_1 respectively, i.e. for each a ∈ LV_n+1,

    λ_i,n(a)={[         0, if a < i/n;         1,  if a ≥i/n ].
                      λ_n,n(a)= a^n = {[       0, if a < 1;       1, if a = 1 ].





 
For every n≥ 2 and every 1≤ i, j≤ n, 𝖫^i_n and 𝖫^j_n are equivalent deductive systems.


It is enough to prove that for every 1≤ i≤ n-1, 𝖫^i_n is equivalent to 𝖫^n_n=Ł_n+1.
Let the translations τ and σ  be given by τ={λ_i,n(p)} and σ={λ_n,n(p)}. It is easy to check that for every set of formulas Γ∪{φ},

    Γ_𝖫^i_nφ{τ(ψ)  :  ψ∈Γ}_𝖫^n_nτ(φ)


    Γ_𝖫^n_nφ{σ(ψ)  :  ψ∈Γ}_𝖫^i_nσ(φ)


    φ_𝖫^i_nσ(τ(φ)) φ_𝖫^n_nτ(σ(φ)).

Thus, 𝖫^i_n and 𝖫^n_n=Ł_n+1 are equivalent deductive systems.


From the equivalence among 𝖫^i_n and Ł_n+1, we can obtain, by translating the axiomatization of the finite valued Łukasiewicz logic Ł_n+1,  a calculus sound and complete with respect 𝖫^i_n that we denote by H^i_n (see <cit.>).

Since Ł_∞ is algebraizable and the class MV of all MV-algebras is its equivalent quasivariety semantics, finitary extensions of Ł_∞ are in 1 to 1 correspondence  with quasivarieties of MV-algebras . Actually, there is a dual isomorphism from the lattice of all finitary extensions of Ł_∞ and the lattice of all quasivarieties of MV. Moreover, if we restrict this correspondence to varieties of MV we get the dual isomorphism from the lattice of all varieties of MV and the lattice of all axiomatic extensions of Ł_∞. Since Ł_n+1=𝖫^n_n is an axiomatic extension of Ł_∞,  Ł_n+1  is an algebraizable logic with the class MV_n = 𝒬(ŁV_n+1), the quasivariety generated by ŁV_n+1, as its equivalent variety semantics. It follows from the previous theorem and from <cit.> that 𝖫^i_n, for every 1≤ i≤ n, is also algebraizable with the same class of MV_n-algebras as its equivalent variety semantics. Thus, the  lattices of all finitary extensions of 𝖫^i_n are isomorphic, and in fact, dually isomorphic to the lattice of all subquasivarieties of MV_n, for all 0<i<n.

Therefore maximality conditions in the lattice of finitary (axiomatic) extensions  correspond to minimality conditions in the lattice of subquasivarieties (subvarieties). Thus, given two finitary extensions L_1 and L_2 of a given logic 𝖫^i_n, where K_L_1 and K_L_2 are its associated MV_n-quasivarieties, L_1 is strongly maximal with respect L_2 iff K_L_1 is a minimal subquasivariety of MV_n among those MV_n-quasivarieties properly containing K_L_2. Moreover, if L_1 and L_2 are axiomatic extensions of 𝖫^i_n, then K_L_1 and K_L_2 are indeed MV_n-varieties. In that case,  L_1 is  maximal with respect L_2 iff K_L_1 is a minimal subvariety of MV_n among those MV_n-varieties properly containing K_L_2.


All the axiomatic extensions of Ł_∞ are characterized by Komori in <cit.>, where it is shown that every axiomatic extension  is finitely axiomatizable and depends only on two finite sets of natural numbers I, J not both empty. Moreover, Panti proved in <cit.> that every axiomatic extension can be axiomatized relative to  Ł_∞ by a single axiom γ_I,J with a single propositional variable. For the case of finite valued Łukasiewicz logics, Komori's characterization depends on just a finite set of natural numbers in the following sense: given n>1, every axiomatic extension of Ł_n+1 is of the form

    ⋂_1≤ j≤ kŁ_m_j+1

for some natural number k where m_j|n for every 1≤ j≤ k. Moreover, from the equivalence of Theorem <ref>, it follows that every axiomatic extension of 𝖫^i_n
is of the form

    ⋂_1≤ j≤ k𝖫^i/n_m_j

for some natural number k where m_j|n for every 1≤ j≤ k,  and it is axiomatized by a single axiom γ^i/n_m_1,…,m_k which depends on one variable.
We denote by H^i/n_m_1,…,m_k the calculus obtained from H^i_n
by adding the axiom γ^i/n_m_1,…,m_k. Note that for every m≥ 1 such that m| n, the calculus  H^i/n_m is the same logic as H^j_m, where j is the natural number  such that F_j/m=F_i/n∩ŁV_m.



The lattice of all axiomatic extensions Ł_∞ is fully described also by Komori in <cit.>, thus from the equivalence of Theorem <ref>, we can obtain the following maximality conditions for all axiomatic extensions of L^i_n.



Let  0<i,m≤  n be natural numbers such that m| n. If L is an axiomatic extension of 𝖫^i_n,  then



  
  * L is maximal with respect to 𝖫^i/n_m iff L=𝖫^i/n_m∩𝖫^i/n_q^k+1 for some prime number q with q | n and a natural k ≥ 0 such that q^k| m and q^k+1 m.





Using the equivalence of Theorem <ref> we obtain that the lattice of axiomatic extensions of 𝖫^i_n is isomorphic to the lattice of axiomatic extensions of Ł_n+1. As mentioned above, every axiomatic extension of Ł_n+1 is characterized by a finite set {m_1, …, m_k} where all
of its elements are divisors of n. Given two such sets {m_1, …, m_k} and {n_1, …, n_s}, we define the following relation among finite subsets of divisors of n: {m_1, …, m_k}≼{n_1, …, n_s} iff for every 1≤ i≤ k there is 1≤ j≤ s such that m_i| n_j. This relation ≼ is the dual order of the lattice of axiomatic extensions of Ł_n+1 in the following sense: {m_1, …, m_k}≼{n_1, …, n_s}  iff ⋂_1≤ j≤ sŁ_n_j+1≤⋂_1≤ i≤ kŁ_m_i+1. Clearly,  {m}≼{m, q} and {m, q}⋠{m} if q is a prime number such that q| n and q  m; Similarly,   {m}≼{m, q^k+1} and {m, q^k+1}⋠{m} if q is a prime number such that q| n,  q^k| m and q^k+1 m. Moreover if {m}≼{m_1, …, m_k} and {m_1, …, m_k}⋠{m}, then there is m_i such that m| m_i.  If m≠ m_i then there is a prime number q such that mq | m_i| n. Thus   {m, q}≼{m_1,…, m_k} if q  m and {m, q^k+1}≼{m_1,…, m_k} if  q^k| m and q^k+1 m. If m= m_i, then  there is an m_j with 1<j<k such that m_j m. If there is a prime number q such that q| m_j| n such that q  m, then {m, q}≼{m_1,…, m_k}. Otherwise, there are a prime number q and a natural k>0 such that q^k+1| m_j| n, q^k| m and q^k+1 m, then {m, q^k+1}≼{m_1,…, m_k}. Duality and Theorem <ref> close the proof.


As a corollary we obtain that the suficient condition of Proposition <ref> is also necessary.


Let 1 ≤ i,m ≤ n. Then 𝖫^i_n=⟨_n+1,F_i/n⟩ is maximal w.r.t.  𝖫_m^i/n=⟨_m+1, F_i/n∩_m+1⟩ if and only if  there is some prime number q and k ≥ 1 such that n=q^k, and  m=q^k-1.





The task of fully describing the lattice of all  all finitary extensions of Ł_∞, isomorphic to the lattice of all subquasivarieties of MV,  turns to be an heroic task since the class of all MV-algebras is Q-universal (see <cit.>). For the finite valued case it is much simpler, since MV_n is a locally finite discriminator variety (cf. <cit.>). Any locally finite quasivariety is generated by its critical algebras (see <cit.>), where an algebra A is said to be critical iff it is a finite algebra not belonging to the quasivariety generated by all its proper subalgebras. A  description of all critical MV-algebras can be found in <cit.>.



<cit.>
  An MV-algebra A is critical if and only if A is isomorphic to a finite MV-algebra 𝐋𝐕_n_0+1×⋯×𝐋𝐕_n_l-1+1 satisfying the following conditions:

 
  * For every i,j<l, i≠ j implies n_i≠ n_j.
 
  * If there exists n_j, j<l such that n_i|n_j for some
  i≠ j, then n_j is unique.



Moreover the following result characterizes the inclusion among locally finite quasivarieties.

 <cit.> 

Let 𝔉 = { 𝐋𝐕_n_i1+1×⋯× 𝐋𝐕_n_il(i)+1 :  i∈ I} and
𝔊 = { 𝐋𝐕_m_j1+1×⋯× 𝐋𝐕_m_jl(j)+1 :  j∈ J} be two finite families of
critical MV-algebras. Then it holds that

    𝒬(𝔉) ⊆𝒬(𝔊)

if, and only if,
for every i∈ I there exists  a non-empty H ⊆ J such that:

 
  * For any 1≤ k≤ l(i) there are j∈ H and 1≤ r≤ l(j) such that
   n_ik|m_jr.
 
  * For any j∈ H and 1≤ r≤ l(j) there exists 1≤ k≤ l(i) such that
   n_ik|m_jr.






 §.§ Strong maximality among logics 𝖫^i_q, L̅^i_q, and classical logic





As a direct application of Lemma <ref>, we have the following particular case that will be used later.


 
Consider the  following two sets of one critical MV-algebra each: 

{ 𝐋𝐕_q+1× 𝐋𝐕_2} and
{ 𝐋𝐕_k+1}, where q is a prime number such that  q > 1. Then

    𝒬({ 𝐋𝐕_q+1× 𝐋𝐕_2}) ⊆𝒬( 𝐋𝐕_k+1)

if and only if  q | k.


  The two families of critical algebras above correspond in Lemma <ref> to take  I = {1} and J = {1}, with n_11 = q, n_12 = 1, m_11 = k. Then one can check that these values satisfy the two conditions of the lemma only in the case that q | k.


Now, for any k > 1, we are able to provide a full description of the minimal subquasivarieties of MV_k=𝒬(𝐋𝐕_k+1) strictly containing the variety of Boolean algebras.

   
Let k>1.
The set of all minimal subquasivarieties of MV_k=𝒬(𝐋𝐕_k+1) among those strictly containing the class of all the Boolean algebras B = 𝒬(𝐋𝐕_2) is 
    M^k={𝒬(𝐋𝐕_q+1×𝐋𝐕_2)  :  q > 1  q|k  }.




 By Lemma <ref> and the previous Corollary <ref>, every K∈ M^k is a subquasivariety of 𝒬(𝐋𝐕_k+1) strictly containing B. Moreover, for every K_1, K_2∈ M^k, if K_1≠ K_2 then K_1⊈K_2 and K_2⊈K_1.

On the other hand, let K be a minimal subquasivariety of 𝒬(𝐋𝐕_k+1) strictly containing B.
Since K≠ B, it must contain a critical algebra C that, by Theorem <ref>, it must be such that C≅ 𝐋𝐕_m_1+1×⋯× 𝐋𝐕_m_s+1, where   m_i| k for every 1 ≤ i ≤ s, and m_j > 1 for some 1≤ j≤ s.
Hence, for every prime number q such that q|m_j, and hence q | k, we have 𝐋𝐕_q+1×𝐋𝐕_2∈𝒬(C)⊆ K, and thus  𝒬(𝐋𝐕_q+1×𝐋𝐕_2) ⊆ K. Since we are assuming the minimality of K, it must be 𝒬(𝐋𝐕_q+1×𝐋𝐕_2) = K.





If q > 0 is a prime number, then 𝒬(𝐋𝐕_q+1×𝐋𝐕_2) is axiomatized by the MV quasi-identities plus:


  * γ_q(x)≈ 1 (the identity axiomatizing 𝒱(𝐋𝐕_q+1))

  * q(x¬ x)≈ 1 ⇒ y  y ≈ 1



It is easy to check that 𝐋𝐕_q+1×𝐋𝐕_2 satisfies these two quasi-identities.
Since the MV-identities and  γ_q(x)≈ 1 axiomatize 𝒱(𝐋𝐕_q+1), and 𝒱(𝐋𝐕_q+1) is a locally finite quasivariety, it is enough to prove that every critical MV-algebra C∈𝒱(𝐋𝐕_q+1) where the quasi-equation q(x¬ x)≈ 1 ⇒ y  y ≈ 1 holds, belongs to 𝒬(𝐋𝐕_q+1×𝐋𝐕_2).

Let C be a critical MV-algebra satisfying the axiomatization, then C is such that
C≅ 𝐋𝐕_m_1+1×⋯× 𝐋𝐕_m_k+1 satisfying conditions of Theorem <ref>. Moreover, every 1 ≤ i ≤  k, is such that either m_i = 1 or m_i = q because  𝐋𝐕_m_i+1 belongs to 𝒱(𝐋𝐕_q+1). If there is c∈ C such that q(c¬ c)=1 then, by the second quasi-equation of the above axiomatization,
b  b ≈ 1 for any b∈ C. Thus we have C∈ B⊆𝒬(𝐋𝐕_q+1×𝐋𝐕_2). Otherwise, recalling that either m_i = 1 or m_i = q for every i, if for every c∈ C one has q(c¬ c)≠ 1 then  m_i=1 for some 1≤ i≤ k. In that case, by the characterization of critical algebras (Theorem <ref>), we have C≅𝐋𝐕_2 or C≅𝐋𝐕_q+1×𝐋𝐕_2. If C≅𝐋𝐕_2, then trivially  C∈𝒬(𝐋𝐕_q+1×𝐋𝐕_2). If C≅𝐋𝐕_q+1×𝐋𝐕_2,
then clearly C ∈𝒬(𝐋𝐕_q+1×𝐋𝐕_2).

Above, note that the identity y  y ≈ 1 corresponds to the previously mentioned Panti's axiom γ_I, J(y), with I = {1} and J = ∅,  axiomatizing CPL as an axiomatic extension of Ł_n+1 for any n > 1.




Finally, we obtain the following characterization result about strong maximality of logics  L̅^j_q with respect to classical logic.


  
Let  q > 1 be a prime number. Then, for every j such that 0 < j ≤ q:

 
  * L̅^j_q is  strongly maximal with respect to CPL  and it is axiomatized by 
  H^j_q plus the rule  j(φ¬φ)/ (ψψ)^q. 

  
  * 𝖫^j_q is strongly maximal w.r.t. L̅^j_q.




 By using the equivalence of Theorem <ref> and the algebraizability of Ł_q+1, the lattice of subquasivarieties of 𝒱(𝐋𝐕_q+1) is dually order isomorphic to the lattice of all finitary extensions of Ł_q+1. Clearly CPL = Ł_2 is the finitary extension of L̅^j_q corresponding to the subvariety 𝒬(𝐋𝐕_2) of  𝒬(𝐋𝐕_q+1×𝐋𝐕_2), and
L̅^j_q
is the finitary extension of 𝖫^j_q corresponding to the subquasivariety  𝒬(𝐋𝐕_q+1×𝐋𝐕_2) of 𝒱(𝐋𝐕_q+1).

By Theorem <ref>, the only critical algebras of 𝒱(𝐋𝐕_q+1) are   𝐋𝐕_q+1, 𝐋𝐕_2 and 𝐋𝐕_2×𝐋𝐕_q+1 and, by   Lemma <ref>, all its  subquasivarieties are 𝒬(𝐋𝐕_2) ⊊𝒬(𝐋𝐕_2×𝐋𝐕_q+1) ⊊𝒬(𝐋𝐕_q+1). Therefore,  by Theorem <ref>, L̅^j_q
is strongly maximal with respect to CPL, while L^j_q
is strongly maximal with respect to L̅^j_q.

Finally, the axiomatization of  L̅^j_q follows from Theorem <ref> and the facts that j φ_𝖫^j_qq φ  holds for every formula φ and that the equation (q x)^q = q x is valid in the class MV_q.



From the above proof, it readily follows the next corollary.

 
 L̅^j_q is the unique strongly maximal logic w.r.t. CPL above L^j_q. In fact, L̅^j_q is the only logic between L^j_q and CPL.



 
It is worth noting that the rule j(φ¬φ)/ (ψψ)^q exactly corresponds to the explosion rule (exp_j) introduced in Section <ref>. Indeed,  the rule j(φ¬φ)/ (ψψ)^q  is clearly derivable from (exp_j). On the other hand, assuming j(φ¬φ), by this rule it follows that (ψψ)^q for every ψ. Hence the logic becomes CPL because the translation of the classical axiom ψψ is precisely (ψψ)^q, and thus  follows from j(φ¬φ).
This does not come as a surprise, since as we have proved above, 𝖫^j_q is strongly maximal w.r.t. L̅^j_q and so the latter is the only proper extension of 𝖫^j_q  (with a finitary rule) properly contained in CPL.


As a corollary of the previous remark, it follows the completeness of H^j_q.

  H^j_q is sound and complete w.r.t.  L̅^j_q.




 §.§ Strong maximality with respect to systems 𝖫^i_n



Next theorems are generalizations of Theorems <ref>, <ref> and <ref> respectively.

 
Let n>0 and k>1.
The set of all minimal subquasivarieties of MV_nk=𝒬(𝐋𝐕_nk+1) among those strictly containing 𝒬(𝐋𝐕_n+1) is 



M^nk_n =   {𝒬({𝐋𝐕_n+1,𝐋𝐕_q+1×𝐋𝐕_2})  :  q  q | k  q n }⋃ 

    {𝒬({𝐋𝐕_n+1, 𝐋𝐕_q^r+1+1×𝐋𝐕_2})  :  q  q|k,  q^r|n  q^r+1 n }. 





 By Lemma <ref>, every K∈ M^nk_n is a subquasivariety of 𝒬(𝐋𝐕_nk+1) strictly containing 𝒬(𝐋𝐕_n+1). Moreover, for every K_1, K_2∈ M^nk_n, if K_1≠ K_2 then K_1⊈K_2 and K_2⊈K_1.

Let K be a minimal subquasivariety of 𝒬(𝐋𝐕_nk+1) strictly containing 𝒬(𝐋𝐕_n+1). Trivially, 𝐋𝐕_n+1∈ K. Since K≠𝒬(𝐋𝐕_n+1), then it must contain a critical algebra C≅ 𝐋𝐕_m_1+1×⋯× 𝐋𝐕_m_s+1 such that  m_i|nk for every 1 ≤ i≤ s and m_j n for some 1≤ j≤ s. If there is a prime number q|m_j such that q n, then 𝐋𝐕_q+1×𝐋𝐕_2∈𝒬(C)⊆ K. Otherwise, there is a prime q such that  q|m_j  and q^r|n, and for some r≥ 1, q^r+1|̸ n and q^r+1|m_j, whence 𝐋𝐕_q^r+1+1×𝐋𝐕_2∈𝒬(C)⊆ K. Thus, in both cases K contains  some K_i∈ M^nk_n, from which it follows that K ∈ M^nk_n since we are assuming minimality of K.




For every  n>0.


  * If q is a prime number such that q  n, 
then 𝒬({𝐋𝐕_n+1,𝐋𝐕_q+1×𝐋𝐕_2}) is axiomatized by the MV identities plus


  * γ_{n, q},∅(x)≈ 1 𝒱({𝐋𝐕_n+1,𝐋𝐕_q+1}))

  * nq(x¬ x)≈ 1 ⇒γ_{n},∅(y)≈ 1.

 
  * If q is a prime number such that q^r| n and q^r+1 n, 
 𝒬({𝐋𝐕_n+1, 𝐋𝐕_q^r+1+1×𝐋𝐕_2}) is axiomatized by the MV identities plus
 
 
  * γ_{n, q^r+1},∅(x)≈ 1𝒱({𝐋𝐕_n+1,𝐋𝐕_q^r+1+1})  )
 
  * nq(x¬ x)≈ 1 ⇒γ_{n},∅(y)≈ 1.
 



 We prove the first item, the other is proved in a analogous way.
It is easy to check that 𝐋𝐕_n+1 and 𝐋𝐕_q+1×𝐋𝐕_2 satisfy all the quasi-identities.
Since the MV-identities with  γ_{n, q},∅(x)≈ 1 axiomatize 𝒱({𝐋𝐕_n+1,𝐋𝐕_q+1}) and 𝒱({𝐋𝐕_n+1,𝐋𝐕_q+1}) is a locally finite quasivariety, it is enough to prove that every critical MV-algebra C∈𝒱({𝐋𝐕_n+1,𝐋𝐕_q+1}) where the quasiequation nq(x¬ x)≈ 1 ⇒γ_{n},∅(y)≈ 1 holds, belongs to 𝒬({𝐋𝐕_n+1,𝐋𝐕_q+1×𝐋𝐕_2}). Therefore, let C be a critical MV-algebra satisfying the axiomatization. Then, C is such that
C≅ 𝐋𝐕_m_1+1×⋯× 𝐋𝐕_m_r+1 satisfying conditions of Theorem <ref>, and moreover for every 1 ≤ i ≤ k,  either m_i|n or m_i = q because  C ∈𝒱({𝐋𝐕_n+1,𝐋𝐕_q+1}). If there is c∈ C such that nq(c¬ c)=1 then, by the second quasi-equation of the axiomatization above,
γ_{n},∅(b)≈ 1 for any b∈ C, thus C∈𝒱({𝐋𝐕_n+1})=𝒬({𝐋𝐕_n+1})⊆𝒬({𝐋𝐕_n+1,𝐋𝐕_q+1×𝐋𝐕_2}). If for every c∈ C, nq(c¬ c)≠ 1 then  m_i=1 for some 1≤ i≤ k. In that case, by the characterization of critical algebras (Theorem <ref>), either C≅𝐋𝐕_2 or C≅𝐋𝐕_m+1×𝐋𝐕_2. If C≅𝐋𝐕_2, then trivially  C∈𝒬({𝐋𝐕_n+1,𝐋𝐕_q+1×𝐋𝐕_2}). Otherwise, if C≅𝐋𝐕_m+1×𝐋𝐕_2, since C∈𝒱({𝐋𝐕_n+1,𝐋𝐕_q+1}), either m|n or m=q. If m|n then C∈𝒱({𝐋𝐕_n+1})=𝒬({𝐋𝐕_n+1})⊆𝒬({𝐋𝐕_n+1,𝐋𝐕_q+1×𝐋𝐕_2}). If m=q then C≅𝐋𝐕_q+1×𝐋𝐕_2∈𝒬({𝐋𝐕_n+1,𝐋𝐕_q+1×𝐋𝐕_2}).


If 1≤ i,m≤ n, by analogy with 𝖫^i/n_m, we define the matrix logic 
    L̅^i/n_m=⟨_m+1×_2, (F_i/n∩_m+1) ×{1}⟩.

Then we have the following generalization of Theorem <ref>.


Let  0<i≤ n be natural numbers  and let q be a prime number. Then we have:

 
  * If
 q  n then, for every j such that (i-1)q<j≤ iq, 𝖫^i_n∩L̅^j/nq_q is  strongly maximal with respect to 𝖫^i_n,  and it is axiomatized by H^j/nq_n, q plus the rule j(φ¬φ)/γ^j/nq_n(ψ).

  
  * If q^r| n and q^r+1 n  then, for every j such that (i-1)q<j≤ iq, 𝖫^i_n∩L̅^j/nq_q^r+1 is  strongly maximal with respect  to 𝖫^i_n,  and it is axiomatized by H^j/nq_n, q^r+1 plus the rule  j(φ¬φ)/γ^j/nq_n(ψ).


Recall that  in the above rules γ^j/nq_n(ψ) refers to the axiom in one variable that axiomatizes  𝖫^j/nq_n relative to 𝖫^j_nq.
Moreover, every finitary  extension of some 𝖫^j_k is strongly maximal with respect 𝖫^i_n iff it is of one of the two preceeding types.



Notice that 𝖫^i_n=𝖫^j/nq_n for  every j such that (i-1)q<j≤ iq.  Thus,  𝖫^i_n is an extension of 𝖫^j_nq. Now, by using the equivalence of Theorem <ref> and the algebraizability of Ł_nq+1, the lattice of subquasivarieties of 𝒱(𝐋𝐕_nq+1) is dually order isomorphic to the lattice of all the finitary extensions of 𝖫^j_nq. Moreover, 𝖫^i_n∩L̅^j/nq_q  and  𝖫^i_n∩L̅^j/nq_q^r+1 are the finitary extensions of 𝖫^j_nq associated to 𝒬({𝐋𝐕_n+1,𝐋𝐕_q+1×𝐋𝐕_2}) and 𝒬({𝐋𝐕_n+1, 𝐋𝐕_q^r+1+1×𝐋𝐕_2}), respectively.  Hence, they are strongly maximal with respect to 𝖫^i_n, by Theorem <ref>.  The axiomatization follows from Theorem <ref> and the facts  that j φ_𝖫^j_nqnq φ

holds for every formula φ and that the equation (nq x)^nq = nq x is valid in the class MV_nq.

Finally, the last statement of this theorem follows from Theorem <ref> and Theorem <ref>.













§ AN APPLICATION TO IDEAL PARACONSISTENT LOGICS
  



As mentioned in Example <ref>, Arieli et al. 
have introduced in  <cit.>  the concept of ideal paraconsistent logics. We recall here this notion.


 
Let L be a propositional logic defined over a signature Θ (with consecuence relation ⊢_L) containing at least a unary connective  and a binary connective → such that:


  (i) L is paraconsistent w.r.t.  (or simply -paraconsistent), that is,  there are formulas φ,ψ∈ℒ(Θ) such that φ, φ⊬_Lψ;

  (ii) → is an implication for which the deduction-detachment theorem holds in L, that is, Γ∪{φ}⊢_L ψ iff  Γ⊢_L φ→ψ, for every set for formulas Γ∪{φ, ψ}⊆ℒ(Θ).


  (ii) There is a presentation of CPL as a matrix logic  L'=⟨𝐀, {1}⟩  over the signature Θ such that the domain of 𝐀 is {0,1}, and  and → are interpreted as the usual 2-valued negation and implication of CPL, respectively.


  (iv) L is a sublogic of CPL in the sense that ⊢_L ⊆ ⊢_L', that is, Γ⊢_L φ implies  Γ⊢_L'φ,  for every set for formulas Γ∪{φ}⊆ℒ(Θ).

Then, L is said to be an ideal paraconsistent logic if it is maximal w.r.t. L', and every proper extension of L over Θ is not -paraconsistent.


An implication connective satisfying the above condition (ii) will be called deductive implication in the rest of the paper.[Such an implication is called deductive in <cit.> and proper in <cit.>. ]


Thus, a -paraconsistent logic L with a deductive implication is ideal if it is maximal w.r.t. CPL (presented over the signature Θ of L) and, if L” is another logic over Θ properly containing L, with Γ∪{φ}⊆ℒ(Θ) such that Γ⊢_L”φ but  Γ⊬_L φ, then the logic obtained from L by adding Γ / φ as an inference rule is not -paraconsistent.

As already noticed, the logics L_i^n with i/n ≤ 1/2 are paraconsistent. In this section, using the results of the previous sections, we study the status of the logics L^i_n in relation to ideal paraconsistency. Namely,
in the following subsection, we will show that the logics of the form L_q^i, where q is prime and i/q ≤ 1/2 are ideal paraconsistent,

while in subsection <ref> the special case of  L_3^1, renamed as J_4, is analyzed in more detail.





 §.§ The ideal paraconsistent logics L_q^i
 

By combining Proposition <ref> with  Corollary <ref> we know a logic 𝖫^i_q is -paracon­sis­tent and  maximal w.r.t. CPL, provided that q is prime and i/q ≤ 1/2. From now on we will assume this is the case when referring to a logic 𝖫^i_q.

Recall 
that
 H^i_q is  the Hilbert calculus obtained from the calculus H^i_q for  𝖫^i_q by adding the i-explosion rule (exp_i). Since φ∧φ⊢_ H^i_q i(φ∧φ), the logic  H^i_q  is explosive. Then, taking into account Corollary <ref>,
 it follows that  every proper extension of 𝖫^i_q defined over its signature is either 𝖫̅^i_q or CPL, and hence not -paraconsistent.

In addition, by Lemma <ref>, we know there is a definable unary connective ∼^i_q such that, for every evaluation e,
e(∼^i_q p)=0 if e(p)  ≥ i/q, and  e(∼^i_q p)=1 otherwise, for every propositional variable p.[Namely, ∼^i_q p = λ_i,q(p).] This is a kind of “classical” negation defined on L_q^i. Using this negation, one can define in turn a new implication ⇒^i_q by stipulating φ⇒^i_q ψ=∼^i_q φψ. In fact, one can easily check that ⇒^i_q is a deductive implication on  L^i_q in the sense of Definition <ref> and that
over {0,1} it coincides with the classical implication.
All the above considerations lead to the following result.

 
Let  q is a prime number, and let 1 ≤ i < q such that i/q ≤ 1/2. Then,  𝖫^i_q is a (q+1)-valued ideal paraconsistent logic.[Strictly speaking, in this claim we implicitly assume that the signature of 𝖫^i_q has been changed by adding the definable implication ⇒^i_q as a primitive connective. ]


Therefore we have a large family of examples of ideal paraconsistent logics. In particular, for each prime q, all the logics in the set PC_q+1 = {𝖫^i_q  :   i < q/2 } are (q+1)-valued ideal paraconsistent logics. Moreover, if we consider “the more theorems a paraconsistent logic has, the more well-behaved is the logic” as a valid further criterion, then we can still refine the set PC_q+1. Indeed, if we denote by Th(L) the set of theorems of a logic L then, as noticed in Remark <ref>, we have the strict inclusions Th(𝖫^i_q) ⊊ Th(𝖫^j_q) ⊊ Th( CPL) whenever i > j. Therefore the logic J_q+1 = 𝖫^1_q appears to be the “best” ideal logic in the set PC_q+1,[We have chosen the name J_q+1 to denote the logic 𝖫^1_q inspired in the 3-valued case, where the ideal paraconsistent logic J_3 coincides with 𝖫^1_2.] since it is the logic in that set having the biggest set of theorems from classical logic.

Finally, it is worth mentioning that all the paraconsistent logics of the form 𝖫^i_n are, indeed, LFIs (recall Section <ref>):

  Suppose that i/n ≤ 1/2. Then, the logic 𝖫^i_n is an LFI w.r.t.  and where the consistency operator is defined as ∘α = ∼^i_n (α∧α).


Straightforward.










 §.§ The four-valued ideal paraconsistent logic J_4
 

As mentioned in Remark <ref>, we know from Theorem 4.3 in <cit.> that it is possible to obtain a standard (that is, without “global” inference rules) Hilbert calculus for a logic 𝖫^i_n for i< n from the usual one for Ł_n+1 by using translations. However, the calculi obtained in this manner can lack an intuitive meaning since they are defined in terms of the implication connective → of Ł_n+1, that is naturally associated to the filter F_1 ={1} but not
to the filter F_i/n = {i/n, …, 1}, which is the one at work in L^i_n.  Actually, the implication naturally associated to the filter F_i/n is  ⇒^i_n, which was considered above, for which modus ponens (MP) and the deduction-detachament theorem hold.

In this section we focus on the particular case of the (ideal paraconsistent) logic J_4 =  L^1_3. J_4 can be considered as a generalization to four values of the paraconsistent 3-valued logic J_3 introduced by da Costa and D'Ottaviano in <cit.> and briefly mentioned in Example <ref>.
For this logic a more natural signature Σ will be
considered for describing it axiomatically in terms
of a deductive implication connective (in the sense of Definition <ref> item (ii)) and a unary connective *  representing the square operation x ⊗ x, which can be seen as a kind of `truth stresser' (see e.g. <cit.>).
A soundness and completeness result  for this calculus proved by using a `separation' technique for truth-values will be presented. Note that dealing with logics J_q = 𝖫^1_q  for a prime q>3 appears to be much more complicated, and certainly it lies outside the scope of this paper.




The signature Σ that will be used in the rest of the section is given by two unary connectives ∗ (square) and  (negation), plus a binary connective  ∨ for disjunction. Abusing the notation, we formally define next J_4 over this signature, and we will show later that it is an equivalent presentation of L^1_3.



 
J_4 is the matrix  logic ⟨ A_4, F_1/3⟩ over  Σ, where the algebra is A_4 = (_4, , , *), with operations defined by the tables below:

    [   ∨   1 2/3 1/3   0;   1   1   1   1   1; 2/3   1 2/3 2/3 2/3; 1/3   1 2/3 1/3 1/3;   0   1 2/3 1/3   0;     ][           ∗;   1   0   1; 2/3 1/3 1/3; 1/3 2/3   0;   0   1   0;     ]



Observe that  is Łukasiewicz negation in _4, while ∗x=x ⊗ x (with ⊗ being Łukasiewicz strong conjunction) and ∨ is the lattice join in _4.

In this signature Σ the following derived connectives can be defined (as usual, the corresponding operators will be denoted using the same symbol): 



-     Δ(p) = ∗∗ p ; 

-      ∼p = Δ(  p) ; 

-      p ⇒ r = ∼p ∨ r ; 

-      p ⇔ r = (p ⇒ r) ∧ (r ⇒ p) ;  

-      p ∧ r = ( p ∨ r) ; 

-      ∇(p)= ∼p; 

-      α_1/3(p)=∇(p) ∧∼∗ p; 

-      β_1/3(p)=α_1/3(p) ∧∗ p.
 


 

It is easy to see that Δ is Monteiro-Baaz Delta-operator) and ∼ is Gödel negation (∼x=1 if x=0, and 0 otherwise). Note that ∼ actually coincides with ∼^1_3, and thus ⇒ is nothing but ⇒^1_3. Furthermore, ∇(x)=0 if x=0, and 1 otherwise; α_1/3(x)=1 and β_1/3(x)=1/3 if x=1/3, and 0 otherwise.

It is worth to remark that Łukasiewicz implication is definable from these operators in the following way:  
    p → r = ((∇( p) ∨ r) ∧ ( p ∨∇(r)) ∧β_1/3(r) )
     ∨ ((∼p ∧α_1/3(r)) ∨ (α_1/3(p) ∧α_1/3(r))).

Then, the following result follows easily:

 
The algebras _4 and A_4 are functionally equivalent.


This means that the proposed operators over Σ constitute an alternative presentation of the algebra _4 underlying Ł_4. Next we define  an axiomatic system for J_4.


   The Hilbert  calculus  H_4  for the logic J_4, defined over the signature Σ, is given as follows:

  Axiom schemas: those of CPL over the signature {∨, ⇒, ∼} plus
  












  (Ax1)    ∼α⇒α 


  (Ax2)    α∨α 


  (Ax3)   α⇔α 


  (Ax4)    (α∨β) ⇒α 


  (Ax5)    (α∨β) ⇒β 


  (Ax6)    α⇒ (β⇒(α∨β)) 


  (Ax7)    ∗α⇒α 


  (Ax8)    ∗(α∨α) 


  (Ax9)    ∗α⇒∼∗α 


  (Ax10)    ∗∗α⇔∼α 


  (Ax11)    ∗α⇔α 


  (Ax12)    ∗(α∨β) ⇔ (∗α∨∗β)


Inference rule:
  

  (MP) α    α⇒β/β



Observe that, since (MP) is the only inference rule, H_4 satisfies the deduction-detachment theorem w.r.t. the implication ⇒: Γ∪{α}⊢_ H_4β iff Γ⊢_ H_4α⇒β, for every set of formulas Γ∪{α,β}. On the other hand, it can be proved that *(α⇒β) ⇒ (*α⇒ *β) is derivable in H_4, which gives additional support to consider * as a truth stresser.

Soundness of H_4 can be proved straightforwardly.


 The calculus H_4 is sound w.r.t. J_4, that is: Γ⊢_ H_4φ implies that Γ_ J_4φ, for every finite set of formulas Γ∪{φ}.


In order to prove completeness, since H_4 is a finitary Tarskian logic, one can use the technique of maximal consistent sets of formulas. Indeed, for any set of formulas Γ∪{φ}, if Γ⊬_ H_4φ then, by Lindenbaum-Łos theorem, Γ can be extended to a maximal set  Λ such that Λ⊬_ H_4φ. We will call the set Λ maximal φ  in  H_4.

Maximal sets w.r.t. a formula enjoy remarkable properties which directly follow from the axioms and rules of H_4.



Let Λ be a maximal set φ  in  H_4. Then, Λ is closed, i.e. for every formula ψ, Λ⊢ψ iff ψ∈Λ. Moreover, for any formulas α and β the following conditions hold: 



(1)    α∨β∈Λ iff α∈Λ or β∈Λ;

(2)    α∉Λ iff ∼α∈Λ;

(3)     α⇒β∈Λ iff α∉Λ or β∈Λ;

(4)    α∉Λ implies α∈Λ;

(5)     α∈Λ iff α∈Λ;

(6)     ∼α∈Λ implies α∈Λ;

(7)     (α∨β) ∈Λ iff α∈Λ and β∈Λ;

(8)     ∗α∈Λ implies α∈Λ;

(9)     ∗(α∨β) ∈Λ iff ∗α∈Λ or ∗β∈Λ;

(10)     ∗∗α∈Λ iff α∉Λ;

(11)     ∗α∈Λ iff α∈Λ;

(12)     ∗α∉Λ iff ∗α∈Λ.




Next we prove a Truth Lemma for H_4.

  Let Λ be a maximal set of formulas φ  in  H_4. Consider the following evaluation e_Λ of propositional variables for J_4:

    (T) 
    e_Λ(γ) = {[                 1         γ∈Λ,  γ∉Λ;               2/3 γ∈Λ,   γ∈Λ,  ∗γ∈Λ;               1/3 γ∈Λ,   γ∈Λ,  ∗γ∉Λ;                 0              γ∉Λ. ].
Then,  (T) holds for every complex formula γ.


The proof is done by induction on the complexity of the formula γ. If γ is atomic then (T) holds by hypothesis.

Now, suppose (T) holds for every formula with complexity ≤ n (induction hypothesis – IH) and let γ be a formula with complexity n.
In order to prove (T) from (IH) by analyzing all the possible cases (namely, γ = α or γ = ∗α or  γ = α∨β), each item of Proposition <ref> should be used.[Observe that it is enough to prove the `only if' part of (T), since the four conditions on the right-hand side are pairwise incompatible, and e(γ) can only take one of the values 0, 1, 1/3, 2/3. Thus, if, for instance, the first condition on the right-hand side of (T) holds  for a  given formula γ then the other 3 conditions are false and so e_Λ(γ) ∉{1/3,1,0}, by the `only if' part of (T). Hence,  e_Λ(γ) must be 2/3. This shows that the `if' part of (T) follows from the `only if' part.] The details are left to the reader.



  The calculus H_4 is complete w.r.t. J_4, that is: Γ_ J_4φ implies that Γ⊢_ H_4φ, for every finite set of formulas Γ∪{φ}.


Let Γ∪{φ} be a set of formulas in the language of J_4
such that Γ⊬_ H_4φ.
By Lindenbaum-Łos, there exists a set Λ  maximal φ in H_4
such that Γ⊆Λ.
Let e_Λ be the evaluation defined as in the Truth Lemma <ref>.
Then, it follows that e_Λ(γ) ∈ F_1/3 iff γ∈Λ, for every formula γ. Therefore e_Λ is an evaluation such that e_Λ[Γ] ⊆ F_1/3 but e_Λ(φ) = 0 since φ∉Λ, hence Γ_ J_4φ.


Recall that, from Theorem <ref> and Remark <ref>, the Hilbert calculus H_4 obtained from  H_4 by adding the explosion rule

    (exp_1)  φφ/

(see Definition <ref>) is the axiomatization of the (only) proper extension of  H_4 which is strongly maximal w.r.t. CPL, and that is semantically characterized by the matrix logic

    J̅_4 =⟨ A_4 × A_2, F_1/3×{1}⟩,

where A_2 is the Boolean algebra over {0,1}  in the signature Σ, where the operator ∗ is defined  as ∗x=x.




§ CONCLUSIONS
 


In this paper we have been concerned with the study of maximality and strong maximality conditions among finite-valued Łukasiewicz logics L^i_n with order filters as designated values. In particular, we have characterized the conditions under which a logic L^i_n is maximal w.r.t. CPL and its unique extension  L̅^i_n by an inference rule is strongly maximal w.r.t. classical logic. This allows us to show that, although they are not strongly maximal w.r.t. CPL,  the logics L^i_n with n prime and i/n ≤ 1/2 are in fact ideal paraconsistent logics.
Thus, they provide interesting and well-motivated examples of  ideal  paraconsistent logical systems which are (n+1)-valued, in contrast with the (n+2)-valued  logics   ℳ_n+2 presented in <cit.> and reproduced here in Example <ref>, whose definition is somewhat ad hoc.

As for future work, there are several interesting problems that we leave open in this paper.

Concerning maximality, a natural question is how to obtain a stronger version of Theorem <ref> which give us sufficient conditions to guarantee that a given matrix logic L_1 is strongly maximal w.r.t. another matrix logic L_2.

On the other hand, notice that the study of strong maximality developed in Section <ref> was heavily based on

results on the algebraic semantics associated to these systems by means of the Blok and Pigozzi's techniques. Thus, another interesting issue to be explored in future work is to obtain more examples of strong maximality for different families of algebraizable logics


Another question raised here is the axiomatization of the ideal paraconsistent logics J_q+1 for q > 3 in a “natural” signature containing a deductive implication. As it was shown in Subsection <ref>, the signature Σ = {, , *} is suitable for the case q = 3. Moreover, besides being apt for axiomatizing J_4 =  L^1_3, it can be proved that the (non-paraconsistent) logic L^2_3 can also be axiomatized over Σ in a relatively simple way. Note that α⇒β = α∨β defines a deductive implication in L^2_3.

The fact that  Łukasiewicz implication is definable in Σ justifies the convenience of using that signature for dealing with the case q=3. However,  this property does not hold for any prime q> 3. Indeed, there are primes q in which Łukasiewicz implication of Ł_q+1 cannot be defined over  Σ, e.g. q = 17. The study of the fragments of L^i_q in the signature Σ is thus a different but closely related problem, which deserves future research.



 §.§ Acknowledgements
 The authors acknowledge partial support by the H2020 MSCA-RISE-2015 project SYSMICS. Coniglio was also financially supported by an individual research grant from CNPq, Brazil (308524/2014-4). Esteva and Godo also acknowledge partial support by the Spanish MINECO/FEDER project RASO (TIN2015- 71799-C2-1-P). Gispert also acknowledges partial support by the Spanish MINECO/FEDER projects (MTM2016-74892 and MDM-2014-044) and grant 2017-SGR-95 of Generalitat de Catalunya.


plain


10

AdDz
Michael E. Adams and Wiesjlaw Dziobiak.
Q-universal quasivarieties of algebras.
Proc. of the American Mathematical Society, 120:1053–1059,
  1994.

ArieliAZ10
Ofer Arieli, Arnon Avron, and Anna Zamansky.
Maximally paraconsistent three-valued logics.
In Fangzhen Lin, Ulrike Sattler, and Miroslaw Truszczynski, editors,
  Principles of Knowledge Representation and Reasoning: Proceedings of the
  Twelfth International Conference, KR 2010, Toronto, Ontario, Canada, May
  9-13, 2010. AAAI Press, 2010.

ArieliAZ11a
Ofer Arieli, Arnon Avron, and Anna Zamansky.
Ideal paraconsistent logics.
Studia Logica, 99(1-3):31–60, 2011.

AvronAZ10
Arnon Avron, Ofer Arieli, and Anna Zamansky.
On strong maximality of paraconsistent finite-valued logics.
In Proceedings of the 25th Annual IEEE Symposium on Logic in
  Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom,
  pages 304–313. IEEE Computer Society, 2010.

Be76
Nuel D. Belnap.
How a computer should think.
In G. Ryle, editor, Contemporary Aspects of Philosophy, pages
  30–56. Oriel Press, Boston, 1976.

Be77
Nuel D. Belnap.
A useful four-valued logic.
In J. M. Dunn and G. Epstein, editors, Modern uses of
  multiple-valued logic (Fifth Internat. Sympos., Indiana Univ.,
  Bloomington, Ind., 1975), pages 5–37. Episteme, Vol. 2. Reidel,
  Dordrecht, 1977.

B_C_V
Javier Blanco, Miguel Campercholi, and Diego Vaggione.
The subquasivariety lattice of a discriminator variety.
Adv. Math., 159:18–50, 2001.

blok:pig:01
Willem J. Blok and Don Pigozzi.
Abstract algebraic logic and the deduction theorem.
Preprint. Available at
 http://www.math.iastate.edu/dpigozzi/papers/aaldedth.pdf, 2001.

Blok-Pigozzi:DeductionTheorems
Willem J. Blok and Don L. Pigozzi.
Local deduction theorems in algebraic logic.
In Algebraic logic (Budapest, 1988), volume 54 of Colloq. Math. Soc. János Bolyai, pages 75–109. North-Holland,
  Amsterdam, 1991.

CarCon16
Walter Carnielli and Marcelo E. Coniglio.
Paraconsistent Logic: Consistency, Contradiction and Negation,
  volume 40 of Logic, Epistemology, and the Unity of Science.
Springer International Publishing, 2016.

car:con:mar:07
Walter A. Carnielli, Marcelo E. Coniglio, and João Marcos.
Logics of Formal Inconsistency.
In Dov Gabbay and Franz Guenthner, editors, Handbook of
  Philosophical Logic (2nd. edition), volume 14, pages 1–93. Springer, 2007.

CM W. A. Carnielli and J. Marcos. A taxonomy of C-systems. In: W. A. Carnielli, M. E. Coniglio, and I. M. L. D'Ottaviano, editors, Paraconsistency: The Logical Way to the Inconsistent, volume 228 of Lecture Notes in Pure and Applied Mathematics, pages 1–94. Marcel Dekker, 2002.

CarMarAmo
Walter A. Carnielli, João Marcos, and Sandra de Amo.
Formal inconsistency and evolutionary databases.
Logic and Logical Philosophy, 8(2):115–152, 2000.

CiMuOt99
Roberto Cignoli, Itala M. L. D'Ottaviano, and Daniele Mundici.
Algebraic foundations of many-valued reasoning, volume 7 of
  Trends in Logic—Studia Logica Library.
Kluwer Academic Publishers, Dordrecht, 2000.

Con:Est:God
Marcelo E. Coniglio, Francesc Esteva, and Lluís Godo.
On the set of intermediate logics between the truth and degree
  preserving Łukasiewicz logics.
Logic Journal of the IGPL, 24(3):288–320, 2016.
DOI: 10.1093/jigpal/jzw006.

CF2014
Marcelo E. Coniglio and Martín Figallo.
On a four-valued modal logic with deductive implication.
Bulletin of the Section of Logic, 43(1-2):1–18, 2014.

Con:Sil
Marcelo E. Coniglio and Luiz H. Silvestrini.
An alternative approach for quasi-truth.
Logic Journal of the IGPL, 22(2):387–410, 2014.
DOI: 10.1093/ljigpal/jzt026.

dac:63
Newton C. A da Costa.
Sistemas formais inconsistentes (Inconsistent formal systems, in
  Portuguese).
Habilitation thesis, Universidade Federal do Paraná, Curitiba,
  Brazil, 1963.
Republished by Editora UFPR, Curitiba, Brazil,1993.

DO2015
Michael De and Hitoshi Omori.
Classical negation and expansions of Belnap-Dunn logic.
Studia Logica, 103(4):825–851, 2015.

dot:dac:70
Itala M. L. D'Ottaviano and Newton C. A. da Costa.
Sur un problème de Jaśkowski (in French).
Comptes Rendus de l'Académie de Sciences de Paris (A-B),
  270:1349–1353, 1970.

Du76
J. Michael Dunn.
Intuitive semantics for first-degree entailment and `coupled trees'.
Philosophical Studies, 29(3):149–168, 1976.

Dz0
Wiesjlaw Dziobiak.
On subquasivariety lattices of semi-primal varieties.
Algebra Universalis, 20:127–129, 1985.

FR2
Josep M. Font and Miquel Rius.
An abstract algebraic logic approach to tetravalent modal logics.
The Journal of Symbolic Logic, 65(2):481–518, 2000.

GpT98
Joan Gispert and Antoni Torrens.
Quasivarieties generated by simple mv-algebras.
Studia Logica, 61:79–99, 1998.

GT14
Joan Gispert and Antoni Torrens.
Locally finite quasivarieties of MV-algebras.
ArXiv, pages 1–14, 2014.
Online DOI: http://arxiv.org/abs/1405.7504.

Ha01c
Petr Hájek.
On very true.
Fuzzy Sets and Systems, 124(3):329–333, 2001.

Komori:SuperLukasiewiczPropositional
Yuichi Komori.
Super-Łukasiewicz propositional logics.
Nagoya Mathematical Journal, 84:119–133, 1981.

Loureiro
Isabel Loureiro.
Principal congruences of tetravalent modal algebras.
Notre Dame Journal of Formal Logic, 26:75–80, 1985.

Marcos
João Marcos.
8K solutions and semi-solutions to a problem of da Costa.
Unpublished manuscript, 2000.

McNaughton:FunctionalRep
Robert McNaughton.
A theorem about infinite-valued sentential logic.
Journal of Symbolic Logic, 16(1):1–13, 1951.

Ml72
Grigore C. Moisil.
Essais sur les logiques non chrysippiennes.
Éditions de l'Académie de la République Socialiste de Roumanie,
  Bucarest, 1972.

Monteiro:69
Antonio Monteiro.
Notas del curso Álgebras de Boole Involutivas.
Technical report, Instituto de Matemática, Universidad Nacional del
  Sur, Bahia Blanca, 1969.
Reprinted as Álgebras de Boole Involutivas, Informe Técnico
  Interno No. 78, Universidad Nacional del Sur, Bahia Blanca, 2002.

LMonteiro
Luiz Monteiro.
Axiomes indépendants pour les algèbres de łukasiewicz
  trivalentes.
Bulletin de la Societé des Sciences Mathématiques et
  Physiques de la R. P. Roumanie, Nouvelle série, 7:199–202, 1963.

Panti:Varieties
Giovanni Panti.
Varieties of MV-algebras.
Journal of Applied Non-Classical Logics, 9(1):141–157, 1999.

RibCon12
Márcio M. Ribeiro and Marcelo E. Coniglio.
Contracting logics.
In L. Ong and R. de Queiroz, editors, Logic, Language,
  Information and Computation. WoLLIC 2012, volume 7456 of Lecture Notes
  in Computer Science, pages 268–281. Springer, 2012.

RTV90
Antonio J. Rodríguez, Antoni Torrens, and Ventura Verdú.
Łukasiewicz logic and Wajsberg algebras.
Bulletin of the Section of Logic, 19:51–55, 1990.

Sette
Antonio M. Sette.
On the propositional calculus 𝐏^1.
Mathematica Japonicae, 18(13):173–180, 1973.

SetCar
Antonio M. Sette and Walter A. Carnielli.
Maximal weakly-intuitionistic logics.
Studia Logica, 55(1):181–203, 1995.

Woj88
Ryszard Wójcicki.
Theory of Logical Calculi: Basic Theory of Consequence
  Operations, volume 199 of Synthese Library.
Springer Netherlans, 1988.




