{"id":"2f2e788d-04c5-46db-9878-33c3ea372fe6","arxiv_id":"1908.02403","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A new logic DHMSH is shown to be complete with respect to dually hemimorphic semi-Heyting algebras, and systematic axiomatizations are given for its extensions, including new proofs for Moisil's and 3-valued Lukasiewicz logics.","lead":"The paper builds a propositional logic called DHMSH whose models are dually hemimorphic semi-Heyting algebras, and proves a completeness theorem linking the logic to that algebraic variety. It then derives Hilbert-style axiomatizations for dozens of extensions, including new presentations of Moisil's logic and 3-valued Lukasiewicz logic.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Completeness of DHMSH (Thm 4.6) rests on unproven external theorems from [CV15]; a gap in SI completeness or in SI implicativity would invalidate the central dual isomorphism and the extension axiomatizations.","rationale":"I read the paper's central proof in good faith. The internal chain of Lemmas 4.4 and 4.5 appears coherent: the induction for (SMP) and (SCP) is sound, and the use of (LALG2) to derive the defining identities of DHMSH is legitimate. The congruence proof in Section 16 also works, assuming the underlying SI results. However, the proof is not self-contained: it inherits Theorem 2.2 (completeness of SI with respect to SH) and Theorem 3.6 (implicativity of SI) from [CV15] as black boxes. These theorems are genuinely load-bearing because every subsequent result, including the dual isomorphism (Theorem 4.7) and the completeness of each axiomatic extension (Theorem 4.8 and its applications), is derived from Theorem 4.6. The paper's claim in Section 16 of a 'self-sufficient' proof is inaccurate, since it still cites [Cor11, Theorem 3.7] for the quotient construction. I also note that the equivalence with 3-valued Łukasiewicz logic (Theorem 9.1) is only sketched, but that is peripheral to the main completeness theorem. No internal contradiction or fatal flaw is apparent; the appropriate verdict remains conditional, pending verification of the cited external theorems.","tokens_in":45910,"tokens_out":19088,"duration_ms":194682,"concrete_test":"Obtain [CV15] and re-derive Theorem 2.2 (Γ ⊢SI α iff Γ |=SH α) and Theorem 3.6 (SI is implicative w.r.t. →H) from the [CV15] axiom system. Specifically, check two points: (i) whether the proof of Theorem 2.2 establishes completeness for arbitrary premise sets Γ or only for Γ = ∅, since Theorem 4.4 applies it to the whole consequence relation; (ii) whether the implicativity proof for the connective → (IL3) goes through with the rule set of SI, which has no counterpart to DHMSH's (SCP). If either check fails, Theorem 4.6 loses its foundation; if both succeed, the concern is resolved.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The central completeness theorem (Theorem 4.6) is proved by invoking Rasiowa's Theorem 7.1 to get completeness with respect to Alg*DHMSH, then proving Alg*DHMSH = DHMSH via Lemmas 4.4 and 4.5. Lemma 4.5 depends directly on Theorem 4.2 (Alg*SH = SH), and Lemma 4.4's induction for axioms (A1)–(A11) uses Theorem 2.2 to validate those axioms in DHMSH. Both Theorem 2.2 and the implicativity theorem 3.6 are imported from [CV15] without proof. The paper's own 'self-sufficient' proof in Section 16 still relies on [Cor11, Theorem 3.7] for the semi-Heyting quotient. If the [CV15] completeness proof for SI turned out to require the deduction theorem (which is known to fail in DHMSH) or if its soundness proof omitted the rule (SCP), then the identification Alg*DHMSH = DHMSH would fail and Theorem 4.6, Theorem 4.7, and every extension completeness claim in Sections 6–15 would be unsupported. No internal check in the paper detects such a gap, because the external theorems are used as black boxes.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":46125,"tokens_out":30840,"duration_ms":314530,"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":[{"comment":"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.","section":"Theorem 8.9"},{"comment":"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":"Theorem 9.1"},{"comment":"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.","section":"Section 16 and Introduction"},{"comment":"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.","section":"Sections 6-15, Corollaries"}],"minor_comments":[{"comment":"The paragraph before Theorem 10.4 contains the unresolved reference 'Theorem ??' and should be replaced by the intended theorem number.","section":"Section 10"},{"comment":"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":"Section 8.2"},{"comment":"The definition of α ↔H γ reads '(α →H β) ∧ (β →H α)'; the second variable should be γ.","section":"Section 8.2"},{"comment":"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":"Remark 5.1"},{"comment":"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.","section":"Section 12.2"}],"recommendation":"major_revision","confidential_remarks":"The paper is a serious contribution, but it currently has at least one substantive error in a displayed axiomatization (Theorem 8.9) as well as numerous typographical issues. The reliance on the authors' earlier algebraic papers is appropriate to the research program, but it makes independent verification harder; I would ask the editor to ensure the authors state precisely which results are imported and to require a careful correction of the formula translations before further consideration."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","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.\n\nThe 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.\n\nThe 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.\n\nNet 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.","headline":"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.","tokens_in":46690,"tokens_out":1990,"would_cite":false,"duration_ms":27718,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03G25","06D20","06D15","08B26","08B15"],"pacs":[],"model":"deepseek-v4-flash","headline":"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…","keywords":["dually hemimorphic semi-Heyting algebra","semi-intuitionistic logic","algebraic semantics","implicative logic","Deduction Theorem","3-valued Łukasiewicz logic","Moisil logic","subvariety lattice"],"falsifier":"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.","tokens_in":45672,"feed_emoji":"🧮","tokens_out":14307,"duration_ms":135184,"temperature":0.7,"pith_summary":"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$.","feed_headline":"A logic that exactly mirrors dually hemimorphic semi-Heyting algebras","feed_subtitle":"Completeness links every extension to a subvariety, giving logics for finite matrices and for LM and Łukasiewicz logic.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the completeness of semi-intuitionistic logic with respect to semi-Heyting algebras and the implicativity of SI with respect to $\\to_H$, the two imported results on which Theorem 4.6 rests.","marker":"[CV15]"},{"why":"Introduces the variety DHMSH, its subvarieties, and the equational bases that the paper converts into Hilbert-style axiomatizations.","marker":"[San11]"},{"why":"Provides the general completeness theorem for implicative logics with respect to their L-algebras, which Theorem 4.3 applies.","marker":"[Ras74]"},{"why":"Introduces semi-intuitionistic logic SI, the base logic that DHMSH expands.","marker":"[Cor11]"},{"why":"Supplies the abstract algebraic logic theorem that yields the dual isomorphism between extensions and subvarieties once completeness is known.","marker":"[Fo17]"},{"why":"Gives the fact that every semi-Heyting algebra becomes a Heyting algebra under $\\to_H$, the derived implication that carries the completeness argument.","marker":"[ACDV13]"},{"why":"Defines semi-Heyting algebras, the underlying structures whose expansions the paper studies.","marker":"[San08]"}],"fun_headline_variants":["Complete logic for dually hemimorphic semi-Heyting algebras","DHMSH logic: subvarieties become axiomatic extensions","Dually hemimorphic semi-Heyting logic: complete and algebraizable","DHMSH logic: complete, algebraizable, with connexive extensions","From dually hemimorphic algebras to a complete logic"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Complete logic for dually hemimorphic semi-Heyting algebras","DHMSH logic: subvarieties become axiomatic extensions","Dually hemimorphic semi-Heyting logic: complete and algebraizable","DHMSH logic: complete, algebraizable, with connexive extensions","From dually hemimorphic algebras to a complete logic"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001854,"raw_usage":{"total_tokens":7392,"prompt_tokens":1162,"completion_tokens":6230,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":778,"completion_tokens_details":{"reasoning_tokens":6139}},"tokens_in":778,"tokens_out":6230,"duration_ms":47325,"temperature":1.0,"reasoning_tokens":6139,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T14:45:12.852736+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}