A Logic for Dually Hemimorphic Semi-Heyting Algebras
and
its Axiomatic Extensions
Juan M. CORNEJO* and Hanamantagouda P. SANKAPPANAVAR
* Departamento de Matemática
Universidad Nacional del Sur
Alem 1253, Bahía Blanca, Argentina
INMABB - CONICET
[email protected]
** Department of Mathematics
State University of New York
New Paltz, New York, 12561
U.S.A.
[email protected]
Abstract.
The variety DHMSH of dually hemimorphic semi-Heyting algebras was introduced in 2011 by the second author
as an expansion of semi-Heyting algebras by a dual hemimorphism.
In this paper, we focus on the variety DHMSH from a logical point of view. Firstly, we present a Hilbert-style axiomatization of a new logic called “Dually hemimorphic semi-Heyting logic” (DHMSH, for short), as an expansion of semi-intuitionistic logic SI (also called SH) introduced by the first author by adding a weak negation (to be interpreted as a dual hemimorphism). We then prove that it is implicative in the sense of Rasiowa and that it is complete with respect to the variety DHMSH. It is deduced that the logic DHMSH is algebraizable in the sense of Blok and Pigozzi, with
the variety DHMSH as its equivalent algebraic semantics and that the lattice of axiomatic extensions of DHMSH is dually isomorphic to the lattice of subvarieties of DHMSH. A new
axiomatization for Moisil’s logic is also obtained.
Secondly, we characterize the axiomatic extensions of
DHMSH in which the “Deduction Theorem” holds.
Thirdly, we present several new logics, extending the logic DHMSH, corresponding to several important subvarieties of the variety DHMSH. These include logics corresponding to the varieties generated by
two-element, three-element and some four-element dually quasi-De Morgan semi-Heyting algebras, as well as a new axiomatization for the 3-valued Łukasiewicz logic.
Surprisingly, many of these logics turn out to be connexive logics, a few of which are presented in this paper. Fourthly, we present axiomatizations for two infinite sequences of logics namely, De Morgan-Gödel logics and dually pseudocomplemented Gödel logics, Fifthly, axiomatizations are also provided for logics corresponding to many subvarieties of regular dually quasi-De Morgan Stone semi-Heyting algebras, of regular De Morgan semi-Heyting algebras of level 1, and of JI-distributive semi-Heyting algebras of level 1.
We conclude the paper with some open problems.
Most of the logics considered in this paper are discriminator logics in the sense that they correspond to discriminator varieties. Some of them, just like the classical logic, are even primal in the sense that their corresponding varieties are generated by primal algebras.
Key words and phrases:
Semi-intuitionistic logic, dually hemimorphic semi-Heyting logic, Dually quasi-De Morgan semi-Heyting logic, De Morgan semi-Heyting logic, dually pseudocomplemented semi-Heyting logic, regular dually quasi-De Morgan Stone semi-Heyting algebras of level 1,
implicative logic, equivalent algebraic semantics, algebraizable logic, De Morgan Gödel logic, dually pseudocomplemented Gödel logic, Moisil’s logic, 3-valued Łukasiewicz logic
2010 Mathematics Subject Classification:
Primary: 03B50, 03G25,06D20,06D15; Secondary: 08B26, 08B15, 06D30.
1. Introduction
Semi-Heyting algebras were introduced by the second author111Parts of this paper were presented by the second author in invited talks at 8th International Conference on
Non-Classical Logics: Theory and Applications, \Lodz (2016), at Maltsev Meeting, Novosibirsk (2017), and at Asubl (Algebra and Substructural Logics-Take 6) workshop, Cagliari (2018).,
during 1983-84, as a result of his research that went into [29] (still a preprint at the time).
Some of the early results were announced in [30]. The first results on these algebras with their proofs, however, were published much later in 2008 (see [33]).
An algebra L=⟨L,∨,∧,→,0,1⟩ is a semi-Heyting algebra if the following conditions hold:
- (SH1)
⟨L,∨,∧,0,1⟩ is a lattice with [math] and 1,
2. (SH2)
x∧(x→y)≈x∧y,
3. (SH3)
x∧(y→z)≈x∧[(x∧y)→(x∧z)],
4. (SH4)
x→x≈1.
A semi-Heyting algebra is a Heyting algebra if it satisfies the identity:
(H) (x∧y)→x≈1.
We will denote the variety of semi-Heyting algebras by SH and that of Heyting algebras by H.
Semi-Heyting algebras share some important properties with Heyting algebras; for instance, semi-Heyting algebras are distributive and pseudocomplemented, with the pseudocomplement x∗:=x→0; the congruences on them are determined by filters and the variety of semi-Heyting algebras is arithmetical. For further results on SH, see [1], [2], [3], [8] and [33].
It is well known that the variety of Heyting algebras is the equivalent algebraic semantics (in the sense of Blok and Pigozzi) of the intuitionistic propositional logic. In 2011, the first author of this paper defined, in [7], a new logic called “semi-intuitionistic logic” (SI, for short, also called SH) and showed, essentially, that the variety of semi-Heyting algebras is an algebraic semantics for this logic and that the intuitionistic logic is an axiomatic extension of it. The axioms of this logic, however, were
expressed in a language that was not the same as
that of semi-Heyting algebras.
In [11], a much simpler, but equivalent, set of axioms for SI (or SH), was presented in the same language as that of semi-Heyting algebras. The logic SI as presented in [11] will play a fundamental role in this paper.
In 1942, Moisil [24] defined a logic called “Logique modale” (LM), an expansion of intuitionistic propositional calculus by a De Morgan negation. He also introduced Heyting algebras endowed with an involution, in [25], as the algebraic models of the logic LM. These algebras were further investigated by
Monteiro [26] under the name of symmetric Heyting algebras. In particular, he presented a proof of an algebraic completeness theorem for Moisil’s calculus
by showing that LM is complete for the variety of symmetric Heyting algebras.
Independently of the previous work,
motivated purely by (universal) algebraic considerations, the second author defined and studied De Morgan Heyting algebras, in [31], by expanding Heyting algebras by a De Morgan operation.
Earlier in 1985, he had also introduced (see [29]) the variety of Heyting algebras with a dual pseudocomplementation. Also, in 1987, the concepts of hemimorphism (without name), semi-De Morgan algebra and (lower) quasi-De Morgan algebra were introduced in [32], unifying (and generalizing) the notions of De Morgan operation and pseudocomplementation.
In 2011, motivated by the similarities of the results and proofs in [29] and [31], he introduced in [34] a more general variety of algebras called “dually hemimorphic semi-Heyting algebras”–
an expansion of semi-Heyting algebras by a dual hemimorphism, as a common
generalization of De Morgan Heyting algebras and dually psedocomplemented Heyting algebras.
Definition 1.1**.**
[34]*
An algebra A=⟨A,∨,∧,→,′,0,1⟩ is a dually hemimorphic semi-Heyting algebra (or, semi-Heyting algebra with a
dual hemimorphism*) if A satisfies the following conditions:
(E1): ⟨A,∨,∧,→,0,1⟩ is a semi-Heyting algebra,
(E2): 0′≈1,
(E3): 1′≈0,
(E4): (x∧y)′≈x′∨y′ (∧-De Morgan law).
The unary operation ′ satisfying (E2)-(E4) is called a dual hemimorphism.
The variety of dually hemimorphic semi-Heyting algebras will be denoted by DHMSH.
Several important subvarieties of the variety
DHMSH, by adding the duals of those given in [32], were introduced in [34], some of which will be recalled in Section 5.
The following problem presents itself naturally.
PROBLEM 1: Find a propositional logic in the language ⟨∨,∧,→,∼,⊥,⊤⟩
with the following properties:
(1) It has the variety DHMSH of dually hemimorphic semi-Heyting algebras
as its equivalent algebraic semantics, and
(2) It has Moisil’s logic as one of its (axiomatic) extensions.
The subvariety DQDSH of DHMSH, consisting of dually quasi-De Morgan semi-Heyting algebras (see LIST 1 in Section 5 for definition), has been intensively investigated in [34, 35, 36, 37, 38, 40]. In Section 8 of [34] (see also [36] and [37])
the following problem was raised:
PROBLEM 2: Find Hilbert-type axiomatization for logics corresponding to
two-valued, three-valued and four-valued dually quasi-De Morgan semi-Heyting algebras, viewed as logical matrices with {1} as the distinguished subset.
In this paper, we focus on the logical aspects of the variety DHMSH of dually hemimorphic semi-Heyting algebras and many of its subvarieties. Firstly, we give a solution to PROBLEM 1. More specifically, we present a Hilbert-style presentation of a new logic called “Dually hemimorphic semi-Heyting logic” (DHMSH, for short), as an expansion of semi-intuitionistic logic presented in [11]. We then
prove that it is implicative in the sense of Rasiowa and that it is complete with respect to the variety DHMSH of dually hemimorphic semi-Heyting algebras. Using the well-known results of Abstract Algebraic Logic we deduce that the logic DHMSH is algebraizable in the sense of Blok and Pigozzi, with
the variety DHMSH as its equivalent algebraic semantics.
It then follows that the lattice of axiomatic extensions of DHMSH is dually isomorphic to the lattice of subvarieties of DHMSH. As applications of these results, we present several new logics, extending the logic DHMSH, corresponding to some interesting subvarieties (studied in [34]) of the variety of hemimorphic semi-Heyting and Heyting algebras. A new
axiomatization for Moisil’s logic is also obtained.
Secondly, we characterize the axiomatic extensions of DHMSH in which the “Deduction Theorem” holds.
Thirdly, we introduce several new logics, extending the logic DHMSH, corresponding to important subvarieties of the variety DHMSH, including some logics corresponding to the varieties generated by
two-element, three-element and some four-element dually quasi-De Morgan semi-Heyting algebras, as well as a new axiomatization for the 3-valued Łukasiewicz logic.
Many of these logics turn out to be connexive logics, a few of which are presented in this paper. Fourthly, we present axiomatizations for two infinite sequences of logics, namely De Morgan-Gödel logics and dually pseudocomplemented Gödel logics, Fifthly, axiomatizations are also provided for logics corresponding to many subvarieties of regular dually quasi-De Morgan Stone semi-Heyting algebras of level 1, of Regular De Morgan Semi-Heyting Algebras of level 1 and of JI-distributive semi-Heyting algebras of level 1.
Many of the logics considered in this paper are discriminator logics in the sense that they correspond to discriminator varieties. Some of them, just like the classical logic, are even primal in the sense that their corresponding varieties are generated by primal algebras.
The paper is organized as follows: Section 2 contains definitions, notation and some preliminary results that are needed later in the paper. It includes the axiomatization for semi-intuitionistic logic as presented in [11] which is crucial for the rest of the paper. In Section 3, we present a Hilbert-style axiomatization for the new logic called “Dually hemimorphic semi-Heyting logic” (DHMSH, for short)”
by expanding the language of semi-intuitionistic logic SI of [11] by a (weak) negation called dually hemimorphic negation and by adding new axioms and a new inference rule to the semi-intitionistic logic SI.
We then prove that the logic DHMSH is an implicative logic with respect to the defined connective →H, where x→y:=x→(x∧y). In Section 4, we prove
the completeness theorem for the logic DHMSH: The logic DHMSH is complete with respect to
the variety DHMSH of dually hemimorphic semi-Heyting algebras. In Section 5, we deduce from Abstract Algebraic Logic that the logic DHMSH is algebraizable, in the sense of Blok and Pigozzi, with the variety DHMSH as its equivalent algebraic semantics, from which it follows that the lattice of axiomatic extensions of DHMSH is dually isomorphic to the lattice of subvarieties of DHMSH. These results enable us to present axiomatizations of several extensions of
DHMSH by translating the (equational) axioms of various (known) subvarieties of DHMSH from [34, 35, 36, 37, 38] (see sections 5 and 8-12)
into (propositional) axioms of the corresponding extensions.
We also show that Moisil’s “logique modale” LM
is equivalent to the logic DMH corresponding to the variety DMH of De Morgan Heyting algebras.
In Section 6, we characterize the (axiomatic) extensions of
DHMSH in which the “Deduction Theorem” holds. Sections 7-12 deal with applications of the results of Section 5 together with the algebraic results proved in [34, 35, 36, 37, 38]. More specifically, in Section 7, we present axiomatizations for some extensions of the logic DQDSH whose equivalent algebraic semantics are subvarieties of DQDSH generated by finitely many finite algebras, including two 2-valued logics and twenty 3-valued logics and three 4-valued logics. Then we revisit the 3-valued Łukasiewicz logic and give an alternative axiomatization for it. In fact, we show that
the logic corresponding to the 3-element De Morgan Heyting algebra is equivalent to the 3-valued Łukasiewicz logic.
Thereafter, we give axiomatizations for extensions of DQDSH corresponding to the subvarieties of the variety DQDBSH generated by dually quasi-De Morgan Boolean semi-Heyting algebras, completing the solution to PROBLEM 2 mentioned earlier. We also give some extensions of the logic DHMSH which fail to possess the disjunction property.
Section 8 describes some connections to Connexive Logic by showing that
some of these 2-valued, 3-valued and 4-valued logics are, in fact, connexive logics.
Section 9 gives axiomatizations for De Morgan Gödel logic and dually pseudocomplemented Gödel logic corresponding to the varieties generated by the De Morgan Heyting chains and the dually pseudocomplemented Heyting chains, respectively. It also provides axiomatizations for the logics corresponding to their subvarieties.
In Section 10, we present axiomatizations for new logics corresponding to several subvarieties
of the variety RDQDStSH1 of regular dually quasi-De Morgan Stone semi-Heyting algebras of level 1.
Section 11 presents axiomatizations for logics corresponding to a number of subvarieties of
RDMSH1 of regular De Morgan Stone semi-Heyting algebras of level 1, while Section 12 presents axiomatizations for logics corresponding to many subvarieties of
JI-distributive linear semi-Heyting algebras of level 1.
Section 13 concludes the paper with several open problems for future research.
2. Preliminaries
A language L is a set of finitary operations (or connectives), each with a fixed arity n≥0. In this paper, we identify ⊥ and ⊤ with [math] and 1 respectively and thus consider the languages ⟨∨,∧,→,∼,⊥,⊤⟩ and ⟨∨,∧,→,′,0,1⟩ as the same; however, we use the former in the context of logics and the latter in the context of algebras.
For a countably infinite set Var of propositional variables, the formulas of the language L are inductively defined as usual.
A logic (or, a deductive system) in the language L is a pair L=⟨L,⊢L⟩, where ⊢L is a substitution-invariant consequence relation on \mboxFmL. We will present logics by means of their “Hilbert style” axioms and inference rules.
The set of formulas \mboxFmL can be turned into an algebra in the usual way. Throughout the paper, Γ denotes a set of formulas and lower case Greek letters denote formulas. The homomorphisms from the formula algebra FmL into an L-algebra (i.e, an algebra of type L) A are called interpretations (or valuations) in A. The set of all such interpretations is denoted by Hom(FmL,A). If h∈Hom(FmL,A) then the interpretation of a formula α under h is its image hα∈A, while hΓ denotes the set {hϕ ∣ ϕ∈Γ}.
As mentioned earlier, Moisil presented in [24] (see also [26]), a propositional logic called, “Logique modale”. We will refer to it as “LM”.
Moisil also introduced the variety of Heyting algebras endowed with an involution, in [25], as the algebraic semantics for the logic LM. Monteiro [26] investigated these algebras under the new name of symmetric Heyting algebras. Among other things, he presented a proof of an algebraic completeness theorem for Moisil’s calculus LM by showing that the logic LM is complete with respect to the variety of symmetric Heyting algebras.
In the next section we will generalize Moisil’s logic to a new logic called “dually hemimorphic semi-Heyting logic”. As a first step to achieve this goal, we need to present a generalization of intutionistic logic called “Semi-intutionistic logic” which was first introduced by the first author in [7] in the language ⟨∨,∧,→,∼⟩. We will actually present below the more streamlined version of semi-Intuitionistic logic SI in the usual language
⟨∨,∧,→,⊥,⊤⟩, as first presented in [11] with the intuitionistic logic as an axiomatic extension. To facilitate this presentation, it will be convenient to use α→Hβ as an abbreviation for α→(α∧β) so that the axioms given are easier to read. Moreover, the connective →H plays a crucial role in this section and in the sections that follow.
Definition 2.1**.**
[11]*
The semi-intuitionistic logic SI (also called SH) is defined in the language
{∨,∧,→,⊥,⊤} and it has the following
axioms and the inference rule:
AXIOMS:**
(A1): α→H(α∨β),
(A2): β→H(α∨β),
(A3): (α→Hγ)→H[(β→Hγ)→H((α∨β)→Hγ)],
(A4): (α∧β)→Hα,
(A5): (γ→Hα)→H[(γ→Hβ)→H(γ→H(α∧β))],
(A6): ⊤,
(A7): ⊥→Hα,
(A8): ((α∧β)→Hγ)→H(α→H(β→Hγ)),
(A9): (α→H(β→Hγ))→H((α∧β)→Hγ),
(A10): (α→Hβ)→H((β→Hα)→H((α→γ)→H(β→γ))),
(A11): (α→Hβ)→H((β→Hα)→H((γ→β)→H(γ→α))).
**RULE OF INFERENCE:
**
(SMP): From ϕ and ϕ→Hγ, deduce γ (semi-Modus Ponens).
The following theorem and the lemma, proved in [11], are useful in later sections.
Theorem 2.2**.**
[11] (Completeness Theorem) **
[TABLE]
Lemma 2.3**.**
[11]*
The following statements hold in the logic SI:*
- (a)
If Γ⊢SIψ then Γ⊢SIα→Hψ,
2. (b)
⊢SIα→Hα,
3. (c)
⊢SI(α∧β)→Hβ,
4. (d)
If ⊢SIα→Hβ then ⊢SI(α∧γ)→H(β∧γ) and ⊢SI(γ∧α)→H(γ∧β),
5. (e)
⊢SI(α→Hβ)→H[(β→Hγ)→H(α→Hγ)],
6. (f)
If Γ⊢SIα and Γ⊢SIβ then Γ⊢SIα∧β.
We now give some useful information about semi-Heyting algebras.
A key feature of semi-Heyting algebras is the following:
Every semi-Heyting algebra ⟨A,∨,∧,→,0,1⟩ gives rise, in a natural way, to a Heyting algebra ⟨A,∨,∧,→H,0,1⟩, where x→Hy:=x→(x∧y), for x,y∈A (see [3]).
Lemma 2.4**.**
[3]* Let A=⟨A,∨,∧,→,0,1⟩ be a semi-Heyting algebra and let
a,b,c∈A. Then,*
a∧b≤c* if and only if a≤b→(b∧c),*
(a→b)∧(b→a)=1* if and only if (a→Hb)∧(b→Ha)=1,*
a=b* if and only if (a→Hb)∧(b→Ha)=1,*
a→b≤a→Hb.
Lemma 2.5**.**
[7, Corollary 3.9]*
Let A=⟨A,∨,∧,→,0,1⟩ be a semi-Heyting algebra and a,b∈A. Then, a→Hb=1 if and only if a≤b.*
3. The logic DHMSH: Axioms, Rules, and Rasiowa’s Implicativeness
In this section we present a new propositional logic called “dually hemimorphic semi-Heyting logic” denoted by DHMSH and prove, as a first step toward a completeness theorem, that
the logic DHMSH is implicative in the sense of Rasiowa with respect to the implication →H.
Definition 3.1**.**
*The dually hemimorphic semi-Heyting logic, DHMSH, is defined in the language
⟨∨,∧,→,∼,⊥,⊤⟩ and it has the following axioms and rules of inference:
AXIOMS:
(A1), (A2), …, (A11)* of the logic SI, together with the following three additional axioms:*
(A12): ⊤→H∼⊥,
(A13): ∼⊤→H⊥,
(A14): ∼(α∧β)→H(∼α ∨∼β).
RULES OF INFERENCE:
(SMP) From ϕ and ϕ→Hγ, deduce γ (semi-Modus Ponens),
(SCP) From ϕ→Hγ, deduce ∼γ→H ∼ϕ (semi contraposition rule).
Since the axioms and the inference rule of the logic SI are included in the logic DHMSH, the following result is immediate.
Theorem 3.2**.**
Let Γ∪{α}⊆\mboxFm. If Γ⊢SIα then Γ⊢DHMSHα.
The following lemma is needed later.
Lemma 3.3**.**
Let Γ∪{α,β,γ,ψ}⊆\mboxFm. The following statements hold in the logic DHMSH:
- (a)
If Γ⊢DHMSHψ, then Γ⊢DHMSHα→Hψ,
2. (b)
⊢DHMSHα→Hα,
3. (c)
⊢DHMSH(α∧β)→Hβ,
4. (d)
Γ⊢DHMSH(α→Hβ)→H[(β→Hγ)→H(α→Hγ)]*,
*
5. (e)
Γ⊢DHMSHα∧β* if and only if Γ⊢DHMSHα and Γ⊢DHMSHβ,*
6. (f)
If Γ⊢DHMSHα→Hβ, then Γ⊢DHMSH(α∧γ)→H(β∧γ) and Γ⊢DHMSH(γ∧α)→H(γ∧β).
**Proof **
Items (a), (b), (c) and (d) follow from Theorem 3.2 and items (a), (b), (c) and (e) of Lemma 2.3, respectively.
We have, by Theorem 3.2 and Lemma 2.3 (f), that if Γ⊢DMSHα and Γ⊢DHMSHβ then Γ⊢DHMSHα∧β. The other half of the item (e) follows easily from axiom (A2.1), item (c) and (SMP). Finally, Item (f) follows from Lemma 2.3 (d).
\hfill□
Lemma 3.4**.**
Let Γ∪{α,β,γ}⊆\mboxFm.
- (a)
If Γ⊢DHMSHα→Hβ and Γ⊢DHMSHβ→Hγ then Γ⊢DHMSHα→Hγ.
2. (b)
Γ,β→Hα⊢DHMSH ∼α→H∼β.**
3. (c)
Γ⊢DHMSH∼(α∨β)→H(∼α∧∼β).**
4. (d)
*If Γ⊢DHMSHα→Hβ, then *
* Γ⊢DHMSH(α∨γ)→H(β∨γ) and Γ⊢DHMSH(γ∨α)→H(γ∨β).*
5. (e)
Γ⊢DHMSH(∼α∨∼β)→H ∼(α∧β).
**Proof **
- (a)
This follows from 3.3 (d), using (SMP).
2. (b)
This is immediate from (SCP).
3. (c)
Using (A1), (A2) and (SCP), we get
[TABLE]
The conclusion follows from (3.1), (A5) and (SMP).
4. (d)
-
Γ⊢DHMSHα→Hβ by hypothesis.
2. 2.
Γ⊢DHMSHβ→H(β∨γ) by (A2.1)
3. 3.
Γ⊢DHMSHα→H(β∨γ) by (a) in d1 and d2.
4. 4.
Γ⊢DHMSHγ→H(β∨γ) by (A2.1)
5. 5.
Γ⊢DHMSH(α→H(β∨γ))→H[(γ→H(β∨γ))→H((α∨γ)→H(β∨γ))] by (A2.1)
6. 6.
Γ⊢DHMSH(γ→H(β∨γ))→H((α∨γ)→H(β∨γ)) by (SMP) in d3 and d5.
7. 7.
Γ⊢DHMSH(α∨γ)→H(β∨γ) by (SMP) in d4 and d6.
8. 8.
Γ⊢DHMSHγ→H(γ∨β) by (A2.1)
9. 9.
Γ⊢DHMSHβ→H(γ∨β) by (A2.1)
10. 10.
Γ⊢DHMSHα→H(γ∨β) by (a) and (SMP) in d1 and d9.
11. 11.
Γ⊢DHMSH(γ→H(γ∨β))→H[(α→H(γ∨β))→H((γ∨α)→H(γ∨β))] by (A2.1)
12. 12.
Γ⊢DHMSH(α→H(γ∨β))→H((γ∨α)→H(γ∨β)) by (SMP) in d8 and d11.
13. 13.
Γ⊢DHMSH(γ∨α)→H(γ∨β) by (SMP) in d10 and d12.
5. (e)
-
Γ⊢DHMSH(α∧β)→Hα by axiom (A2.1).
2. 2.
Γ⊢DHMSH ∼α→H ∼(α∧β) by (SCP).
3. 3.
Γ⊢DHMSH(α∧β)→Hβ by 3.3 (c).
4. 4.
Γ⊢DHMSH ∼β→H ∼(α∧β) by (SCP).
5. 5.
Γ⊢DHMSH(∼α→H ∼(α∧β))→H[(∼β→H ∼(α∧β))→H(( ∼α∨∼β)→H ∼(α∧β))] by axiom (A2.1).
6. 6.
Γ⊢DHMSH( ∼β→H ∼(α∧β))→H(( ∼α∨∼β)→H ∼(α∧β)) by (SMP) in e2, e5.
7. 7.
Γ⊢DHMSH(∼α∨∼β)→H ∼(α∧β) by (SMP) in e4 and e6,
proving the lemma. \hfill□
3.1. DHMSH as an implicative logic in the sense of Rasiowa
In 1974, Rasiowa ([27, page 179]) introduced an important class of logics called “standard systems of implicative extensional propositional calculus” and associated a class of algebras with each of them, by a generalization of the classical Lindenbaum-Tarski process. We will refer to these logics as “implicative logics in the sense of Rasiowa” (“implicative logics”, for short). These logics have played a pivotal role in the development of Abstract Algebraic Logic. We now recall the definition
of implicative logics. We follow Font [15].
Definition 3.5**.**
[27]* Let L be a logic in a language L that includes a binary connective →, either primitive or defined by a term in exactly two variables. Then L is called an implicative logic with respect to the binary connective →, if the following conditions are satisfied:*
⊢Lα→α,
α→β,β→γ⊢Lα→γ,
For each symbol f∈L of arity n≥1,
\left\{\begin{array}[]{c}\alpha_{1}\to\beta_{1},\ldots,\alpha_{n}\to\beta_{n},\\
\beta_{1}\to\alpha_{1},\ldots,\beta_{n}\to\alpha_{n}\end{array}\right\}\vdash_{\mathcal{L}}f(\alpha_{1},\ldots,\alpha_{n})\to f(\beta_{1},\ldots,\beta_{n}),
α,α→β⊢Lβ,
α⊢Lβ→α.
The following lemma was proved in [11, Lemma 4.6].
Lemma 3.6**.**
[11, Lemma 4.6]*
The logic SI is implicative with respect to the connective →H.*
The following theorem follows from Theorem 3.2, Lemma 3.4 (b) and Lemma 3.6.
Theorem 3.7**.**
The logic DHMSH is implicative with respect to the connective →H.
4. Completeness of DHMSH
Let L denote a language. Identities in L are ordered pairs of L-formulas that will be written in the form α≈β.
An interpretation h in A satisfies an identity α≈β if hα=hβ.
We denote this satisfaction relation by the notation: A⊨hα≈β. An algebra A satisfies the equation α≈β if all the interpretations in A satisfy it; in symbols,
[TABLE]
A class K of algebras satisfies the identity α≈β when all the algebras in K satisfy it; i.e.
[TABLE]
If xˉ is a sequence of variables and h is an interpretation in A, then we write aˉ for h(xˉ).
For a class K of L-algebras, we define the relation ⊨K that holds between a set Δ of identities and a single identity α≈β as follows:
[TABLE]
for every A∈K and every interpretation aˉ of the variables of Δ∪{α≈β} in A,
ϕA(aˉ)=ψA(aˉ), for every ϕ≈ψ∈Δ⇒αA(aˉ)=βA(aˉ).
In this case, we say that α≈β is a K-consequence of Δ.
The relation ⊨K is called the semantic equational consequence relation determined by K.
Our goal in this section is to prove that the logic DHMSH is complete with respect to the variety DHMSH. For this we need the following definition from [27].
Definition 4.1**.**
[27, Definition 6, page 181], [15, Definition 2.5]
Let L be an implicative logic in the language L with an implication connective →. An L-algebra is an algebra A in the language L that has an element 1 with the following properties:
For all Γ∪{ϕ}⊆\mboxFm and all h∈Hom(FmL,A),
if Γ⊢Lϕ and hΓ⊆{1} then hϕ=1,
For all a,b∈A, if a→b=1 and b→a=1 then a=b.
The class of L-algebras is denoted by Alg∗L.
We also need the following result from [11].
Theorem 4.2**.**
[11, Corollary 4.8]*
Alg∗SI=SH.*
Since DHMSH is an implicative logic with respect to the binary connective →H by Theorem 3.7, we obtain the following result, in view of [27, Theorem 7.1, pag 222].
Theorem 4.3**.**
The logic DHMSH is complete with respect to the class
Alg∗DHMSH.
In other words,
[TABLE]
As a last step to complete the proof of algebraic completeness of the logic DHMSH, we need to prove that Alg∗DHMSH=DHMSH.
Lemma 4.4**.**
DHMSH=Alg∗DHMSH.
**Proof ** First, we wish to prove that DHMSH⊆Alg∗DHMSH.
Let A∈DHMSH, Γ∪{ϕ}⊆\mboxFm and h∈Hom(\mboxFmL,A) such that Γ⊢DMSHϕ
and hΓ⊆{1}. We need to verify that hϕ=1. We will proceed by induction on the length of the proof of Γ⊢DMSHϕ.
Assume that ϕ is an axiom.
If ϕ is one of the axioms (A2.1) to (A2.1) then ⊢SIϕ. Hence, by theorem 2.2, ⊨DHMSHϕ and so, h(ϕ)=⊤.
If ϕ is the axiom (A3.1) then, using (E1.1), we have h(ϕ)=h(⊤→H ∼⊥)=1→H0′=1.
If ϕ is the axiom (A3.1) then, using (E1.1), we get that h(ϕ)=h(∼⊤→H⊥)=0→H0=1.
If ϕ is the axiom (A3.1) then, using (E1.1), we obtain that h(ϕ)=h(∼(α∧β)→H( ∼α∨∼β))=(h(α)∧h(β))′→H(h(α)′∨h(β)′)=(h(α)∧h(β))′→H(h(α)∧h(β))′=1.
If ϕ∈Γ then h(ϕ)=⊤ by hypothesis.
Assume now that Γ⊢Lϕ is obtained from an application of (SMP). Then there exist a formula ψ such that Γ⊢Lψ and Γ⊢Lψ→Hϕ. By induction, h(ψ)=1 and h(ψ→Hϕ)=1. Then 1=h(ψ)→Hh(ϕ)=1→Hh(ϕ)=h(ϕ).
Assume that Γ⊢Lϕ is the result of an application of the rule (SCP). Then for α,β∈\mboxFm, ϕ=∼β→H∼α and Γ⊢Lα→Hβ. By induction, 1=h(α→Hβ)=h(α)→Hh(β) and, consequently h(α)≤h(β). Then, using condition (E1.1), h(β)′≤h(α)′. Hence h(β)′→Hh(α)′=1. Therefore h(ϕ)=h(∼β→H∼α)=h(β)′→Hh(α)′=1.
Hence, the induction is complete and so, we concludes that A satisfies (LALG1). It is easy to see that the condition (LALG2) also holds, implying A∈Alg∗DHMSH.
Next, we prove the other inclusion.
Let A=⟨A,∨,∧,→,′,0,1⟩∈Alg∗DHMSH. Notice that ⟨A,∨,∧,→,0,1⟩∈Alg∗SI. By Theorem 4.2, ⟨A,∨,∧,→,0,1⟩∈SH. Now, it only remains to show that A satisfies the conditions (E1.1) to (E1.1).
In view of axiom (A\refaxiombotneg) and (LALG1), we have that A⊨1→H0′≈1. Using (LALG1) and Lemma 3.3 (a), we get A⊨0′→H1≈1. Then by (LALG2), A⊨1≈0′.
In view of axioms (A\refaxiomabot) and (A\refaxiomtopneg), together with (LALG1), we have that A⊨0→H1′≈1 and A⊨1′→H0≈1. Then by (LALG2), A⊨1′≈0.
By Lemma 3.4 (e) and the condition (LALG1), A satisfies the identity (x′∨y′)→H(x∧y)′≈1. Also, In view of axiom (A\refaxiomDMlaw1), and (LALG1), A satisfies the identity (x∨y)′→H(x′∧y′)≈1. Applying (LALG2), the algebra satisfies (E1.1).
Consequently A∈DHMSH.
\hfill□
We are now ready to present the completeness theorem for the logic DHMSH.
Theorem 4.5**.**
The logic DHMSH is complete with respect to the variety
DHMSH.
**Proof ** From Lemma 4.4 we have Alg∗DHMSH=DHMSH. The conclusion follows from Theorem 4.3.
\hfill□
5. Equivalent Algebraic Semantics and Axiomatic Extensions of the logic DHMSH
Our goal in this section is to improve Theorem 4.5 by proving that
the logic DHMSH is algebraizable and DHMSH is an equivalent algebraic semantics of the logic DHMSH.
Here we first recall some relevant notions and results from Abstract Algebraic Logic (see [5, Section 2.1], [14], or [15]).
Definition 5.1**.**
[5, Definition 2.2] [15, Definition 3.4]*
Let ⟨L,⊢L⟩ be a logic (i.e., deductive system) and K a class of L-algebras. K is called an “algebraic semantics” for ⟨L,⊢L⟩ if ⊢L can be interpreted in ⊨K in the following sense:
There exists a finite set δi(p)≈ϵi(p), for i<n, of identities with a single variable p such that, for all Γ∪ϕ⊆Fm and each j<n,
[TABLE]
where δ[ψ/p] denotes the formula obtained by the substitution of ψ at every occurrences of p in δ.
The identities δi≈ϵi, for i<n, are called “defining identities” for
⟨L,⊢L⟩ and K.
In what follows, we will use “Γ=\joinrel∣⊨KΔ” as an abbreviation for “Γ⊨KΔ and Δ⊨KΓ.” Also, δ(Δ(ϕ,ψ)) denotes the formula obtained by the substitution of the formula Δ(ϕ,ψ) at every occurrence of p in δ(p).
Definition 5.2**.**
[5, Definition 2.8]*, [15, Definition 3.11]
Let ⟨L,⊢L⟩ be a logic and K an algebraic semantics for
⟨L,⊢L⟩ with defining identities δi=ϵi, for i<n.
K is said to be “equivalent to” ⟨L,⊢L⟩ if there exists a finite set Δj(p,q), for j<m, of formulas with two variables p,q such that*
for every identity ϕ≈ψ, for i<n, and for j<m,
[TABLE]
The set Δj(p,q), j<m, of formulas with two variables, satisfying (E) is called a set of “equivalence formulas” for ⟨L,⊢L⟩ and K.
A logic L is said to be “algebraizable” if and only if it has an equivalent algebraic semantics K.
The following theorem, proved in [5], is crucial in what follows.
Theorem 5.3**.**
([5], [15, Proposition 3.15])
Every implicative logic L is algebraizable with respect to the class Alg∗L and the algebraizability is witnessed by the defining identity p≈p→p and the equivalence formulas
Δ={p→q,q→p}.
As an immediate consequence of Theorem 5.3, Theorem 3.7 and Theorem 4.5, we obtain the following
crucial result.
Corollary 5.4**.**
*The logic DHMSH is algebraizable, and the variety
DHMSH is the equivalent algebraic semantics for DHMSH with the defining identity p≈p→Hp *(equivalently, p≈1) and the equivalence formulas Δ={p→Hq,q→Hp}.
Also, we just mention, in passing, the following fact which follows from Theorem 5.3, Lemma 3.6 and Theorem 4.2 about the semi-intuitionistic logic SH.
Corollary 5.5**.**
*The logic SI is algebraizable, and the variety
SH is the equivalent algebraic semantics for SI with the defining identity p≈p→Hp and the equivalence formulas Δ={p→Hq,q→Hp}.
5.1. Axiomatic Extensions of DHMSH
A logic L′ is an axiomatic extension of L if L′ is obtained by adjoining new axioms but keeping the rules of inference the same as in L.
In the sequel, we sometimes use the term “extension” for “axiomatic extension”. Let Ext(L) denote the lattice of axiomatic extensions of the logic L and
LV(K) denote the lattice of subvarieties of the variety K of algebras.
The following theorem is one of the hallmark accomplishments of Abstract Algebraic Logic.
Theorem 5.6**.**
[15, Theorem 3.33]*
Let L be an algebraizable logic with the equivalent algebraic semantics K. Then
Ext(L) is dually isomorphic to LV(K).*
The following theorem is a consequence of Theorem 5.6, Theorem 4.5 and
Corollary 5.4.
Theorem 5.7**.**
(Isomorphism Theorem for DHMSH)*
Ext(DHMSH) is dually isomorphic to LV(DHMSH).*
In a similar fashion, the following result is a consequence of Theorem 5.6, Theorem 2.2 and
Corollary 5.5.
Theorem 5.8**.**
(Isomorphism Theorem for SH)*
Ext(SH) is dually isomorphic to LV(SH).*
The following theorem is an immediate consequence of Theorem 5.7 and plays an important role in the rest of the paper.
Let Mod(E):={A∈DHMSH:A⊨δ≈1,\mboxforeveryδ∈E}.
Theorem 5.9**.**
*Let E be an extension of the logic DHMSH. Then
*(a) E is algebraizable with the same equivalence formulas and defining equations as those of the logic DHMSH.
(b) Mod(E) is the equivalent algebraic semantics for E.
Note that Theorem 5.8 justifies the use of the phrase “the logic corresponding to the subvariety V” of DHMSH.
In the later sections of the paper, we give various applications of the results proved above and the algebraic results proved in [34, 35, 36, 37, 38].
We now give Hilbert-style axiomatizations for several important extensions of the logic DHMSH.
To facilitate the presentation of the extensions of the logic DHMSH, we first list several important subvarieties of the variety DHMSH of dually hemimorphic semi-Heyting algebras that were introduced (or implicit) in [34].
LIST 1: SOME IMPORTANT SUBVARIETIES OF THE VARIETY DHMSH
- (1)
DHMH: Dually hemimorphic Heyting algebras are DHMSH-algebras satisfying the identity:
(H): (x∧y)→x≈1.
2. (2)
OCKSH: Ockham semi-Heyting algebras are
DHMSH-algebras satisfying the identity:
(E5): (x∨y)′≈x′∧y′.
3. (3)
OCKH: Ockham Heyting algebras are
OCKSH-algebras satisfying the identity (H).
4. (4)
DmsSH: Dually ms semi-Heyting algebras are
OCKSH-algebras satisfying the identity:
(E6): x′′≤x.
5. (5)
DmsH: Dually ms Heyting algebras are DmsSH-algebras satisfying the identity (H).
6. (6)
DMSH: De Morgan semi-Heyting algebras are
OCKSH-algebras (or DHMSH-algebras) satisfying the identity
(E7): x′′≈x.
7. (7)
DMH: De Morgan Heyting algebras are DMSH-algebras satisfying the identity (H).
8. (8)
DSDSH: Dually semi-De Morgan semi-Heyting algebras
([32]) are DHMSH-algebras satisfying the identities:
(E8): (x∨y)′′≈x′′∨y′′,
(E9): x′′′≈x′.
9. (9)
DSDH:* Dually semi-De Morgan Heyting algebras are DSDSH-algebras satisfying the identity *(H).
10. (10)
DQDSH: Dually quasi-De Morgan semi-Heyting algebras ([32]) are
DSDSH-algebras satisfying the identity (E4).
11. (11)
DQDH: Dually quasi-De Morgan Heyting algebras are DQDSH-algebras satisfying the identity (H).
12. (12)
DPCSH: Dually pseudocomplemented semi-Heyting algebras are
DQDSH-algebras satisfying the identity:
(E10): x∨x′≈1.
13. (13)
DPCH: Dually pseudocomplemented Heyting algebras are
DPCSH-algebras satisfying the identity (H).
14. (14)
BDQDSH: *Blended dually quasi-De Morgan semi-Heyting algebras * are
DQDSH-algebras satisfying the identity:
(E11): (x∨x∗)′≈x′∧x∗′ (Blended ∨-De Morgan law).
15. (15)
BDQDH: *Blended dually quasi-De Morgan Heyting algebras * are
BDQDSH-algebras satisfying the identity (H).
16. (16)
SBDQDSH: Strongly blended dually quasi-De Morgan semi-Heyting algebras are DQDSH-algebras satisfying the identity:
(E12): (x∨y∗)′≈x′∧y∗′
(Strongly blended ∨-De Morgan law).
17. (17)
SBDQDH: *Strongly blended dually quasi-De Morgan Heyting algebras * are
SBDQDSH-algebras satisfying the identity (H).
18. (18)
DQDBSH: Dually quasi-De Morgan Boolean semi-Heyting algebras are
DQDSH-algebras satisfying the identity:
(E13): x∨x∗≈1.
19. (19)
DQDBH: *dually quasi-De Morgan Boolean Heyting algebras * are
DQDBSH-algebras satisfying the identity (H).
20. (20)
DQStSH: Dually quasi-Stone semi-Heyting algebras are
DHMSH-algebras satisfying the identities: (E4),
(E14): (x∨y′)′≈x′∧y′′ (weak ∨-De Morgan law),
(E15): x′∧x′′≈0 (Dual Stone identity).
21. (21)
DQStH: *Dually quasi-Stone Heyting algebras * are
DQStSH-algebras satisfying the identity (H).
22. (22)
BDQStSH: Blended dually quasi-Stone semi-Heyting algebras are
DQStSH-algebras satisfying the identity (E14).
23. (23)
BDQStH: *Blended dually quasi-Stone Heyting algebras * are
BDQStSH-algebras satisfying the identity (H).
24. (24)
SBDQStSH: Strongly blended dually quasi-Stone semi-Heyting algebras are DQStSH-algebras satisfying the identity (E12).
25. (25)
SBDQStH: *Strongly blended dually quasi-Stone Heyting algebras * are
SBDQStSH-algebras satisfying the identity (H).
26. (26)
DStSH:Dually Stone semi-Heyting algebras are DPCSH-algebras satisfying the identity (E15).
27. (27)
DStH:Dually Stone Heyting algebras are DStSH-algebras satisfying the identity (H).
28. (28)
DSCSH: *Dually semi-complemented semi-Heyting algebras * are
DHMSH-algebras satisfying the identity (E12).
29. (29)
DSCH: *Dually semi-complemented Heyting algebras * are
DSCSH-algebras satisfying the identity (H).
30. (30)
DDPCSH: Dually demi-pseudocomplemented semi-Heyting algebras are DSDSH-algebras satisfying the identity:
(E16): x′∨x′′≈1.
31. (31)
DDPCH: *Dually demi-pseudocomplemented Heyting algebras * are
DDPCSH-algebras satisfying the identity (H).
32. (32)
DAPCSH: Dually almost pseudocomplemented semi-Heyting algebras are
DDPCSH-algebras in which ′ satisfies the identity dual to (E18).
33. (33)
DAPCH: *Dually almost pseudocomplemented Heyting algebras * are
DAPCSH-algebras in which ′ satisfies the identity (H).
Next, we present Hilbert-type axiomatizations for the (new) logics that are extensions of DHMSH and that correspond to the subvarieties of DHMSH mentioned in LIST 1. For the relationships of these logics to the varieties in LIST 1, the reader is referred to Theorem 5.10 below.
LIST 2: SOME IMPORTANT EXTENSIONS OF DHMSH
- (1)
DHMH: The dually hemimorphic Heyting logic is the extension of DHMSH given by
(A15): (α∧β)→α.
2. (2)
OCKSH: The Ockham semi-Heyting logic is the extension of DHMSH given by
(A16): ∼(α∨β)→H(∼α∧∼β),
(A17): (∼α∧∼β)→H ∼(α∨β).
3. (3)
OCKH: The Ockham Heyting logic is the extension of OCKSH given by
(A1).
4. (4)
DmsSH: The dually ms semi-Heyting logic is the extension of OCKSH given by
(A18): ∼∼α→Hα.
5. (5)
DmsH: The dually ms Heyting logic is the extension of DmsSH given by (A1).
6. (6)
DMSH: The De Morgan semi-Heyting logic is the extension of OCKSH given by (A4) and
(A19): α→H ∼∼α.
7. (7)
DMH: The De Morgan Heyting logic is the extension of DMSH given by (A1).
8. (8)
DSDSH: The dually semi-De Morgan semi-Heyting logic is the extension of DHMSH given by
(A20): ∼∼(α∨β)→H(∼∼α ∨ ∼∼β),
(A21): (∼∼α ∨ ∼∼β)→H ∼∼(α∨β),
(A22): ∼∼∼α→H ∼α,
(A23): ∼α→H ∼∼∼α.
9. (9)
DSDH: The dually semi-De Morgan Heyting logic is the extension of DSDSH given by (A1).
10. (10)
DQDSH: The dually quasi-De Morgan semi-Heyting logic is the extension of DSDSH given by (A4).
11. (11)
DQDH: The dually quasi-De Morgan Heyting logic is the extension of DQDSH given by (A1).
12. (12)
DPCSH: The dually pseudocomplemented semi-Heyting logic is the extension of DQDSH given by
(A24): α ∨ ∼α.
13. (13)
DPCH: The dually pseudocomplemented Heyting logic is the extension of DPCSH given by (A1).
14. (14)
BDQDSH: The blended dually quasi-De Morgan semi-Heyting logic is the extension of DQDSH given by
(A25): ∼(α∨(α→⊥))→H(∼α ∧ ∼(α→⊥)),
(A26): (∼α ∧ ∼(α→⊥))→H ∼(α ∨ (α→⊥)).
15. (15)
BDQDH: The blended dually quasi-De Morgan Heyting logic is the extension of BDQDSH given by
(A1).
16. (16)
SBDQDSH: The strongly blended quasi-De Morgan semi-Heyting logic is the extension of DQDSH given by
(A27): ∼(α∨(β→⊥))→H(∼α ∧ ∼(β→⊥)),
(A28): (∼α ∧ ∼(β→⊥))→H ∼(α∨(β→⊥)).
17. (17)
SBDQDH: The strongly blended dually quasi-De Morgan Heyting logic is the extension of SBDQDSH given by
(A1).
18. (18)
DQDBSH: The dually quasi-De Morgan Boolean semi-Heyting logic is the extension of DQDSH given by (A15).
(A29): α∨(α→⊥).
19. (19)
DQDBH: The dually quasi-De Morgan Boolean Heyting logic is the extension of DQDBSH given by (A1).
20. (20)
DQStSH: The dually quasi-Stone semi-Heyting logic is the extension of DHMSH given by
(A4) and the following axioms:
(A30): ∼(α ∨ ∼β)→H(∼α ∧ ∼∼β),
(A31): (∼α ∧ ∼∼β)→H ∼(α ∨∼β),
(A32): (∼α ∧∼∼α)→H⊥.
21. (21)
DQStH: The dually quasi-Stone Heyting logic is the extension of DQStSH given by
(A1).
22. (22)
BDQStSH: The blended dually quasi-Stone semi-Heyting logic is the extension of DHMSH given by (A4), (A14), (A14), (A20), (A20) and (A20).
23. (23)
BDQStH: The blended dually quasi-Stone Heyting logic is the extension of BDQStSH given by
(A1).
24. (24)
SBDQStSH: The strongly blended dually quasi-Stone semi-Heyting logic is the extension of DHMSH given by (A4), (A16), (A16), (A20), (A20) and (A20).
25. (25)
SBDQStH: The strongly blended dually quasi-Stone Heyting logic is the extension of SBDQStSH given by
(A1).
26. (26)
DStSH: The dually Stone semi-Heyting logic is the extension of DPCSH given by (A32).
27. (27)
DStH: The dually Stone Heyting logic is the extension of DStSH given by (A15).
28. (28)
DSCSH: The dually semi-complemented semi-Heyting logic is the extension of DHMSH given by (A12).
29. (29)
DSCH: The dually semi-complemented Heyting logic is the extension of DSCSH given by (A1).
30. (30)
DDPCSH: The dually demi-pseudocomplemented semi-Heyting logic is the extension of
DSDSH given by
(A33): ∼α ∨ ∼∼α.
31. (31)
DDPCH: The dually demi-pseudocomplemented Heyting logic is the extension of DDPCSH given by (A1).
32. (32)
DAPCSH: The dually almost pseudocomplemented semi-Heyting logic is the extension of DDPCSH given by
∼∼α→Hα.
33. (33)
DAPCH: The dually almost pseudocomplemented Heyting logic is the extension of DAPCSH given by (A1).
The following theorem which is immediate from Theorem 5.9 describes the correspondence between the logics in LIST 2 and the varieties in LIST 1.
Theorem 5.10**.**
Let Vi be the variety of algebras mentioned in the i-th item of LIST 1 and Vi be the logic appearing in the i-th item of LIST 2. Then, the logic Vi corresponds to the variety Vi in the sense that Vi is its equivalent algebraic semantics for Vi.
In the figure below, we present a (partial) poset describing the mutual relationships among the varieties, whose names end with “SH”, mentioned in PART 1 above. The dual of this poset will show the relations among the logics, whose names end with “SH”, presented in PART 2, T being the trivial variety. Note that the links do not necessarily represent covers.
\mathbb{T}$$\mathbb{V}(\mathbf{2}^{e})$$\mathbb{V}(\mathbf{\bar{2}^{e}})$$\mathbb{V}(\mathbf{2^{e}},\mathbf{\bar{2}^{e}})$$\mathbb{DS}\rm t\mathbb{SH}$$\mathbb{DQDBSH}$$\mathbb{DPCSH}$$\mathbb{DMSH}$$\mathbb{SBDQDSH}$$\mathbb{SBDQS}\rm t\mathbb{SH}$$\mathbb{DAPCSH}$$\mathbb{BDQDSH}$$\mathbb{D}{\rm ms}\mathbb{SH}$$\mathbb{BDQS}\rm t\mathbb{SH}$$\mathbb{DDPCSH}$$\mathbb{DQDSH}$$\mathbb{DQS}\rm t\mathbb{SH}$$\mathbb{DSDSH}$$\mathbb{OCKSH}$$\mathbb{DHMSH}$$\mathbb{DSCSH}Figure 1
PARTIAL POSET OF SUBVARIETIES OF DHMSH
Note that it is not yet known if DPCSH⊂SBDQDSH, although we conjecture it to be true. So we mention the following open problem.
PROBLEM: Is DPCSH⊂SBDQDSH? In particular, is DPCH⊂SBDQDH?
Corollary 5.11**.**
The (Moisil’s) logic LM is equivalent to the logic DMH.
**Proof **
We know from Moisil’s result (see Monteiro [26]) that LM corresponds to DMH. Also, observe from Theorem 5.10 that the logic DMH correspond to DMH as well.
\hfill□
Definition 5.12**.**
Let L be an algebraizable logic.
We say that L is a discriminator logic if its corresponding (quasi-) variety is a discriminator variety. Furthermore, L is a (quasi)primal logic if its corresponding (quasi-) variety is a variety generated by a (quasi)primal algebra.
The classical logic is the first well-known example of a primal logic (as the Boolean algebra 2 is a primal algebra).
Remark 5.13**.**
It was shown in [34] that the variety RDQDStSH1 is a discriminator variety. Thus RDQDStSH1 is a discriminator logic. Most of the logics considered in the rest of this paper are discriminator logics. We will point them out as they appear.
We conclude this section by noting that
the lattice of extensions of the logic DMH is an interval of the lattice of extensions of DMSH, which, in turn, is an interval in the lattice of extensions of DHMSH.
6. The Deduction Theorem in extensions of DHMSH
In this section we first show that the “usual” form of the Deduction Theorem” fails in the logic DHMSH, and then characterize those extensions of DHMSH where it does hold.
A logic L is said to have the Deduction Property for the connective → if the following statement holds:
[TABLE]
for all Γ∪{α,β}⊆\mboxFm.
In the logic SI the Deduction Property for the conective →H is known to hold [7, Theorem 3.18]. But, this property fails in the logic DHMSH, as shown in the following remark.
Remark 6.1**.**
First, we note, by Lemma 3.4 (b), that
[TABLE]
*Consider the algebra L1dm∈DHMSH defined in Section *8. Observe that L1dm ⊨DHMSH (x→Hy)→H(y′→Hx′)≈1 (by taking x=1 and y=a). Hence, DHMSH⊨(x→Hy)→H(y′→Hx′)≈1 and therefore, by Theorem 4.5,
[TABLE]
Thus, the Deduction Property fails in DHMSH, in view of (6.1).
We now wish to characterize the extensions of
DHMSH in which the Deduction Property holds. For this, we need a preliminary lemma.
Lemma 6.2**.**
Let E be an extension of the logic DHMSH such that
[TABLE]
Then E satisfies the Deduction Property for the connective →H.
**Proof **
Assume that Γ∪{ϕ}⊢Eψ. We shall prove Γ⊢Eϕ→Hψ by induction on the proof for ψ. By hypothesis,
[TABLE]
If ψ is an axiom of E or a formula in Γ, then Γ⊢Eψ. By Lemma 3.3, part (a) we have Γ⊢Eϕ→Hψ.
Let us assume that Γ∪{ϕ}⊢Eψ is the result of applying the rule (SMP). Then we may assume that there is some formula α such that Γ∪{ϕ}⊢Eα and Γ∪{ϕ}⊢Eα→Hψ. So, by inductive hypothesis, we have,
-
Γ⊢Eϕ→Hα,
2. 2.
Γ⊢Eϕ→H(α→Hψ),
3. 3.
Γ⊢Eϕ→Hϕ by Lemma 3.3, part (b),
4. 4.
Γ⊢Eϕ→H(ϕ∧α) by (A2.1) and SMP applied to 1 and 3,
5. 5.
Γ⊢E(ϕ∧α)→Hψ by (A2.1) and SMP applied to 2,
6. 6.
Γ⊢Eϕ→Hψ by Lemma 3.3 (d) and SMP applied to 4 and 5.
Assume that Γ∪{ϕ}⊢Eψ is the result of applying the rule (SCP). Hence ψ= ∼β→H∼α and Γ∪{ϕ}⊢Eα→Hβ. By induction we have that
-
Γ⊢Eϕ→H(α→Hβ),
2. 2.
Γ⊢E(α→Hβ)→H(∼β→H ∼α) by (6.2),
3. 3.
Γ⊢Eϕ→H(∼β→H ∼α) by 3.3 (d) and SMP applied to 1 and 2.
For the other implication, we assume that Γ⊢Eϕ→Hψ. Then Γ∪{ϕ}⊢Eϕ→Hψ. Since Γ∪{ϕ}⊢Eϕ, we have Γ∪{ϕ}⊢Eψ by (SMP).
\hfill□
Theorem 6.3**.**
The Deduction Property holds in an extension E of the logic DHMSH for the connective →H if and only if E⊢(α→H β)→H( ∼β→H ∼α).
**Proof **
Let us assume that the Deduction Property holds in E for the conective →H. Note that α→Hβ⊢E α→Hβ and
α→Hβ⊢E ∼β→H ∼α by (SCP). Hence
⊢E(α→H β)→H(∼β→H ∼α) by Deduction Property, or equivalently, E⊢DHMSH(α→H β)→H(∼β→H∼α).
For the converse, let us assume that E⊢(α→H β)→H(∼β→H∼α). By Lemma 6.2, the Deduction Property holds in E for the conective →H.
\hfill□
Recall that semi-Heyting algebras are pseudocomplemented with x∗:=x→0 as the pseudocomplement of x. A semi-Heyting algebra L is a Stone semi-Heyting algebra if L satisfies the Stone identity: x∗∨x∗∗≈1. Let StSH
denote the variety of Stone semi-Heyting algebras.
Recall also that if A is a semi-Heyting algebra, then ⟨A,∨,∧,→H0,1⟩ is a Heyting algebra.
Lemma 6.4**.**
Let A∈DHMSH such that A⊨(x→Hy)→H(y′→Hx′)≈1. Then
- (a)
A⊨x∧x′≈0,**
2. (b)
A⊨x∗≈x′,
3. (c)
A⊨x∗∨x∗∗≈1.**
**Proof **
Let a∈A.
- (a)
Since a→H(a′→H0)=(1→Ha)→H(a′→H0)=(1→Ha)→H(a′→H1′)=1 in view of hypothesis, we have that a∧(a′→H0)=a∧(a→H(a′→H0))=a∧1=a. Hence
[TABLE]
Then,
a∧a′
=(\refequation26021902)a∧(a′→H0)∧a′
=a∧(a′→0)∧a′
=a∧a′∧0
=0, proving (a).
2. (b)
Observe that a∗→Ha′=a∗→H(1→Ha′)=(a→H0)→H(1→Ha′)=(a→H0)→H(0′→Ha′)=1 by hypothesis. Hence
[TABLE]
Next,
a′∧a∗
=a′∧(a→0)
=a′∧((a′∧a)→(a′∧0))
=(\ref27021901)a′∧(0→0)
=a′.
Hence A⊨x′≤x∗.
Now, using (6.4) we conclude that a′=a∗.
3. (c)
a∗∨a∗∗
=(\ref26021903)a′∨a′′
=(E\refinfDMlaw)(a∧a′)′
=(\ref27021901)0′
=1,
proving the lemma.
\hfill□
Lemma 6.5**.**
Let A∈DHMSH. Then the following conditions are equivalent in the algebra A.
- (1)
(x→Hy)→H(y′→Hx′)≈1,
2. (2)
x∗≈x′.
**Proof ** Let a,b∈A.
Observe that (1) implies (2) from Lemma 6.4.
For the converse, suppose A satisfies the identity (2). Then, using (SH3) and the fact that →H is a Heyting implication, we have that (a→Hb)→H(b′→Ha′)=(a→Hb)→H(b∗→Ha∗)=(b∗∧(a→Hb))→Ha∗=(b∗∧(((b∗∧a)→H(b∗∧b))→Ha∗=(b∗∧((b∗∧a)→H0))→Ha∗=(b∗∧(a→H0))→Ha∗=(b∗∧a∗)→Ha∗=1, proving (1).
\hfill□
Lemma 6.6**.**
Let L be a Stone semi-Heyting algebra. Let Le be the expansion of L to the language ⟨∨,∧,→,′,0,1⟩, where we define ′ by: x′:=x∗.
Then
- (1)
Le∈DHMSH* and satisfies the identity: x′≈x∗,*
2. (2)
Le⊨(x∨y)′′≈x′′∨y′′.
**Proof **
The lemma clearly follows from the well-known facts that L⊨(x∨y)∗≈x∗∧y∗ and L⊨(x∧y)∗≈x∗∨y∗.
\hfill□
We will refer to the algebra Le as an “essentially a Stone semi-Heyting algebra”.
For V a subvariety of StSH, we let
[TABLE]
It is clear that Ve is a subvariety of DHMSH.
We are now ready to present our main result of this section that describes precisely those extensions of the logic DHMSH that have the Deduction Property. The following theorem is immediate from Theorem 6.3, Lemma 6.5 and Lemma 6.6.
Theorem 6.7**.**
The Deduction Property holds in an extension E of the logic DHMSH for the connective →H if and only if the corresponding variety E is of the form
Ve, where V⊆StSH.
6.1. Deduction Theorem in the Extensions of the logic DQDSH
Recall that the variety DQDSH of dually quasi-De Morgan semi-Heyting algebras
and the corresponding extension DQDSH of DHMSH were defined in Section 5.
In this section we show that Theorem 6.7 can be significantly improved for the extensions of the logic DQDSH. In fact, we shall give an explicit description of the extensions of the logic DQDSH in which the Deduction Property holds.
For this purpose we need the following 2-element semi-Heyting algebras, 2 and 2ˉ
which are, up to isomorphism, the only two 2-element algebras in SH.
2:
→:
0
1
0
1
1
1
0
1
2ˉ:
→:
0
1
0
1
0
1
0
1
Figure 2
The algebras 2e and 2ˉe denote the expansions of the semi-Heyting algebras
2 and 2ˉ by the unary operation ′ defined as follows: 0′=1 and 1′=0. It is clear that 2e and 2ˉe are, up to isomorphism, the only two 2-element algebras in DQDSH (in fact, in DMSH).
Lemma 6.8**.**
Let V be a subvariety of DQDSH such that V⊨(x→Hy)→(y′→Hx′)≈1. Then,
V⊆V(2e,2ˉe), where V(2e,2ˉe) denotes the variety generated by
{2e,2ˉe}.
**Proof **
The hypothesis and Lemma 6.5 (b) imply that V⊨x′≈x∗. Hence
V ⊆ V(2e,2ˉe) by [34, Theorem 5.11].
\hfill□
The following theorem describes precisely those extensions of DQDSH in which the Deduction Property holds. Let T denote the trivial variety.
Theorem 6.9**.**
The Deduction Property holds in a logic E∈Ext(DQDSH) for →H if and only if the corresponding variety is either either T or V(2e) or V(2ˉe) or V(2e,2ˉe).
**Proof **
The theorem is immediate in view of Theorem 5.9, Theorem 6.3,
and Lemma 6.8.
\hfill□
Since DMSH⊆DQDSH and DPCSH⊆DQDSH (see [34]), the following corollaries are immediate.
Corollary 6.10**.**
The Deduction Property holds in a logic E∈Ext(DMSH) for →H if and only if the corresponding variety is either T or V(2e) or V(2ˉe) or V(2e,2ˉe).
Corollary 6.11**.**
The Deduction Property holds in a logic E∈Ext(DPCSH) for →H if and only if the corresponding variety is either T or V(2e) or V(2ˉe) or V(2e,2ˉe).
7. Logics in Ext(DQDSH) corresponding to subvarieties of DQDSH generated by finitely many finite algebras
In this section, as applications of Theorem 5.9 and the algebraic results from [34], we will present several extensions of the logic DQDSH corresponding to subvarieties of DQDSH generated by finitely many finite algebras, thus providing a solution to PROBLEM 2.
7.1. 2-valued Extensions of DQDSH
It was shown in Theorem 6.9 that the Deduction Property holds in an extension of the logic
DQDSH if and only if the corresponding variety is a subvariety of V(2e,2ˉe). So, it is only natural to ask for the axiomatizations of the extensions of the logic DQDSH corresponding to the subvarieties of V(2e,2ˉe).
The variety V(2e,2ˉe) and its only non-trivial proper subvarieties V(2e) and V(2ˉe) were axiomatized in [34, Theorem 5.11]. V(2e,2ˉe) is defined by the identity: x≤x′∗ (equivalently, x≈x′∗), relative to the variety DQDSH.
The varieties V(2e) and V(2ˉe) are defined, respectively, by the identities: 0→1≈1 and 0→1≈0,
relative to V(2e,2ˉe).
In view of these observations,
we obtain from Theorem 5.9, the following corollaries defining their corresponding logics.
Let L(2e,2ˉe) (or L(V(2e,2ˉe))) be the extension of the logic DQDSH corresponding to the variety V(2e,2ˉe). Let α⇔Hβ denote the formula: (α→Hβ)∧(β→Hα).
Corollary 7.1**.**
The logic L(2e,2ˉe) is defined, as an extension of the logic DQDSH,
by the axiom:
- (∼ϕ→⊥)⇔Hϕ.
Let L(2e) (or L(V(2e))) and L(2ˉe) (or L(V(2ˉe))) denote, respectively, the extensions of the logic L(2e,2ˉe) corresponding to the varieties V(2e) and V(2ˉe).
Corollary 7.2**.**
The logic L(2e) is defined, as an extension of the logic L(2e,2ˉe), by the axiom:
- ⊥→⊤.**
(We note that L(2e) is yet another axiomatization of the classical logic.).
Corollary 7.3**.**
The logic L(2ˉe) is defined, as an extension of the logic L(2e,2ˉe), by the axiom:
- (⊥→⊤)→H⊥*.
Remark 7.4**.**
Some features of the logics L(2ˉe) and L(2e):
*The logic L(2ˉe) is “anti-classical” or “contra-classical”
in the sense that the classically provable formula ⊥→⊤ fails in it. *
(It is somewhat perplexing to us that the intuitionists accept the principle that says, “False→True=True′′.)
The logics L(2ˉe) and L(2e) are coatoms in the lattice of extensions of the logic DMSH and hence that of DQDSH (and of DHMSH).
The implication → in L(2ˉe) is commutative.
The logics L(2ˉe) and L(2e) are not only disriminator logics, but, in fact, are primal logics, since 2e and (2ˉe) are primal algebras.
The logics L(2ˉe) and L(2e) do not have the Disjunction Property. (i.e., if α∨β is provable, then α is provable or β is provable.)
More features of the logic L(2ˉe) will be given in Remark 8.1 of Section 8.
Remark 7.5**.**
The Deduction Theorem holds only in the preceding three non-trivial logics in the lattice of extensions of the logic DQDSH, in view of Theorem 6.9.
7.2. 3-valued Extensions of the logic DQDSH
It was shown in [33] that there are, up to isomorphism, ten 3-element
semi-Heyting algebras whose → operations are defined in figure 2 below, where 0<a<1.
[math]
a
1
L1:
[TABLE]
[math]
a
1
L2:
[TABLE]
[math]
a
1
L3:
[TABLE]
[math]
a
1
L4:
[TABLE]
[math]
a
1
L5:
[TABLE]
[math]
a
1
L6:
[TABLE]
[math]
a
1
L7:
[TABLE]
[math]
a
1
L8:
[TABLE]
[math]
a
1
L9:
[TABLE]
[math]
a
1
L10:
[TABLE]
Figure 3
Since 0′=1 and 1′=0, it is easy to see that there are exactly two expansions on each of the above 10 semi-Heyting algebras by a unary operation ′ so that the expansions are DQDSH-algebras. Ten of these that correspond to a′=a are clearly in
DMSH.
The other ten, that correspond to a′=1 are in DPCSH.
To put it more precisely,
let Lidm, i=1,2,…,10, denote the expansion of Li by adding the unary operation ′ such that 0′=1, 1′=0, and a′=a, Similarly, let Lidp, i=1,2,…,10, denote the expansion of Li by adding the unary operation ′ such that 0′=1, 1′=0, and a′=1.
Then, clearly, Lidm∈DMSH and Lidp∈DPCSH.
Let Cdm:={Lidm:i=1,2,…,10}, Cdp:={Lidm:i=1,2,…,10} and let C20:=Cdm∪Cdp. Thus there are exactly 20 three-element
DQDSH-algebras, whose lattice reducts are chains.
Let
DQDSHC3:=V(C20), the subvariety of DQDSH generated by all the 20 3-element DQDSH-chains. Also, let DMSHC3:=V(Cdm) and let DPCSHC3:=V(Cdp).
We shall now present axiomatizations for the logics corresponding to DQDSHC3, DMSHC3, and DPCSHC3.
The following theorem is immediate from
[34, Lemma 10.2, Theorem 10.3, Corollary 10.4 and Theorem 11.1]. Let x+:=x′∗′. In the rest of the paper, “equational base” is abbreviated to “base”.
Theorem 7.6**.**
[34]**
A base for DQDSHC3, relative to DQDSH, is given by:
- (i)
x∗∗≈x∗′,
2. (ii)
x∧x+≤y∨y∗* *(Regularity).
The following theorem follows from
Theorem 5.9 and Theorem 7.6.
Theorem 7.7**.**
The logic DQDSHC3 corresponding to the variety
DQDSHC3 is defined, as an extension of DQDSH,
by the following axioms:
[(ϕ→⊥)→⊥]⇔H ∼(ϕ→⊥),
[ϕ ∧ ∼(∼ϕ→⊥)]→H[ψ∨(ψ→⊥)].
Since the logic DQDSHC3 is finitely axiomatized and the corresponding variety DQDSHC3=V(C20) is finitely generated, the following corollary is immediate.
Corollary 7.8**.**
The logic DQDSHC3 is decidable.
**Proof **
Observe that C20⊨x∗∨x∗∗≈1.
\hfill□
7.3. Logics DMSHC3 and DPCSHC3
We know from Section 7.2 that DMSHC3=V(Cdm), DPCSHC3=V(Cdp), Lidm∈DMSH and
Lidp∈DPCSH,
i=1,2,…,10.
The following theorem is immediate from Theorem 7.6.
Theorem 7.9**.**
A base for DMSHC3, relative to DQDSHC3, is given by:
- x′′≈x.
A base for DPCSHC3, relative to DQDSHC3, is given by:
- x∨x′≈1.
Let DMSHC3 and DPCSHC3
denote the extensions of
the varieties
DMSHC3 and DPCSHC3, respectively.
The following theorem is immediate from
Theorem 5.9 and Theorem 7.9.
Theorem 7.10**.**
DMSHC3*
is defined, as an extension of DQDSHC3
by the following axioms:*
- ϕ→H ∼∼ϕ.
- (b)
DPCSHC3* is defined, relative to the logic DQDSHC3
by the following axiom:*
- ϕ ∨∼ϕ.
It is clear that the logics DMSHC3 and DPCSHC3 are decidable.
7.4. 3-valued Extensions of DMSHC3 and of DPCSHC3
We are ready to look at the problem of axiomatization for the logics associated with the 20 3-element chains
in C20.
We need to recall another (algebraic) result from [34] that gives a base for each of 3-chains in Cdm and Cdp. To this end,
we need the
following identities from [34]:
- (C1)
x∨(x→y)≈(x→y)∗→x,
2. (C2)
x∨[y→(x∨y)]≈(0→x)∨(x→y),
3. (C3)
x∨(y→x)≈[(x→y)→y]→x,
4. (C4)
x∨(x→y)≈x→[x∨(y→1)],
5. (C5)
(x→y)→(0→y)≈x∨[(x∧y)→1],
6. (C6)
x∗∨(x→y)≈(x∨y)→y,
7. (C7)
x∨(0→x)∨(y→1)≈x∨[(x→1)→(x→y)],
8. (C8)
x∨y∨(x→y)≈x∨[(x→y)→1],
9. (C9)
x∨[(0→y)→y]≈x∨[(x→1)→y],
10. (C10)
x∨[x→(y∧(0→y))]≈x→[(x→y)→y],
11. (C11)
(0→1)∗=0,
12. (C12)
x∨y∨[y→(y→x)]≈x→[x∨(0→y)],
13. (C13)
x∨(x→y)≈x∨[(x→y)→1],
14. (C14)
0→1≈0 (FTF identity),
15. (C15)
x→y≈y→x (commutative identity).
In the sequel, we abbreviate
“is a base, relative to DMSHC3 [DPCSHC3]” to just “is a base”.
The reader should keep in mind that the following theorem is really a simultaneous presentation of two separate theorems (in order to keep the size of the paper within limits). One of the two theorems is regarding DMSHC3-algebras and the other is about DPCSHC3-algebras.
As an illustration, item (i), when decoded, yields the following two (independent) statements:
(idm): {(C1)} is a base, relative to DMSHC3, for the variety V(L1dm),
and
(idp): {(C1)} is a base, relative to DPCHC3, for the variety V(L1dp).
Similar remark applies to each of the other items of Theorem 7.11 as well.
Theorem 7.11 is immediate from [34, Theorem 11.2].
Theorem 7.11**.**
{(C1)}* is a base for the variety V(L1dm) [V(L1dp)],*
{(C2), (C3)}* is a base for the variety V(L2dm) [V(L2dp)],*
{(C2), (C4)}* is a base for the variety V(L3dm) [V(L3dp)],*
{(C4), (C5)}* is a base for the variety V(L4dm) [V(L4dp)],*
{(C7)}* is a base for the variety V(L5dm) [V(L5dp)],*
{(C8)}* is a base for the variety V(L6dm) [V(L6dp)],*
{(C9), (C10)}* is a base for the variety V(L7dm) [V(L7dp)],*
{(C11), (C12)}* is a base for the variety V(L8dm) [V(L8dp)],*
{(C6), (C13), (C14)}* is a base for the variety V(L9dm) [V(L9dp)],*
{(C15)}* is a base for the variety V(L10dm) [V(L10dp)].*
We are now ready to present the axiomatizations for the logics associated with the 20 3-element chains
in C20.
Let L(Lidm) (or L(V(Lidm)))
denote the extension of the logic DMSHC3
corresponding to the variety V(Lidm),
for i=1,2,⋯,10.
Also, let L(Lidp) (or L(V(Lidp)))
denote the extension of the logic DPCSHC3 corresponding to the variety V(Lidp).
In what follows, “defined, as an extension of the logic
DMSHC3 [DPCSHC3],
by” is abbreviated to “defined by”. The following theorem will follow from
Theorem 5.9, Theorem 7.9, Theorem 7.10, and Theorem 7.11.
Theorem 7.12**.**
L(L1dm)* [L(L1dp)] is defined
by the following axiom:*
- [ϕ∨(ϕ→ψ)]⇔H[((ϕ→ψ)→⊥)→ϕ].
- (b)
L(L2dm)* [L(L2dp)] is
defined by the following axioms:*
[ϕ∨{ψ→(ϕ∨ψ)}]⇔H[(⊥→ϕ)∨(ϕ→ψ)],
[ϕ∨(ψ→ϕ)]⇔H[{(ϕ→ψ)→ψ}→ϕ].
L(L3dm)* [L(L3dp)] is defined by the following axioms:*
[ϕ∨{ψ→(ϕ∨ψ)}]⇔H[(⊥→ϕ)∨(ϕ→ψ)]*,
*
[ϕ∨(ϕ→ψ)]⇔H[ϕ→{ϕ∨(ψ →⊤)}].
L(L4dm)* [L(L4dp)] is defined by the following axioms:*
[ϕ∨(ϕ→ψ)]⇔H[ϕ→{ϕ∨(ψ →⊤)}],
[(ϕ→ψ)→(⊥→ψ)]⇔H[ϕ∨{(ϕ∧ψ)→⊤}].
L(L5dm)* [L(L5dp)] is defined
by the following axiom:*
- [ϕ∨(⊥→ϕ)∨(ψ→⊤)]⇔H[ϕ∨{(ϕ→⊤)→(ϕ →ψ)}].
- (f)
L(L6dm)* [L(L6dp)] is defined by the following axiom:
*
- [ϕ∨ψ∨(ϕ→ψ)]⇔H[ϕ∨{(ϕ→ψ)→⊤}].
- (g)
L(L7dm)* [L(L7dp)] is
defined by the following axioms:*
[ϕ∨{(⊥→ψ)→ψ}]⇔H[ϕ∨{(ϕ→⊤)→ψ}],
[(ϕ∨{ϕ→(ψ∧(⊥→ψ))}]⇔H[ϕ→{(ϕ→ψ)→ψ}].
L(L8dm)* [L(L8dp)] is
defined
by the following axioms:*
((⊥→⊤)→⊥)→H⊥,
[(ϕ∨ψ∨{ψ→(ψ→ϕ)}]⇔H[ϕ→{ϕ∨(⊥→ψ)}]*.
*
L(L9dm)* [L(L9dp)] is
defined by the following axioms:*
[ϕ∗∨(ϕ→ψ)]⇔H[(ϕ∨ψ)→ψ],
[ϕ∨(ϕ→ψ)]⇔H[ϕ∨{(ϕ→ψ)→⊤}],
(⊥→⊤)→H⊥.
L(L10dm)* [L(L10dp)] is
defined by the following axioms:*
- (ϕ→ψ)→H(ψ→ϕ).
Remark 7.13**.**
Some features of these logics:
The logics L(Lidp),i∈{2,3,…,10} and the logics L(Lidm),i∈{2,3,…,10} are, just
like the logic L(2ˉe), “anti-classical”
in the sense that the classically provable formula ⊥→⊤ fails in these logics.
Each of the logics L(Lidp),i∈{5,6,7,8} and L(Lidp),i∈{5,6,7,8}, just like L(2e) and L(2ˉe), is a coatom in the lattice of extensions of the logic DQDSH.
Each of the logics L(Lidp),i∈{1,2,3,4} and L(Lidm),i∈{1,2,3,4} is covered by the coatom L(2e), the classical propositional logic, while each of the logics L(Lidp),i∈{9,10} and L(Lidm),i∈{9,10} is covered by the coatom L(2ˉe).
In the logics L(Lidp),i∈{9,10} and L(Lidm),i∈{9,10}, Moreover, in the logics L(L10dp) and L(L10dm),
the connective → is commutative.
The logics L(Lidm), and
L(Lidp), i=1,2,⋯,10, do not have the (DP) as the formula α∗∨α∗∗ is provable in these logics.
The logics L(Lidp),i∈{1,2,3,⋯,10} and the logics L(Lidm),i∈{1,2,3,⋯,10} are quasiprimal in the sense that their corresponding varieties are quasiprimal ([34].
Each of the logics L(Lidp),i∈{5,6,7,8} and L(Lidp),i∈{5,6,7,8}, just like L(2e) and L(2ˉe), is primal.
Further features of some of these logics will be given in Remark 8.1.
We note that all the logics mentioned in this subsection are decidable as their corresponding varieties are easily seen to have the finite model property.
7.5. 3-valued Łukasiewicz Logic Revisited
It is worthwhile to point out that the logic L(L1dm), defined earlier, has an interesting relationship with the well-known 3-valued Łukasiewicz logic. Let us recall the definition of 3-valued Łukasiewicz algebras.
An algebra A=⟨A,∨,∧,′,d1,d2,0,1⟩ is a 3-valued Łukasiewicz algebras if
- (1)
⟨A,∨,∧,′,0,1⟩ is a De Morgan algebra,
2. (2)
di(x∨y)=di(x)∨di(y), for i=1,2,
3. (3)
di(x)∨(di(x))′=1, for i=1,2,
4. (4)
di(dj(x))=dj(x), for i=1,2,
5. (5)
di(x′)=(d3−i(x))′, for i=1,2,
6. (6)
d1(x)≤d2(x),
7. (7)
If d1(x)=d1(y) and d2(x)=d2(y) then x=y.
Let L=⟨{0,a,1},∨,∧,′.d1,d2,0,1⟩ be the algebra such that
⟨{0,a,1},∨,∧,′,0,1⟩ is a 3-element Kleene algebra with 0<a<1, and d1 and d2 are unary operations defined as follows: d1(0)=d1(a)=0,d1(1)=1, and d2(0)=0, and d2(1)=d2(a)=1. Then it is routine to verify that L is a 3-valued Łukasiewicz algebra.
It is well-known that V(L) is precisely the variety of all 3-valued Łukasiewicz algebras.
Theorem 7.14**.**
The logic L(L1dm) is equivalent to the 3-valued Łukasiewicz logic.
**Proof **
It suffices to prove that the variety V(L1dm) is term-equivalent to the variety V(\L). Without loss of generality, we can assume that L1dm and \L have the same universe, say L={0,a,1} with 0<a<1. Given L1dm,
define the unary operations d1 and d2 on L by: d1(x)=x′∗ and d2=x∗′. Then it is straightforward to verify that ⟨L;∨,∧,′,d1,d2,0,1⟩=\L. To prove the converse, let us first define the unary function ∗ on L by: x∗:=d1((d2(x))′). It is routine to verify that ∗ is the pseudocomplement operation on L. Using ∗ we can now define the Katriňák’s implication → by:
[TABLE]
Then, → is the Heyting implication (see [19]). Hence, it follows that ⟨L;∨,∧,→,′,0,1⟩=L1dm.
The theorem is now proved.
\hfill□
7.6. 4-valued Extensions of DQDSH with Boolean semi-Heyting Reducts
Recall that the variety DQDSH was defined in Section 5.
An algebra L is a dually quasi-De Morgan Boolean semi-Heyting algebra (DQDBSH-algebra, for short)
if its term-reduct
⟨L,∨,∧,∗,0,1⟩ is a Boolean semi-Heyting algebra, that is, L⊨x∨x∗≈1. The variety of such algebras is denoted by DQDBSH.
The following theorem is now immediate, in view of Theorem 5.9.
Theorem 7.15**.**
The logic DQDBSH is
defined, relative to DQDSH by the following
axiom:
ϕ∨(ϕ→⊥).**
The concrete description of the lattice of subvarieties of DQDBSH was given in [34]. We now wish to present the axiomatizations for corresponding extensions of the logic DQDBSH. Toward this end, the following three algebras will be needed.
Figure 3 defines the → operation on the three 4-element algebras D1, D2 and D3, each of whose lattice reduct is the 4-element Boolean lattice
having the universe {0,a,b,1}, with b as the complement of a, and ′ is defined as follows: a′=a, b′=b, 0′=1 and 1′=0.
\begin{picture}(15.0,4.0)\par\par\put(1.0,2.5){D1 \ :}
\par\put(8.5,2.5){D2 \ :}
\par\par\put(2.2,2.5){\begin{tabular}[]{c|cccc}→&\ 0&\ 1&\ a&\ b\
\hline\cr&&&&\
0&1&0&b&a\
&&&&\
1&0&1&a&b\
&&&&\
a&b&a&1&0\
&&&&\
b&a&b&0&1\
\end{tabular}
}
\put(9.5,2.5){\begin{tabular}[]{c|cccc}→&\ 0&\ 1&\ a&\ b\
\hline\cr&&&&\
0&1&1&1&1\
&&&&\
1&0&1&a&b\
&&&&\
a&b&1&1&b\
&&&&\
b&a&1&a&1\
\end{tabular}
}
\end{picture}
D1:
D2:
[TABLE]
[TABLE]
D3:
[TABLE]
Figure 4
The algebras D1, D2, and D3 are the only simple (=subdirectly irreducible) algebras in DQDBSH.
The following theorem, which follows immediately from [34, Corollary 9.4], reveals the structure of DQDBSH.
Theorem 7.16**.**
DQDBSH=V(D1,D2,D3)=DMBSH.
The above theorem leads us to the following decidability result, in view of Theorem 5.9.
Corollary 7.17**.**
The logic DQDBSH is decidable.
We will now turn our attention to the axiomatization of logics corresponding to the varieties generated by these algebras. The following theorem is taken from [34, Theorem 9.5].
Theorem 7.18**.**
A base for the variety V(D1), modulo DQDBSH, is given by
0→1≈0,
A base for V(D2), modulo DQDBSH, is given by
0→1≈1,
A base for the variety V(D3), modulo DQDBSH, is given by
(0→1)′≈0→1.
The following corollary will now follow as an application of
Theorem 5.9, Theorem 7.16 and Theorem 7.18.
Let L(Di) (or L((V(Di))))
denote the extension of the logic DMBSH
corresponding to the variety V(Di) for i=1,2,3.
In the rest of this section, “defined, relative to the logic DMBSH, by” is abbreviated to “defined by”.
Corollary 7.19**.**
The logic L(D1) is defined by the axiom:
- (⊥→⊤)→H⊥,
- (2)
The logic L(D2) is defined by the axiom:
The logic L(D3) is defined by the axiom:
- ∼(⊥→⊤)⇔H(⊥→⊤).
It is clear that the logics L(Di),i∈{1,2,3}, are decidable.
Remark 7.20**.**
Some features of these logics:
The logics L(Di),i∈{1,3}, are anti-classical since the formula ⊥→⊤ is not provable in each of them.
The logics L(D1) and L(D2),
are covered, respectively, by the coatoms L(2ˉe) and L(2e) in the lattice of extensions of the logic DQDSH.
In the logic L(D1),
the connective, →, is commutative.
The logics L(D1) and L(D2) are quasiprimal, in the sense that their corresponding varieties are generated by quasiprimal algebras D1 and D2 respectively.
The logic L(D3), just like L(2e) and L(2ˉe), is a coatom in the lattice of extensions of the logic DMSH and hence, of DHMSH.
The logic L(D3) is primal.
Further features of some of these logics will be given in Remark 8.1.
8. Connection to Connexive Logics
Let L be a language containing the connective symbols: → for implication and ¬ for negation.
A logic L in L is a connexive logic (see [43], for example) if the following Aristotle’s Theses and Boethius’ Theses are theorems in L:
Aristotle’s Theses:
(AT) ¬(¬α→α),
(AT’) ¬(α→¬α),
Boethius’ Theses:
(BT) (α→β)→¬(α→¬β),
(BT’) (α→¬β)→¬(α→β).
For more details on the motivation, the origin and the history of connexive logics, see [43] and [18].
Many of the extensions of the logics SH and DHMSH, to our surprise, turn out to be connexive logics with ¬α:=α→⊥. We present a few of these below. (More will be said in the paper [10] which is in preparation.)
Recall that 2ˉ, L9, and L10, are in SH.
Remark 8.1**.**
The logics L(2ˉ) and L(L9), which are extensions of the semi-intuitionistic logic SI, are connexive logics since the corresponding varieties V(2ˉ) and V(L9) satisfy the following identities:
(x∗→x)∗≈1,
(x→x∗)∗≈1,
(x→y)→(x→y∗)∗≈1,
(x→y∗)→(x→y)∗≈1.
(AT)* and (AT’) are theorems in the logic L(L10), since the corresponding variety V(L10) satisfies the identities (i) and (ii), while (BT) and (BT’) are not theorems in the logics L(L10).*
Remark 8.2**.**
The logics L(2ˉe), L(L9dp), L(L9dm) and D1, which are extensions of the logic DHMSH,
are connexive logics since it is easily verified that their corresponding varieties V(2ˉe), L(L9dp), L(L9dm), and V(D1) satisfy the identities (i)–(iv).
(AT)* and (AT’) are theorems in the logics L(L10dp) and L(L10dm), since the corresponding varieties V(L10dp) and V(L10dp) satisfy the identities (i) and (ii).*
(BT)* and (BT’) are not theorems in the logics L(L10dp) and L(L10dm).*
Jarmuzek and Malinowski [18] have recently introduced the notion of a “quasi-connexive” logic.
A logic is quasi-connexive iff it is not connexive, but at least one of (AT), (AT’), (BT) and (BT’) is a theorem in the logic.
Thus, in view of the above remark, the logics L(L10dp) and L(L10dm), as well as the extension L(L10) of SH, can be viewed as quasi-connexive logics.
We now mention a few facts about the relationships among the Aristotle’s Theses and Boethius’ Theses in the logics SH and DHMSH whose proofs will appear in a forthcoming paper.
Theorem 8.3**.**
*In the logic SH, and hence in DHMSH,
(a) (AT) and (AT’) are equivalent.
(b) (AT), (AT’) and (BT’) are provable from (BT).
(c) (AT), (AT’) are provable from (BT’), but (BT) is not.*
Remark 8.4**.**
We propose that any logic in which the (classically provable) formula ⊥→⊤ is not provable be included in the family of connexive logics since such a logic would be not only anti-classical but also anti-intuitionistic logic. Accordingly, the logics L(2ˉe), L(Lidp),i=5,…,10, L(Lidm),i=5,…,10, V(D1) and V(D3) can be considered as connexive logics.
9. Two Infinite Chains of Extensions of the logic DQDH
Recall that the logic DQDH corresponds to the variety of dually quasi-De Morgan Heyting algebras. In this section, we present two infinite chains of logics that are extensions of the logic DQDH.
9.1. De Morgan-Gödel logic and its extensions: Logics corresponding to the subvarieties of the variety generated by all De Morgan Gödel algebras
Recall that the variety DMH of De Morgan Heyting algebras is the subvariety of DQDH defined by the axiom: x′′≈x. A De Morgan Heyting algebra whose lattice reduct is a chain is called a De Morgan Heyting chain.
Let DMG (or DMHC) denote the subvariety of DMSH generated by the De Morgan Heyting chains. It is proved in
[34, Theorem 12.5] that the lattice of subvarieties of the variety
DMG is an ω+1-chain. Let DMG (or DMHC) denote the extension of the logic DMH, corresponding to DMG. We will refer to the logic DMG as “De Morgan-Gödel logic.” Then it follows
that the lattice of extensions of DMG is a chain dual to ω+1.
In this subsection, we present axiomatizations for the logics corresponding to the subvarieties of
DMG. For this purpose, we need
the following algebraic result which was proved in [34, Theorem 12.3].
Theorem 9.1**.**
[34]**
A base for DMG, relative to DMSH, is given by:
x∗′≈x∗∗,
(x→y)∨(y→x)≈1.
Hence we have the following axiomatization for the logic DMG, relative to the logic DMSH.
Corollary 9.2**.**
The logic DMG, relative to the logic DMSH is defined by :
∼(α→⊥)⇔H((α→⊥)→⊥),
(α→β)∨(β→α)*. *
In view of the axiom (ii) it is clear that the logic DMG does not have the Disjunction Property.
Next we will present an axiomatization for the logic DMGn corresponding to each subvariety DMGn of DMG generated by the n-element DMH-chain, where n∈N with n≥2.
Theorem 9.3**.**
[34] *
Let n∈ω such that n≥2. Then
DMGn is defined, mod DMG, by the following axiom:
[TABLE]
Hence we have the following axiomatization of the logic DMGn.
Corollary 9.4**.**
*Let n∈ω such that n≥2. Then the logic DMGn, relative to the logic DMG, is defined by
[TABLE]
9.2. Dually pseudocomplemented Gödel Logic and its extensions: Logic corresponding to the variety generated by dually pseudocomplemented Heyting chains
A DPCSH-algebra L=⟨L,∧,∨,→,′,0,1⟩, whose lattice reduct is a chain, is called a DPCSH-chain. Let DPCG (or DPCHC) denote the subvariety of DPCH generated by the DPCH-chains. Observe that DPCHC=DStHC. It was implicit in
[34, Section 13] that the lattice of subvarieties of the variety
DPCG is an ω+1-chain and was explicitly proved in [38, Theorem 4.7]. We let DPCG (or DPCHC) denote the extension of the logic DPCH corresponding to DPCG. The logic DPCG will be referred to as “dually pseudocomplemented Gödel logic”. It follows from the just mentioned algebraic result
that the extensions of DPCG form a chain dual to ω+1.
In this subsection, we present axiomatizations for the logics corresponding to the subvarieties of
DPCG. For this purpose, we need the following algebraic result which
was proved in [34, Theorem 13.2]. Let x+:=x′∗′.
Theorem 9.5**.**
The following identities form an equational base, mod DQDSH, for DPCG.
- (i)
x+≈x′,
2. (ii)
(x→y)∨(y→x)≈1*.
*
Corollary 9.6**.**
The logic DPCG corresponding to the variety DPCG is defined, as an extension of the logic DQDSH by
- (i)
α+⇔H ∼α, where α+:= ∼(∼α→⊥).
2. (ii)
(α→β)∨(β→α)*. *
In view of the axiom (ii) it is clear that the logic DPCG does not have the Disjunction Property.
Let n∈ω such that n≥2 and let DPCGn denote the variety generated by the n-element DPCH-chain.
The following theorem, which follows from [34, Theorem 13.3], gives an equational base for each subvariety DPCGn of DPCG.
Theorem 9.7**.**
Let n∈ω such that n≥3. Then,
{(An)} is an equational base, mod DPCG, for DPCGn, where (An) is the following axiom:
[TABLE]
Corollary 9.8**.**
Let n∈ω such that n≥2. Then the logic DPCGn corresponding to the variety DPCGn is defined, relative to the logic DPCG by
- (Λn)
⋁j=1j=nαj∨⋁j=1j=n−1(αj→αj+1)*. *
10. Logics corresponding to subvarieties of regular dually quasi-De Morgan Stone semi-Heyting algebras
In the rest of the paper we will give axiomatizations for more new logics that are extensions of DQDSH, as applications of Theorem 5.9, and the algebraic results from [35, 36, 37, 38, 40]).
Recall from Section 7.2 that C20=Cdm∪Cdp, where
Cdm:={Lidm:i=1,2,…,10}, Cdp:={Lidm:i=1,2,…,10} and that the algebras Lidm, Lidp were defined in Section 8.2 and the three 4-element algebras D1, D2 and D3 were defined in
Section 7.6. Recall also that
V(C20) is the subvariety of DQDSH generated by all the 20 3-element DQDSH-chains. Let DQDSHC3:=V(C20).
The notion of regularity has played an important role in [41, 4, 34, 35, 36, 37].
An algebra A∈DQDSH is called regular ([36]) if A satisfies:
[TABLE]
where x+:=x′∗′.
The subvariety of DQDSH of regular algebras is denoted by RDQDSH.
(We caution the reader that the term “regular” was used in [34] to mean something else.)
Observe from Theorem 7.6 that DQDSHC3⊂RDQDSH.
The concept of level has played an important role in finding discriminator subvarieties of DQDSH (see [34, Corollary 8.2]). Here we only define
DQDSH-algebras of level 1.
An algebra A∈DQDSH is of level 1 if A satisfies:
[TABLE]
For the varieties of level 1 considered in the rest of the paper, the above definition of “level 1” is equivalent to the following:
[TABLE]
Let DQDSH1 denote the variety of DQDSH-algebras of level 1.
Let DQDStSH denote the subvariety of DQDSH
that satisfies the Stone identity:
[TABLE]
DQDStSH1 denotes the subvariety of DQDStSH of level 1, while RDQDStSH1 denotes the subvariety of DQDStSH1 defined by (R).
In this section we present axiomatizations for new logics corresponding to several subvarieties of the variety RDQDStSH1 of regular dually quasi-De Morgan Stone semi-Heyting algebras of level 1.
In what follows, V (or L(V)) denotes the logic corresponding to the subvariety V
of DQDSH-algebras.
(Thus, for example, the logic DQDStSH1 corresponds to the variety DQDStSH1.)
The following corollary is immediate from the above definitions and Theorem 5.9.
Corollary 10.1**.**
{thlist}
The logic DQDStSH1
is defined, as an extension of
the logic DQDSH, by the following axioms:
[∼{(α∧ (∼α)∗}]∗⇔H α∧ (∼α)∗,
α∗∨α∗∗.**
The logic RDQDStSH1
is defined, as an extension of
the logic DQDStSH1 by the following axiom:
- (α∧α+) →H (β∨β∗).
The following result is taken from [36, Theorem 3.1].
Theorem 10.2**.**
RDQDStSH1=V(C20∪{D1,D2,D3}).*
In particular,
RDQDStH1=V({L1dm,L1dp,D2}).*
The following corollary is immediate from Theorem 10.2 and Theorem 5.9, as the variety RDQDStSH1 is finitely axiomatized and is generated by a finite set of finite algebras.
Corollary 10.3**.**
The logics RDQDStSH1 and RDQDStH1 are decidable.
In view of the above corollary, it would be of interest to know if
the logic DQDStSH1 is decidable;
in particular, if the logic DQDStH1 is decidable.
This naturally leads us to the following open problem.
PROBLEM: Is the variety DQDStSH1 (or even DQDStH1) generated by its finite members?
Remark 10.4**.**
It was shown in [34] that the variety RDQDStSH1 is a discriminator variety. Thus RDQDStSH1 is a discriminator logic.
Let RDMStSH1 and RDMStH1 denote, respectively, the varieties of regular De Morgan Stone semi-Heyting algebras and regular De Morgan Stone semi-Heyting algebras. Similarly, the varieties
RDPCStSH1 and RDPCStH1 denote, respectively,
the varieties of regular dually pseudocomplemented Stone semi-Heyting algebras and regular dually pseudocomplemented Stone Heyting algebras. Note that all these varieties are subvarieties of RDQDStSH1.
Recall DMSHC3=V(Cdm) and let DPCSHC3=V(Cdp).
Observe that DMSHC3⊂RDMSH and DPCSHC3⊂RDPCSH.
The following corollary is immediate from Theorem 10.2, where “is defined by” means
“is defined, as an extension of RDQDStSH1, by ”.
Corollary 10.5**.**
{thlist}
The logic RDMStSH1 is defined by
- α →Hα′′.
The logic RDPCStSH1 is defined by
- α ∨ α′.
The logic RDMStH1 is defined by
- (α∧β)→α.
The logic RDPCStH1 is defined by
- (α∧β)→α.
The following theorem was recently proved in [40].
Theorem 10.6**.**
[40, Corollary 3.4]*
DMSH1=DMStSH1.
In particular,
RDMSH1=RDMStSH1.*
The following theorem is immediate from Theorem 10.6 and [36, Corollary 3.4].
Theorem 10.7**.**
{thlist}
RDMSH1=RDMStSH1=V(Cdm)∨V({D1,D2,D3})*,
RDMH1=RDMStH1=V({L1dm,D2})=V(L1dm)∨V(D2),
RDPCStSH1=V(Cdp),
RDPCStH1=V(L1dp).*
It is clear from Theorem 10.7 that the logics RDMSH1 and RDMStSH1 are equivalent and so are RDMH1 and RDMStH1.
The following corollary is immediate from Theorem 10.7.
Corollary 10.8**.**
The logics RDMSH1 and RDPCStSH1
are decidable.
Let RDQDcmStSH1 be the subvariety of
RDQDStSH1 defined by the commutative law:
x→y≈y→x.
Corollary 10.9**.**
The logic RDQDcmStH1 is defined, as an extension of RDQDStSH1, by
- (α→β)→H (β→α).
The following theorem is an immediate consequence of Theorem 10.2 and Theorem 10.7.
Theorem 10.10**.**
[36, Corollary 3.5]*
{thlist}
RDQDcmStSH1 =V(L10dm)∨V(L10dp)∨V(D1),
RDMcmSH1=RDMcmStSH1=V({L10dm,D1}),
RDPCcmStSH1=V((L10dp),
RDMcmSH1∩RDPCcmStSH1=V(2ˉe).*
It follows from the preceding theorem that the logics RDQDcmStSH1, RDMcmSH1 and RDPCcmStSH1 are decidable.
**In the rest of this section, unless otherwise stated, the phrase “defined, modulo
RDQDStSH1, by” is abbreviated to the phrase “defined by”
in the context of varieties. Similarly, the phrase “defined, as an extension of the logic
RDQDStSH1, by” is also abbreviated to the phrase “defined by” in the case of logics.
**The theorems that appear in the rest of this section were proved in [36].
Each of the corollaries appearing below follows from the theorem immediately preceding it and Theorem 5.9.
Theorem 10.11**.**
*The variety V({L1dm,L1dp,L3dm,L3dp,D2}) is defined by the identity:
*
- (x→y)→(0→y)≈(x→y)→1.
Corollary 10.12**.**
The logic L(V(L1dm,L1dp,L3dm,L3dp,D2)) is defined by
- [(α→β)→(⊥→β)]⇔H[(α→β)→⊤].
The variety generated by D1 was axiomatized earlier in Section 7.
Here are two more bases for it.
Theorem 10.13**.**
V(D1)* is defined
by*
- x→(y→z)≈z→(x→y).
*It is also defined
by
*
- (x→y)→(u→w)≈(x→u)→(y→w)* *(Medial Law).
Corollary 10.14**.**
The logic L(V(D1)) is defined by
- α→(β→γ)⇔Hγ→(α→β).
It is also defined by
- (α→β)→(γ→δ)⇔H((α→γ)→(β→δ))*, *(Medial Law).
Theorem 10.15**.**
The variety V({L1dm,L1dp,L2dm,L2dp,D2}) is defined
by:
It is also defined
by:
- [(x→y)→y]→(x→y)≈x→y.
It is also defined
by
- x→(y→z)≈(x→y)→(x→z)* *(Left distributive law).
Corollary 10.16**.**
The logic L(V({L1dm,L1dp,L2dm,L2dp,D2}) is defined by
- β∧(α→β).
It is also defined by:
- [(α→β)→β]→(α→β)⇔H(α→β).
It is also defined by
- α→(β→γ)⇔H[(α→β)→(α→γ).
Theorem 10.17**.**
The variety
V({L1dm,L1dp,L2dm,L2dp,L5dm,L5dp,L6dm,L6dp,D2}) is defined
by:
- [x→(y→x)]→x≈x.
Corollary 10.18**.**
*The logic L(V({L1dm,L1dp,L2dm,L2dp,L5dm,L5dp,L6dm,L6dp,D2})) is defined by
*
- [{α→(β→α)}→α]⇔Hα.
Theorem 10.19**.**
V({L1dp,L2dp,L5dp,L6dp})* is defined
by:*
[x→(y→x)]→x≈x,
x∨x′≈1.
Corollary 10.20**.**
The logic L(V({L1dp,L2dp,L5dp,L6dp})) is defined
by
[{α→(β→α)}→α]⇔Hα*,
*
α ∨ ∼α.
Recall that x+:=x′∗′.
Theorem 10.21**.**
*The variety
V({L1dm,L1dp,L2dm,L2dp,L3dm,L3dp,L4dm,L4dp,L5dm,L6dm,
L7dm,L8dm,D2,D3}) is defined by the identity:
*
- (0→1)+→(0→1)′≈0→1.
Corollary 10.22**.**
*The logic L((V({L1dm,L1dp,L2dm,L2dp,L3dm,L3dp,L4dm,L4dp,L5dm,L6dm,
L7dm,L8dm,D2,D3})) is defined
by*
- [(⊥→⊤)+→ ∼(⊥→⊤)]⇔H(⊥→⊤).
Theorem 10.23**.**
The variety
V({L1dp,L2dp,L3dp,L4dp})
is defined
by the identities:
(0→1)+→(0→1)′≈0→1,
x∨x′≈1.
Corollary 10.24**.**
The logic L(V({L1dp,L2dp,L3dp,L4dp})) is defined by
[(⊥→⊤)+→ ∼(⊥→⊤)]⇔H(⊥→⊤),
α ∨∼α.
Theorem 10.25**.**
*The variety
V({L1dm,L2dm,L3dm,L4dm,L5dm,L6dm,L7dm,L8dm,
D2,D3}) is defined
by the identities:*
(0→1)+→(0→1)′≈0→1,
x′′≈x.
Corollary 10.26**.**
The logic L(V({L1dm,L2dm,L3dm,L4dm,L5dm,L6dm,L7dm,L8dm,D2,D3})) is defined by
[(⊥→⊤)+→ ∼(⊥→⊤)]⇔H(⊥→⊤)*,
*
α→H ∼∼α.
Theorem 10.27**.**
The variety
V({L5dm,L6dm,L7dm,L8dm,D3}) is defined
by the identity:
- (0→1)+→(0→1)≈(0→1)′.
Corollary 10.28**.**
The logic L(V({L5dm,L6dm,L7dm,L8dm,D3})) is defined by
- [(⊥→⊤)+→(⊥→⊤)]⇔H ∼(⊥→⊤).
V(D3) was axiomatized in Section 7. Here is another base for it.
Theorem 10.29**.**
V(D3)* is defined
by the identities:*
(0→1)+→(0→1)≈(0→1)′,
x∨x∗≈1.
Corollary 10.30**.**
The logic L(V({D3})) is defined by
(⊥→⊤)+→(⊥→⊤)⇔H ∼(⊥→⊤),
α∨α∗.
Theorem 10.31**.**
The variety generated by the algebras
L1dm,L2dm,
L3dm,L4dm,
D2,D3 is defined
by the identities:
(0→1)+→(0→1)′≈0→1,
(0→1)+→(0→1)∗′∗≈0→1,
x′′≈x.
Corollary 10.32**.**
The logic L(V({L1dm,L2dm,L3dm,L4dm,D2,D3})) is defined by
(⊥→⊤)+→ ∼(⊥→⊤)⇔H(⊥→⊤),
[(⊥→⊤)+→ (∼(⊥→⊤)∗)∗]⇔H(⊥→⊤)*,
*
α→H ∼∼α.
Theorem 10.33**.**
*The variety generated by the algebras
L5dm,L5dp,L6dm,L6dp,L7dm,L7dp,L8dm,L8dp,L9dp,L9dm,L10dp,L10dm,
D1,D3 is defined
by the identity:*
- (0→1)+→(0→1)′≈(0→1)′.
Corollary 10.34**.**
*The logic
L(V({L5dm,L5dp,L6dm,L6dp,L7dm,L7dp,L8dm,L8dp,L9dm,L9dp,L10dm,L10dp,D1,D3})) is defined by*
- [(⊥→⊤)+→ ∼(⊥→⊤)]⇔H ∼(⊥→⊤).
Theorem 10.35**.**
*The variety generated by the algebras
L5dp,L6dp,L7dp,L8dp,L9dp,L10dp
is defined
by the identities:*
(0→1)+→(0→1)′≈(0→1)′,
x∨x′≈1.
Corollary 10.36**.**
*The logic L(V({L5dp,L6dp,L7dp,L8dp,L9dp,L10dp})) is defined
by*
[(⊥→⊤)+→ ∼(⊥→⊤)]⇔H ∼(⊥→⊤),
α ∨ ∼α.
Theorem 10.37**.**
*The variety generated by the algebras
L5dm,L6dm,L7dm,L8dm,L9dm,L10dm,
D1,D3 is defined
by the identities:*
(0→1)+→(0→1)′≈(0→1)′,
x′′≈x.
Corollary 10.38**.**
*The logic L(V({L5dm,L6dm,L7dm,L8dm,L9dm,L10dm,D1,D3})) is defined
by*
[(⊥→⊤)+→ ∼(⊥→⊤)]⇔H ∼(⊥→⊤)*,
*
α→H ∼∼α.
Theorem 10.39**.**
*The variety generated by the algebras
D1,D3 is defined by the identities:
*
(0→1)+→(0→1)′≈(0→1)′,
x∨x∗≈1.
Corollary 10.40**.**
*The logic L(V({D1,D3})) is defined
by*
[(⊥→⊤)+→ ∼(⊥→⊤)]⇔H ∼(⊥→⊤),
α∨α∗.
Theorem 10.41**.**
*The variety generated by the algebras
L5dm,L6dm,L7dm,L8dm,
D3 is defined
by the identities:
*
(0→1)+→(0→1)′≈(0→1)′,
(0→1)+→(0→1)′≈(0→1).
It is also defined
by
- (0→1)′≈0→1.
Corollary 10.42**.**
*The logic L(V({L5dm,L6dm,L7dm,L8dm,D3})) is defined
by*
[(⊥→⊤)+→ ∼(⊥→⊤)]⇔H ∼(⊥→⊤),
[(⊥→⊤)+→ ∼(⊥→⊤)]⇔H(⊥→⊤).
It is also defined by
- ∼(⊥→⊤)⇔H(⊥→⊤).
Theorem 10.43**.**
*The variety generated by the algebras
L1dm,L1dp,L2dm,L2dp,L3dm,L3dp,L4dm,L4dp,L5dp,L6dp,L7dp,L8dp,
L9dm,L9dp,L10dm,L10dp,D1,D2 is defined
by the identity:*
- (0→1)′→(0→1)≈0→1.
Corollary 10.44**.**
*The logic corresponding to the variety generated by the algebras
L1dm,L1dp,L2dm,L2dp,L3dm,L3dp,L4dm,L4dp,L5dp,L6dp,L7dp,L8dp,L9dm,L9dp,L10dm,L10dp,D1,D2 is defined
by*
- [∼(⊥→⊤)→(⊥→⊤)]⇔H(⊥→⊤).
Theorem 10.45**.**
*The variety generated by the algebras
L1dm,L2dm,L3dm,L4dm,L9dm,L10dm,
D1,D2
is defined
by the identities:*
(0→1)′→(0→1)≈0→1,
x′′≈x.
Corollary 10.46**.**
The logic L(V({L1dm,L2dm,L3dm,L4dm,L9dm,L10dm,D1,D2})) is defined
by
[∼(⊥→⊤)→(⊥→⊤)]⇔H(⊥→⊤)*,
*
α→H ∼∼α.
Theorem 10.47**.**
*The variety generated by the algebras
D1,D2 is defined
by the identities:*
(0→1)′→(0→1)≈0→1,**
x∨x∗≈1.
Corollary 10.48**.**
The logic L(V({D1,D2})) is defined
by
[∼(⊥→⊤)→(⊥→⊤)]⇔H(⊥→⊤),
α ∨ α∗.
Theorem 10.49**.**
*The variety generated by the algebras
L1dm,L1dp,L3dm,L3dp,L6dm,L6dp,L8dm,L8dp,D1,D2,D3 is defined by the identity:*
- x∨[y→(x∨y)]≈(0→x)∨x∨y.
Corollary 10.50**.**
The logic L(V({L1dm,L1dp,L3dm,L3dp,L6dm,L6dp,L8dm,L8dp,D1,D2,D3})) is defined
by
- [α∨{β→(α∨β)}]⇔H[(⊥→α)∨α∨β]*. *
Theorem 10.51**.**
*The variety generated by the algebras
L2dm,L2dp,L5dm,L5dp,D2 is defined by the identity:*
- x∨(y→x)≈[(x→y)→y]→x.
Corollary 10.52**.**
The logic L(V({L2dm,L2dp,L5dm,L5dp,D2})) is defined
by
- [α∨(β→α)]⇔H[{(α→β)→β}→α].
Theorem 10.53**.**
*The variety generated by the algebras
L3dm,L3dp,L4dm,L4dp,D1,D2,D3 is defined
by the identity:
*
- x∨(x→y)≈x→[x∨(y→1)].
Corollary 10.54**.**
The logic L(V({L3dm,L3dp,L4dm,L4dp,D1,D2,D3})) is defined
by
- [α∨(α→β)]⇔H[α→{α∨(β→⊤)}].
Theorem 10.55**.**
*The variety generated by the algebras
L5dm,L6dp,L7dm,L8dp,D3 is defined by the identity:*
- (0→1)∗→(0→1)≈(0→1)′.
Corollary 10.56**.**
The logic L(V({L5dm,L6dp,L7dm,L8dp,D3})) is defined
by
- [(⊥→⊤)∗→(⊥→⊤)]⇔H ∼(⊥→⊤).
Theorem 10.57**.**
*The variety generated by the algebras
L1dm,L1dp,L2dm,L2dp,L3dm,L3dp,
L4dm,L4dp,D2 is defined
by the
identity:*
- 0→1≈1* *(FTT identity).
Corollary 10.58**.**
The logic L(V({L1dm,L1dp,L2dm,L2dp,L3dm,L3dp,L4dm,L4dp,D2})) is defined
by
- ⊥→⊤* *(FTT identity).
Theorem 10.59**.**
*The variety generated by the algebras
L1dm,L1dp,L3dm,L3dp,L6dm,L6dp,
L8dm,L8dp,D1,D2,D3 is
defined
by the identity:
*
- x∨(y→x)≈(x∨y)→x.
Corollary 10.60**.**
*The logic L(V({L1dm,L1dp,L3dm,L3dp,L6dm,L6dp,L8dm,L8dp,D1,D2,D3})
is defined
by*
- [α∨(β→α)]⇔H[(α∨β)→α].
Theorem 10.61**.**
*The variety generated by the algebras
L1dp,L3dp,L6dp,
L8dp is
defined by the identities:
*
x∨(y→x)≈(x∨y)→x,
x∨x′≈1.
Corollary 10.62**.**
The logic L(V({L1dp,L3dp,L6dp,L8dp})) is defined
by
[α∨(β→α)]⇔H[(α∨β)→α],
α ∨ ∼α.
Theorem 10.63**.**
*The variety generated by the algebras
L1dm,L3dm,L6dm,
L8dm,D1,D2,D3 is
defined
by the identities:*
x∨(y→x)≈(x∨y)→x,
x′′≈x.
Corollary 10.64**.**
The logic L(V({L1dm,L3dm,L6dm,L8dm,D1,D2,D2})) is defined
by
[α∨(β→α)]⇔H[(α∨β)→α]*,
*
α→H ∼∼α.
Theorem 10.65**.**
*The variety generated by the algebras
L1dm,L1dp,L2dm,L2dp,L5dm,L5dp,L6dm,L6dp,L9dm,L9dp,
D1,D2,D3
is defined
by the identity:*
- x∗∨(x→y)≈(x∨y)→y.
Corollary 10.66**.**
*The logic
L(V({L1dm,L1dp,L2dm,L2dp,L5dm,L5dp,L6dm,L6dp,L9dm,L9dp,D1,D2,D2})) is defined
by*
- [α∗∨(α→β)]⇔H[(α∨β)→β]*. *
Theorem 10.67**.**
V({L1dp,L2dp,L5dp,L6dp,L9dp})*
is defined
by the identity:*
x∗∨(x→y)≈(x∨y)→y,
x∨x′≈1.
Corollary 10.68**.**
The logic L(V({L1dp,L2dp,L5dp,L6dp,L9dp})) is defined
by
[α∗∨(α→β)]⇔H[(α∨β)→β]*, *
α ∨ ∼α.
Theorem 10.69**.**
*The variety generated by the algebras
L1dm,L2dm,L5dm,L6dm,L9dm,
D1,D2,D3
is defined
by the identity:
*
x∗∨(x→y)≈(x∨y)→y,
x′′≈x.
Corollary 10.70**.**
The logic L(V({L1dm,L2dm,L5dm,L6dm,L9dm,D1,D2,D3})) is defined
by
[α∗∨(α→β)]⇔H[(α∨β)→β]*, *
α→H ∼∼α.
Theorem 10.71**.**
*The variety generated by the algebras
L5dm,L5dp,D2 is defined
by the identity:
*
- x∨(0→x)∨(y→1)≈x∨[(x→1)→(x→y)].
Corollary 10.72**.**
The logic L(V({L5dm,L5dp.D2})) is defined
by
- [α∨(⊥→α)∨(β→⊤)]⇔Hα∨[(α→⊤)→(α→β)]*.
Theorem 10.73**.**
*The variety generated by the algebras
L6dm,L6dp,D2 defined
by the identity:
*
- x∨y∨(x→y)≈x∨[(x→y)→1].
Corollary 10.74**.**
The logic L(V({L6dm,L6dp,D2})) is defined
by
- α∨β∨(α→β)⇔Hα∨[(α→β)→⊤].
Theorem 10.75**.**
*The variety generated by the algebras
L1dm,L1dp,L7dm,L7dp,D2 is defined
by the identity:
*
- x∨[(0→y)→y]≈x∨[(x→1)→y].
Corollary 10.76**.**
The logic L(V({L1dm,L1dp,L7dm,L7dp,D2})) is defined
by
- [α∨{(⊥→β)→β}]⇔H[α∨[(α→⊤)→β].
Theorem 10.77**.**
*The variety generated by the algebras
L7dm,L7dp,L8dm,L8dp,D1,D2,D3 is defined
by the identity:
*
- x ∨[x→(y∧(0→y))]≈x→[(x→y)→y].
Corollary 10.78**.**
The logic L(V({L7dm,L7dp,L8dm,L8dp,D1,D2,D3})) is defined
by
- [α∨[α→{β∧(⊥→β)}]]⇔H[α→[(α→β)→β].
Theorem 10.79**.**
*The variety generated by the algebras
L8dm,L8dp,D1,D2,D3
is defined by the identity:*
- x∨y∨[y→(y→x)]≈x→[x∨(0→y)].
It is also defined
by the identity:
- x∨[y→{0→(y→x)}]≈x∨y∨(y→x).
Corollary 10.80**.**
The logic L(V({L8dm,L8dp,D1,D2,D3})) is defined
by
- [α∨β∨{β→(β→α)}]⇔H[α→{α∨(0→β)}]*. *
It is also defined by:
- [α∨{β→(0→(β→α))}]⇔H[α∨β∨(β→α)].
Theorem 10.81**.**
*The variety generated by the algebras
L7dm,L7dp,L8dm,L8dp,L9dm,L9dp,
L10dm,L10dp,D1,D2,D3 is defined
by the identity:
*
- x∨(x→y)≈x∨[(x→y)→1].
Corollary 10.82**.**
The logic L(V({L7dm,L7dp,L8dm,L8dp,L9dm,L9dp,L10dm,L10dp,D1,D2,D3})) is defined
by
- [α∨(α→β)]⇔H[α∨{(α→β)→⊤}]*. *
Theorem 10.83**.**
*The variety generated by the algebras
2e,L7dp,L8dp,L9dp,
L10dp is defined
by the identities:
*
x∨(x→y)≈x∨[(x→y)→1],
x∨x′≈1.
Corollary 10.84**.**
The logic L(V({2e,L7dp,L8dp,L9dp,L10dp}) is defined
by
[α∨(α→β)]⇔H[α∨{(α→β)→⊤}]*, *
α ∨ ∼α.
Theorem 10.85**.**
*The variety generated by the algebras
L7dm,L8dm,L9dm,
L10dm,D1,D2,D3 is defined
by the identities:*
x∨(x→y)≈x∨[(x→y)→1],
x′′≈x.
Corollary 10.86**.**
The logic L(V({L7dm,L8dm,L9dm,L10dm,D1,D2,D3})) is defined
by
[α∨(α→β)]⇔H[α∨{(α→β)→⊤}]*, *
α→H ∼∼α.
Theorem 10.87**.**
*The variety generated by the algebras
L9dm,L9dp,L10dm,L10dp,D1 is
defined
by the identity:*
- 0→1≈0* (FTF identity).*
Corollary 10.88**.**
The logic L(V({L9dm,L9dp,L10dm,L10dp,D1})) is defined
by
- (⊥→⊤)⇔H⊥* (FTF identity).*
Theorem 10.89**.**
*The variety generated by the algebras
L10dm,L10dp,D1 is
defined by
the identity:*
- x→y≈y→x* (commutative identity).*
Corollary 10.90**.**
The logic L(V({L10dm,L10dp,D1})) is defined
by
- (α→β)⇔H(β→α)* (commutative identity).*
Theorem 10.91**.**
The variety V(C20)
is defined
by
- x∗≤x′.
Corollary 10.92**.**
The logic L(V(C20))
is defined
by
- α∗→H ∼α.
Theorem 10.93**.**
The variety V(D2)
is defined
by
- (x→y)∗≈x∧y∗.
Corollary 10.94**.**
The logic L(V(D2) is defined
by
- (α→β)∗⇔Hα∧β∗.
Theorem 10.95**.**
*The variety generated by the algebras in
{Lidp:i=1,…,8}∪{Lidm:i=1,…,8}∪{D2}
is defined
by the identity:*
- (x→y)∗≈(x∧y∗)∗∗.
It is also defined by
- (0→1)∗≈0.
Corollary 10.96**.**
The logic L(V({Lidp:i=1,…,8}∪{Lidm:i=1,…,8}∪{D2}) is defined
by
- (α→β)∗→H(α∧β∗)∗∗.
It is also defined by
- (⊥→⊤)∗⇔H⊥.
Theorem 10.97**.**
The variety generated by the algebras
Lidp, i=1,…,8, is
defined
by the identities:
(x→y)∗≈(x∧y∗)∗∗,
x∨x′≈1.
Corollary 10.98**.**
*The logic L(V({Lidp:i=1,…,8})) is
defined
by
*
(α→β)∗⇔H(α∧β∗)∗∗,
α ∨ ∼α.
Theorem 10.99**.**
The variety generated by the algebras
Lidm, i=1,…,8, and D2 is
defined
by the identities:
(x→y)∗≈(x∧y∗)∗∗,
x′′≈x*. *
Corollary 10.100**.**
The logic L(V({Lidm:i=1,…,8}∪{D2})), is
defined
by
(α→β)∗⇔H(α∧β∗)∗∗,
α→H ∼∼α.
Theorem 10.101**.**
*The variety generated by the algebras
L1dm,L1dp,L2dm,L2dp,D2
is defined
by the identity:*
- x∧z≤y∨(y→z).
Corollary 10.102**.**
The logic L(V({L1dm,L1dp,L2dm,L2dp,D2})) is defined
by
- (α∧γ)→H{β∨(β→γ)}.
Theorem 10.103**.**
*The variety generated by
L1dm,L1dp,L2dm,L2dp,L5dm,L5dp,L6dm,L6dp,D2
is defined
by the identity:*
- x∨y≤(x→y)→y.
Corollary 10.104**.**
The logic L(V({L1dm,L1dp,L2dm,L2dp,L5dm,L5dp,L6dm,L6dp,D2})) is defined
by
- (α∨β)→H[(α→β)→β].
Theorem 10.105**.**
*The variety generated by
L1dp,L2dp,L5dp,L6dp
is defined
by the identity:*
x∨y≤(x→y)→y,
x∨x′≈1.
Corollary 10.106**.**
The logic L(V({L1dp,L2dp,L5dp,L6dp})) is defined
by
(α∨β)→H[(α→β)→β],
α ∨ ∼α.
Theorem 10.107**.**
*The variety generated by
L1dm,L2dm,L5dm,L6dm,D2
is defined
by the identity:*
x∨y≤(x→y)→y,
x′′≈x.
Corollary 10.108**.**
The logic L(V({L1dm,L2dm,L5dm,L6dp,D2})) is defined
by
(α∨β)→H[(α→β)→β]*, *
α→H ∼∼α.
The variety V({D1,D2,D3}) was axiomatized in Theorem 7.16.
Here are two more bases for it.
Theorem 10.109**.**
The variety V({D1,D2,D3})
is defined
by the identity:
- x∨(y→z)≈(x∨y)→(x∨z)* *(Strong JID).
It is also defined by the identity:
- x′∗′∗≈x.
Corollary 10.110**.**
The logic L(V({D1,D2,D3})) is defined
by
- (α∨(β→γ))⇔H[(α∨β)→(α∨γ)].
*It is also defined
by the identity:
*
- (∼((∼α)∗))∗⇔Hα.
Theorem 10.111**.**
The variety generated by
L2dm,L2dp,D2
is defined
by the identity:
- (x→y)→x≈x.
Corollary 10.112**.**
The logic L(V({L2dm,L2dp,D2})) is defined
by
- ((α→β)→α)⇔Hα.
V(D2) was axiomatized in Theorem 7.18. Here are some more bases for it.
Theorem 10.113**.**
V(D2)*
is defined by the identity:*
- x∨y≈(x→y)→y.
It is also defined by the identities:
x∨(y→z)≈(x∨y)→(x∨z),
(x→y)→x≈x.
It is also defined by the identity:
- x∨(x→y)≈x∨((x∨y)→1).
Corollary 10.114**.**
The logic L(V(D2)) is axiomatized by
- (α∨β)⇔H((α→β)→β).
*This logic has an interesting property in that ∨ is definable in terms of →.
It is also axiomatized by*
(α∨(β→γ))⇔H[(α∨β)→(α∨γ)]*,
*
((α→β)→α)⇔Hα.
It is also axiomatized by
- (α∨(α→β))⇔H[α∨{(α∨β)→⊤}].
Theorem 10.115**.**
*The variety generated by
L1dm,L1dp,L2dm,L2dp,L9dm,L9dp,D1,D2,D3
is defined by the identity:*
- x→(y→z)≈y→(x→z).
Corollary 10.116**.**
The logic L(V({L1dm,L1dp,L2dm,L2dp,L9dm,L9dp,D1,D2,D3})) is defined
by
- [α→(β→γ)]⇔H[β→(α→γ)].
Theorem 10.117**.**
*The variety generated by
L1dm,L1dp,L2dm,L2dp,L5dm,L5dp,D2
is defined by the identity:*
- (x→y)→z≤((y→x)→z)→z**
Corollary 10.118**.**
The logic L(V({L1dm,L1dp,L2dm,L2dp,L5dm,L5dp,D2})) is defined
by
- [(α→β)→γ]→H[((β→α)→γ)→γ]* *
We note that a new extension of each of the logic defined in this section is obtained by adding the axiom α′′⇔Hα, as an extension of the logic DMSH. Similarly, the addition of the axiom: α∨α′ yields new extensions to the logics, over the logic DPCSH, defined in the preceding corollaries.
We conclude this section by remarking that all the logics described in this section are discriminator logics and also are decidable.
11. **Logics corresponding to subvarieties of
Regular De Morgan Semi-Heyting Algebras of level 1**
In this section, we present axiomatizations for logics corresponding to several subvarieties of the variety
RDMSH1 of regular De Morgan semi-Heyting algebras of level 1.
The algebraic results mentioned (or referred to) in this section were proved in [37].
Recall that DMSH1 denotes the logic corresponding to the variety DMSH1.
The following corollary is immediate from Theorem 5.9 and definitions.
**In what follows, V (or L(V)) denotes the logic corresponding to the variety V.
**Recall that the variety DMSH1 was defined in Section 10.
Corollary 11.1**.**
{thlist}
*The logic DMSH1
is defined,
relative to DMSH, by
α ∧(∼α)∗⇔H [∼(α ∧(∼α)∗)]∗.
The logic RDMSH1 is defined, relative to DMSH1, by
(α∧α+)→H(β∨β∗).
The logic RDMH1 is defined, relative to RDMSH1,
by
(α∧β)→α.
The logic RDMcmSH1 is defined, relative to RDMSH1, by
(α→β)→H(β→α).*
It follows from Theorem 10.6 that the logic RDMH1 is decidable. However, teh following problem is still open.
PROBLEM: Is the logic RDMH1 is decidable?
Let L∈DHMSH. We say L is pseudocommutative if
L satisfies the identity:
(PCM) x∗→y∗≈y∗→x∗.
RDMpcmSH denotes the variety of regular De Morgan pseudocommutative semi-Heyting algebras.
The following corollary is immediate from Theorem 5.9 and the above definition.
Corollary 11.2**.**
*The logic L(RDMpcmSH1) is defined by
(α∗→β∗)⇔H(β∗→α∗).*
Theorem 11.3**.**
[37]**
RDMpcmSH1=V(L9dm,L10dm,D1).
Corollary 11.4**.**
The logic L(RDMpcmSH1) is decidable.
In the rest of this section, unless otherwise stated, the phrase “defined, modulo
RDMSH1, by” is abbreviated to the phrase “defined by”
in the context of varieties. Similarly, the phrase “defined, as an extension of the logic
RDMSH1, by” is also abbreviated to the phrase “defined by” in the case of logics.
The theorems that appear in the rest of this section were proved in [37].
Each of the corollaries given below follows from the theorem immediately preceding it and Theorem 5.9.
Here is another axiomatization for RDMpcmSH.
Theorem 11.5**.**
The variety RDMpcmSH
is defined by
-
- (x→y)∗≈(y→x)∗.
Corollary 11.6**.**
*The logic L(RDMpcmSH) is defined by
(α→β)∗⇔H(β→α)∗.*
Theorem 11.7**.**
The variety V(L1dm,L2dm,L3dm,L4dm,D2,D3) is defined by
- (0→1)+→ [∼{(0→1)∗}]∗≈0→1.
Corollary 11.8**.**
The logic L(V(L1dm,L2dm,L3dm,L4dm,D2,D3)) is defined by
- ((⊥→⊤)+→ [∼{(⊥→⊤)∗}]∗)⇔H(α→⊤).
The variety V(D1,D2,D3)(=DQDBSH) was axiomatized earlier.
Here are some more bases for V(D1,D2,D3).
Theorem 11.9**.**
Each of the following identities is a base for
the variety V(D1,D2,D3):
x→y≈y∗→x∗* (Law of contraposition),*
[{x∨(x→y∗)}→(x→y∗)]∨(x∨y∗)=1.
Corollary 11.10**.**
{thlist}
*The logic L(V(D1,D2,D3)) is defined by
(α→β)⇔H(β∗→α∗).
The logic L(V(D1,D2,D3)) is also defined by
[{α∨(α→β∗)}→(α→β∗)]∨(α∨β∗).*
Theorem 11.11**.**
The variety
V(L1dm,L2dm,L5dm,L6dm,L9dm,D1,D2,D3) is defined
by
- x→y∗≈y→x∗.
Corollary 11.12**.**
*The logic L(V(L1dm,L2dm,L5dm,L6dm,L9dm,D1,D2,D3)) is defined by
(α→β∗)⇔H(β→α∗).*
Theorem 11.13**.**
The variety V(L7dm,L8dm,L9dm,L10dm,D1,D2,D3) is defined by
- x∨(x→y)≈x∨[(x→y)→1].
Corollary 11.14**.**
The logic L(V(L7dm,L8dm,L9dm,L10dm,D1,D2,D3)) is defined by
- [α∨(α→β)]⇔H[α∨{(α→β)→⊤}],
Theorem 11.15**.**
The variety V(L7dm,L8dm,D2) is defined by
x∨(x→y)≈x∨[(x→y)→1],
(0→1)∗∗≈1.
Corollary 11.16**.**
The logic L(V(L7dm,L8dm,D2)) is defined by
[α∨(α→β)]⇔H[α∨{(α→β)→⊤}],
(⊥→⊤)∗∗.
Theorem 11.17**.**
*The variety V(2e,L7dm,L8dm,L9dm,L10dm) is
defined by*
x∨(x→y)≈x∨[(x→y)→1],
x∗′≈x∗∗* (⋆-regular).*
We caution the reader that in [34], (2) was referred to as “regular”.
Corollary 11.18**.**
The logic L(V(2e,L7dm,L8dm,L9dm,L10dm)) is defined by
[α∨(α→β)]⇔H[α∨{(α→β)→1}],
∼(α∗)⇔Hα∗∗.
Theorem 11.19**.**
The variety
V(2e,L9dm,L10dm) is defined by
x∨(x→y)≈x∨[(x→y)→1],
x∗′≈x∗∗,
(0→1)∨(0→1)∗≈1.
Corollary 11.20**.**
The logic L(V(2e,L9dm,L10dm)) is defined by
[α∨(α→β)]⇔H[α∨{(α→β)→⊤}],
∼(α∗)⇔Hα∗∗,
(⊥→⊤)∨(⊥→⊤)∗.
Theorem 11.21**.**
*The variety
V(L9dm,L10dm) is defined by
*
x∨(x→y)≈x∨[(x→y)→1],
x∗′≈x∗∗,
(0→1)∗≈1.
Corollary 11.22**.**
The logic L(V(L9dm,L10dm)) is defined by
[α∨(α→β)]⇔H[α∨{(α→β)→1}],
∼(α∗)⇔Hα∗∗,
(⊥→⊤)∗.
Theorem 11.23**.**
*The variety
V(L1dm,L2dm,L3dm,L4dm,L5dm,L6dm,L7dm,L8dm) is defined by
*
x∗′≈x∗∗,
(0→1)∗∗≈1.
Corollary 11.24**.**
The logic L(V((L1dm,L2dm,L3dm,L4dm,L5dm,L6dm,L7dm,L8dm) is defined by
∼(α∗)⇔Hα∗∗.
(⊥→⊤)∗∗.
Theorem 11.25**.**
The variety V(L1dm,L2dm,L3dm,L4dm,D2) is defined by
(0→1)∨(0→1)∗≈1,
(0→1)∗∗≈1.
Corollary 11.26**.**
The logic L(V((L1dm,L2dm,L3dm,L4dm,D2)) is defined by
(⊥→⊤)∨(⊥→⊤)∗,
(⊥→⊤)∗∗.
Theorem 11.27**.**
The variety V(L1dm,L3dm,D1,D2,D3) is
defined by
x∨(y→x)≈(x∨y)→x,
(0→1)∨(0→1)∗≈1.
Corollary 11.28**.**
The logic L(V((L1dm,L3dm,D1,D2,D3)) is defined by
[α∨(β→α)]⇔H[(α∨β)→α],
(⊥→⊤)∨(⊥→⊤)∗.**
Theorem 11.29**.**
The variety V(L1dm,L3dm,D2) is defined by
x∨(y→x)≈(x∨y)→x,
(0→1)∨(0→1)∗≈1,
(0→1)∗∗≈1.
Corollary 11.30**.**
The logic L(V((L1dm,L3dm,D2)) is defined by
[α∨(β→α)]⇔H[(α∨β)→α],
(⊥→⊤)∨(⊥→⊤)∗,**
(⊥→⊤)∗∗.
Theorem 11.31**.**
*The variety V(L1dm,L2dm,L8dm,D1,D2,D3) is defined by
*
- y∨(y→(x∨y))≈(0→x)∨(x→y).
Corollary 11.32**.**
The logic L(V((L1dm,L2dm,L8dm,D1,D2,D3)) is defined by
- [β∨(β→(α∨β))]⇔H[(⊥→α)∨(α→β)].
Theorem 11.33**.**
The variety V(L8dm,D1,D2,D3) is defined by
- x∨[y→(0→(y→x))]≈x∨y∨(y→x).
Corollary 11.34**.**
The logic L(V(L8dm,D1,D2,D3)) is defined by
- [α∨{β→(⊥→(β→α))}]⇔H[α∨β∨(β→α)].
Theorem 11.35**.**
The variety V(Cdm) is defined by
- x∧x′≤y∨y′* (Kleene identity).*
Corollary 11.36**.**
The logic L(V(Cdm)) is defined by
- (α ∧ ∼α)→H(β ∨ ∼β* (Kleene identity)*
Theorem 11.37**.**
The variety V(L10dm) is defined by
x∧x′≤y∨y′* (Kleene identity),*
x→y≈y→x.
Corollary 11.38**.**
The logic L(V(L10dm)) is defined by
(α ∧ ∼α)→H(β ∨ ∼β) (Kleene identity),
α→β⇔Hβ→α.
V(D2) was axiomatized in Section 7. Here are some more bases for it, but relative to RDMH1.
Theorem 11.39**.**
Each of the following identities is a base for
V(D2), mod RDMH1:
[y→{0→(y→x)}]≈y∨(y→x).
x∨(y→z)≈(x∨y)→(x∨z).
[{x∨(x→y∗)}→(x→y∗)]∨x∨y∗≈1.**
Corollary 11.40**.**
Each of the following axioms defines the logic L(V(D2), relative to RDMH1:
[β→{⊥→(β→α)}]⇔H[β∨(β→α)],
[α∨(β→γ)]⇔H[(α∨β)→(α∨γ)]*,
*
[{α∨(α→β∗)}→(α→β∗)]∨α∨β∗.**
V(D1) was axiomatized in Section 8. Here are more bases for it.
Let RDMcmSH1 denote the subvariety of
RDMSH1 defined by: x→y≈y→x.
Theorem 11.41**.**
Each of the following identities is an equational base for
V(D1), mod RDMcmSH1:
y∨(y→(x∨y))≈(0→x)∨(x→y),
x∨[y→(y→x)∗]≈x∨y∨(y→x),
[{x∨(x→y∗)}→(x→y∗)]∨x∨y∗≈1,
x∨(y→z)≈(x∨y)→(x∨z).
Corollary 11.42**.**
Each of the following axioms defines the logic L(V(D1)), relative to RDMcmSH1:
[β∨(β→(α∨β))]⇔H[(⊥→α)∨(α→β)],
[α∨{β→(β→α)∗}]⇔H[α∨β∨(β→α)],
[{α∨(α→β∗)}→(α→β∗)]∨α∨β∗,
[α∨(β→γ)]⇔H[(α∨β)→(α∨γ)]*. *
We conclude this section with the remark that all logics introduced in this section are discriminator logics as their corresponding varieties are discriminator varieties.
12. Extensions of the logic JIDSH1
Algebras closely related to DStSH-algebras, called “JI-distributive semi-Heyting algebras”, were introduced in [38].
An algebra A in DQDSH is JI-distributive if A satisfies:
x′∨(y→z)≈(x′∨y)→(x′∨z) ((restricted) Join over Implication Distributivity).
We note that the identity (JID) is obtained by slightly weakening the identity (Strong JID) that has appeared earlier in Theorem 10.109.
Let JIDSH denote the variety of JI-distributive DQDSH-algebras and
let JIDSH1 (or JID1, for short) denote the subvariety of JIDSH of level 1.
In what follows, V (or L(V)) denotes the logic corresponding to the subvariety V.
In this section we present axiomatizations of the logics corresponding to the subvarieties of JIDSH1 which we denote simply by JID1.
Corollary 12.1**.**
The logic JID1 corresponding to JID1 is defined, as an extension of DQDSH, by
- (a)
(∼α∨(β→γ))⇔H((∼α∨β)→(∼α∨γ)),
2. (b)
α ∧(∼α)∗⇔H [∼(α ∧ (∼α)∗)]∗.**
Let DSt [DStH] denote the variety of dually Stone semi-Heyting [Heyting] algebras.
The following theorem was proved in [38, Corollary 5.10].
Theorem 12.2**.**
JID1=DSt∨V(D1,D2,D3).**
The preceding Theorem leads us naturally to raise the following open problems.
**PROBLEM **: Is the logic DSt decidable?
We make the following conjecture about an extension of DSt:
CONJECTURE: The logic DStH is decidable.
We let JIDL1 denote the subvariety of JID-algebras of level 1 defined by
(x→y)∨(y→x)≈1.
The results in the rest of this section depend on the corresponding algebraic results of [38].
The relevant results, however, are stated here for the convenience of the reader. The following corollary is immediate from the above definitions in view of Theorem 5.9.
Corollary 12.3**.**
The logic JIDL1 corresponding to JIDL1 is defined, modulo JID1, by
- (α→β)∨(β→α).
Let DStL denote the subvariety of DSt defined by the identity (L) and DStHC denote the subvariety of DStH generated by its chains.
Theorem 12.4**.**
[38].*
JIDL1=DStHC∨V(D2).*
For n∈N, let Cndp denote the n-element DStH-chain (= DPCH-chain)
denotes the variety generated by
Cndp. (Note that C3dp= L1dp.) Since the variety of Boolean algebras is the smallest non-trivial subvariety of JIDL1, we denote by
LV+(JIDL1) the latttice of non-trivial subvarieties of JIDL1.
The following theorem was proved in [38, Corollary 7.1].
Theorem 12.5**.**
{thlist}
LV+(JIDL1)≅[(ω+1)×2]*, where × represents the direct product.
JIDL1 and DStHC are the only two elements of infinite height in the lattice LV+(JIDL1).
V∈LV+(JIDL1) is of finite height if and only if V is either V(D2) or V(Cndp), for some n∈N∖{1}, or V(Cmdp)∨V(D2), for some m∈N∖{1}.*
The following corollary is immediate from the preceding theorem and Theorem 5.9.
Corollary 12.6**.**
The logic JIDL1 has the finite model property and hence it is decidable.
Bases for all subvarieties of JIDL1 were given in [38].
The theorems presented below are taken from [38] and each of the corollaries given below follows from the theorem that precedes it and Theorem 5.9.
In the rest of this section, the phrase “defined, modulo JIDL1, by” is abbreviated to “defined by”,
in the context of varieties.
Similarly, the phrase “defined, as an extension of the logic
JIDL1, by” is also abbreviated to the phrase “defined by” in the case of logics.
The theorems that appear below were proved in [37].
Each of the corollaries given below follows from the theorem immediately preceding it and Theorem 5.9.
Theorem 12.7**.**
The variety DStHC is defined by
- x∨x′≈1.
Corollary 12.8**.**
*The logic DStHC is defined by
*
- α ∨ ∼α.
The variety V(D2) was axiomatized earlier. Here is another one.
Theorem 12.9**.**
The variety V(D2) is defined by
- x′′≈x.
Corollary 12.10**.**
*The logic L(V(D2)) is defined by
*
- α⇔H ∼∼α.
Let n∈N such that n≥2.
Theorem 12.11**.**
The variety V(Cndp) ∨ V(D2) is defined by
- (En)
x1∨x2∨⋯∨xn∨(x1→x2)∨(x2→x3)∨⋯∨(xn−1→xn)=1.**
Corollary 12.12**.**
*The logic L(V(Cndp) ∨ V(D2)) is defined by
*
- (En)
α1∨α2∨⋯∨αn∨(α1→α2)∨(α2→α3)∨⋯∨(αn−1→αn).**
Theorem 12.13**.**
The variety V(Cndp) is defined by
- (1)
x∨x′≈1,**
2. (2)
x1∨x2∨⋯∨xn∨(x1→x2)∨(x2→x3)∨⋯∨(xn−1→xn)=1.**
Corollary 12.14**.**
*The logic L(V(Cndp))
is defined by
*
- (a)
α ∨ ∼α,**
2. (Cn)
α1∨α2∨⋯∨αn∨(α1→α2)∨(α2→α3)∨⋯∨(αn−1→αn).**
Theorem 12.15**.**
The variety V(C3dp)∨V(D2) is defined by
- x∧x+ ≤ y∨y∗* (Regularity).*
It is also defined by
- x∧x′≤y∨y∗.
Corollary 12.16**.**
*The logic L(V(Ch3dp) ∨ V(D2)) is defined by
*
- (α∧α+)→H(β∨β∗).
It is also defined by
- (α ∧ ∼α)→H(β∨β∗).
The variety V(L1dp) is axiomatized in Corollary
7.11.
Here is yet another axiomatization for it.
Theorem 12.17**.**
The variety V(L1dp) is defined by
x∧x+≤y∨y∗* (Regularity),*
x∗′=x∗∗.
Corollary 12.18**.**
*The logic L(V(L1dp))
is defined by
*
- (1)
(α∧α+)→H(β∨β∗),
2. (2)
∼α∗→Hα∗∗.
We note that the extensions of JIDL1 are all decidable.
We conclude this aection with a partial poset of subvarieties of DQDSH discussed in the last sections. Its dual will give the partial poset of the axiomatic extensions of the logic DQDSH. Note that the links in the poset do not, in general, represent the covers.
PARTIAL POSET OF SUBVARIETIES OF DQDSH
\mathbb{RDMSH}_{1}=\mathbb{RDMS}\rm t\mathbb{SH}_{1}=\mathbb{V}(C_{10}^{dm}\cup\{D_{1},D_{2},D_{3}\})$$\mathbb{DM}\mathbb{SH}_{1}$$\mathbb{=DMS}\rm t\mathbb{SH}_{1}$$\mathbb{DMS}\rm t\mathbb{SH}$$\mathbb{DMSH}$$\mathbb{RDMSH}$$\mathbb{V}(\mathbf{2},\mathbf{\bar{2}})$$\mathbb{RDQDS}\rm t\mathbb{SH}_{1}$$\mathbb{RDQDSH}_{1}$$\mathbb{RDQDSH}$$\mathbb{DQDSH}$$\mathbb{RDPCS}\rm t\mathbb{SH}_{1}=\mathbb{V}(C_{10}^{dp})$$=\mathbb{RDS}\rm t\mathbb{S}\rm t\mathbb{SH}_{1}$$\mathbb{RDS}\rm t\mathbb{SH}_{1}=\mathbb{RDS}\rm t\mathbb{SH}$$=\mathbb{RDPCSH}$$\mathbb{DS}\rm t\mathbb{SH}_{1}=\mathbb{DS}\rm t\mathbb{SH}$$\mathbb{DPCSH}$$\mathbb{JIDSH}_{1}$$\mathbb{JIDSH}Figure 5
13. Concluding Remarks
It is, perhaps, worthwhile to mention here that we know from [34] that every simple algebra in RDQDStH1 is quasiprimal.
Of all the 25 simple algebras in RDQDStSH1 (Section 7), 2e,
2ˉe, and Li,i=5,6,7,8, and D3 are primal algebras and the rest, except D1 and D2, are semiprimal algebras.
We will now collect here all the open problems that were mentioned in the earlier sections.
PROBLEM 1: Is RDQDSH⊆BDQDSH? In particular, is RDQDStSHimply(B)?
PROBLEM 2: Is DPCSH⊂SBDQDSH? In particular, is DPCH⊂SBDQDH?
PROBLEM 3: Is the variety DQDStSH1 (or even DQDStH1) generated by its finite members?
PROBLEM 4: Is the logic RDMH decidable? We conjecture that the logic RDMH1 is decidable.
PROBLEM 5: Is the variety DQDStSH1 (or even DQDStH1) generated by its finite members?
PROBLEM 6: Is the logic DSt decidable? We, however, conjecture that DStH is decidable.
We conclude the paper by mentioning a few open-ended problems for future research.
PROBLEM: Investigate the extensions of the logic DHMSH in relation to, among others, the following:
(a) Decidability,
(b) Various interpolation properties,
(c) Definability,
(d) Disjunction property,
(e) Finite model property, (f) Finite embedability,
(g) Structural completeness. (h) The property ES (i.e., the epimorphisms are surjective)
Acknowledgements
The first author wants to thank the institutional support of CONICET (Consejo Nacional de Investigaciones Científicas y Técnicas) and Universidad Nacional del Sur. The authors would like to express their gratitude to Dr. Alex Citkin for his encouraging remarks and insightful comments on an earlier version of this paper.