A Logic for Dually Hemimorphic Semi-Heyting Algebras and its Axiomatic Extensions

Hanamantagouda P. Sankappanavar; Juan M. Cornejo

REVIEW 4 major objections 5 minor 23 references

A Logic for Dually Hemimorphic Semi-Heyting Algebras and its Axiomatic Extensions

T0 review · 4 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper proves that the logic DHMSH, built by adding a dually hemimorphic negation to semi-intuitionistic logic, is complete with respect to the variety of dually hemimorphic semi-Heyting algebras, so every subvariety yields an…

desk verdict A solid but uneven algebraic-logic paper: the main completeness theorem and dual-isomorphism machinery look right, while the manuscript's presentation and several side claims need real work before it can serve as a reference. read the letter →

arxiv 1908.02403 v2 pith:WEDC3G4F submitted 2019-08-07 math.LO

Juan M. Cornejo , Hanamantagouda P. Sankappanavar This is my paper · ORCID

classification math.LO MSC 03G2506D2006D1508B2608B15

keywords duallyhemimorphicsemi-Heytingalgebrasemi-intuitionisticlogicalgebraicsemanticsimplicativeDeductionTheorem3-valuedŁukasiewiczMoisilsubvarietylattice

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper builds a Hilbert-style logic, also called DHMSH, by adding a weak negation (a dual hemimorphism) to semi-intuitionistic logic, and proves that the logic is complete with respect to the variety of dually hemimorphic semi-Heyting algebras: a formula is provable exactly when it is true in every algebra of the variety. This completeness makes the variety the logic's equivalent algebraic semantics and makes the lattice of axiomatic extensions dually isomorphic to the lattice of subvarieties, so that each equational theory of these algebras automatically yields a logic. The paper then harvests that correspondence: it axiomatizes logics for the two-, three-, and four-element dually hemimorphic semi-Heyting matrices, recovers the modal logic LM and the 3-valued Łukasiewicz logic as special cases, and produces infinite chains of De Morgan-Gödel and dually pseudocomplemented Gödel logics. It also characterizes exactly which extensions have a Deduction Theorem for the derived implication $\to_H$.

What carries the argument

The load-bearing device is the derived implication $x \to_H y := x \to (x \wedge y)$, which turns any semi-Heyting algebra into a Heyting algebra on the same lattice. The logic is engineered so that it is implicative with respect to $\to_H$: axioms A1-A14 together with semi-modus ponens (from $\varphi$ and $\varphi \to_H \gamma$, infer $\gamma$) and semi-contraposition (from $\varphi \to_H \gamma$, infer $\gamma' \to_H \varphi'$). Implicativity allows the standard Lindenbaum-Tarski construction to build an algebra from any extension of the logic, and the axioms for $0'$, $1'$, and the De Morgan law force that algebra to lie in DHMSH. This round trip, from logic to algebra and back, is what yields completeness and the dual isomorphism between extensions and subvarieties.

What would settle it

Try to derive the contraposition formula $(x \to_H y) \to_H (y' \to_H x')$ in the Hilbert system; the paper shows this formula is false in the four-element algebra $L^{\mathrm{dm}}_1$, so a successful derivation would refute the soundness half of the completeness theorem.

Watch

Extended reading notes

Core claim

The central claim is Theorem 4.6: for all sets of formulas $\Gamma \cup \{\varphi\}$, $\Gamma \vdash_{\mathrm{DHMSH}} \varphi$ if and only if $\Gamma \vDash_{\mathrm{DHMSH}} \varphi$. The proof shows that the class of algebras canonically associated with an implicative logic collapses exactly onto the variety DHMSH: every dually hemimorphic semi-Heyting algebra satisfies the axioms and rules, and conversely any algebra satisfying all validities of the logic must satisfy the defining identities $0' \approx 1$, $1' \approx 0$, and $(x \wedge y)' \approx x' \vee y'$. From this completeness, the paper derives the dual isomorphism between axiomatic extensions of the logic and subvarieties of the algebra variety, and then converts known equational bases for many subvarieties into explicit Hilbert-style axiomatizations.

Load-bearing premise

The proof leans on an earlier result that semi-intuitionistic logic exactly captures truth in semi-Heyting algebras and behaves like a proper implication logic; if that earlier result had a gap, the completeness of DHMSH and all of its derived logics would lose their foundation.

Editorial extensions

If this is right

Every extension of DHMSH is complete with respect to a subvariety of DHMSH, so adding axioms to the logic is the same as restricting to a subvariety; algebraic bases translate verbatim into Hilbert axioms.
The modal logic LM and the 3-valued Łukasiewicz logic each receive new Hilbert-style axiomatizations, because they coincide with the logic of De Morgan Heyting algebras and with the logic of a specific three-element dually hemimorphic semi-Heyting algebra.
The Deduction Theorem for $\to_H$ holds in an extension exactly when the corresponding variety is the expansion of a Stone semi-Heyting variety by the pseudocomplement, and within the dually quasi-De Morgan extensions only four varieties qualify.
The logics corresponding to the two-, three-, and four-element dually hemimorphic semi-Heyting matrices are decidable and have finitely many finite characteristic matrices, and two infinite chains, the De Morgan-Gödel logics and the dually pseudocomplemented Gödel logics, are axiomatized.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The dual isomorphism means algebraic decidability questions and logical decidability questions are the same problem; for instance, the paper's open question about the logic DSt could be attacked by studying the variety DSt directly.
Because the contraposition rule is what breaks the Deduction Theorem in full DHMSH, a useful deduction metatheorem for the whole logic would likely need side conditions on negated formulas or a different choice of implication connective.
The term-equivalence with 3-valued Łukasiewicz logic and with Gödel-chain logics suggests that DHMSH is a common parent of several finite-valued logics, and other many-valued systems may be recovered by selecting further subvarieties.
The semi-contraposition rule naturally produces connexive-looking validities, so the framework may provide a uniform source of paraconsistent as well as many-valued logics, a direction the paper itself flags as promising.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The core of this paper is a genuine and useful contribution. The authors define the logic DHMSH as an expansion of semi-intuitionistic logic with a dual hemimorphism, prove it complete with respect to the variety DHMSH via a standard Rasiowa/Lindenbaum argument, and derive the dual isomorphism between extensions and subvarieties. The Deduction Theorem characterization (Theorem 5.7) is a real new result, and the systematic translation of equational bases from the authors' earlier algebraic papers into axiomatizations for dozens of extensions is a useful service to the community. The new axiomatizations for Moisil's logic and 3-valued Lukasiewicz logic are plausible and potentially valuable, though the latter is only sketched.

The main theorem itself appears sound. The proof correctly reduces completeness to Rasiowa's theorem plus the identification Alg*DHMSH = DHMSH, and the direct dual-isomorphism proof in Section 16 is a worthwhile addition. I do not share the stress-test's alarm about the use of external theorems from [CV15] and [Cor11]: relying on published, peer-reviewed results is normal practice, and the paper does not hide its dependencies. That said, the introduction and Section 16 overstate self-sufficiency: the 'direct and self-sufficient proof' still imports [Cor11, Theorem 3.7] for the semi-Heyting quotient. That is a minor mismatch between claim and content, not a fatal flaw.

The paper's real weaknesses are presentation and unsubstantiated side claims. There are broken cross-references ('Theorem ??'), duplicated or malformed axioms in several corollaries, and a level of typographical sloppiness that makes verification unnecessarily hard. More importantly, the abstract promises connexive logics, but the body never actually proves the characteristic connexive theses; that claim needs either real proofs or removal. The equivalence with 3-valued Lukasiewicz logic is asserted after a brief term-equivalence sketch, which is too thin for a result presented as one of the paper's highlights. Many corollaries are dismissed as 'immediate' from the earlier algebraic theorems; that is probably true, but a referee should spot-check several of them, especially where the displayed formulas show signs of transcription errors.

Net verdict: the central load-bearing argument holds up, and the paper deserves a serious referee. It should not be published in its current form—the connexive claim, the Lukasiewicz sketch, and the general presentation all need attention. I would send it to review with a request for a careful revision and spot-checking of the extension axiomatizations.

Referee Report

4 major / 5 minor

Summary. The paper introduces a Hilbert-style logic DHMSH, expanding semi-intuitionistic logic SI by a unary connective ' intended to be interpreted as a dual hemimorphism. It proves that DHMSH is an implicative logic with respect to the derived implication →H (Theorem 3.7) and that it is complete with respect to the variety DHMSH (Theorem 4.6), using Rasiowa's framework and the identification of the class of L-algebras with the variety. It then derives the dual isomorphism between the lattice of axiomatic extensions of DHMSH and the lattice of subvarieties of DHMSH (Theorem 4.7), characterizes the extensions in which the Deduction Property holds, and gives axiomatizations for a large number of extensions corresponding to subvarieties of DHMSH, including 2-, 3-, and 4-valued logics, De Morgan and Gödel-type chains, and a claimed equivalence with 3-valued Łukasiewicz logic. Section 16 purports to give a direct and self-sufficient proof of the correspondence between extensions and subvarieties.

Significance. If the results are correct, the paper provides a systematic bridge between the algebraic theory of semi-Heyting algebras and propositional logics, solves problems raised by Sankappanavar, and produces many new examples of logics, some of which are connexive. The central completeness proof is a genuine proof and uses the Rasiowa framework appropriately; the Deduction Theorem characterization is a clean and useful result. The paper also benefits from being directly tied to a substantial body of equational-base results in the literature. The main caveats are the heavy reliance on external results from [CV15] and [Cor11] for load-bearing steps, the somewhat compressed verification of many 'immediate' corollaries, and the large number of typographical and notational errors that currently reduce confidence in the details.

major comments (4)

[Theorem 8.9] Theorem 8.9 claims that the logic DMSHC3 is the extension of DQDSHC3 by the axioms ((φ → ⊥) → ⊥) →H φ and φ →H ((φ → ⊥) → ⊥), i.e., the identity x** ≈ x. However, Theorem 8.8 and the definition of DMSH require the identity x'' ≈ x. In the three-element algebra Ldm_1 of Figure 2, a** = 1 ≠ a while a'' = a, so the axioms stated in Theorem 8.9 do not define the variety DMSHC3. The displayed axioms should presumably be (φ')' →H φ and φ →H (φ')'. Since the subsequent axiomatizations L(Ldm_i) in Section 8 are presented relative to this base, this error affects a load-bearing part of the applications.
[Theorem 9.1] The proof of Theorem 9.1 asserts that it suffices to prove the term-equivalence of the varieties V(Ldm_1) and V(Ł3). Term-equivalence of the algebraic semantics is a strong indication, but the paper does not state or prove the Abstract Algebraic Logic transfer theorem that would turn this into an equivalence of the logics themselves; in particular, no formula translation between the two languages is exhibited, and no check that the distinguished value 1 is preserved is given. Please either supply the AAL argument or explicitly state the weaker claim that the varieties are term-equivalent.
[Section 16 and Introduction] The Introduction and Section 16 advertise a 'direct and self-sufficient proof' of Theorem 4.6, but Section 16 actually proves the dual isomorphism (Theorem 16.6) and relies on [Cor11, Theorem 3.7] to obtain a semi-Heyting Lindenbaum algebra, while Theorem 4.6 itself still depends on the external results Theorem 2.2 and Theorem 3.6 of [CV15] through Lemmas 4.4 and 4.5 and Theorem 3.7. The claims of self-sufficiency and the target theorem should be corrected, and the dependence on [CV15] should be stated explicitly.
[Sections 6-15, Corollaries] Many of the corollaries in Sections 6-15 are stated as 'immediate' or as 'following from Theorem 4.8' without displaying the equational verification. This would be acceptable for routine translations, but there are already at least two places where the formula translation is visibly wrong or duplicated: Corollary 13.101(1b) is identical to (1a), and Corollary 13.79(1b) repeats (1a). The authors should systematically check that each pair of converse axioms is actually present and that the displayed formulas correspond to the cited equational bases.

minor comments (5)

[Section 10] The paragraph before Theorem 10.4 contains the unresolved reference 'Theorem ??' and should be replaced by the intended theorem number.
[Section 8.2] The sentence defining Cdp contains a typo: it should be Cdp = {Ldp_i : i = 1,...,10}, not {Ldm_i : ...}. Also, the surrounding discussion says both families have a′ = a for a ≠ 0,1; the DPCSH expansion should have a′ = 1.
[Section 8.2] The definition of α ↔H γ reads '(α →H β) ∧ (β →H α)'; the second variable should be γ.
[Remark 5.1] The reference to 'Page 22' should be replaced by a section or equation number, since page numbers are not stable identifiers in a journal submission.
[Section 12.2] Notation is inconsistent in this section, e.g., DPCHC⋉ versus DPCHCn, and several theorems have minor typos such as unbalanced parentheses or missing braces (e.g., Theorem 10.3(i)). A thorough proofreading pass is needed.

Circularity Check

0 steps flagged · score 2.0 of 10

No circular reduction; completeness of DHMSH is a standard transfer argument, though it inherits SI completeness from self-cited external work.

full rationale

The central theorem (4.6) is proved by showing Alg*DHMSH = DHMSH via Lemmas 4.4 and 4.5. Lemma 4.4 checks the new axioms (A12)-(A14) directly against (E2)-(E4) and transfers the SI-fragment soundness from Theorem 2.2 of [CV15]; Lemma 4.5 reduces the converse to Theorem 4.2 ([CV15, Corollary 4.8]), Alg*SH = SH. Neither step defines the logic in terms of the target completeness; the DHMSH-specific content is verified directly. The use of [CV15] and [Cor11] is self-citational, and Section 16's claim of a 'direct and self-sufficient proof' is overstated because Theorem 16.3 still invokes [Cor11, Theorem 3.7] for the Lindenbaum quotient. However, those cited results are published external theorems about SI, not about DHMSH, and are not fitted parameters or definitions smuggled in as predictions. A gap in [CV15] would be a correctness risk, not a circularity. No equation in the paper reduces to its own input by construction.

Assumptions & free parameters 0 free parameters · 7 assumptions · 0 invented entities

No free parameters or new postulated entities. All assumptions are standard results or cited theorems from the authors' own previous papers, which creates a moderate circularity burden only through heavy self-citation.

assumptions (7)

domain assumption Semi-Heyting algebra identities (SH1)-(SH4) define the underlying algebras of DHMSH.
Introduced in [San08], these are the base equations the logic is designed to model.
domain assumption Completeness of semi-intuitionistic logic SI with respect to the variety SH (Theorem 2.2 of [CV15]).
Used without proof in Lemma 4.4 and Theorem 4.6 to establish validity and completeness for DHMSH.
domain assumption SI is implicative with respect to →H (Theorem 3.6 of [CV15]).
Needed to conclude DHMSH is implicative (Theorem 3.7), a prerequisite for the Rasiowa completeness theorem.
standard math Rasiowa's Theorem 7.1: an implicative logic is complete with respect to its class of L-algebras.
Invoked in Theorem 4.3 and Theorem 16.7; a classical result in algebraic logic.
standard math Font's theorem (or standard AAL theorem) that algebraizable logics have their extension lattice dually isomorphic to the subvariety lattice of their algebraic semantics.
Used to state Theorem 4.7; referenced as [Fo17].
domain assumption Equational bases for subvarieties of DHMSH from [San11], [San14b], [San16], and [San17].
The many axiomatizations in Sections 8-15 are direct translations of these bases; their correctness is assumed from prior work.
standard math Term-equivalence results from [Ka73] used in Theorem 9.1 to connect L(Ldm1) with 3-valued Lukasiewicz algebras.
The proof of Theorem 9.1 relies on Katrinak's definition of Heyting implication in 3-valued Lukasiewicz algebras.

how reviews work

0 comments

Cite this review

Pith. "Pith review of A Logic for Dually Hemimorphic Semi-Heyting Algebras and its Axiomatic Extensions." pith.science (2026). https://pith.science/paper/WEDC3G4F

@misc{pith2026190802403,
  author       = {Pith},
  title        = {Pith review of: A Logic for Dually Hemimorphic Semi-Heyting Algebras and its Axiomatic Extensions},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/WEDC3G4F}},
  note         = {Machine review of arXiv:1908.02403}
}

read the original abstract

In this paper, we focus on the variety DHMSH of dually hemimorphic semi-Heyting algebras 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 Lukasiewiczlogic. 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-Goedel logics and dually pseudocomplemented Goedel 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.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

23 extracted references · 23 canonical work pages

[1]

M. Abad, J. M. Cornejo, and J. P. Diaz Varela. The variety generated by semi-Heyting chains Soft Comput (2011) 15:721-728

work page 2011
[2]

M. Abad, J. M. Cornejo, and J. P. Diaz Varela. Semi-Heyting algebras term-equivalent to G\" o del algebras . Order, (2):625--642, 2013

work page 2013
[3]

J. M. Cornejo. Semi-intuitionistic logic . Studia Logica, 98(1-2):9--25, 2011

work page 2011
[4]

J. M. Cornejo and I. D. Viglizzo. On some semi-intuitionistic logics . Studia Logica, 103(2):303--344, 2015

work page 2015
[5]

J. M. Font, R. Jansana, and D. Pigozzi. A survey of abstract algebraic logic . Studia Logica, 74(1-2):13--97, 2003. Abstract algebraic logic, Part II (Barcelona, 1997)

work page 2003
[6]

J.M. Font. Abstract Algebraic Logic. An Introductory Textbook. College Publications, 2016

work page 2016
[7]

Hilbert and P

D. Hilbert and P. Bernays, Grundlagen der Mathematik , Volume 1 (1934) and Volume 2 (1939)

work page 1934
[8]

Katri n \' a k, The structure of distributive double p-algebras

T. Katri n \' a k, The structure of distributive double p-algebras. Regularity and congruences , Algebra Universalis 3 (1973), 238--246

work page 1973

Show all 23 references

[9]

G. C. Moisil, Logique modale , Disquisitiones Mathematicae et Physica (2): 3-98, 1942. Reproduced in [24, pp. 341-431]

1942
[10]

Moisil, Essais sur les logiques non chrysippiennes, Editions de l\'Academie de la Republique Socialiste de Roumanie, Bucharest 1972

G.C. Moisil, Essais sur les logiques non chrysippiennes, Editions de l\'Academie de la Republique Socialiste de Roumanie, Bucharest 1972

1972
[11]

A. A. Monteiro. Sur les alg\`ebres de H eyting sym\'etriques . Portugal. Math., 39(1-4):1--237, 1980. Special Issue in honor of Ant \'o nio Monteiro

1980
[12]

H. Rasiowa. An algebraic approach to non-classical logics . North-Holland Publishing Co., Amsterdam, 1974. Studies in Logic and the Foundations of Mathematics, Vol. 78

1974
[13]

Rasiowa and R

H. Rasiowa and R. Sikorski, The Mathematics of Metamathematics, Polska Akademia Nauk, Monografie Matematyczne, Tom 41, Warszawa 1963

1963
[14]

H. P. Sankappanavar. Heyting algebras with dual pseudocomplementation Pacific J. math (117): 405--415, 1985

1985
[15]

Sankappanavar Heyting algebras with a dual lattice endomorphism

H.P. Sankappanavar Heyting algebras with a dual lattice endomorphism. Zeitschr. f. math. Logik und Grundlagen d. Math. (33): 565--573, 1987

1987
[16]

Sankappanavar, Semi-Heyting algebras, Amer

H.P. Sankappanavar, Semi-Heyting algebras, Amer. Math. Soc. Abstracts, January 1987, Page 13

1987
[17]

H. P. Sankappanavar. Semi- H eyting algebras: an abstraction from H eyting algebras . In Proceedings of the 9th `` D r. A ntonio A . R . M onteiro'' C ongress ( S panish), Actas Congr. ``Dr. Antonio A. R. Monteiro'', pages 33--66, Bah\' a Blanca, 2008. Univ. Nac. del Sur

2008
[18]

H. P. Sankappanavar. Expansions of semi- H eyting algebras I : D iscriminator varieties . Studia Logica, 98(1-2):27--81, 2011

2011
[19]

H. P. Sankappanavar. Dually quasi-De Morgan Stone semi-Heyting algebras I. Regularity . Categories, General Algebraic Structures and Applications, 2(1): 47--64, 2014

2014
[20]

H. P. Sankappanavar. Dually quasi-De Morgan Stone semi-Heyting algebras II. Regularity . Categories, General Algebraic Structures and Applications, 2(1): 65--82, 2014

2014
[21]

H. P. Sankappanavar. On regular De Morgan Stone semi-Heyting algebras . Demonstracio mathematica, 2016

2016
[22]

H. P. Sankappanavar. JI -distributive, dually quasi-De Morgan semi-Heyting and Heyting algebras. ArXiv: 1512.05441v3 [math.LO] 26 sep 2017

2017 arXiv
[23]

H. P. Sankappanavar. De Morgan semi-Heyting and Heyting algebras. South East Asian Bulletin of Mathematics, 2019. (To appear)

2019

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [1]

M. Abad, J. M. Cornejo, and J. P. Diaz Varela. The variety generated by semi-Heyting chains Soft Comput (2011) 15:721-728

work page 2011

[2] [2]

M. Abad, J. M. Cornejo, and J. P. Diaz Varela. Semi-Heyting algebras term-equivalent to G\" o del algebras . Order, (2):625--642, 2013

work page 2013

[3] [3]

J. M. Cornejo. Semi-intuitionistic logic . Studia Logica, 98(1-2):9--25, 2011

work page 2011

[4] [4]

J. M. Cornejo and I. D. Viglizzo. On some semi-intuitionistic logics . Studia Logica, 103(2):303--344, 2015

work page 2015

[5] [5]

J. M. Font, R. Jansana, and D. Pigozzi. A survey of abstract algebraic logic . Studia Logica, 74(1-2):13--97, 2003. Abstract algebraic logic, Part II (Barcelona, 1997)

work page 2003

[6] [6]

J.M. Font. Abstract Algebraic Logic. An Introductory Textbook. College Publications, 2016

work page 2016

[7] [7]

Hilbert and P

D. Hilbert and P. Bernays, Grundlagen der Mathematik , Volume 1 (1934) and Volume 2 (1939)

work page 1934

[8] [8]

Katri n \' a k, The structure of distributive double p-algebras

T. Katri n \' a k, The structure of distributive double p-algebras. Regularity and congruences , Algebra Universalis 3 (1973), 238--246

work page 1973