{"id":"bdd5febb-a9ac-4621-9a06-541708dc2f20","arxiv_id":"1908.00922","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Classifying the logic of a finite consistent Hilbert calculus inside the Leibniz or Frege hierarchy is undecidable.","lead":"This paper proves that no algorithm can decide where the logic of a finite consistent Hilbert calculus sits in the Leibniz or Frege hierarchies of abstract algebraic logic. The proof encodes undecidable problems, integer solutions to Diophantine equations and one-variable equations of relation algebras, into finite logical rules.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified: the appendix proof of Lemma 4.5 is sound, and the completeness step in Theorem 4.6 is supported by completeness w.r.t. reduced models.","rationale":"The Reader identified Lemma 4.5 as the most fragile load-bearing premise, and I agree that it is the natural point to verify. However, after checking the appendix proof, the lemma holds: Lemma 4.4 justifies linearizing any CR-derivation because all rules are one-premise and symmetric; the preservation proofs for −, +, and · are complete and correct. The only other place where the written argument is compressed is the completeness direction of Theorem 4.6, but it is justified by the standard reduced-model completeness theorem for logics: a non-derivable rule is refuted by a reduced model whose algebra lies in AlgCR=CR, and that matrix is automatically an LCR-model since every subset is a filter in the semantics of LCR. Thus the equivalence CR=LCR and the subsequent use of Lemma 4.4 in Theorem 4.8 stand. The Frege hierarchy reduction similarly checks out: the model construction in Claim 5.2.1 satisfies the rules, and the consistency argument for RA-valid equations via Boolean expansions is standard. I found only minor typographical issues (e.g., 'i≤7' where the list has six items, and 'free relation algebra' where 'free algebra' is meant), none of which affect the central undecidability claims. The paper's central assertion therefore survives scrutiny, and the Reader's ACCEPT verdict should remain unchanged.","tokens_in":18515,"tokens_out":38459,"duration_ms":407849,"concrete_test":"Write a small proof checker or use an interactive prover to verify the appendix chains of Lemma 4.5 rule-by-rule; in particular, confirm that each displayed sequence is a valid chain of substitution instances of the rules in Definition 4.3, and that the step from CR⊨γ≈φ to γ⊢CRφ follows from the displayed equational basis and congruence closure.","verdict_should_be":"UNCHANGED","load_bearing_attack":"No significant objection identified. I examined the step that the Reader flagged: Lemma 4.5. The appendix proof is a valid induction: Lemma 4.4 legitimately linearizes proofs because every rule of CR has exactly one premise and is symmetric; the displayed chains show that ⊢⊣CR is preserved under −, and condition (Y) extends this to + and ·, giving a congruence. The derivation of B′, D′, E′, H′, I′, L′, M′ by instantiating (N) and (O) is correct. I also checked the completeness direction of Theorem 4.6, which initially looks compressed: to get LCR⩽CR from AlgCR=CR, one uses the standard fact that a logic is complete with respect to its reduced models; if Γ⊬CRφ, a reduced model over A∈AlgCR=CR separates Γ from φ, and since F⊆A, that matrix is a model of LCR, so Γ⊬LCRφ. Minor typos (i≤7 in Theorem 5.2; 'free relation algebra' for free algebra) do not affect the central results.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies the computational problem of classifying syntactically presented logics within the Leibniz and Frege hierarchies of abstract algebraic logic. The main results (Theorems 4.10 and 5.3) state that for every level K of the Leibniz hierarchy (resp. Frege hierarchy), the problem of deciding whether the logic of a given finite consistent Hilbert calculus in a finite language belongs to K is undecidable. The Leibniz case is proved by a reduction from Hilbert's tenth problem: for each Diophantine equation p≈0 the author constructs a finite consistent calculus L(p) whose membership in any Leibniz-hierarchy level is equivalent to the solvability of p. A key technical ingredient is the finite Hilbert-style axiomatization of the logic L_CR associated with commutative rings (Theorem 4.6), supported by the selfextensionality proof of the calculus CR in the appendix. The Frege case is proved by a reduction from the one-variable equational theory of relation algebras: for each equation α≈β the author constructs a finitely algebraizable calculus L(α,β) whose membership in any Frege-hierarchy level is equivalent to the validity of α≈β in the variety of relation algebras. The Frege-undecidability result persists when restricted to finite consistent calculi that determine a finitely algebraizable logic.","tokens_in":18618,"tokens_out":42126,"duration_ms":314427,"significance":"If the results are correct, they establish a fundamental negative metatheorem: no general algorithm can locate a syntactically presented propositional logic in the Leibniz or Frege hierarchies. This is a significant contribution to abstract algebraic logic and to the metamathematics of nonclassical logics. The paper's strengths include explicit reductions from classical undecidable problems, a self-contained finite axiomatization of the logic of commutative rings, and a long but detailed appendix proof of the selfextensionality of the auxiliary calculus CR. The stress-test review confirmed that the load-bearing Lemma 4.5 is sound and that the completeness step in Theorem 4.6 is justified by standard completeness with respect to reduced models. I found no circularity: the negative results are derived from external undecidable problems, and the internal prior work (Lemma 4.1) is cited from a published source with stated assumptions.","major_comments":[],"minor_comments":[{"comment":"In the proof of (iii)⇒(i), the text says \"Then consider any i≤7\" but Definition 5.1 lists only six formulas ϕ1,...,ϕ6; this should be i≤6.","section":"Section 5, Theorem 5.2 proof"},{"comment":"The phrase \"A is the free relation algebra\" should read \"A is the free algebra in V\"; A is the free algebra on countably many generators in the variety V, not necessarily the free relation algebra.","section":"Section 5, Theorem 5.2 proof, Claim 5.2.1"},{"comment":"The sentence \"Since K contains the class of selfextensional logics and is included in the of class of fully Fregean ones\" has the inclusions reversed; it should state that K contains the fully Fregean logics and is contained in the selfextensional ones.","section":"Section 5, Theorem 5.3 proof"},{"comment":"Rule (A) is missing a closing parenthesis on the right-hand side; it should end with \"w + (u· (x· (y· z)))\".","section":"Definition 4.3"},{"comment":"In the chain for the case of rule (O), the step \"⊢⊣CR −x +−y (0)\" should cite rule (O), not \"(0)\".","section":"Appendix, proof of Lemma 4.5"},{"comment":"The case analysis in the proof of (iii)⇒(iv) claiming that any derivation of y must use (MP') or (A3') is quite compressed; an explicit justification that these are the only rules with non-↔ conclusions (and that the premise p(z)↔0 must therefore be derived) would improve readability.","section":"Section 4, Theorem 4.8 proof"},{"comment":"The completeness direction LCR≤CR is stated briefly; it would be helpful to explicitly invoke the standard fact that a logic is complete with respect to its reduced models, as the argument uses that a separating reduced model over A∈AlgCR=CR is, by definition of LCR, a model of LCR.","section":"Section 4, Theorem 4.6 proof"},{"comment":"The claim that ⟨Z,{s}⟩ is a model of L(p) is correct for every Diophantine equation p≈0, but since the earlier verification of this matrix in Theorem 4.8 was made under the assumption that p has no integer solution, a brief remark clarifying that the verification does not require that assumption would prevent confusion.","section":"Corollary 4.9"}],"recommendation":"minor_revision","confidential_remarks":"This is a strong paper with sound central results. The minor issues listed are local typos and clarifications that do not affect the validity of the theorems. The paper is well within the scope of the journal and should be accepted after minor revision."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper delivers what it promises: it shows that classifying the logic of a finite consistent Hilbert calculus inside the Leibniz hierarchy, and inside the Frege hierarchy, is undecidable in general. That is genuinely new, and it is not a routine adaptation. The Leibniz side is built on a purpose-built finite Hilbert calculus for the logic of commutative rings, with the reduction going through Hilbert's tenth problem. The Frege side goes through the one-variable equational theory of relation algebras, and it even survives the restriction to finitely algebraizable logics. The constructions are explicit and the reductions are real. I checked the step that looks most fragile—Lemma 4.5, the selfextensionality of the ring calculus, which the author himself suggests skipping. The appendix proof is a valid induction. Lemma 4.4 legitimately linearizes the proofs because every rule has one premise and is symmetric, so checking the primitive rules under −, +, and · is enough. The derivations using (I'), (L'), (M'), (N), and (O) are correct. The completeness direction of Theorem 4.6, which is compressed, uses the standard fact that a logic is complete with respect to its reduced models, so that gap is not a problem. The minor typo in Theorem 5.2 ('free relation algebra' for 'free algebra') is cosmetic. The only real soft spot is the density of the case analysis in Theorem 4.8, where the claim that any derivation of y from x and ρ(x,y) must use (MP') or (A3') is stated quickly. I believe the claim is true, but a referee should ask for a few more lines there. Self-citation is not an issue here: the cited prior lemmas are published and independent, and the new content is the construction of CR and the reductions. The paper is written for people inside abstract algebraic logic; for them the payoff is clear. It deserves a serious referee and, if the small clarifications are made, acceptance. I would bring it to reading group.","headline":"Two genuinely new undecidability results for the Leibniz and Frege hierarchy classification problems, built on honest reductions; the fragile-looking selfextensionality lemma checks out on close reading.","tokens_in":19223,"tokens_out":529,"would_cite":true,"duration_ms":6946,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":null,"created_at":"2026-08-14T15:50:38.466126+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":null,"supporting_citations":[],"review_version":1}