{"id":"7c543021-c9d3-4661-8033-56c7db9316d4","arxiv_id":"1908.06479","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Using Prover9 and Mace4, the authors prove the double-negation homomorphism properties for ⊕ and ⊖ in bounded hoops and present human-readable proofs.","lead":"This book chapter shows how the Prover9 theorem prover and Mace4 model finder helped prove that the double-dual operation on hoops preserves both addition and subtraction. It also lays out a workflow for turning long machine-generated equational proofs into readable human proofs, with implications for teaching algebra.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 2.18's proof relies on an unproved identity (x⊕y)⊥⊥ = (y⊥⊖x⊥⊥)⊥; the stronger x⊕y = y⊕x⊥⊥ already fails in Table 2's L3⌢L2, so the bridge needs proof.","rationale":"The paper's contribution is a human-readable proof of the double-dual homomorphism property for bounded hoops. Theorem 2.10 (for ⊖) is supported by a sequence of lemmas with detailed proofs; Theorem 2.18 (for ⊕) is the harder result. The final step of Theorem 2.18 is: Lemma 2.17 gives (y⊥ ⊖ x⊥⊥)⊥ = x⊥⊥ ⊕ y⊥⊥ after substituting x := x⊥, y := y⊥, and then the paper asserts (x ⊕ y)⊥⊥ = (y⊥ ⊖ x⊥⊥)⊥. This asserted identity is the only connection between the theorem's left-hand side and Lemma 2.17. It is not proved and it is not derivable from the immediately preceding text. The failure of the stronger identity x⊕y = y⊕x⊥⊥ in L3⌢L2 shows that the bridge cannot be replaced by a naive cancellation; it requires its own argument. Since the theorem itself was checked by Prover9 over 7 hours, the mathematical claim is probably sound, but the paper's proof as written has a gap. This is the most load-bearing concern because it affects the second main theorem's human-readable proof, which is the paper's core methodological demonstration. The fix is straightforward: prove or machine-check the bridge identity and add it as a lemma. The reader's weakest_assumption identified compressed 'easy' steps (e.g., Lemma 2.12); this is in the same family but more acute because it is the pivotal last step of Theorem 2.18. The verdict should remain CONDITIONAL pending this gap being filled.","tokens_in":14180,"tokens_out":27633,"duration_ms":217707,"concrete_test":"Run Prover9 with the hoop axioms (hoop-eq-ax) on the goal (x + y)'' = (y' - x'')' (i.e., (x⊕y)⊥⊥ = (y⊥⊖x⊥⊥)⊥ in Prover9 syntax). If Prover9 finds a proof in a reasonable time, add the identity as an explicit lemma with its proof. If Prover9 fails, run Mace4 to search for a finite hoop of size ≤20 satisfying the hoop axioms and falsifying the identity; any such model invalidates the proof of Theorem 2.18. Also, independently re-derive the identity from the paper's Lemmas 2.6 and 2.12 to confirm it is not a hidden assumption.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 2.18 is the second half of the paper's headline homomorphism claim, but its human-readable proof is a single sentence: Lemma 2.17 '(y ⊖ x⊥)⊥ = x⊥ ⊕ y⊥' is said to imply (x ⊕ y)⊥⊥ = x⊥⊥ ⊕ y⊥⊥ 'since (x ⊕ y)⊥⊥ = (y⊥ ⊖ x⊥⊥)⊥'. This bridge identity is not proved, and it is not a superficial algebraic triviality: the stronger identity x⊕y = y⊕x⊥⊥ fails in the hoop L3⌢L2 of Table 2 (x=b, y=a gives b⊕a = b, while a⊕0 = a), so the bridge must be justified separately. If the asserted identity is false, the proof of Theorem 2.18 collapses; if true, the paper omits a load-bearing step. The underlying theorem is supported by a separate 7-hour Prover9 run, so the mathematical claim may survive, but the paper's own proof is incomplete.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents a case study of using Prover9 and Mace4 to discover and prove algebraic results about hoops, a class of structures generalizing Heyting algebras. After an introductory section that uses semilattices to illustrate the tools and that introduces the hoop axioms, the paper states Theorem 1.1, a count of finite linearly ordered hoops, based on Mace4 data and a human-directed induction. The main mathematical contribution is in Section 2, where the authors investigate whether the double-dual operation x⊥ = 1 ⊖ x is a homomorphism for the subtractive and monoidal operations of a hoop. They report Prover9 proofs of the identities (x ⊖ y)⊥⊥ = x⊥⊥ ⊖ y⊥⊥ and (x ⊕ y)⊥⊥ = x⊥⊥ ⊕ y⊥⊥, and they present human-readable proofs obtained by mining the machine proofs for derived operations (∪, ∩, \\, ↓) and for a series of lemmas (Lemmas 2.1–2.17). The chapter concludes with a discussion of proof mining, explanation, and teaching applications.","tokens_in":14312,"tokens_out":14855,"duration_ms":124569,"significance":"If the results are correct, the paper illustrates a compelling workflow that combines machine search, model generation, and human proof analysis. The two homomorphism identities are nontrivial and are supported by separately reported Prover9 runs and by the provided scripts, which is a real strength. The methodological sections are clear and accessible. However, the human-readable proof of Theorem 2.18, which is the paper's headline second result, contains an unproved bridge identity, and a number of lemmas rely on 'easy' steps that are not expanded. Since the chapter explicitly promises full human-readable proofs, these gaps are significant and need to be addressed before the paper is ready.","major_comments":[{"comment":"The proof of Theorem 2.18 is reduced to Lemma 2.17 by the assertion 'since (x ⊕ y)⊥⊥ = (y⊥ ⊖ x⊥⊥)⊥'. This bridge identity is neither proved nor derived from the earlier lemmas. It is not a superficial consequence of Lemma 2.17: the stronger identity x ⊕ y = y ⊕ x⊥⊥ fails in the hoop L3⌢L2 of Table 2 (take x = b and y = a), so the variables in Lemma 2.17 cannot simply be swapped. The bridge is, in fact, an instance of the general duality (x ⊖ y)⊥ = x⊥ ⊕ y⊥⊥ mentioned in Remark 2.1, but that duality is also not proved in the paper. The authors should prove the bridge identity explicitly (or prove the general duality) before claiming that Lemma 2.17 'immediately implies' the theorem.","section":"2.5, proof of Theorem 2.18"},{"comment":"Lemma 2.7 is proved using two identities that are merely asserted as 'It is easy to show' and 'It is also easy to see', namely (∗) x ⊕ (x⊥ ⊖ (x ⊖ x⊥⊥)) = 1 and (†) ((X ⊥ ⊖ x) ⊖ ((x ⊕ (x⊥ ⊖ X)) ⊖ x)) = 0 with X = x ⊖ x⊥⊥. These identities are not algebraically obvious, and the second is quite complex. Since Lemma 2.7 is used in the proof of Lemma 2.8, which in turn is used in the proof of Theorem 2.10, the reader cannot verify the human-readable proof chain without filling these gaps. Please expand the derivations or give pointers to the specific Prover9 proof steps where these identities appear.","section":"2.3, proof of Lemma 2.7"},{"comment":"The proof of Theorem 1.1 rests on two unproved assertions: that every finite linearly ordered hoop decomposes as Lm ⌢ K for some m and subhoop K, and that ordinal sums Lm1 ⌢ ... ⌢ Lmk are classified up to isomorphism by the sequence (m1,...,mk). The first is sketched in a single sentence ('This observation may be proved by considering the subhoop generated by the least non-zero element'), and the second is declared 'easy to see'. Because the theorem is stated as a result and the proof is the basis for counting 2^(n−2) hoops, the authors should either provide a full proof or cite a reference where this structure theorem is established.","section":"1.2, proof of Theorem 1.1"}],"minor_comments":[{"comment":"There are several typos, including 'resonably' for 'reasonably', 'inacessible' for 'inaccessible', 'avoiding' for 'avoided', and a stray '/suppress' prefix on 'Lukasiewicz'.","section":"Throughout"},{"comment":"The identity (x ∪ y)⊥ = (y ⊖ x)⊥ ⊖ x is asserted without proof; it follows from axiom (5) in about two lines and should be shown or at least labelled.","section":"2.3, proof of Lemma 2.12"},{"comment":"In the displayed step '= x⊕y⊥) ⊖ x Easy', there are mismatched parentheses; it should read '= (x⊕y⊥) ⊖ x'.","section":"2.4, proof of Lemma 2.15"},{"comment":"The paper would benefit from a brief explanation of how the model counts are obtained from the Mace4 output, particularly the assertion that there are 8 linearly ordered hoops of order 5.","section":"1.2, after Table 2"}],"recommendation":"major_revision","confidential_remarks":"Dear Editor, I believe the mathematical results are likely correct, since they are backed by the reported Prover9 proofs and the submitted scripts, but the human-readable proofs—which are a main advertised contribution—contain gaps that need repair, especially the unproved bridge identity in Theorem 2.18. A revision that expands the compressed steps would make the chapter suitable for publication. I do not see grounds for rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe paper has a genuine result and a genuine flaw. The double-dual operation is a homomorphism for both ⊖ and ⊕ in bounded hoops, and the Prover9-based discovery process is a nice case study. But the human-readable proof of the ⊕ half (Theorem 2.18) is not just missing a step; it asserts a false identity. The line \"since (x⊕y)⊥⊥ = (y⊥⊖x⊥⊥)⊥\" is wrong. In the hoop L3⌢L2 from their own Table 2, take x=b, y=a: the left side equals b, the right side equals 1. I checked this directly from their operation tables. The stronger identity x⊕y = y⊕x⊥⊥ also fails there, so this is not a superficial gap. The Prover9 run may still establish the theorem, but the paper's claimed human-readable derivation is invalid.\n\nThe good parts: Theorem 2.10 (the ⊖ half) and the accompanying lemmas are real, and the methodology of mining machine proofs for reusable concepts is worth airing. The lemmas in Section 2.3 are interesting in their own right, and the proof of Theorem 2.10 holds up as far as I can see. The authors are honest about Prover9's limitations, and the scripts are available, though without a stable archive or commit hash.\n\nSoft spots beyond the bridge identity: the proof of Theorem 1.1 is a sketch, with a load-bearing observation that every finite linearly ordered hoop splits as Lm ⌢ K. That may be known from Blok–Ferreirim, but it is not proved here. Several lemmas rely on \"easy\" or \"immediate\" steps that are not expanded. No independent formal check (Lean, Coq) is provided.\n\nBottom line: the mathematical claims may well be true, but the current paper does not deliver a correct human-readable proof of (10). That is a major flaw. I would send it to peer review with a request for major revision, not desk reject it. The topic is narrow but relevant to algebraic logic and automated reasoning, and the methodology discussion is useful for a wider audience.","headline":"A real result about double-dual homomorphisms in hoops, but the human-readable proof of Theorem 2.18 contains a false bridge identity.","tokens_in":14861,"tokens_out":4018,"would_cite":false,"duration_ms":36626,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B35","06F05","03G25"],"pacs":[],"model":"deepseek-v4-flash","headline":"In every bounded hoop, the double-dual operation preserves both $\\ominus$ and $\\oplus$.","keywords":["hoops","bounded hoops","double dual","automated theorem proving","counter-example search","proof mining","Heyting algebras","algebraic identities"],"falsifier":"Search exhaustively for a bounded hoop with more than 20 elements (or any size) in which either $(x \\ominus y)^{\\perp\\perp} \\neq x^{\\perp\\perp} \\ominus y^{\\perp\\perp}$ or $(x \\oplus y)^{\\perp\\perp} \\neq x^{\\perp\\perp} \\oplus y^{\\perp\\perp}$; finding one would refute the theorems. Conversely, checking the two machine derivations with an independent proof checker would confirm them.","tokens_in":13914,"feed_emoji":"🧮","tokens_out":8225,"duration_ms":72241,"temperature":0.7,"pith_summary":"This paper seeks to establish that in every bounded hoop — an algebraic structure generalizing Heyting algebras, with operations $\\oplus$ and $\\ominus$ — the double-dual operation $x \\mapsto x^{\\perp\\perp}$, where $x^\\perp = 1 \\ominus x$, commutes with both operations: $(x \\ominus y)^{\\perp\\perp} = x^{\\perp\\perp} \\ominus y^{\\perp\\perp}$ and $(x \\oplus y)^{\\perp\\perp} = x^{\\perp\\perp} \\oplus y^{\\perp\\perp}$. The authors argue that this can be discovered and proved by combining an automated first-order theorem prover with a counter-example generator and careful human analysis of machine-generated proofs. They extract derived operations and lemmas from long machine proofs, turning a 177-step derivation and a 624-step derivation into short human-readable proofs. If the two identities hold, the double-dual map is a homomorphism for both basic operations of a hoop, a property known for Heyting algebras but nontrivial here because hoops need not be idempotent. The paper also presents the workflow as a model for both research and undergraduate teaching.","feed_headline":"Double-dual is a homomorphism in every bounded hoop","feed_subtitle":"Automated proof search plus human analysis proves two identities for structures that generalize Heyting algebras.","key_machinery":"The central object is the double-dual operation on a bounded hoop, with $x^\\perp = 1 \\ominus x$. The argument is carried by three derived operations mined from the theorem prover's output: $x \\cap y = x \\ominus (x \\ominus y)$, $y \\setminus x = (x \\oplus y) \\ominus x$, and $x \\downarrow y = x^\\perp \\oplus (x \\ominus y)$. These operations organize the proof: commutativity of $\\downarrow$ (Lemma 2.2), the duality $(x \\cap y)^\\perp = x \\downarrow y$ (Lemma 2.3), the decomposition $x = (x \\cap y) \\oplus (x \\ominus y)$ (Lemma 2.11), and the final duality $(y \\ominus x^\\perp)^\\perp = x^\\perp \\oplus y^\\perp$ (Lemma 2.17) lead directly to the two homomorphism theorems.","core_discovery":"In a bounded hoop, define $x^\\perp = 1 \\ominus x$. The central claim is that the double-dual map $x \\mapsto x^{\\perp\\perp}$ preserves both operations: Theorem 2.10 proves $(x \\ominus y)^{\\perp\\perp} = x^{\\perp\\perp} \\ominus y^{\\perp\\perp}$, and Theorem 2.18 proves $(x \\oplus y)^{\\perp\\perp} = x^{\\perp\\perp} \\oplus y^{\\perp\\perp}$. The proof turns on a weaker replacement for idempotence: while $x \\ominus x^{\\perp\\perp}$ need not be $0$, it is negligible in the sense that $(x \\ominus x^{\\perp\\perp})^\\perp = 1$, and more generally $(y \\ominus x^\\perp)^\\perp = x^\\perp \\oplus y^\\perp$. These identities were found by mining a 177-step machine proof for the first theorem and a 624-step proof for the second, isolating the derived operations $x \\cap y = x \\ominus (x \\ominus y)$, $y \\setminus x = (x \\oplus y) \\ominus x$, and $x \\downarrow y = x^\\perp \\oplus (x \\ominus y)$, whose simple properties make the final proofs short.","pith_inferences":["If the double-dual is a homomorphism, the double-dual elements of any bounded hoop form a retract of the hoop, and this subalgebra may inherit Heyting-algebra-like behavior even when the ambient hoop is not idempotent; the authors leave this corollary unstated.","The same lemma-extraction recipe could be tested on other classes of algebras with a pseudocomplement, such as residuated lattices or BCK-algebras, to look for double-negation homomorphisms; this would show whether the method generalizes.","A natural testable extension is whether the two identities survive dropping the constants $0$ and $1$ (unbounded hoops) or adding operations, since the proofs rely on the boundedness constants.","An independent formal verification of Theorems 2.10 and 2.18 would settle the residual reliance on the unverified output of the automated search; the paper does not include one."],"forward_implications":["In every bounded hoop, the set of double-dual elements is closed under $\\ominus$ and $\\oplus$, so it carries the structure of a subhoop.","The identity $(x \\ominus y)^\\perp = x^\\perp \\oplus y^{\\perp\\perp}$ gives a De Morgan-style duality in hoops, expressing a difference as a sum even though hoops lack idempotence.","The proof-mining cycle reduces a 7-hour, 624-step automated derivation to a few lemmas with proofs of about ten steps each, showing that machine proofs can be converted into explanatory human proofs.","The guided workflow—conjecture, search for small counterexamples, prove with automation, mine the proof—is presented as a practical template for undergraduate algebra projects."],"supporting_citations":[{"why":"Supplies the definition and basic theory of hoops as the algebraic structures under study.","marker":"[1]"},{"why":"Original source for complemented semigroups, the forerunner of hoops and the source of the hoop axioms.","marker":"[2]"},{"why":"Independent introduction of hoops and complemented monoids, referenced for the class of structures.","marker":"[3]"},{"why":"Describes the theorem prover and model finder that find the machine proofs and counterexamples used throughout the paper.","marker":"[8]"}],"fun_headline_variants":["Machine proof: double-dual is a homomorphism in hoops","Prover9+Mace4 prove double-dual homomorphism in hoops","Double-dual preservation proven for bounded hoops","Automated proof: double-dual homomorphism in hoops","Bounded hoop double-dual: a homomorphism (machine proof)"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The paper assumes that the automated proof search output is correct and that the 'easy' or 'immediate' steps in the human-readable lemmas are valid; one such step, the identity $(x \\cup y)^\\perp = (y \\ominus x)^\\perp \\ominus x$ in Lemma 2.12, is asserted without proof.","fun_headline_variants_meta":{"raw":{"variants":["Machine proof: double-dual is a homomorphism in hoops","Prover9+Mace4 prove double-dual homomorphism in hoops","Double-dual preservation proven for bounded hoops","Automated proof: double-dual homomorphism in hoops","Bounded hoop double-dual: a homomorphism (machine proof)"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00157,"raw_usage":{"total_tokens":6275,"prompt_tokens":962,"completion_tokens":5313,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":578,"completion_tokens_details":{"reasoning_tokens":5225}},"tokens_in":578,"tokens_out":5313,"duration_ms":32798,"temperature":1.0,"reasoning_tokens":5225,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T13:20:44.587288+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Search exhaustively for a bounded hoop with more than 20 elements (or any size) in which either $(x \\ominus y)^{\\perp\\perp} \\neq x^{\\perp\\perp} \\ominus y^{\\perp\\perp}$ or $(x \\oplus y)^{\\perp\\perp} \\neq x^{\\perp\\perp} \\oplus y^{\\perp\\perp}$; finding one would refute the theorems. Conversely, checking the two machine derivations with an independent proof checker would confirm them.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the definition and basic theory of hoops as the algebraic structures under study."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Original source for complemented semigroups, the forerunner of hoops and the source of the hoop axioms."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Independent introduction of hoops and complemented monoids, referenced for the class of structures."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Describes the theorem prover and model finder that find the machine proofs and counterexamples used throughout the paper."}],"review_version":1}